mlkem: add test vector for ml-kem 768 #148

GaloisInc · Oct 4, 2024 · af48a95 · af48a95
1 parent 38834ec
commit af48a95
Showing 1 changed file with 179 additions and 0 deletions.
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry
@@ -0,0 +1,179 @@
+/*
+ * Test vectors for ML-KEM768.
+ *
+ * These are sourced from the Post Quantum Cryptography KAT repo:
+ * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM
+ */
+
+import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 as ML_KEM
+
+/**
+ * This takes ~35 seconds to prove.
+ * ```repl
+ * :prove t0
+ * ```
+ */
+property t0 = keygenWorks && encapsWorks && decapsWorks where
+    keygenWorks = ML_KEM::ML_KEM_KeyGen (z, d) == (pk, sk)
+    encapsWorks = ML_KEM::ML_KEM_Encaps (pk, msg) == (ss, ct)
+    decapsWorks = ML_KEM::ML_KEM_Decaps (ct, sk) == ss
+
+    z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68
+    d = split 0x6dbbc4375136df3b07f7c70e639e223e177e7fd53b161b3f4d57791794f12624
+    msg = split (join [
+        0x20a7b7e10f70496cc38220b944def699,
+        0xbf14d14e55cf4c90a12c1b33fc80ffff
+    ])
+    pk = split (join [
+        0x01f60af1dc8e6360ae78b59d4a5042eb9145a269046d6236b8304f305c2d9dcb,
+        0x189fe5a62df89b2f5a7bce3bbc753c1e78f730a99869f809aba856b676b707b2,
+        0x6601d1d909bab32451494eb7d0a2153a6350b79789a9b115f83ea12037256562,
+        0xf06a1d5aba378da77039d3bdecaca8e6a22a49050a76300a0267cdb38b7ac779,
+        0x03c50ca53b99283cac6b95fba651b11a4d1a692e4072965060587669f253b1bb,
+        0x182e661446168ac60221894660020e9bb5f5b7124a0303e2543ea3ea6ce97a24,
+        0x82b255ca346fb27a847b33b93f3ab2d33064c6e6632d1a23f1144e907b246b47,
+        0x9f4a5c928929a1e24150f5241258a5b67766a66f6a33846495907828ebe44ecc,
+        0x5b73124071ba479073910410a16d5d5696b48b194752979795772a91c348f502,
+        0xb37aa650983ebb89bf3c081ff273544129c9137a6e1834c8f2e7ce14c7870c53,
+        0xc05b9b94ecd38e6645911b0912336863ec168831f811881075cf38a59de4b5c7,
+        0x38aa6ef03d779b295588cfb62491cc7b3e08b48473354f9ac8061c152a9e2059,
+        0x97499b970b69bce66fe42bca2924ccdf0103d0a4c39193c2df25118d72b17aab,
+        0x26b0c60d4cd2c306ca4696c185de05035f4a09cf970aecc8cc93436f83b1aeaf,
+        0x452c41929a2eabc151938f74c93b858546df2264eeeab602e04a85c522f8fb1a,
+        0x5214afd8d4cae57a47b6f381a23126bd9917173128af917f1d483691c450d115,
+        0x1cfe9a1492d473ed862e27da92500c86a20019e9f975e4f54ad319ba2c5630c4,
+        0x014219d7ba235456fe530140193d662445e6a941d1e238567ba8d4d95ab1c744,
+        0x7d690821876d017270cfb169f2d792f03c800720697b410ab41c66f2b2458512,
+        0x5655eb10aa1087ffcb7750cb887ad4467377500a6a7d3a82976b415a54469577,
+        0xb4138d919b03f4c9a4d3390bdcb6f1717a5fa4ab25a34f4ba5039bb22c7f3c23,
+        0x4ea4427347aa7251464e631904d7cac4784f78b49d5f4a104a301809a779f646,
+        0x6131f9c62bb67147f4cd4973a6aa1c29ae6a8647b6268be089fe048ce990cd63,
+        0x8743d285c889a707f581b63af41731f0246b054bc4b47aab01b6842a2709d02e,
+        0x8158ab90f48b69d136082b34cb0673b74aa3f54508ed029fb8f5045ee0639e15,
+        0x0ee3b3c85f68a310ec0441980100b42abf2bad10d4a9e0c7b2bc5bbcaf73cbcd,
+        0xc49dc2c949111936779b178974a0392947745a47189bc3fa8a679c80af964a9f,
+        0x9b1b56577274a2a669d2da6704aa496af407fa1aa964cc3dc3140f5f959a7ea9,
+        0x74bdb1b83e48a99c0a3e2d75b0669b5c1278962540609166266da18886fc237a,
+        0xf30cefd569dbe399e6652e45f06a5dfc9a758a4987088ff8e38a3cf36b9d988f,
+        0x0e070b68d0b88f7bcc41306080d889780c7e238895ccaa4f3577225cca4c8a93,
+        0x30ce613e717798c9670924b271ac402b51538b8b5967ac490dcab5300e6c54d6,
+        0xa3632f3b973e4186ee1a7e2e85649185b26370c387235c4df28a9937a49d4078,
+        0xbf883f4e6346cb3251d9e13f1bda087b285afaa80e262641c5527b0a184b8bc8,
+        0x4a62e577314658e2029d850064f7a7b81f253e7cc124a9c5b039dc9b179a80c2,
+        0xf6aee6ea0815172537331a57b505baa76ff5b4c1f0da754b6194f4b39a9b1873,
+        0x0d3cdab925d691ed77a8db9927ea233ac2a12744fdc27e5d221b9369adb325d8
+    ])
+    sk = split (join [
+        0x9c700fe444904db5708e16b1ba7650fbe94f24a6abba262ad7acbd1a13877565,
+        0x66e1ac7a1e545b236c548e8661c5f468c58c3bbc49cccafb7a66a3b616786107,
+        0x84a88a8872255139d979bdb140649b06acbcc91c74d3bc791591b0f31f2c9ab2,
+        0x4d329934795405b7570a994e0d128aa08681a3cc58680937401a563bfb4e621a,
+        0x4193416ccb1c3c9d9b23dfc9979f91140b37c6e7a517ae6c8f268b3346e52ad0,
+        0xa311f79acea0a56cb9291ca0161a98aac43ef2ba55618312910012ab603ac4c0,
+        0xbe64a498e58ecb217e2a102b8a518bbbf9c457412f030c1a82cc7ea67c8fd145,
+        0x11e55436daa7383ee2c942da15f67581f069563e8ba3752ba159314973dbc737,
+        0x4244ed486c6ad77abbd89cab1c1934153439b58f586bcf00813b050744debb78,
+        0x9dc4b3a1d054e710905f066bc2ab7643d2883e096e749988a0612667633a9b98,
+        0x748c23c708d29891e84edc8c4cbc43999ec88c8a854d69402b8ebaa4d6cc09ab,
+        0x42220b8413da34b7cfaab2c6b47f1610cbb1d8b080051fa7d974ff53b71c8726,
+        0xaaac2f3daa9c6a68932d0172f2174d989090b822bacf105b7ae70fa59296d6b2,
+        0xc7614900a9f869db16600939bb1e116b1ce913ceea4ce60a2cd98cab92e28800,
+        0x70866fe04b0423c0dcec04d3f921fb8c0ad5c16a077a3f2484212d90ab2bdb14,
+        0x29ca837af87d29d63438440a273c3e9484a1481b54e68712e3fcc1e562799243,
+        0xba3f339bf1025c5c1b29e1294a0a7a3efbb75e47b31c12fa65c90a7adbcc2aea,
+        0xb0278c96513b25945dc32b9f382d2751a27ca572524127695765f9b45c88f923,
+        0xc28869bda5c7af4060042913f4d330c0453c985442dca58ee28a94bfeb85f2b4,
+        0x9c21a556fff04e09d66aba875a4819390bba7586f77bdfc0b1f639b586fc591a,
+        0xb9250c8951e143c2f9c790697ac51a9c153b493315644a73274674fb083c852a,
+        0x1072b80181be1ecb8f59769ee0903757326625376f9fba3380a55cca42786e11,
+        0xa4769c7b4761c5f5db112df69839579d82ab0340a34dd62c15165bcd67b66f04,
+        0x65546af56b6a637467393b28242c40c387000349a60a730237250709b208956d,
+        0x00fd715b239af96c418ac0147d0c63f8f9af30a272cbd629293395cad10937c3,
+        0x2e7454815f93aa9a4c0661dba4dbb1069fa4b59474cf8f10ad45563c983906ed,
+        0x324b5f776e5725be938696c0f6799e489d8b80656913c687374dfeac8adb3153,
+        0x6c90c6079069ee142fd800b3721b0aea35220dd04d85b19b872548e7005e92e6,
+        0x74a235164d6a2e53b6774af42d211c77bd6454c2445f68d04f357106afc8c0a2,
+        0xbc8e4fa467676a2957b060f0e9923a639274977216341b1aea876a0b7dee4013,
+        0xbde2459c957dcc2b5263b02e2ae3a6904cb856c49bdb5699c16997953cb1056a,
+        0x4cfb362ad3646fb5d7393418b8fe556f1dc924cc74b3f9d7876473355e2751f3,
+        0xe98ef5eab3bb974fbe884d0bda85b8fc4dce0c852853ad7a62528c3bbc32002f,
+        0xa469bb89895621944ffa29429c106c3946320ee9bf3c822115d53e968a76c258,
+        0x1e00f906e60ca372a22686d74c9ffb52a24abee52b788d015bf6a5c757549352,
+        0x7c97f927561df15d47f558b5466c8247277ab35c0170c6c05a8af8e67edf524a,
+        0x01f60af1dc8e6360ae78b59d4a5042eb9145a269046d6236b8304f305c2d9dcb,
+        0x189fe5a62df89b2f5a7bce3bbc753c1e78f730a99869f809aba856b676b707b2,
+        0x6601d1d909bab32451494eb7d0a2153a6350b79789a9b115f83ea12037256562,
+        0xf06a1d5aba378da77039d3bdecaca8e6a22a49050a76300a0267cdb38b7ac779,
+        0x03c50ca53b99283cac6b95fba651b11a4d1a692e4072965060587669f253b1bb,
+        0x182e661446168ac60221894660020e9bb5f5b7124a0303e2543ea3ea6ce97a24,
+        0x82b255ca346fb27a847b33b93f3ab2d33064c6e6632d1a23f1144e907b246b47,
+        0x9f4a5c928929a1e24150f5241258a5b67766a66f6a33846495907828ebe44ecc,
+        0x5b73124071ba479073910410a16d5d5696b48b194752979795772a91c348f502,
+        0xb37aa650983ebb89bf3c081ff273544129c9137a6e1834c8f2e7ce14c7870c53,
+        0xc05b9b94ecd38e6645911b0912336863ec168831f811881075cf38a59de4b5c7,
+        0x38aa6ef03d779b295588cfb62491cc7b3e08b48473354f9ac8061c152a9e2059,
+        0x97499b970b69bce66fe42bca2924ccdf0103d0a4c39193c2df25118d72b17aab,
+        0x26b0c60d4cd2c306ca4696c185de05035f4a09cf970aecc8cc93436f83b1aeaf,
+        0x452c41929a2eabc151938f74c93b858546df2264eeeab602e04a85c522f8fb1a,
+        0x5214afd8d4cae57a47b6f381a23126bd9917173128af917f1d483691c450d115,
+        0x1cfe9a1492d473ed862e27da92500c86a20019e9f975e4f54ad319ba2c5630c4,
+        0x014219d7ba235456fe530140193d662445e6a941d1e238567ba8d4d95ab1c744,
+        0x7d690821876d017270cfb169f2d792f03c800720697b410ab41c66f2b2458512,
+        0x5655eb10aa1087ffcb7750cb887ad4467377500a6a7d3a82976b415a54469577,
+        0xb4138d919b03f4c9a4d3390bdcb6f1717a5fa4ab25a34f4ba5039bb22c7f3c23,
+        0x4ea4427347aa7251464e631904d7cac4784f78b49d5f4a104a301809a779f646,
+        0x6131f9c62bb67147f4cd4973a6aa1c29ae6a8647b6268be089fe048ce990cd63,
+        0x8743d285c889a707f581b63af41731f0246b054bc4b47aab01b6842a2709d02e,
+        0x8158ab90f48b69d136082b34cb0673b74aa3f54508ed029fb8f5045ee0639e15,
+        0x0ee3b3c85f68a310ec0441980100b42abf2bad10d4a9e0c7b2bc5bbcaf73cbcd,
+        0xc49dc2c949111936779b178974a0392947745a47189bc3fa8a679c80af964a9f,
+        0x9b1b56577274a2a669d2da6704aa496af407fa1aa964cc3dc3140f5f959a7ea9,
+        0x74bdb1b83e48a99c0a3e2d75b0669b5c1278962540609166266da18886fc237a,
+        0xf30cefd569dbe399e6652e45f06a5dfc9a758a4987088ff8e38a3cf36b9d988f,
+        0x0e070b68d0b88f7bcc41306080d889780c7e238895ccaa4f3577225cca4c8a93,
+        0x30ce613e717798c9670924b271ac402b51538b8b5967ac490dcab5300e6c54d6,
+        0xa3632f3b973e4186ee1a7e2e85649185b26370c387235c4df28a9937a49d4078,
+        0xbf883f4e6346cb3251d9e13f1bda087b285afaa80e262641c5527b0a184b8bc8,
+        0x4a62e577314658e2029d850064f7a7b81f253e7cc124a9c5b039dc9b179a80c2,
+        0xf6aee6ea0815172537331a57b505baa76ff5b4c1f0da754b6194f4b39a9b1873,
+        0x0d3cdab925d691ed77a8db9927ea233ac2a12744fdc27e5d221b9369adb325d8,
+        0x6ff694a73b6701f2a7408773f9909118ef52e1c89285b2cde465a0b04980120a,
+        0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68
+    ])
+    ct = split (join [
+        0x16a61ff84787fd4a5f19ca59b3657db3a106a7329e2d62747a2ef85149163109,
+        0xbefff6bcb33df66230b8f6725ce719f58f71196e895befc9754d9f042494648c,
+        0x88a6ed4c4cf13f2faf9f651de79dae077733cb235f9dce448977fd42d5486b7d,
+        0xfdf6d7bd9172b14247655d34f10524d469478d9a9639f34d2acde6e3c048d52b,
+        0x308b66245fe9a28cde7983b9d14c03b37715fe3970cd35734771add7aa9b58cf,
+        0xb0adf8c613deafb2b31f6e5c8364d4334e93af8e4943fa947cc67667447cffd0,
+        0x36235afaea7f603cb2ea277b97dadf82ea746f6b27396dd08c85cff9304a2e5c,
+        0xe0571fde2e926716bc9f8e4d474b4e8fd34b0dc28376204ea306d30e9a6dd882,
+        0x50b79823e77319f2ef3a77704f409dde8beb6db1be4a9f25ae2e15939dedf1b1,
+        0x1a5aa51fcff04068b46d42fbbafd2498264cca4fb78b0f2ab162c7ef569875a1,
+        0x3148b9a4b0b9da1787ca0a7033e3eca13471dbcbbe15e34f2b5065b995fe221c,
+        0x2b7ac150334d14e68edc5e049663de362fae8d35e24c202c5fad2153cd044ea9,
+        0x62a388f030cdc5dec1c3423183b173c32b22f5800ae45e8e89c8ee4617ce24e6,
+        0x0f278bfd1ea0f8fa92486b6f849127da99be7be4c661e2ba26669d6acf619a33,
+        0x056809683e24a2f29e33be7f5f9ac668697e59488e9b8685956cd87b7c47109d,
+        0x603202c201472ec829ea64922e4d0eadd4a4b5a8fb06e0f4bf25a59ced545573,
+        0x88dcd91b387cb6148597edf84a22595801851ca4b9e9e096fdfc96f2444ac9f1,
+        0x247a5e640787fca23e3eb21ec1059c42a65803441df01279013c448dfc3eedfc,
+        0x3355eee1f510086a115f854c36db797a85ede19a473a33e79a80f6f7f6467e1b,
+        0x0d866fe0e57a8abd379934a6a6a492f5f32594d43de2ec2eea81487981bb6394,
+        0xbfa6df5498d74c6db2202a6348a325fbc906b8e820bb00659a2ee12740b14b2e,
+        0x36f4c5dab411c0cd096c5e63ba4d48aa9e92b31f44dc97c0fef661bcf4db895f,
+        0x174613d9d5ed9e836657745ec9deec7af273cec87ef0eaf805da1bc840160881,
+        0x0b8a86f952c6326d09fc8d1d7fd83b4e862e05058e877c056cc5465ec3192b03,
+        0xa4c33cc6b16558d2482d5f84518cbbc526aae6e8840317efb3a1982c3d1719ef,
+        0x15d10f8b077c5c68680be6d3d92e86aaa6eb378cf0559d493257147b55730f49,
+        0xa042325af066b4f9741b9fff5d47972d5acaf52b6bea4e9e354ef9448b62f6d2,
+        0xa1317675a922e14e31578d6cab5a09a71ab270d865151b8ab4c612b5fd5dcc97,
+        0xe45419a1cfb6b8b9aec60f62602098f91f07c238186657941c7a18e4d7ee220f,
+        0x022d5fffd291853b9c063e561b7176f7a235ce45bc86ce4718086df9536c5a5f,
+        0x0abf04c0a84d82bdf69552ade3135433c10a1ba69d688969e6d9dce54d3b3aae,
+        0x3a7f2ab904e657e3fb05241fac110aa07e62cc3991d7d0d6329b5ab9d69d7336,
+        0xc0d148588c9f0921325b85df5fd30db80a56a3724372153641961aa7e042bf26,
+        0x46ff46022c059d5794c3a4b7f90c410de71a5231dd9b83bbd0e6bdab1bf9e62f
+    ])
+    ss = split 0xb408d5d115713f0a93047dbbea832e4340787686d59a9a2d106bd662ba0aa035