Merge pull request #198 from cryspen/karthik/minimize-diff-pass1

Merge some changes from extraction to extraction-edited
cryspen · Feb 7, 2024 · 05a7c7a · 05a7c7a
2 parents ca845fd + fc49af1
commit 05a7c7a
Show file tree

Hide file tree

Showing 73 changed files with 3,656 additions and 3,457 deletions.
diff --git a/proofs/fstar/extraction-edited.patch b/proofs/fstar/extraction-edited.patch
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,
- "85561bc0b31937bb58fa81295e630a5e"
+ "61d19e21e5ba401ccd51fac8dd4dc1bb"
  ]
  ]
 ]
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,
- "776c403496c6101a5e549bedcdf06d68"
+ "89069ae0acc72a78e2efa55464713004"
  ],
  [
  "Core.Convert.impl_6_refined",
@@ -71,7 +71,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "4ee3850617bf742063814d94c541060a"
+ "2e69cb8f79fbe8510f2c581d195eb17e"
  ],
  [
  "Core.Convert.integer_into",
@@ -93,7 +93,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "2f85519fe3abcc75daa2e1b30615daba"
+ "4a75fc2edb3ec33d8d7d9232b2b0a9c1"
  ]
  ]
 ]
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,
- "3ecc0dd1b3858521a9105734362b2361"
+ "6385868cd0d0e2d5436d295085d9ece7"
  ]
  ]
 ]
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,
- "792cc060a645ed5b1a7f4c64adcdb56b"
+ "cd17466b7eba81a3ad18f29a54ecdcfa"
  ]
  ]
 ]
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,
- "3a3c9afc9b5e4c1cb03540e357d97eff"
+ "5e67dd92d9e724f630d50532cb4f36b6"
  ],
  [
  "Core.Iter.iterator_array_contains",
@@ -64,7 +64,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "2d9eb0ecbf9d4cf085c95dbb41ddd32d"
+ "9b3a6eac4d2d790e261dc9a792d7115c"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Num.fsti.hints b/proofs/fstar/extraction-edited/.hints/Core.Num.fsti.hints
@@ -8,7 +8,7 @@
  1,
  [ "@query", "equation_Rust_primitives.Integers.i32_inttype" ],
  0,
- "312c6ec65c8a63c762b9d3448cc5c92b"
+ "49c30328cc62eb103e966138f7d6bc4c"
  ],
  [
  "Core.Num.impl__u32__from_le_bytes",
@@ -47,7 +47,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "5746f48c356c86b82e8cd96f98edb188"
+ "d81dfb79264e3e188fbd87697cc43338"
  ],
  [
  "Core.Num.impl__u32__from_be_bytes",
@@ -86,7 +86,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "e5364e57dad18e8325c7a26e113c09c5"
+ "aeb67c6090d6b471aa2b210a53a97b4d"
  ],
  [
  "Core.Num.impl__u32__to_le_bytes",
@@ -125,7 +125,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "12454d00d84c02302ace7c6291e3f8d7"
+ "0ce9b8888a37d21a25e81a5a5c4bfe6e"
  ],
  [
  "Core.Num.impl__u32__to_be_bytes",
@@ -164,7 +164,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "1c80570e2bb5a5a5ec00e682a53c0eb8"
+ "7f04f9ea22cd0a14da00914f8d408fcf"
  ],
  [
  "Core.Num.impl__u64__from_le_bytes",
@@ -203,7 +203,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "022eff849b907bdee54aaf903771d626"
+ "c93947dab1fb3013cff8cad6b52b3c9c"
  ],
  [
  "Core.Num.impl__u64__from_be_bytes",
@@ -242,7 +242,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "1c2ee314345badaa4b0a9f37603f4992"
+ "6a4e7bb9ec276bef8b1d210371d17790"
  ],
  [
  "Core.Num.impl__u64__to_le_bytes",
@@ -281,7 +281,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "16985d5260eded8284e8cfb6d8cc327f"
+ "56167e58dc1efe630d223cd100c10899"
  ],
  [
  "Core.Num.impl__u64__to_be_bytes",
@@ -320,7 +320,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "f63c69cca1ddc958827bf63ffb4a1865"
+ "903d9cc70ccbdfb98677bb2c9338bd37"
  ],
  [
  "Core.Num.impl__u128__from_le_bytes",
@@ -359,7 +359,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "89745637cff927916d62016d7992dfc0"
+ "db8393219f7f9368ad04f51fda9d4439"
  ],
  [
  "Core.Num.impl__u128__from_be_bytes",
@@ -398,7 +398,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "5c5f5e0de34e79f78a9cf3c3921ed4d7"
+ "e94c37e3e522f5b3f7d584eb358af67f"
  ],
  [
  "Core.Num.impl__u128__to_le_bytes",
@@ -437,7 +437,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "d87c0017b522e60736ce6287c02b6525"
+ "15582e3fdf25975b9f64604ea6865777"
  ],
  [
  "Core.Num.impl__u128__to_be_bytes",
@@ -476,7 +476,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "90206980db06463ddfb8d2cdeb137621"
+ "948bf2141fe892e8e60b3930afd99afa"
  ],
  [
  "Core.Num.impl__u16__pow",
@@ -530,7 +530,7 @@
  "typing_tok_Lib.IntTypes.U32@tok"
  ],
  0,
- "844a8a52362dd37b11ef806fd449c26f"
+ "f81005b265bd0f2c8a69c3a58ef3957f"
  ],
  [
  "Core.Num.impl__u32__pow",
@@ -579,7 +579,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
  ],
  0,
- "3cbeeb9b9eef20abb1a42bc3814145dc"
+ "66242ac093c2f011ce65faa03ae6c3d1"
  ],
  [
  "Core.Num.impl__i32__pow",
@@ -632,7 +632,7 @@
  "typing_tok_Lib.IntTypes.U32@tok"
  ],
  0,
- "b92feb66af9dbbca634f3428a03dfce8"
+ "ee1449dfadf27251393f073b2b5a9b3b"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Ops.Range.fsti.hints b/proofs/fstar/extraction-edited/.hints/Core.Ops.Range.fsti.hints
@@ -8,7 +8,7 @@
  1,
  [ "@query" ],
  0,
- "5398350df56eb89c20a8ba53b10573fa"
+ "2f1c4ebd64b4ef2de2bf8ead9ea5fbd5"
  ],
  [
  "Core.Ops.Range.t_RangeFrom",
@@ -17,7 +17,7 @@
  1,
  [ "@query" ],
  0,
- "437362cec397474f5b8925b3245783f2"
+ "1c8410e9fff6969980b1c779dc7a0d0e"
  ],
  [
  "Core.Ops.Range.t_Range",
@@ -26,7 +26,7 @@
  1,
  [ "@query" ],
  0,
- "23b6132c3f6e53c1bc895ac90049e232"
+ "97054f685c7336ede743fd1deab8e3b7"
  ],
  [
  "Core.Ops.Range.fold_range'",
@@ -113,7 +113,7 @@
  "well-founded-ordering-on-nat"
  ],
  0,
- "de7afb4742bd05ac1a2150ce9b2f66ff"
+ "004d04f9ceb5b61d57ad4936af6b6f8e"
  ],
  [
  "Core.Ops.Range.iterator_range",
@@ -146,7 +146,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "70cffc878822fef0980e4605f5616d5a"
+ "6f470bc2d150339f7391d9c6ccee779c"
  ],
  [
  "Core.Ops.Range.impl_index_range_slice",
@@ -195,7 +195,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "3de7ca01540ee1194c44d8fa7d0cc728"
+ "922ce28a5109ef85001234f7492a0dd7"
  ],
  [
  "Core.Ops.Range.impl_index_range_to_slice",
@@ -243,7 +243,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "b24cda752d36c7df291a1050fec62b4a"
+ "7cb344bf8fc7ef9338622f5691294604"
  ],
  [
  "Core.Ops.Range.impl_index_range_from_slice",
@@ -285,7 +285,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "ce04978f6a0585224764eba2b493f2b2"
+ "cadfa962a493ca1f875624c5bb8081e9"
  ],
  [
  "Core.Ops.Range.impl_range_index_array",
@@ -306,7 +306,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "3692684509378c8ea71a01470c75b15b"
+ "96d0f32e631ac69972d6d9ad7aefabcf"
  ],
  [
  "Core.Ops.Range.impl_range_to_index_array",
@@ -327,7 +327,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "66d32ff6feda8c597d7d4116e9f346a2"
+ "f69ff4da52b25e1566b624876409c9c8"
  ],
  [
  "Core.Ops.Range.impl_range_from_index_array",
@@ -348,7 +348,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "5fb6376bf677c4b640d4709d955f92d0"
+ "71c1bfa7f48d8b4b2d92bd3231c7f2bc"
  ],
  [
  "Core.Ops.Range.impl_range_full_index_array",
@@ -369,7 +369,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "230722d2ec5e7889c8f2285ce4bfe03c"
+ "d162d4e11cb4daead2ee7c3d5687931c"
  ],
  [
  "Core.Ops.Range.update_at_tc_array_range",
@@ -386,7 +386,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "e6d465c3c1745148c6f9478bd5ea1196"
+ "8b243bdeabb6cac5ba23598c9c69e978"
  ],
  [
  "Core.Ops.Range.update_at_tc_array_range_to",
@@ -403,7 +403,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "63e37c8f5397769c870b7fe556d27916"
+ "31da2a6b84cfee9dd11aac73eb824c46"
  ],
  [
  "Core.Ops.Range.update_at_tc_array_range_from",
@@ -420,7 +420,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "6b197c3ba1b712eb23e9d66f798cd017"
+ "007bbd2a56f1b36601ce100c74d40e60"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Ops.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Ops.fst.hints
@@ -15,7 +15,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "2696b555db278ac0471d721e1d1e7fcd"
+ "3cd847f4f421eb1541c8febade998a71"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Panicking.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Panicking.fst.hints
@@ -11,7 +11,7 @@
  "refinement_interpretation_Tm_refine_f1ecc6ab6882a651504f328937700647"
  ],
  0,
- "b287358079d8631514c604e1d2ba8f28"
+ "924b83b2aead9f8e444ff57052e45f51"
  ],
  [
  "Core.Panicking.assert_failed",
@@ -23,7 +23,7 @@
  "refinement_interpretation_Tm_refine_f1ecc6ab6882a651504f328937700647"
  ],
  0,
- "8d32a257d54ea6209af4fa4daed14c75"
+ "d81c70fbf19b0ef9df144ad56f85efe8"
  ]
  ]
 ]