hints

cryspen · Feb 1, 2024 · 38aea7d · 38aea7d
1 parent dcdaf1a
commit 38aea7d
Show file tree

Hide file tree

Showing 48 changed files with 3,863 additions and 5,602 deletions.
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Array.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Array.fst.hints
@@ -1,5 +1,5 @@
 [
-  "\u000f�\\�\u0006�$\u000b�5\"0M�)",
+  "!\u000fh�?��U�KC�&�G�",
   [
     [
       "Core.Array.impl_23__as_slice",
@@ -20,7 +20,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "6f4ce370b8866e98540496030b9ea2bc"
+      "85561bc0b31937bb58fa81295e630a5e"
     ]
   ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Convert.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Convert.fst.hints
@@ -1,5 +1,5 @@
 [
-  "���h\u0013�J\u0019����[�ל",
+  "���T��>�\u0016\u0004.~e��o",
   [
     [
       "Core.Convert.impl_6",
@@ -40,7 +40,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "f1bc017bd20d2ef7663ed3a86cfa560d"
+      "776c403496c6101a5e549bedcdf06d68"
     ],
     [
       "Core.Convert.impl_6_refined",
@@ -71,7 +71,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "3f9a9ed660e48fd52e177d202c0ea8b2"
+      "4ee3850617bf742063814d94c541060a"
     ],
     [
       "Core.Convert.integer_into",
@@ -93,7 +93,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "8fe5bd2209d844468d8621aba258ab14"
+      "2f85519fe3abcc75daa2e1b30615daba"
     ]
   ]
 ]
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,
-      "cbed40f98cd777329f1b2316fb374fde"
+      "3ecc0dd1b3858521a9105734362b2361"
     ]
   ]
 ]
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,
-      "540a3ab535433f04a217511a2ee1d003"
+      "792cc060a645ed5b1a7f4c64adcdb56b"
     ]
   ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Iter.Traits.Collect.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Iter.Traits.Collect.fst.hints
@@ -1 +1 @@
-[ "_x�ql�V�D�\"Z�4xi", [] ]
+[ "t\f����\t\u001f�a���pH\u001a", [] ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Iter.Traits.Iterator.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Iter.Traits.Iterator.fst.hints
@@ -1 +1 @@
-[ "���Z\u0007+-�>\u000b��7l؇", [] ]
+[ "עZ�6��Ǆ\u0010#Y��\u001d�", [] ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Iter.fsti.hints b/proofs/fstar/extraction-edited/.hints/Core.Iter.fsti.hints
@@ -43,7 +43,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "ec19e6631c38e3182d7c50839db89cf8"
+      "3a3c9afc9b5e4c1cb03540e357d97eff"
     ],
     [
       "Core.Iter.iterator_array_contains",
@@ -64,7 +64,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "f5117c85c72962bb0a58ab19c428ab57"
+      "2d9eb0ecbf9d4cf085c95dbb41ddd32d"
     ]
   ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Num.fsti.hints b/proofs/fstar/extraction-edited/.hints/Core.Num.fsti.hints
@@ -1,5 +1,5 @@
 [
-  "KWRBF��>|]�\fS�u�",
+  "_�/ґ��ї2�'��",
   [
     [
       "Core.Num.impl__i32__abs",
@@ -8,7 +8,7 @@
       1,
       [ "@query", "equation_Rust_primitives.Integers.i32_inttype" ],
       0,
-      "9630ee37c31ef00ab4ef862b3a82f753"
+      "312c6ec65c8a63c762b9d3448cc5c92b"
     ],
     [
       "Core.Num.impl__u32__from_le_bytes",
@@ -47,7 +47,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "92790a027199601eac121ca1d8f73f11"
+      "5746f48c356c86b82e8cd96f98edb188"
     ],
     [
       "Core.Num.impl__u32__from_be_bytes",
@@ -86,7 +86,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "773cfcb5736810e096ed9e306e0fbeca"
+      "e5364e57dad18e8325c7a26e113c09c5"
     ],
     [
       "Core.Num.impl__u32__to_le_bytes",
@@ -125,7 +125,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "c84b6c59e1c5d821d204cc5c21fa4225"
+      "12454d00d84c02302ace7c6291e3f8d7"
     ],
     [
       "Core.Num.impl__u32__to_be_bytes",
@@ -164,7 +164,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "511b8f6ff9d3e6589982c466baf5be68"
+      "1c80570e2bb5a5a5ec00e682a53c0eb8"
     ],
     [
       "Core.Num.impl__u64__from_le_bytes",
@@ -203,7 +203,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "712bfc0a8968173e028e4bfdac7bd10b"
+      "022eff849b907bdee54aaf903771d626"
     ],
     [
       "Core.Num.impl__u64__from_be_bytes",
@@ -242,7 +242,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "6ee430cca71e4000ec55161d2cc92268"
+      "1c2ee314345badaa4b0a9f37603f4992"
     ],
     [
       "Core.Num.impl__u64__to_le_bytes",
@@ -281,7 +281,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "b664f1d907ee9a3da2c12bd033d87e40"
+      "16985d5260eded8284e8cfb6d8cc327f"
     ],
     [
       "Core.Num.impl__u64__to_be_bytes",
@@ -320,7 +320,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "e58595728c8c2eb19cb37488c1dab3fb"
+      "f63c69cca1ddc958827bf63ffb4a1865"
     ],
     [
       "Core.Num.impl__u128__from_le_bytes",
@@ -359,7 +359,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "d906bd8158e664764046b75644747e0f"
+      "89745637cff927916d62016d7992dfc0"
     ],
     [
       "Core.Num.impl__u128__from_be_bytes",
@@ -398,7 +398,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "2a72008d06176dd0c18e8ff9f9aab93b"
+      "5c5f5e0de34e79f78a9cf3c3921ed4d7"
     ],
     [
       "Core.Num.impl__u128__to_le_bytes",
@@ -437,7 +437,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "f221d00f0f8273404150142d023d23a7"
+      "d87c0017b522e60736ce6287c02b6525"
     ],
     [
       "Core.Num.impl__u128__to_be_bytes",
@@ -476,7 +476,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "f3a53fc4fd0707de5776f57375914a00"
+      "90206980db06463ddfb8d2cdeb137621"
     ],
     [
       "Core.Num.impl__u16__pow",
@@ -530,7 +530,7 @@
         "typing_tok_Lib.IntTypes.U32@tok"
       ],
       0,
-      "ad786856041d609067afa3239a85cdb6"
+      "844a8a52362dd37b11ef806fd449c26f"
     ],
     [
       "Core.Num.impl__u32__pow",
@@ -579,7 +579,7 @@
         "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
       ],
       0,
-      "541e02295b185f69213b941b8bc2dff5"
+      "3cbeeb9b9eef20abb1a42bc3814145dc"
     ],
     [
       "Core.Num.impl__i32__pow",
@@ -632,7 +632,7 @@
         "typing_tok_Lib.IntTypes.U32@tok"
       ],
       0,
-      "3e92424cad7be60da6b35e7c91fdac0c"
+      "b92feb66af9dbbca634f3428a03dfce8"
     ]
   ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Ops.Range.fsti.hints b/proofs/fstar/extraction-edited/.hints/Core.Ops.Range.fsti.hints
@@ -1,5 +1,5 @@
 [
-  "�%��\u0013�\u000e\u0001*�'[��\u001bQ",
+  "\u0003RjP'{b\u0003\t�\u0000��\u000f�U",
   [
     [
       "Core.Ops.Range.t_RangeTo",
@@ -8,7 +8,7 @@
       1,
       [ "@query" ],
       0,
-      "599978869034aed653ac2dc914c48182"
+      "5398350df56eb89c20a8ba53b10573fa"
     ],
     [
       "Core.Ops.Range.t_RangeFrom",
@@ -17,7 +17,7 @@
       1,
       [ "@query" ],
       0,
-      "dcc7765e25f537b833808d4de52f944b"
+      "437362cec397474f5b8925b3245783f2"
     ],
     [
       "Core.Ops.Range.t_Range",
@@ -26,7 +26,7 @@
       1,
       [ "@query" ],
       0,
-      "f61b2ca1bb24ff07bb1d24b7be03286c"
+      "23b6132c3f6e53c1bc895ac90049e232"
     ],
     [
       "Core.Ops.Range.fold_range'",
@@ -113,7 +113,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "066b242a5310c3a14051e9dad032ff94"
+      "de7afb4742bd05ac1a2150ce9b2f66ff"
     ],
     [
       "Core.Ops.Range.iterator_range",
@@ -146,7 +146,7 @@
         "typing_tok_Lib.IntTypes.PUB@tok"
       ],
       0,
-      "f338800437571d0ece3361b2341125f8"
+      "70cffc878822fef0980e4605f5616d5a"
     ],
     [
       "Core.Ops.Range.impl_index_range_slice",
@@ -195,7 +195,7 @@
         "typing_tok_Lib.IntTypes.PUB@tok"
       ],
       0,
-      "9ff2acb15337e75cd275920883614933"
+      "3de7ca01540ee1194c44d8fa7d0cc728"
     ],
     [
       "Core.Ops.Range.impl_index_range_to_slice",
@@ -243,7 +243,7 @@
         "typing_tok_Lib.IntTypes.PUB@tok"
       ],
       0,
-      "b7467fd36ca30cd49913262cef19b78d"
+      "b24cda752d36c7df291a1050fec62b4a"
     ],
     [
       "Core.Ops.Range.impl_index_range_from_slice",
@@ -285,7 +285,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "1615a0726f007fb31a609c39c15bcf48"
+      "ce04978f6a0585224764eba2b493f2b2"
     ],
     [
       "Core.Ops.Range.impl_range_index_array",
@@ -306,7 +306,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "90ae7248866f152fb1ac9e979f2da4ff"
+      "3692684509378c8ea71a01470c75b15b"
     ],
     [
       "Core.Ops.Range.impl_range_to_index_array",
@@ -327,7 +327,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "b17cc5ec7b7b8ce2c00704057bd360fa"
+      "66d32ff6feda8c597d7d4116e9f346a2"
     ],
     [
       "Core.Ops.Range.impl_range_from_index_array",
@@ -348,7 +348,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "b567d71cc1fb2608bbb605e723b88983"
+      "5fb6376bf677c4b640d4709d955f92d0"
     ],
     [
       "Core.Ops.Range.impl_range_full_index_array",
@@ -369,7 +369,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "0e9975537c15d7955c0958aa5fb7f0ca"
+      "230722d2ec5e7889c8f2285ce4bfe03c"
     ],
     [
       "Core.Ops.Range.update_at_tc_array_range",
@@ -386,7 +386,7 @@
         "token_correspondence_Core.Ops.Index.in_range"
       ],
       0,
-      "50ce3c5981834330293ab0a311b0ba9e"
+      "e6d465c3c1745148c6f9478bd5ea1196"
     ],
     [
       "Core.Ops.Range.update_at_tc_array_range_to",
@@ -403,7 +403,7 @@
         "token_correspondence_Core.Ops.Index.in_range"
       ],
       0,
-      "82fe0fdd6bc4b760d56edf1d6432dd25"
+      "63e37c8f5397769c870b7fe556d27916"
     ],
     [
       "Core.Ops.Range.update_at_tc_array_range_from",
@@ -420,7 +420,7 @@
         "token_correspondence_Core.Ops.Index.in_range"
       ],
       0,
-      "01b1538ef1368989f0f8ebfbe5421ba7"
+      "6b197c3ba1b712eb23e9d66f798cd017"
     ]
   ]
 ]