Merge branch 'main' of github.com:cryspen/libcrux into x25519-benchmarks

cryspen · Mar 14, 2024 · 950df71 · 950df71
2 parents a98e242 + 700700f
commit 950df71
Show file tree

Hide file tree

Showing 87 changed files with 10,331 additions and 5,184 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -48,7 +48,7 @@ wasm-bindgen = { version = "0.2.87", optional = true }
 # When using the hax toolchain, we have more dependencies.
 # This is only required when doing proofs.
 [target.'cfg(hax)'.dependencies]
-hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax" }
+hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax", branch = "main" }
 hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax/", branch = "main" }
 
 [target.'cfg(all(not(target_os = "windows"), target_arch = "x86_64", libjade))'.dependencies]
@@ -75,3 +75,4 @@ rand = []
 wasm = ["wasm-bindgen"]
 log = ["dep:log"]
 tests = []              # Expose functions for testing.
+experimental = []       # Expose experimental APIs.
diff --git a/hax-driver.py b/hax-driver.py
@@ -127,7 +127,7 @@ def shell(command, expect=0, cwd=None, env={}):
             f"-** +libcrux::kem::kyber::** +!libcrux_platform::platform::* {exclude_sha3_implementations} -libcrux::**::types::index_impls::**",
             "fstar",
             "--interfaces",
-            "+* -libcrux::kem::kyber::types +!libcrux_platform::**",
+            "+* -libcrux::kem::kyber::types +!libcrux_platform::** +!libcrux::digest::**",
         ],
         cwd=".",
         env=hax_env,
@@ -136,6 +136,7 @@ def shell(command, expect=0, cwd=None, env={}):
     # remove this when https://github.com/hacspec/hax/issues/465 is
     # closed)
     shell(["rm", "-f", "./sys/platform/proofs/fstar/extraction/*.fst"])
+
 elif options.kyber_specification:
     shell(
         cargo_hax_into

diff --git a/kyber-c.yaml b/kyber-c.yaml
@@ -2,6 +2,8 @@ files:
   - name: libcrux_digest
     api:
       - [libcrux, digest]
+    include_in_h:
+      - '"libcrux_hacl_glue.h"'
   - name: libcrux_platform
     api:
       - [libcrux_platform]

diff --git a/kyber-crate.sh b/kyber-crate.sh
@@ -90,5 +90,6 @@ if [[ -n "$HACL_PACKAGES_HOME" ]]; then
     cp internal/*.h $HACL_PACKAGES_HOME/libcrux/include/internal/
     cp *.h $HACL_PACKAGES_HOME/libcrux/include
     cp *.c $HACL_PACKAGES_HOME/libcrux/src
+else
+    echo "Please set HACL_PACKAGES_HOME to the hacl-packages directory to copy the code over" 1>&2
 fi
-echo "Please set HACL_PACKAGES_HOME to the hacl-packages directory to copy the code over" 1>&2
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,
-      "59286762d349f5b9996787df0af368ff"
+      "6a574a6f81c5274515c87add317414d6"
     ],
     [
       "BitVecEq.bit_vec_equal_intro_principle",
@@ -21,7 +21,7 @@
         "refinement_interpretation_Tm_refine_5ea27f29671734c284c74b54ac71be4c"
       ],
       0,
-      "3d0c51c3f21387d10ee3aa036bd8db3f"
+      "374053bd3504bc87451f12484059f709"
     ],
     [
       "BitVecEq.bit_vec_equal_elim_principle",
@@ -35,7 +35,7 @@
         "refinement_interpretation_Tm_refine_f7508cd976fab894dc1e01a7483287a6"
       ],
       0,
-      "fb4df4d22434569a63b52b3218e8f855"
+      "02772f8a9f8084edf942cd24f3d6cb52"
     ],
     [
       "BitVecEq.bit_vec_equal_trivial",
@@ -49,7 +49,7 @@
         "refinement_interpretation_Tm_refine_c9b1a93dc7180dbdeb887c6ba6a0bb06"
       ],
       0,
-      "a5dee7de8b06e3799cab7df1effbcf3b"
+      "cf68ac27da6fe8ae5157e5a28a8130cf"
     ],
     [
       "BitVecEq.bit_vec_sub",
@@ -65,7 +65,7 @@
         "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
       ],
       0,
-      "71775bf4907d2e9a78fd031450e8c8b8"
+      "6f307d59f44e1885f7a07d2a406058c4"
     ],
     [
       "BitVecEq.bit_vec_equal_trivial_sub_smtpat",
@@ -78,7 +78,7 @@
         "refinement_interpretation_Tm_refine_c5efe95b1f250c44fbd9d953d94aff03"
       ],
       0,
-      "05922fc60aa639c5fdae7ff386e6afb1"
+      "5b2e0a625de73e6e1805cdb2737266d7"
     ],
     [
       "BitVecEq.retype",
@@ -90,7 +90,7 @@
         "refinement_interpretation_Tm_refine_0dee8cb03258a67c2f7ec66427696212"
       ],
       0,
-      "16f3278bdf9a68771f24f37804da3c34"
+      "e4c87258d3cdfcf4dedbacc6663e6694"
     ],
     [
       "BitVecEq.bit_vec_sub_all_lemma",
@@ -119,7 +119,7 @@
         "typing_Tm_abs_eb643fbfbab7ef908ba32052bb948a4f"
       ],
       0,
-      "5e840c192bca659cc1bf0712abcb1518"
+      "cf05827893638854ad27d07daf2ec103"
     ],
     [
       "BitVecEq.int_t_array_bitwise_eq'",
@@ -155,7 +155,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "0ba66af0f657c91b2cc8a74a30e60f05"
+      "a486f9f95b292dba0b04817197ecffdc"
     ],
     [
       "BitVecEq.int_t_array_bitwise_eq",
@@ -167,7 +167,7 @@
         "refinement_interpretation_Tm_refine_4e3dded9bf4fcf599168cbb137ff3724"
       ],
       0,
-      "85a311e3e1961e4f078860f8115a4e4e"
+      "2746823a0349065377721a63ad3fb6be"
     ],
     [
       "BitVecEq.int_t_seq_slice_to_bv_sub_lemma",
@@ -255,7 +255,7 @@
         "typing_tok_Lib.IntTypes.PUB@tok"
       ],
       0,
-      "ef738c7466342befcd8b3034bfffae5c"
+      "b5028a1765520ca8148e006efe228cf9"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -269,7 +269,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "30858238a464e5c4ad0717a6f6c18cc8"
+      "af892a6ccc37e4b5257ac828e7c3cfad"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -283,7 +283,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "ae4a6a72282782af80c5cdf5eba27264"
+      "e627b7c97bf4a305252f129e4d99268c"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -298,7 +298,7 @@
         "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
       ],
       0,
-      "47b98f832e2fbb8e465077c8e85f8d45"
+      "01e9f26e6ed6c409ddcec9c171f8da4a"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -312,7 +312,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "7f1a73a0b63defe94e6fd819bb8a9322"
+      "d5ff3c1c5713a86f1bcbde3602d9fd00"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -326,7 +326,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "5906e3ef95f02a54636fa0b5ad4ebe2c"
+      "58d5a1b396729fb7bc74b0f684fba4e5"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -341,7 +341,7 @@
         "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
       ],
       0,
-      "6420ceb33586fff6632de715ba4c8a62"
+      "aa7f079cf196531bbbcdf09084bf58de"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -356,7 +356,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "15bc552eec8074539add83fd6fd6860d"
+      "821359d47804856c9bc65d8680476fef"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -370,7 +370,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "eabfb42b4b25d271ac9e25fc5087db07"
+      "bf19e9e89c9b9d201fe90216bc239ea5"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -385,7 +385,7 @@
         "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
       ],
       0,
-      "a3594ab47cfb3172b83525084cd15aa0"
+      "2b66012ab81f6b94629914e5049b0952"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -400,7 +400,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "3e4a3b84589bbad98942a5ff49b35d85"
+      "8d98efff316f7dda6056b7936e6e3927"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -414,7 +414,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "45cf555c20c371deb335e95c4fa385e4"
+      "8709db768b1264f948cd4c4e46b00bdd"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -429,7 +429,7 @@
         "refinement_interpretation_Tm_refine_53d7089a905511e9e713c7dbc2f68178"
       ],
       0,
-      "a62605948d6dc81aacd2f3b35e8a8086"
+      "aee822ea1efbe9193bf30b8ad58c071a"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -445,7 +445,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "cb51082c08944ddb750bf5986bee2436"
+      "01c470e7d79fd55df31477976c1ee64b"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -478,7 +478,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "ef0d0901ecceaebdfd9c2dc671838624"
+      "09e58b5172b12c3a7535c8799a51d655"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -493,7 +493,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "5dc44008c007807c1865c9864404c3b2"
+      "6e98af62ae0fe1f0feb143b6c27fb4ea"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -506,7 +506,7 @@
         "refinement_interpretation_Tm_refine_90b5d2df39645a4835173a203da069e4"
       ],
       0,
-      "11484adb2bfd480f49799a588c6c2089"
+      "43ef1a4fbe8292c08bc6b0c5289cb8f8"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -551,7 +551,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "3c9bcb87d09adc01578b5c138f6953f4"
+      "686a5a59d01e564277aa7dd6006d3a92"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -583,7 +583,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "43e11403c8477940124f71b6c9bd6eac"
+      "c882f3bf0e83ab723b3471fd5b841550"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -598,7 +598,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
       ],
       0,
-      "d8dd5ea9e5ad6ee14ab9df1fbff54b2f"
+      "5c75df913421b4019c9aba3eb558386e"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -611,7 +611,7 @@
         "refinement_interpretation_Tm_refine_90b5d2df39645a4835173a203da069e4"
       ],
       0,
-      "f81fd4ebba605222fa35e0f95ad9968f"
+      "c24aee061d663aedf323efdf700220c4"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -664,7 +664,7 @@
         "typing_Rust_primitives.Integers.usize_inttype"
       ],
       0,
-      "7889c89b1c0a2b405d736c0ef8eac088"
+      "1965bd1bdb0d5a3d195793cbceeb124e"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -693,7 +693,7 @@
         "typing_Rust_primitives.Integers.v"
       ],
       0,
-      "d43c1e98741782237557ac46f9ee39a6"
+      "b696d39adfdeaffa9de6ba5636311f52"
     ],
     [
       "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,
-      "45d878fc2a402454f4ce4a8270753833"
+      "51342383de916fbe77cf2477bf6b8b94"
     ],
     [
       "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,
-      "d80a0f4aeab61c20bef4845a3dca55cd"
+      "06714e4af0fcbeeda1945d064ffc7ee4"
     ],
     [
       "BitVecEq.int_t_eq_seq_slice_bv_sub_lemma",
@@ -863,7 +863,7 @@
         "unit_inversion"
       ],
       0,
-      "6213700a8a1c881dd848638983196926"
+      "797ebaced8dc237dbadcb3501e07e361"
     ],
     [
       "BitVecEq.bit_vec_equal_extend",
@@ -905,7 +905,7 @@
         "typing_Tm_abs_eb643fbfbab7ef908ba32052bb948a4f"
       ],
       0,
-      "381db8a80993f6e8254bf0eee19b774c"
+      "352982a792534fa365ac5926e87e6d54"
     ]
   ]
 ]
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,
-      "c86718181e1e8d01f7209e7c2a75f48f"
+      "5adccb8550fe495b40c6be68b7d30511"
     ]
   ]
 ]