chore(kyber/F*): hints

cryspen · Feb 20, 2024 · 0bbf8b6 · 0bbf8b6
1 parent 255ff5c
commit 0bbf8b6
Show file tree

Hide file tree

Showing 53 changed files with 1,302 additions and 2,775 deletions.
diff --git a/proofs/fstar/extraction-edited/.hints/BitVecEq.fsti.hints b/proofs/fstar/extraction-edited/.hints/BitVecEq.fsti.hints
@@ -8,7 +8,7 @@
  1,
  [ "@query" ],
  0,
- "60e1e3a1b0657e1ef8b6fb8c44e91af7"
+ "59286762d349f5b9996787df0af368ff"
  ],
  [
  "BitVecEq.bit_vec_equal_intro_principle",
@@ -21,7 +21,7 @@
  "refinement_interpretation_Tm_refine_5ea27f29671734c284c74b54ac71be4c"
  ],
  0,
- "9eb39bc3f929df05faa995e038fa24c1"
+ "3d0c51c3f21387d10ee3aa036bd8db3f"
  ],
  [
  "BitVecEq.bit_vec_equal_elim_principle",
@@ -35,7 +35,7 @@
  "refinement_interpretation_Tm_refine_f7508cd976fab894dc1e01a7483287a6"
  ],
  0,
- "0c1b0fd5c22ef36e2e79431269396e1b"
+ "fb4df4d22434569a63b52b3218e8f855"
  ],
  [
  "BitVecEq.bit_vec_equal_trivial",
@@ -49,7 +49,7 @@
  "refinement_interpretation_Tm_refine_c9b1a93dc7180dbdeb887c6ba6a0bb06"
  ],
  0,
- "9897f35a19afff6fedcb38e1369706ef"
+ "a5dee7de8b06e3799cab7df1effbcf3b"
  ],
  [
  "BitVecEq.bit_vec_sub",
@@ -65,7 +65,7 @@
  "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
  ],
  0,
- "61a1b287b51b1c895655e0762bd6f7f4"
+ "71775bf4907d2e9a78fd031450e8c8b8"
  ],
  [
  "BitVecEq.bit_vec_equal_trivial_sub_smtpat",
@@ -78,7 +78,7 @@
  "refinement_interpretation_Tm_refine_c5efe95b1f250c44fbd9d953d94aff03"
  ],
  0,
- "b9b3af32693fce5bb85a44a1e9639827"
+ "05922fc60aa639c5fdae7ff386e6afb1"
  ],
  [
  "BitVecEq.retype",
@@ -90,7 +90,7 @@
  "refinement_interpretation_Tm_refine_0dee8cb03258a67c2f7ec66427696212"
  ],
  0,
- "18a7e026386fc849e27050538198c617"
+ "16f3278bdf9a68771f24f37804da3c34"
  ],
  [
  "BitVecEq.bit_vec_sub_all_lemma",
@@ -119,7 +119,7 @@
  "typing_Tm_abs_eb643fbfbab7ef908ba32052bb948a4f"
  ],
  0,
- "03f859d292f743d39f6ecd2e18b2d056"
+ "5e840c192bca659cc1bf0712abcb1518"
  ],
  [
  "BitVecEq.int_t_array_bitwise_eq'",
@@ -155,7 +155,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "28544dbb12a8fe1eabb18fccbd648576"
+ "0ba66af0f657c91b2cc8a74a30e60f05"
  ],
  [
  "BitVecEq.int_t_array_bitwise_eq",
@@ -167,7 +167,7 @@
  "refinement_interpretation_Tm_refine_4e3dded9bf4fcf599168cbb137ff3724"
  ],
  0,
- "889060dd1f82baf1b4917e9f05a445f4"
+ "85a311e3e1961e4f078860f8115a4e4e"
  ],
  [
  "BitVecEq.int_t_seq_slice_to_bv_sub_lemma",
@@ -255,7 +255,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "4476f280b3d12f7b1726aaaad32037ff"
+ "ef738c7466342befcd8b3034bfffae5c"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -269,7 +269,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "10ecfeef80e9751d7b6a05fd765550b3"
+ "30858238a464e5c4ad0717a6f6c18cc8"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -283,7 +283,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "eb7e83b907a83837d4bd5b3061093595"
+ "ae4a6a72282782af80c5cdf5eba27264"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -298,7 +298,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "42a754aacdb1af9ef797ab856ee1f776"
+ "47b98f832e2fbb8e465077c8e85f8d45"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -312,7 +312,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "d2cb43a219c8f367e1c79c1258eb6b51"
+ "7f1a73a0b63defe94e6fd819bb8a9322"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -326,7 +326,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "1c30c29faab5af079d36dd177be86c4a"
+ "5906e3ef95f02a54636fa0b5ad4ebe2c"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -341,7 +341,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "5319fe59ecc0e0898a983a12eed8ce8e"
+ "6420ceb33586fff6632de715ba4c8a62"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -356,7 +356,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "63eae815ba68ca6332254ed8e2da1efa"
+ "15bc552eec8074539add83fd6fd6860d"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -370,7 +370,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "578bb4427fde5113da56ca5ebc9ddd78"
+ "eabfb42b4b25d271ac9e25fc5087db07"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -385,7 +385,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "2efa9326e03ee2aa277afbf835d95e67"
+ "a3594ab47cfb3172b83525084cd15aa0"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -400,7 +400,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "0fbcb9f8b6d69473b1e32cb2e11cca74"
+ "3e4a3b84589bbad98942a5ff49b35d85"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -414,7 +414,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "1a8620b9d4352c83f3c311b3fa48653d"
+ "45cf555c20c371deb335e95c4fa385e4"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -429,7 +429,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "22c5c8607acfa2e206759eb76f64545d"
+ "a62605948d6dc81aacd2f3b35e8a8086"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -445,7 +445,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "5674d2d2dac278bfe54317fa305069db"
+ "cb51082c08944ddb750bf5986bee2436"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -478,7 +478,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "5da3aec69faa436b25f8ba6c52f7a0b3"
+ "ef0d0901ecceaebdfd9c2dc671838624"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -493,7 +493,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "4b84c483c465495ecf039b775bf45fa1"
+ "5dc44008c007807c1865c9864404c3b2"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -506,7 +506,7 @@
  "refinement_interpretation_Tm_refine_90b5d2df39645a4835173a203da069e4"
  ],
  0,
- "9957475e03480465fa5081cb25813fa1"
+ "11484adb2bfd480f49799a588c6c2089"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -551,7 +551,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "203c38cd0c104134e64fd98681137931"
+ "3c9bcb87d09adc01578b5c138f6953f4"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -583,7 +583,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "7a28c228bae929a29220da29ef6cd5d5"
+ "43e11403c8477940124f71b6c9bd6eac"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -598,7 +598,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "fe7a8a5c8e3d5c9f82dddc7d5a9116df"
+ "d8dd5ea9e5ad6ee14ab9df1fbff54b2f"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -611,7 +611,7 @@
  "refinement_interpretation_Tm_refine_90b5d2df39645a4835173a203da069e4"
  ],
  0,
- "52f89eb81f038900b8ba0c5b7f78f47b"
+ "f81fd4ebba605222fa35e0f95ad9968f"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -664,7 +664,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "3204c211be4ba24cdca8724b128a555c"
+ "7889c89b1c0a2b405d736c0ef8eac088"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -693,7 +693,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "25ae33b145f90b643a0b93c4ed40e15f"
+ "d43c1e98741782237557ac46f9ee39a6"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -740,7 +740,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.S32@tok"
  ],
  0,
- "c9db393ad629283552bcf6c923ea2e1f"
+ "45d878fc2a402454f4ce4a8270753833"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -787,7 +787,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.S32@tok"
  ],
  0,
- "f50ea1dccb506e7a1cb8fe838a80269d"
+ "d80a0f4aeab61c20bef4845a3dca55cd"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -863,7 +863,7 @@
  "unit_inversion"
  ],
  0,
- "534c0d0384e24ecb6588e181cdf752e3"
+ "6213700a8a1c881dd848638983196926"
  ],
  [
  "BitVecEq.bit_vec_equal_extend",
@@ -905,7 +905,7 @@
  "typing_Tm_abs_eb643fbfbab7ef908ba32052bb948a4f"
  ],
  0,
- "7187a7da18cbe30e10bb688266860a3b"
+ "381db8a80993f6e8254bf0eee19b774c"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Array.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Array.fst.hints
@@ -20,7 +20,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "e7d21dacc3688031de64601ef59ea2a5"
+ "c86718181e1e8d01f7209e7c2a75f48f"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Convert.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Convert.fst.hints
@@ -40,7 +40,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "2c40157c8d6b75a4deefae3e1d793625"
+ "d99065ab1cecc1f4e429ca3f1178b733"
  ],
  [
  "Core.Convert.impl_6_refined",
@@ -71,7 +71,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "807cffe0a20f63c12a5a4dbd0b60c667"
+ "820c7d9e75762bc2bddd4d373dcc524a"
  ],
  [
  "Core.Convert.integer_into",
@@ -93,7 +93,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "3ffc0c3360aa457e8fea13753772796a"
+ "2042829462f72cebdcb44987cae88e04"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Iter.Adapters.Enumerate.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Iter.Adapters.Enumerate.fst.hints
@@ -23,7 +23,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "cc848d2a849235236a53a272464abd27"
+ "01184cffc5ee0606003bb72c54bfe157"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Iter.Adapters.Step_by.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Iter.Adapters.Step_by.fst.hints
@@ -23,7 +23,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "a71ce0b317f6223ed363584f8427b899"
+ "706694a0e0e6c2c02dc3b1a4e942410e"
  ]
  ]
 ]