chore: update patches and hints

cryspen · Feb 19, 2024 · b0ac623 · b0ac623
1 parent b2a83ee
commit b0ac623
Show file tree

Hide file tree

Showing 24 changed files with 2,568 additions and 1,592 deletions.
diff --git a/proofs/fstar/extraction-edited.patch b/proofs/fstar/extraction-edited.patch
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,
- "7d113386bf8129430348f4a1bcb40b5e"
+ "50e48954f211ad1646acccc5b1638e4e"
  ],
  [
  "BitVecEq.bit_vec_equal_intro_principle",
@@ -21,7 +21,7 @@
  "refinement_interpretation_Tm_refine_5ea27f29671734c284c74b54ac71be4c"
  ],
  0,
- "552cd36a84fc808a197ae5cb3c498654"
+ "9991131703620dad74cb2464112d928e"
  ],
  [
  "BitVecEq.bit_vec_equal_elim_principle",
@@ -35,7 +35,7 @@
  "refinement_interpretation_Tm_refine_f7508cd976fab894dc1e01a7483287a6"
  ],
  0,
- "f3c7ef5f8dacd5c9b4a4a02b0cf8fc75"
+ "579103b3bb866ae3e8cde20a1d2e0fdd"
  ],
  [
  "BitVecEq.bit_vec_equal_trivial",
@@ -49,7 +49,7 @@
  "refinement_interpretation_Tm_refine_c9b1a93dc7180dbdeb887c6ba6a0bb06"
  ],
  0,
- "e2c29892f7e41b9b1a85451c32723717"
+ "0948462f0358e9917fbafa395f3e1297"
  ],
  [
  "BitVecEq.bit_vec_sub",
@@ -65,7 +65,7 @@
  "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
  ],
  0,
- "0ef51fd4d263b0d6330f17df194f3ea9"
+ "0f3524a039b45618745544d63b0ed2f5"
  ],
  [
  "BitVecEq.bit_vec_equal_trivial_sub_smtpat",
@@ -78,7 +78,7 @@
  "refinement_interpretation_Tm_refine_c5efe95b1f250c44fbd9d953d94aff03"
  ],
  0,
- "a0a54b5b0e2993b26d80f6edb7e9a2a7"
+ "2e57e63fe338d382d22dff2c3db71592"
  ],
  [
  "BitVecEq.retype",
@@ -90,7 +90,7 @@
  "refinement_interpretation_Tm_refine_0dee8cb03258a67c2f7ec66427696212"
  ],
  0,
- "fa5d62def1fd9cf22e2275218e62da74"
+ "54c8e20b094b5dd3c2aa000ba42b13ca"
  ],
  [
  "BitVecEq.bit_vec_sub_all_lemma",
@@ -119,7 +119,7 @@
  "typing_Tm_abs_eb643fbfbab7ef908ba32052bb948a4f"
  ],
  0,
- "883349f8552924d33241b38f04026266"
+ "98a1b37cdc0480675550e14a61639a1f"
  ],
  [
  "BitVecEq.int_t_array_bitwise_eq'",
@@ -155,7 +155,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "0e83aa7092cdfd321ecdee8265d68758"
+ "2092b83a6458cec609264b1f0fefb224"
  ],
  [
  "BitVecEq.int_t_array_bitwise_eq",
@@ -191,7 +191,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "90dc436f56cf9f222799b7a52ef00801"
+ "a084b2b0e654e229665aacb21af31c54"
  ],
  [
  "BitVecEq.int_t_seq_slice_to_bv_sub_lemma",
@@ -213,15 +213,14 @@
  "constructor_distinct_Lib.IntTypes.U32",
  "constructor_distinct_Lib.IntTypes.U64",
  "constructor_distinct_Lib.IntTypes.U8",
- "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
+ "equality_tok_Lib.IntTypes.PUB@tok",
  "equality_tok_Lib.IntTypes.U32@tok",
  "equality_tok_Lib.IntTypes.U64@tok", "equation_BitVecEq.bit_vec_sub",
  "equation_FStar.FunctionalExtensionality.feq",
- "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
- "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
- "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.unsigned",
- "equation_Lib.IntTypes.v", "equation_Prims.nat",
- "equation_Rust_primitives.Arrays.t_Array",
+ "equation_FStar.UInt.min_int", "equation_Lib.IntTypes.bits",
+ "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
+ "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
+ "equation_Prims.nat", "equation_Rust_primitives.Arrays.t_Array",
  "equation_Rust_primitives.BitVectors.bit_vec_of_int_t_array",
  "equation_Rust_primitives.BitVectors.num_bits",
  "equation_Rust_primitives.Integers.bits",
@@ -261,7 +260,8 @@
  "refinement_interpretation_Tm_refine_bacb80e693f1faab8ffabcbb77914bec",
  "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
  "refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
- "typing_Lib.IntTypes.v", "typing_Rust_primitives.Integers.bits",
+ "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v",
+ "typing_Rust_primitives.Integers.bits",
  "typing_Rust_primitives.Integers.int_t",
  "typing_Rust_primitives.Integers.unsigned",
  "typing_Rust_primitives.Integers.usize_inttype",
@@ -271,7 +271,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "9a2d19b4ec17e0bf3713644dbccc952d"
+ "8d944104b7cbf36578e09c56d99cf675"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -285,7 +285,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "5fdeaeb27bd0286953d2294f930a3aaa"
+ "52a310baea0e571b43bd1d1d9e09bebb"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -299,7 +299,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "c1621ba27a1256f1dd27f58d75725a38"
+ "be9eb7ad0669061379f343ce0cddee16"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -314,7 +314,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "23400b5869d640b4dfc610a8b042d9b2"
+ "259b00430a53458107836f6fa4b06ada"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -328,7 +328,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "5e35eed7d09a367220372098991a61de"
+ "071578eeded5ea9a97098ef61526cd40"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -342,7 +342,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "25e0cea7f334345f8a41c4329a343994"
+ "abb89dc61f67a355fe3eaba22d778381"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -357,7 +357,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "97f0bc28cded799812090c1c5187f9d2"
+ "3cd641f0c552fe5fb78b92c788a05c45"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -372,7 +372,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "3f31655a40ea7dc9ed00d13cf6ba7a94"
+ "0b76ba0935fddaec857566a40b08235d"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -386,7 +386,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "f38f60abb7a01c1c1972a42a3a04e247"
+ "74ea1852fe6a89c810645b1cdb7a5cd7"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -401,7 +401,7 @@
  "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
  ],
  0,
- "158d15eb5b72b705493eca0fbdafe983"
+ "29647efa21fda92fa42a1c298e8103d5"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -416,7 +416,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "467084a51077de8d70ef43e7abb3fcfc"
+ "3a7ddc45c82cc8d66f1820de819b0b75"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -430,7 +430,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "6f510faa0141f53c3fed1783ab39dd71"
+ "fbf86012d1f71a04e9ce2887a98bf74a"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -445,7 +445,7 @@
  "refinement_interpretation_Tm_refine_53c655668b35152fbbd9a7948c262451"
  ],
  0,
- "5dc21fc2d06a64ffed7a6fb2ea6b26b5"
+ "8d373ea75cb1ddadf0b3db8874c920dc"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -461,7 +461,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "5553c8c8296eb55e6e4e4b4c6f3e6b3b"
+ "f86134c284107fc746281b7885c36dbe"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -494,7 +494,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "3deb0859575ca6ca1ff2ece3a8c307a5"
+ "8323833375071f780ed3f50de23c2e64"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -509,7 +509,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "0c60f15e88fa522062dd9eaf89cc9878"
+ "2cfc92ffa6c180dca8b8fa8a332e11a7"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -522,7 +522,7 @@
  "refinement_interpretation_Tm_refine_90b5d2df39645a4835173a203da069e4"
  ],
  0,
- "c617bd349ddaf89a785eb0dc845fcdfb"
+ "fb6ac0dce82486b0a6371d76dc5eb163"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -549,7 +549,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "3b7b37d5cb1b868ae54cb47b21d053ce"
+ "c0929f924ec1d9cd7dafd41c7329d08d"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -585,7 +585,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "364c36acec8c3c696aec98a2354511eb"
+ "e82f30d52484a6dfa4220fd6019a3bca"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -600,7 +600,7 @@
  "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
  ],
  0,
- "939a6c468ef112bfcfba4094efae0591"
+ "1a4bc01026aedcacdae36e1c0d6f5a67"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -613,7 +613,7 @@
  "refinement_interpretation_Tm_refine_90b5d2df39645a4835173a203da069e4"
  ],
  0,
- "2cf006bafc1e9df3fd0f8c89e2d8fb49"
+ "f8fab7120dab06892adb3192f352509b"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -676,7 +676,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "7fb631fff435366b093db310850b7953"
+ "417bc5d537d2ba01439108e32897a657"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -705,7 +705,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "ff93f6f5b03e0dcf1a6d1df3977c9341"
+ "0410efec11f2cfa242fe841d2e4181d8"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -752,7 +752,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.S32@tok"
  ],
  0,
- "dd8d7110641eec01e1d16eea3c93519c"
+ "07db0ddb0bfc7a65f3dbe1399d4e3d3c"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -799,7 +799,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.S32@tok"
  ],
  0,
- "5fedcb1210b60621e7dedb2294f5115b"
+ "4f8abdde6722dff99357a5e428ebeb7a"
  ],
  [
  "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -871,7 +871,7 @@
  "unit_inversion"
  ],
  0,
- "f29027b3fec1e2a1a3597eaf2bbb4667"
+ "9705f4183b1922a6dbe02d1950fabf38"
  ],
  [
  "BitVecEq.bit_vec_equal_extend",
@@ -913,7 +913,7 @@
  "typing_Tm_abs_eb643fbfbab7ef908ba32052bb948a4f"
  ],
  0,
- "ebccf09c0e7cf83bc822f0e27483395f"
+ "3deeb34c8a56fe7fc16bced42e42b09d"
  ]
  ]
 ]