chore(kyber/F*): hints

cryspen · Feb 19, 2024 · 5094126 · 5094126
1 parent 4bb61da
commit 5094126
Show file tree

Hide file tree

Showing 23 changed files with 2,687 additions and 1,049 deletions.
diff --git a/proofs/fstar/extraction-edited/.hints/BitVecEq.fsti.hints b/proofs/fstar/extraction-edited/.hints/BitVecEq.fsti.hints
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Arithmetic.fst.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Arithmetic.fst.hints
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Arithmetic.fsti.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Arithmetic.fsti.hints
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Compress.fst.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Compress.fst.hints
@@ -112,7 +112,7 @@
  "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "9a13bc10c97ddb98d679a2ac9999f0cc"
+ "5bd64c17052fb0314d0ba3349767b1f6"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient",
@@ -134,7 +134,7 @@
  "refinement_interpretation_Tm_refine_d52c8280671922ccb8dd394e8746776f"
  ],
  0,
- "14db1e69b3b2efd4fcd06a5a588a3764"
+ "5ca5a52d66ce9e644b611a5285c3cb30"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.compress_ciphertext_coefficient",
@@ -241,7 +241,7 @@
  "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "45b28cb73b040b63924af203ad2d0d0f"
+ "ccc1bcae607bd0cbbc23a902d113da67"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.decompress_ciphertext_coefficient",
@@ -303,7 +303,7 @@
  "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "77a19947ef2029ad4a16bd2569cbc0d6"
+ "1b4c272d5221a3e336b9eae34e559dde"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.decompress_ciphertext_coefficient",
@@ -398,7 +398,7 @@
  "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "4e58f59645938724eca35ad10a9904af"
+ "233426f2745557f804be7120b93fe48c"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.decompress_ciphertext_coefficient",
@@ -490,7 +490,7 @@
  "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "5c6e16947678ad8183f2eb2535fa6537"
+ "255ade0fe0b4c24a2d23f38c19cf3be4"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.decompress_message_coefficient",
@@ -560,7 +560,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.S32@tok"
  ],
  0,
- "93ba2fc92d5526bb3729443c341f523e"
+ "cdae6d70b15bedf5ae59dd7d5752a2b0"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Compress.fsti.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Compress.fsti.hints
@@ -21,7 +21,7 @@
  "refinement_interpretation_Tm_refine_d52c8280671922ccb8dd394e8746776f"
  ],
  0,
- "4e6b444d3b7e8e928fa12ba1a1286ecd"
+ "7eca6fd61d534d77941e9b563f968fd9"
  ],
  [
  "Libcrux.Kem.Kyber.Compress.decompress_ciphertext_coefficient",
@@ -85,7 +85,7 @@
  "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "187d178c2877ab9c3b3e2d89ca0c6709"
+ "ab33702b69f730f9da64e13a6bd8e6cf"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Constant_time_ops.fst.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Constant_time_ops.fst.hints
@@ -96,7 +96,7 @@
  "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "bc417ca8e8a7d928f5138881eb800548"
+ "cfa335b57cb37d7fb556b56f10ea6303"
  ],
  [
  "Libcrux.Kem.Kyber.Constant_time_ops.compare_ciphertexts_in_constant_time",
@@ -120,7 +120,7 @@
  "typing_FStar.UInt8.t"
  ],
  0,
- "59dbebc2615dc38c2c0279d74e341efc"
+ "49676724744d7a1b7fd8923e8bd59fa2"
  ],
  [
  "Libcrux.Kem.Kyber.Constant_time_ops.compare_ciphertexts_in_constant_time",
@@ -233,7 +233,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "ab82d074731dd60693ecc4589f0b83a6"
+ "dac1f00c6d64a9ab76f928d539d9a08b"
  ],
  [
  "Libcrux.Kem.Kyber.Constant_time_ops.select_shared_secret_in_constant_time",
@@ -282,7 +282,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "f0e0c12b79b791710fc35136896180c7"
+ "1805c579d01bcdc870c49acedfa8394a"
  ],
  [
  "Libcrux.Kem.Kyber.Constant_time_ops.select_shared_secret_in_constant_time",
@@ -442,7 +442,7 @@
  "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "ada2e0df6ee0135ccc977606f5c96ab4"
+ "a20eefc4b77d6c7c6cbe584945b867e9"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Hash_functions.fst.hints b/proofs/fstar/extraction-edited/.hints/Libcrux.Kem.Kyber.Hash_functions.fst.hints
@@ -1,5 +1,5 @@
 [
- "�s�^D'�+��$\u0005$�ӿ",
+ "\u0019�^�L���\u0004<�\u000b\u0000�E",
  [
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_G",
@@ -38,7 +38,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "f903dde1194a19eb8f58aad69d38e28d"
+ "4c64b1b5f0ae7ccdcaf211226160b7a9"
  ],
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_G",
@@ -76,7 +76,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "c294982b143142880515113a584f47a8"
+ "9a621a5efa2795facbecb8e353f229d1"
  ],
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_H",
@@ -115,7 +115,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "254ff6580d8a9cc20246f1725a34b37a"
+ "1dcafd3f6bf619380edb5a054d561d2a"
  ],
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_H",
@@ -153,7 +153,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "37cfc7388d840e80135794d8b491930f"
+ "a624988a23f290a1350ab26ee1e06522"
  ],
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_XOFx4",
@@ -204,7 +204,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "c0526891dbd1d762087bbb1beb3a9954"
+ "c5f34303e49964aef1e46154e8009727"
  ],
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_XOFx4",
@@ -322,7 +322,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U8@tok"
  ],
  0,
- "50ae8f48857befd1e307f8ac52daea1a"
+ "15bcc28b12e5a010f05b31ffcd7727f8"
  ],
  [
  "Libcrux.Kem.Kyber.Hash_functions.v_XOFx4",
@@ -412,7 +412,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "3c65b82758866123e527b49708301225"
+ "14f034f87e9875bb6d6078bf9855ffde"
  ]
  ]
 ]