ML-DSA: add keygen_internal

Primitive/Asymmetric/Signature/ML_DSA/Specification.cry

@@ -130,7 +130,7 @@ property modPlusMinusWorks m = inRange && congruent where
  * names, we define the following functions.
  */
 NTT_Vec = map NTT
-NTTInv_Vec = map NTT
+NTTInv_Vec = map NTTInv
 
 /**
  * Wrapper function around SHAKE256, specifying the length `l` in bytes.
@@ -278,6 +278,35 @@ type d = 13
  */
 type β = η * τ
 
+/**
+ * Generate a public-private key pair from a seed.
+ * [FIPS-204] Section 6.1, Algorithm 6.
+ */
+KeyGen_internal : [32]Byte -> (PublicKey, PrivateKey)
+KeyGen_internal ξ = (pk, sk) where
+    // Step 1.
+    (ρ # ρ' # K) = H`{128} (ξ # IntegerToBytes`{1} `k # IntegerToBytes`{1} `ell)
+
+    // Step 3.
+    A_hat = ExpandA ρ
+    // Step 4.
+    (s1, s2) = ExpandS ρ'
+
+    // Explicitly typecast vectors in `R` to `Rq`.
+    s1' = [map fromInteger s1_i | s1_i <- s1]
+    s2' = [map fromInteger s2_i | s2_i <- s2]
+    // Step 5.
+    t = NTTInv_Vec (A_hat ∘∘ NTT_Vec s1') + s2'
+    // Step 6.
+    (t1, t0) = Power2Round t
+
+    // Step 8.
+    pk = pkEncode ρ t1
+    // Step 9.
+    tr = H`{64} pk
+    // Step 10.
+    sk = skEncode ρ K tr s1 s2 t0
+
 /**
  * Compute a base-2 representation of the input mod `2^α` using little-endian
  * order.
@@ -1209,6 +1238,9 @@ private
  * that [NTT-Guide] uses different notation: their `ψ` is our `ζ`; their `a`
  * is our `f`; and we set their `n = 256`.
  *
+ * There is one divergence between [NTT-Guide] and [FIPS-204]: the spec uses
+ * bit-reversed indexes for the NTT representation, but the guide does not.
+ *
  * @design Marcella Hastings <marcella@galois.com>: This is neither efficient
  * nor obviously spec-adherent. We should aim to make it at least one of those.
  * Ideally we will consolidate all the NTT implementations across the cryptol-
@@ -1217,9 +1249,13 @@ private
  * @see https://github.com/GaloisInc/cryptol-specs/issues/163
  */
 NTT : Rq -> Tq
-NTT f = [f_hat_j j | j <- [0..255]] where
+NTT f = [f_hat_j j | j <- bitrev_indexes] where
     f_hat_j j = sum [ (ζ ^^ (2 * i * j + i)) * fi | i <- [0..255] | fi <- f]
 
+    // Rearrange the indexes so that the NTT representation is in
+    // bit-reversed-index order.
+    bitrev_indexes = map toInteger (map reverse [0..255 : [8]])
+
 /**
  * Inverse of the number theoretic transform: converts from the "NTT
  * representation" in `T_q` to a polynomial in `R_q`.
@@ -1230,6 +1266,9 @@ NTT f = [f_hat_j j | j <- [0..255]] where
  * that [NTT-Guide] uses different notation: their `ψ` is our `ζ`; their `a`
  * is our `f`; and we set their `n = 256`.
  *
+ * There is one divergence between [NTT-Guide] and [FIPS-204]: the spec uses
+ * bit-reversed indexes for the NTT representation, but the guide does not.
+ *
  * @design Marcella Hastings <marcella@galois.com>: This is neither efficient
  * nor obviously spec-adherent. We should aim to make it at least one of those.
  * Ideally we will consolidate all the NTT implementations across the cryptol-
@@ -1241,7 +1280,13 @@ NTTInv : Tq -> Rq
 NTTInv f_hat = [f_i j * inv_root | j <- [0..255]] where
     inv_root = recip 256 : Z q
     inv_ζ = recip ζ
-    f_i j = sum [ (inv_ζ ^^ (2 * i * j + j)) * f_hat_j | i <- [0..255] | f_hat_j <- f_hat]
+    f_i j = sum [ (inv_ζ ^^ (2 * i * j + j)) * f_hat_j
+        | i <- [0..255]
+        | f_hat_j <- indexReversedFHat]
+
+    // Rearrange the NTT representation to bit-reverse the indexes.
+    bitrev_indexes = map reverse [0..255 : [8]]
+    indexReversedFHat = [f_hat@i | i <- bitrev_indexes]
 
 private
     /**

Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry

@@ -0,0 +1,246 @@
+/**
+ * Known answer tests for ML_DSA_44.
+ *
+ * These can be drawn from several trusted sources, including
+ * [PQC-KAT]: Kris Kwiatkowski and Roderick Chapman. Post-quantum-cryptography.
+ *     GitHub repo "KAT".
+ *     @see https://github.com/post-quantum-cryptography/KAT
+ * [ACVP]: NIST. usnistgov. GitHub repo "ACVP-Server".
+ *     @see https://github.com/usnistgov/ACVP-Server/tree/master/gen-val/json-files/ML-DSA-keyGen-FIPS204
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+import Primitive::Asymmetric::Signature::ML_DSA::Instantiations::ML_DSA_44 as ML_DSA
+
+/**
+ * Test function for running a KAT from [PQC-KAT] in the "deterministic, raw"
+ * category.
+ *
+ * "Deterministic" categorizes how the signing seeds `ρ'` are computed.
+ * "Raw" categorizes the set of functions being tested -- in this case, the
+ * `{KeyGen, Sign, Verify}_internal` functions. See [PQC-KAT] README.md for
+ * more details.
+ */
+tryDetKAT xi expected_pk expected_sk = keygenWorks where
+    (pk, sk) = ML_DSA::KeyGen_internal xi
+    keygenWorks = (pk == expected_pk) && (sk == expected_sk)
+
+/**
+ * Test the raw, deterministic KAT with count 0.
+ * ```repl
+ * :prove det0
+ * ```
+ */
+property det0 = tryDetKAT xi pk sk where
+    xi = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68
+    seed = join [
+        0x23f1c88bd0e65f2c891ce865bd3275a7ffdbe4f9036e75b9,
+        0x6aad0412650e9cd2ea4591d4ab7131ea971b34c23a4ed245
+    ]
+    pk = split (join [
+        0xbd4e96f9a038ab5e36214fe69c0b1cb835ef9d7c8417e76aecd152f5cddebec8,
+        0xa1ac25f03b3643700dbf76eef49a324f93d5042e203f3c70658ad1ad13b917cc,
+        0x1ed23f06a4dd1c543350525a9e2451dfe5f3969b1fa530488cc8903fdeb7718d,
+        0x123b17843f82a838976c6596f4b18e7b1f15ab3c526b90118506f33338d539cb,
+        0x77021f0ea75d424a7d90a9b689d3ffcec54e47d9f2d06f606d35868ee4fc3a03,
+        0x8c29e1496592715ea8fb7a8a5e5340d8ba8ac8d81ee38f78161879a0564ded36,
+        0x899e88f6be522e5463810dcdad14a9ec1a9994b1cd74601aefd31c9d3d009653,
+        0xcfb8233c06d89b4c0d8c2560f8f6bbf2b8cdf37483710b87206fcb16f7b54720,
+        0x33c6e9fcd81e05c284c168b82899532782dbf7897aecf7033e85512237371271,
+        0x330ad1b29f613a5de56d54d5d78f50a41725601daaea33ad0bbd8fcb77ad6342,
+        0xdf6c2890688bccea1c7d9d92c7c57a5c2196b346718381bc00072a62f8ebc31e,
+        0x6d3bdd99d55d80e17d21163b61406ad4eaa70927e4fa74add922624d964725f1,
+        0x1c9b7b52a5f9e3a6ec36e1f17d0ea61baf68ed8c04851a1a82730d39da1ad2e6,
+        0x9e38288f55c13f75fc65dec5af6634ade84ee77459453a126f5a5902a806903c,
+        0x7914fbfb25515be9e57aebb8ca258d281e1a06109d85ea687de74a40f14235bd,
+        0x4d7541c05096800c47ad4d7f1554817c962d23840050c3f1c12966e586bcb6e7,
+        0x1659168d96e6610ca391970581979aa40e6247b5c1661042468fa50e20e0435c,
+        0x7e7159b12fb3ec2d06dba6aa40030531f48071f645f7838d9faef5ed83ec5676,
+        0xcd4f5aa25e095cecceabc2df851488a5188ef9ef47b75ea42795d73b63800796,
+        0x331688fbf6e0c2fc0a6193c729209e013af51d52d1805b5ef72dda8e7827d38d,
+        0x92a70c4e09f6b0223dbc3e55c15ddb6aa5650d62078cfb6fe30668dd0c283ff3,
+        0x20c75cc595ea043d063562058e2d5b80d0ec8830f4f0065acda05b4a132ffc6a,
+        0x06ee439a62de3c46bd6526f7d788c2e0ed47da1081db163d58624ca8702c5568,
+        0x07e721224b060702e7d7c49b339bfda25a631cc65a0185bf17f32fc444347bbb,
+        0x5a43ec1e934aaae874a2dcfa1e1371d61f0b6a7b24b8eaf25a9e02f8fa38d959,
+        0x6db39b5d8d4d245469de1eef739200c9309a01346268db557f18ee192640a57f,
+        0x764304e4e0ca56d4cb3dc16be0ace079d6dd6c27d9b0c76a122614b6f423d586,
+        0xae5bd1a8437b7efd0d69f2890de5d17252512d4c83a1b612217b15f594c7ff1c,
+        0xa5aa13fa8abe19300085d807c7acb4caa80db574fa450684fe643581dbc7901f,
+        0xc564d1d7d4d2b3a8956577100ed62b3804589aa7c30b27060b57586ae9563289,
+        0x9fc81a6349ea674938db8facb975bbda16f185c5f5d8d3230d9d60a62fa0a258,
+        0x5f95a6b26d6b3f3ed2555ef2e88e1488508499d6191f2cf05ad22ae44efb958a,
+        0x6c0d172f25732636224f3b855158999ed5e8467ff7ec0c96666798a47aae92dd,
+        0x55e209895d4e9defa1ef257ba07e290433f2deff707948b38b53c34be66becd9,
+        0x0327f0894e42bab1033391a365295cdadb7c99fd0e0a4fe22efec6cf2df80895,
+        0xa98b65b2aa03e7cd05918446165b177652dd5baf1e293c940c07bb620b4a99fe,
+        0x98b1a42501181e66f161864758dd146c70e018793351dead59d9347b4e524367,
+        0xb11c8d12d83682a922360c46fc524a5ecdd6aa3ee54c56cd6db930e5283d3009,
+        0xc8d2541811d262d35513c22569ea1198ebb9353d6d26ef3417be145358adf63f,
+        0xf243858a98bf53554a7ed4469ca8b09a76aec882db0c358e76da955ee26dbe17,
+        0xdaf57a3a46aa208deaa1ce352dcb09c27067cabd233d5a251ccdc1ac077edb9c
+    ])
+    sk = split (join [
+        0xbd4e96f9a038ab5e36214fe69c0b1cb835ef9d7c8417e76aecd152f5cddebec8,
+        0xe9355a9ab1bcfbfc7d4decdf5ddd94b4359823a9578a19d161c4e9ad5afd7d61,
+        0x746119a59589b3630773bfd350c45d029f1cd0b03163feac00f77d814cb89d96,
+        0x3b11a8dfad7d0f31b0a542ba61044a2968d6cc435f00f5330f65063f5a46db23,
+        0x23b1691c044d0cb28c2487014a9230dab8510802115848401928228a46881907,
+        0x0c5c002a0b18109b3632493810c404428498048444259a323024a4259c062cd9,
+        0x344454000018c58d64142113888020400c02a220811484823685d2086010a540,
+        0x52b231a4a48c64000c11048522868954c609cab6845346898b101122038044b0,
+        0x915ca00952a2288bb488612880120580c948668124925906429b280ed1300501,
+        0x9631dbb804e2c63011024ccb406549088e0a470d53c08919b8711091651a3112,
+        0xca125080242e24134a22014c1c48100a274e03354801c0819098845908851489,
+        0x115b400ee09885d93462c48440e4a8901b418d444031d0b420008665a2b60464,
+        0x964d4b1802a130660a020ee4862dd2162a9c186103220c5b3228980445d93465,
+        0xcb18521b11444c8084124470dca201920851100912a4880c109708c2b0290ac0,
+        0x48e2260cdb344d9b226e030951149160c0042a1819884202665802321a366ed3,
+        0x127298b82914034d90b200a1c6841c121102c6015004525842685a160c032046,
+        0x03a40d04480c52426821271291902cd92489cb088de30481a18270c1b8280848,
+        0x310c499023079049b04c883422118009138225189204c240061ac18422b270e3,
+        0x36904bc60081b83152a04923c3215206318b2605cc306a581626641080532272,
+        0x89348cc1288c1a118a98406008098dc9246ee4840054140e4ba00543826da018,
+        0x8d03922d10852519072c6440908a107064c66c51308219b56122b420540866d4,
+        0x1641089828c3160a60286841002e492206502205ca262ddc380582203004c165,
+        0x62a660da0620098510888844e1c011432466c394711c47324c28125904625b80,
+        0x49db40211915490b3184e1206600c588c4264542c871c4263120050549127049,
+        0xb66dd4b66884c830c44406c1826123874dc9127018116e8b10915c0291cb8485,
+        0xd032620a8160423820c91820003544982886020331c120818030280c0551cc86,
+        0x890022065c388e24264da42888188701c2c06dd4368904b16404278ada448120,
+        0xc128a4a80114350e530031624651d9126d0b88040b856904c96d429050808881,
+        0x004b402ec8f9a63ad7db8f6c580a15254857376b862730d93f80c4976e1ef194,
+        0x7efa8513adc92867a377e74969510fd7417fa21bd3d773f60d20e4b2ba56cc54,
+        0xf7671e087c16d996c25ec97259cf8e0a4a5c823bcb4ee3ab5aa58ece39111e15,
+        0x13c30cb90a6453d09d79e35e7bc77a3875efea5a2f0f8e070dd14cf4fcb75f13,
+        0xd61ee24dbc6b9977fe0c44f17166b06d4e2425524e4ee455ced586033641c2c8,
+        0xba5e9c0a8317ab418233d9ee411ef2bb013bb1d4b12d1ef8a82bc591218c3e5f,
+        0x7ffeb2f7b95a643b8cc46e49fdbb83656be0167b0afd3ae9205c1b02694f7df9,
+        0x39eea45529189cd8c6ac518cdfdd0e7d0a04e521ad366d99b65b9f389dc774b1,
+        0x5168907fba80ad2e6f540f8c36d81407f12d3dbb83ba0ef403a9db8453374c2b,
+        0x65aa76fb31ce475f4a857e4d155e929a77086dd169c0657c9306465910dc1596,
+        0x6a9cde2923d9c36ecf9a82fb6ce8ad6e3362f2dfe4a6b6ff54ef1bda398d3ae0,
+        0x32590e81923b1c5b287ef18e6d480f06d4f57552c6c74e329eb7f1326f663893,
+        0x5afc9a87d08147f6a3c081dbe4b7660d3bf7cc2a86bfb22cdc2a3932ecd9b20f,
+        0x770088c5d4a409950c3d91b5c0a87017f394af3d26d083986355553b98757202,
+        0x04e03eb2a8a1abc9f486ad1956717ed7d12a11a34b30b69eb3945f575f16f783,
+        0xe395bc63d757e0ee19e57e0fe999edc75c8ceb7d3753a1172e31255f383371a2,
+        0x3e9914d373278d8437aa45c6cf55c188a7559659742fccf775150f8290e7faa6,
+        0x9dbe48b09960db647c9a58c87668b534d0a3f621a7054aa67dd8e5ec09fef842,
+        0xad1629d9f85462c9461afe770926bcf939769f939e8c35f61e4300a4db286463,
+        0xbf34eef5f4282d6b0b18be8d8eebae6863f3eaf0b0adaf8468d7264e44af2652,
+        0x216291ede5689f9a153e886486cdc5538ecbe575926c362f2c0c2ac473c144f9,
+        0xe7ccb620cee886df07fbfd812ec65f19f8d3bca0de9c999733973b3f42b354ca,
+        0xc27cdbcb39c0988f9aedbfa3f0f772306c51260810ed526aa061ed7df06d1f90,
+        0x50c8efbc872e71ba80b8266b5b3da89c6a6adce973945cf6a8c25af71247bc35,
+        0x6b92b35ba82d9cdfa189d5f1c60fece7246cddad8e3856ecf048487dc5c05cf0,
+        0x47296b35b3d81ef889948e0a2fcd1210bb4511a5ce15a0a4d81b635b024fffcb,
+        0x63c3f97ccbf418fb8ab815a565a82e8065d256bd803d5b176e86c46eaaf85066,
+        0xe598f9ea2b7823c09c4dcdc281cc0593f2c45eafd439f067bb03712d5f2d0c44,
+        0x07538d9f15873474e1aac69b8bbcc4bd7fa9cda8cb20e4a551b9598a41215ae2,
+        0x2e0d04069bffe26f338b6dcf4e25c8a36a8fc79d8abb424e40ea6e56b8549de4,
+        0xeca8c27151047953a5048d73d13bb718185cfcab1e85ea2ef8757306ff964c42,
+        0x28a004d4aa709eddd54a11cf25ca6c1c6cd70dd7eb5f8721e9f0a7d8f4a71d85,
+        0x9b31d421099b49c393ba3044254935aba5cc5222bef7cd7e7068cee47c416579,
+        0x4e9c0d6f6416bb51476460c0e104cf883f482c97c2aa6ec3cfc5ce68eab2a06a,
+        0x1b97024cb62b4ea046e07727c328b0eda1bbda3a7a635c64a4638f93fa3efbdf,
+        0x757fbc9be9029bc132f296abc3b9a44224faf6bb1a3974763d81b0a1fb91472d,
+        0xae04ec26ef7255e449ae6e628532b912d827ad44897ee7fee066ac6062e20cd5,
+        0x9f5481751f2751ff2dc3e117b5059e5403fd61fb36083d7ee07d053e0c52a43e,
+        0xcd1884a5c279364bd29f04856e92427b45cfc5b6c3d345725e0887a1b47c9f8d,
+        0x8607bdb88bf0321d70cb33be6fe1c002865150aebdf3b9c5d1e004df937c565a,
+        0x7d3883158615e7eb13decbd2dd89a04390475e1d214eb60b7ac7ee220e3f980d,
+        0x1515247e0910b55a3cfab29142ebeea1e2eb8a420f33ecb1c25fa3d430ba2f47,
+        0x13d4cbf5a71389f96caf42943a15de969cf972bface48699a57596076f8eceb7,
+        0x6070174d39decd0bd5866116e1a67e57d61b6b1da5c4eb830c34bce3919cd70d,
+        0x446da248169deacb42a5f14f4f0d12ff7575f1dd91cfcf8304b286aa4272ff32,
+        0xdad6156b21c3ce56a28455c88ec4b5a8003a1baa074d6a38af77c07d29854e1e,
+        0x7bcc6f5ef1948212831f93128b197e0383a3d2cb5ca528b16d35728fc63e41e6,
+        0xc5b8730e4fe3905f7ceb914d5eb239fcdc0fbe6d9d3de141129a466d68ce2622,
+        0x4aa997d36b2eb089fd653d9efe3ba91e0fa64d5b3e495fdfab2af2a4ca04dee4,
+        0xc948b75cdc3fb6ec3afdf4901d53b96fae5c5a8f7fd97b4e38e09b11a41594a3,
+        0x3b057a150dad19abc9f6541c30fcfdf73b97d10c641eb2b8c08cf2c3cb333ea3,
+        0x07094ac5409babb3d42bba60cb4941cc63481122177421e07a99d4710f471569
+    ])
+    msg = 0x6dbbc4375136df3b07f7c70e639e223e
+    mlen = 16
+    sm = join [
+        0xa8bb75e2f0902b5a2330d586ac172f8a09f66d9b83867b705dbb40c8d032df0e,
+        0x56029a5b7a6701b50bd9f0c28a9d1cf0f64c2f3e01d6cbd7fd358c2de8d34de1,
+        0x328693586ee45861b3142a80f9e2039bc53719bdead3ed17c760770c8c542154,
+        0xc351f13a480f14d4e5683deb9990b6ca20a0093f28d5d9905863497b2ae319e4,
+        0xd0d5621479a28c03e0c370837e1cd1827fec8e502c9c3b4e40bf82e7c4be1843,
+        0x5d9d125bb5a8a6f37aaa7b26842d02c63a5eca09900a3a6f9cae5c08dde68f89,
+        0x15ae64a91887466f6f97330c98f36b79a64db44d8d785d71c37756a348c550b3,
+        0xf205427eacdbda08fa6b94bf013fd5e2cc780086687be61c26fb07fe428c9538,
+        0xad022f2da58fa83a93623e2a9067e9ba8b7c1f637edab43198d12e3e01a3c40f,
+        0xcfa9bdb1345d006969af85aa1323670dc2ba9b38f9d11afa9b5d4baf5f27803d,
+        0x7d7e33b3b4e4649cacf88891405b80360316f1174b06a3ef356f4f25194b6243,
+        0x57b1860684e57c0280ccb011651f7003e458a58ab401e6e550844c0e85beb1c6,
+        0xd7e7971fcb0617132d4c6f7961dcab500ab77de23a6906e2cdc107454e98025b,
+        0x1b8dcfcd7685d33c9e8269ddc685bb6b47ea4f6490cfbc6f78f35ff881cad61a,
+        0x2f2a61e3728f59610b0151e9c271156d5e3834d48e9c69094e9f8141d469f73a,
+        0xb9f5d962a96c1d5889fd49738d2000c4050bec944a54b87cd7c192dc4e87157a,
+        0xc1f9f4136d8540c7adb7f4492bb9096d2c35395d7e31ef0bf81736c1d7348aa9,
+        0x43eb81d6336dd3a975db138bd6e2cf41b8cc8b96b9bedda752edea5b4d9c2e55,
+        0x9b85fb9c09b1ccfa92d249917966e8046ad97e6ab249a47f8617885081abfd87,
+        0xf668f06352e6702b22cb47a005dea5ab5df334bf64e88a49cf6053a907f77b43,
+        0x0608aaaa8d564e7d44e69993ff1c4966a4e30c1235dc24cf219000a3320061a4,
+        0x23a58da214d62d4ae1c44e2d820ecef60c34c5475bb8fcc9272e32cef5762014,
+        0xf5a34110cc0e28904bd98dbf377ec24614cbdc09f987a6e407081e48a57065ca,
+        0x46d8d020036e91411034770588330d37e2e591ae080e1c7cc338922d81bf331a,
+        0xcd1415bdccf9595523004666381755fbddc73ad53698f52a008c6f0551b4a6d9,
+        0x4122b7484ebefa247a1442d523181b2febed23d001c82c51daf62ff91d322f13,
+        0x75318f1feaa504936e59c444d8f83720ea2189c289baaf3b754bfe3c8d50dc09,
+        0x7a6f612c3254e578d3b14cd37d5435f0e4df1899e71375da950e14b0a73a987a,
+        0x86be5dd19bbf045462425d69f9910eab1de3434775033eb4bb3b0eb65d289cf9,
+        0x46c12c8bece01c6a600db30824dc7bd0294dfa76612359f55578699e9287b9de,
+        0x0354cb2e5243e8f2d79839d59703a763dd1000b5d006c7a35d6a1858092f9d7d,
+        0x44d750680998eb7db2712c7ae035affcbc27d5dd3b30c38bd879d63d003c49f8,
+        0x147b9c6c066b368ae94184fd4d41075eed2f93497d0cf4eda2ebd2a4fbf45ced,
+        0x3f9f5de79995b5667963610ca74c57aefd35bbe335ee5540eb52436f06097d32,
+        0xbdfe5aed560ae142ccd37cdd726a40fb978f3e7a6db69c19419626659d0a72b7,
+        0xed8d138cb23bd0eb12965276a0728a4b573d24c871e4af81798d8c96ac2e0586,
+        0x9def247cd85e70bb819e3689428a9409a31c58cf64f1d69f5c4d0ca28466fec7,
+        0x9550a8bb3b7fb2b055d729a421aea514c1f13b97cf7fbb4a6249a3e11969024e,
+        0x52b2e1fa5ae11086e6c900f0d784b61cf2f40e8f1ddad6ff4c02bbb6089d6f6e,
+        0x10470aac8fedffbff37432c9d4fa7d5936952d011b4104c2de2ef76d1c9c5891,
+        0x0b9624ed174e189ddbd2c0ec980c88324895ff3b048c7ff529645f115e443ea1,
+        0xcd816e7fa1b33e1cc9b3f02de31263bd0d700bcfed28e8a4c9420c3a54420fe9,
+        0xcb4c819c5662d53d62a58cf4db69d9618d74f4b017077530a0eb7b49422530b9,
+        0x163d10da12f05ceab61ee8459f0c22950aef44f31a6cf959dc74e0b5281ab3fb,
+        0xbd1ed9f75d7fe768d07fb35114a3f81cd6e2e48d2d3a7a7df4ddbcd7d4f92845,
+        0xa637be39fc9857646ab4d4b680f5a42d0815f7edf9ba31c050056ad05effa19e,
+        0xef2c1a78bbae58d3b768389cad6398a2748d21f12f3a681d5c5ea54b8b061c20,
+        0xf40d1cbea4d2748e28d8dc0c8d4e6364151beebcad1ee7c725b404c29b3e40e9,
+        0x862d70039e1beac80eb4e208f8dcb4890a16fb5a98a4224e825b6ac8014a1885,
+        0x2c1a89582bdf1d82a71ef7c0b510384ed76f2654078ba42dff5a35aad7c1bf39,
+        0xbd74be7f44e289566a74835a455de3c24d78901dccbf650c822c402411772283,
+        0x863e66905cb7860acab853a08a13369e06d81b937b351c38c1e1237606abace4,
+        0x9dde5fdf1a3d73ccb6749559d30418612423b470302f4610d5f0d7c0bf77fc50,
+        0xd50d5803c4d2226787b85b4892b5cd99aa38d8ac2bdde40168077d3e7dc61968,
+        0x68b924152b536cde4c33aae54a15f42f4d73836ec26af66c098f7ae57c1c0726,
+        0x43abadcf477e01d774ca80969d1c1c977581bdc017c350a0d6a93a5b82b3bb55,
+        0x3ea1c142f20374da7e0bbfaa8fb6f37182623feb4daae6b309115656f9b06ff3,
+        0xd3c57cf2149466548b61fbe1a0b4921dd4dd991b6b3ca4545f4215620c10d3f0,
+        0x04a003fe13db83f061fbf31972ed26b5f79b13f3be4453bccd0b84e9a80b74bd,
+        0xd32dcbf248a852c3ffd1784e82bb22c33c1b1814e0ba71d71becea62974fc0d4,
+        0x43442a8677ddb917ab9b618c5ac154b55a92d833b80464aba1d86d6d2f5f4099,
+        0x0098416f6990a93a47db5a582e306cd7b058281c173c0346680c6d3e967d74dc,
+        0x87ebb2ba71869f768f7118f6eadfd1a66080fc2acd736948780fb36cb9e3021e,
+        0x25238966c8488762c2eaf3fbb7959e0c339bdcfeb8dd549a6c9af2881369081a,
+        0x77d6e3d2024cb078de0aa1df106e87e3b38e4965aab8f5a0e2410c30250fb443,
+        0xa25392f145b37f44f64c9674c6f3626847b9bd7cdf4d9f9de61cfad68dfcb67f,
+        0xcc313e0a37f7fc8a3bd09fbed64aa0267ab9358c6450fb5ce98c9db71bd61eaa,
+        0x64ae4f4e6ac626c4ff5c46f0ce721667623fdb9057fc6183a5c8621bde5e4950,
+        0xec5b7c92e82474c2d2d6ed5b909b1cbb4b258e995b1ed2152c4f4e813941eb34,
+        0x1c1311b97a5d1f2d2cf7faabb4ebbba9b5951b5c417437f702238bf63a310252,
+        0x8b83ea486b0de8903ff04963c76d0ac8408da90cfe083f90d270e1ca395c04f7,
+        0x40289a51c164842f7693464f7c2e8e0f3b6eb190b32db1abcb5d872b2af96cd8,
+        0x573ca6df1d0b05c95d5e4296320b180a8b6708eadd4d3339d84f842d1a24ab15,
+        0x090e32537987888f92959e9fb5cacdf2fd020d1f48556168696a72a0a5addce8,
+        0xeefcfe1b275b7b829daeafc1c4d1de193e43474e4f6e7f96adb7bfd200000000,
+        0x0000000000000000000000000000000011232f3c6dbbc4375136df3b07f7c70e
+    ] # 0x639e223e
+    smlen = 2436