Merge pull request #202 from cryspen/lucas/serialize-proofs

Kyber: add proofs for `serialize_uncompressed_ring_element`
cryspen · Feb 20, 2024 · 795a599 · 795a599
2 parents 244ac38 + d686389
commit 795a599
Show file tree

Hide file tree

Showing 65 changed files with 6,982 additions and 5,497 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
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,
- "61d19e21e5ba401ccd51fac8dd4dc1bb"
+ "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,
- "89069ae0acc72a78e2efa55464713004"
+ "d99065ab1cecc1f4e429ca3f1178b733"
  ],
  [
  "Core.Convert.impl_6_refined",
@@ -71,7 +71,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "2e69cb8f79fbe8510f2c581d195eb17e"
+ "820c7d9e75762bc2bddd4d373dcc524a"
  ],
  [
  "Core.Convert.integer_into",
@@ -93,7 +93,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "4a75fc2edb3ec33d8d7d9232b2b0a9c1"
+ "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,
- "6385868cd0d0e2d5436d295085d9ece7"
+ "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,
- "cd17466b7eba81a3ad18f29a54ecdcfa"
+ "706694a0e0e6c2c02dc3b1a4e942410e"
  ]
  ]
 ]
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,
- "5e67dd92d9e724f630d50532cb4f36b6"
+ "66a9932a69b20c4a8f98d17fd83e53d6"
  ],
  [
  "Core.Iter.iterator_array_contains",
@@ -64,7 +64,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "9b3a6eac4d2d790e261dc9a792d7115c"
+ "e4c9913d7800c1eaa00ba7c16917f402"
  ]
  ]
 ]
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,
- "49c30328cc62eb103e966138f7d6bc4c"
+ "1a6141588a98f6a13327acb76aefcdf7"
  ],
  [
  "Core.Num.impl__u32__from_le_bytes",
@@ -47,7 +47,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "d81dfb79264e3e188fbd87697cc43338"
+ "b90a3012ce103b8f88b68a00a16caca3"
  ],
  [
  "Core.Num.impl__u32__from_be_bytes",
@@ -86,7 +86,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "aeb67c6090d6b471aa2b210a53a97b4d"
+ "55f8274f6b74b3aa0127595734423f8f"
  ],
  [
  "Core.Num.impl__u32__to_le_bytes",
@@ -125,7 +125,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "0ce9b8888a37d21a25e81a5a5c4bfe6e"
+ "5fe96e8ef6e2a1d99064e86fd374fdfe"
  ],
  [
  "Core.Num.impl__u32__to_be_bytes",
@@ -164,7 +164,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "7f04f9ea22cd0a14da00914f8d408fcf"
+ "259ad4b001842d020242998aaac5d6d7"
  ],
  [
  "Core.Num.impl__u64__from_le_bytes",
@@ -203,7 +203,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "c93947dab1fb3013cff8cad6b52b3c9c"
+ "e08e2ac36362ada4f519d369291b14c7"
  ],
  [
  "Core.Num.impl__u64__from_be_bytes",
@@ -242,7 +242,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "6a4e7bb9ec276bef8b1d210371d17790"
+ "182240cd37bb5ddba594ab5dcfe7f385"
  ],
  [
  "Core.Num.impl__u64__to_le_bytes",
@@ -281,7 +281,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "56167e58dc1efe630d223cd100c10899"
+ "f8492a1bfc04f6abac0940aab21fde92"
  ],
  [
  "Core.Num.impl__u64__to_be_bytes",
@@ -320,7 +320,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "903d9cc70ccbdfb98677bb2c9338bd37"
+ "88c2d9763fd89800abe716f80102f178"
  ],
  [
  "Core.Num.impl__u128__from_le_bytes",
@@ -359,7 +359,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "db8393219f7f9368ad04f51fda9d4439"
+ "887b154a5d2cae46f088e6a6d6b5eb42"
  ],
  [
  "Core.Num.impl__u128__from_be_bytes",
@@ -398,7 +398,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "e94c37e3e522f5b3f7d584eb358af67f"
+ "083e5e94e244f346dd1119176f10360f"
  ],
  [
  "Core.Num.impl__u128__to_le_bytes",
@@ -437,7 +437,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "15582e3fdf25975b9f64604ea6865777"
+ "0bd722eb7ee7a8f48106504fe46393ca"
  ],
  [
  "Core.Num.impl__u128__to_be_bytes",
@@ -476,7 +476,7 @@
  "typing_Rust_primitives.Integers.usize_inttype"
  ],
  0,
- "948bf2141fe892e8e60b3930afd99afa"
+ "9ad536f1aa71edd5edf1fc9d4c865041"
  ],
  [
  "Core.Num.impl__u16__pow",
@@ -530,7 +530,7 @@
  "typing_tok_Lib.IntTypes.U32@tok"
  ],
  0,
- "f81005b265bd0f2c8a69c3a58ef3957f"
+ "f0d9ee449fb2d70bd4c2ef2a69699e89"
  ],
  [
  "Core.Num.impl__u32__pow",
@@ -579,7 +579,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
  ],
  0,
- "66242ac093c2f011ce65faa03ae6c3d1"
+ "188ce25bae866baa7924954c732c7e30"
  ],
  [
  "Core.Num.impl__i32__pow",
@@ -623,16 +623,15 @@
  "refinement_interpretation_Tm_refine_a6d4eccfb2603ce5e66d6162c32df2b0",
  "refinement_interpretation_Tm_refine_bacb80e693f1faab8ffabcbb77914bec",
  "token_correspondence_Prims.pow2.fuel_instrumented",
- "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
- "typing_Rust_primitives.Integers.range",
+ "typing_Lib.IntTypes.v", "typing_Rust_primitives.Integers.range",
  "typing_Rust_primitives.Integers.unsigned",
  "typing_Rust_primitives.Integers.usize_inttype",
  "typing_Rust_primitives.Integers.v",
  "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.S32@tok",
  "typing_tok_Lib.IntTypes.U32@tok"
  ],
  0,
- "ee1449dfadf27251393f073b2b5a9b3b"
+ "f7921d8f289ecc4a100c8c4d629bc166"
  ]
  ]
 ]
diff --git a/proofs/fstar/extraction-edited/.hints/Core.Ops.Index.fst.hints b/proofs/fstar/extraction-edited/.hints/Core.Ops.Index.fst.hints
@@ -1 +1 @@
-[ "���B��Qtq�u���V\u0004", [] ]
+[ "IT�\"�֤�S+I�`���", [] ]
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,
- "2f1c4ebd64b4ef2de2bf8ead9ea5fbd5"
+ "44802066e80e4c98fe0a5522fa8d77fc"
  ],
  [
  "Core.Ops.Range.t_RangeFrom",
@@ -17,7 +17,7 @@
  1,
  [ "@query" ],
  0,
- "1c8410e9fff6969980b1c779dc7a0d0e"
+ "cbf8164fc30162c1d873ea3690811a50"
  ],
  [
  "Core.Ops.Range.t_Range",
@@ -26,7 +26,7 @@
  1,
  [ "@query" ],
  0,
- "97054f685c7336ede743fd1deab8e3b7"
+ "73f8d83e4d7ace78f9bb275b6ada4c6b"
  ],
  [
  "Core.Ops.Range.fold_range'",
@@ -113,7 +113,7 @@
  "well-founded-ordering-on-nat"
  ],
  0,
- "004d04f9ceb5b61d57ad4936af6b6f8e"
+ "afbc273a622a53b6b9e90bab13313c65"
  ],
  [
  "Core.Ops.Range.iterator_range",
@@ -146,7 +146,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "6f470bc2d150339f7391d9c6ccee779c"
+ "59671aa05874272d4ee72812d3550023"
  ],
  [
  "Core.Ops.Range.impl_index_range_slice",
@@ -195,7 +195,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "922ce28a5109ef85001234f7492a0dd7"
+ "003fe8264515ab8b0ef4ba55335b87bd"
  ],
  [
  "Core.Ops.Range.impl_index_range_to_slice",
@@ -243,7 +243,7 @@
  "typing_tok_Lib.IntTypes.PUB@tok"
  ],
  0,
- "7cb344bf8fc7ef9338622f5691294604"
+ "85f3152a14fd46cde8c2e6e48e6c0192"
  ],
  [
  "Core.Ops.Range.impl_index_range_from_slice",
@@ -285,7 +285,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "cadfa962a493ca1f875624c5bb8081e9"
+ "3e98e6c80e1781977669d9d104d3dfcc"
  ],
  [
  "Core.Ops.Range.impl_range_index_array",
@@ -306,7 +306,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "96d0f32e631ac69972d6d9ad7aefabcf"
+ "2f2f0c3904069e1dfada5bd6852fe37c"
  ],
  [
  "Core.Ops.Range.impl_range_to_index_array",
@@ -327,7 +327,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "f69ff4da52b25e1566b624876409c9c8"
+ "030a540e8763c6ff54660532fc151a01"
  ],
  [
  "Core.Ops.Range.impl_range_from_index_array",
@@ -348,7 +348,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "71c1bfa7f48d8b4b2d92bd3231c7f2bc"
+ "3c62c0577dff57fb3b9e6210bd5d4e1f"
  ],
  [
  "Core.Ops.Range.impl_range_full_index_array",
@@ -369,7 +369,7 @@
  "typing_Rust_primitives.Integers.v"
  ],
  0,
- "d162d4e11cb4daead2ee7c3d5687931c"
+ "d9901e0ec1592849572a39f7583f5c56"
  ],
  [
  "Core.Ops.Range.update_at_tc_array_range",
@@ -386,7 +386,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "8b243bdeabb6cac5ba23598c9c69e978"
+ "91c133608a751b616967f9ef3254331b"
  ],
  [
  "Core.Ops.Range.update_at_tc_array_range_to",
@@ -403,7 +403,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "31da2a6b84cfee9dd11aac73eb824c46"
+ "8194aa85d51d0296cfa3c14059e8a592"
  ],
  [
  "Core.Ops.Range.update_at_tc_array_range_from",
@@ -420,7 +420,7 @@
  "token_correspondence_Core.Ops.Index.in_range"
  ],
  0,
- "007bbd2a56f1b36601ce100c74d40e60"
+ "9b9bfff4e9780936c49455895a70726e"
  ]
  ]
 ]
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,
- "3cd847f4f421eb1541c8febade998a71"
+ "37bba1d678031983b3fa984afca61e02"
  ]
  ]
 ]