how to use hax macros

cryspen · Oct 31, 2023 · f550e13 · f550e13
1 parent ded63e9
commit f550e13
Show file tree

Hide file tree

Showing 7 changed files with 13,482 additions and 138 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -37,6 +37,11 @@ log = { version = "0.4", optional = true }
 # WASM API
 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" }
+
 # WASM needs the js feature on getrandom
 [target.'cfg(target_arch = "wasm32")'.dependencies]
 getrandom = { version = "0.2", features = ["js"] }

diff --git a/hax-driver.py b/hax-driver.py
@@ -9,6 +9,7 @@
 def shell(command, expect=0, cwd=None, env={}):
     subprocess_stdout = subprocess.DEVNULL
 
+    print("Env: ", env)
     print("Command: ", end="")
     for i, word in enumerate(command):
         if i == 4:
@@ -118,43 +119,43 @@ def shell(command, expect=0, cwd=None, env={}):
     shell(["make", "-C", "proofs/fstar/extraction/"], custom_env)
     exit(0)
 
+cargo_hax_into = ["cargo", "hax", "into"]
+hax_env = {"RUSTFLAGS": "--cfg hax"}
+
 if options.kyber_reference:
     shell(
-        [
-            "cargo",
-            "hax",
-            "into",
+        cargo_hax_into
+        + [
             "-i",
             "-** +libcrux::kem::kyber::** -libcrux::hacl::sha3::** -libcrux::digest::**",
             "fstar",
         ],
         cwd=".",
+        env=hax_env,
     )
 elif options.kyber_specification:
     shell(
-        [
-            "cargo",
-            "hax",
-            "into",
+        cargo_hax_into
+        + [
             "-i",
             "-** +compress::* +ind_cpa::* +hacspec_kyber::* +matrix::* +ntt::* +parameters::* +sampling::* +serialize::* -libcrux::hacl::sha3::* -libcrux::digest::*",
             "fstar",
         ],
         cwd=os.path.join("specs", "kyber"),
+        env=hax_env,
     )
 
 else:
     if filter_string:
         shell(
-            [
-                "cargo",
-                "hax",
-                "into",
+            cargo_hax_into
+            + [
                 "-i",
                 "-** {}".format(filter_string),
                 "fstar",
             ],
             cwd=options.crate_path,
+            env=hax_env,
         )
     else:
-        shell(["cargo", "hax", "into", "fstar"], cwd=options.crate_path)
+        shell(cargo_hax_into + ["fstar"], cwd=options.crate_path, env=hax_env)
diff --git a/proofs/fstar/extraction/.depend b/proofs/fstar/extraction/.depend
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst
@@ -8,7 +8,12 @@ let v_BARRETT_R: i32 = 1l <<! v_BARRETT_SHIFT
 
 let v_BARRETT_MULTIPLIER: i32 = 20159l
 
-let barrett_reduce (value: i32) : i32 =
+let barrett_reduce (value: i32)
+    : Prims.Pure i32
+      (requires
+        value >. ((Core.Ops.Arith.Neg.neg v_BARRETT_R <: i32) /! 2l <: i32) &&
+        value <. (v_BARRETT_R /! 2l <: i32))
+      (fun _ -> Prims.l_True) =
   let _:Prims.unit =
     if true
     then

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Conversions.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Conversions.fst
@@ -39,7 +39,7 @@ class t_UpdatingArray (#v_Self: Type) = {
   f_push:v_Self -> t_Slice u8 -> v_Self
 }
 
-type t_UpdatableArray (#v_LEN: usize) = {
+type t_UpdatableArray (v_LEN: usize) = {
   f_value:t_Array u8 v_LEN;
   f_pointer:usize
 }
@@ -53,7 +53,7 @@ let impl_1 (#v_LEN: usize) : t_UpdatingArray (t_UpdatableArray v_LEN) =
   {
     f_push
     =
-    fun (#v_LEN: usize) (self: t_UpdatableArray v_LEN) (other: t_Slice u8) ->
+    fun (self: t_UpdatableArray v_LEN) (other: t_Slice u8) ->
       let self:t_UpdatableArray v_LEN =
         {
           self with