Adapt Kyber to use Init-Absorb-Squeeze* API

Cargo.toml

@@ -47,7 +47,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]

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

kyber-crate.sh

@@ -64,7 +64,7 @@ rm src/kyber512.rs
 rm src/kyber1024.rs
 
 # Build & test
-cargo test
+cargo build
 
 # Extract
 if [[ -z "$CHARON_HOME" ]]; then
@@ -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

proofs/fstar/extraction/Libcrux.Digest.fsti

@@ -9,23 +9,53 @@ val sha3_256_ (payload: t_Slice u8)
 val sha3_512_ (payload: t_Slice u8)
     : Prims.Pure (t_Array u8 (sz 64)) Prims.l_True (fun _ -> Prims.l_True)
 
-val shake128 (v_LEN: usize) (data: t_Slice u8)
-    : Prims.Pure (t_Array u8 v_LEN) Prims.l_True (fun _ -> Prims.l_True)
-
 val shake256 (v_LEN: usize) (data: t_Slice u8)
     : Prims.Pure (t_Array u8 v_LEN) Prims.l_True (fun _ -> Prims.l_True)
 
-val shake128x4_portable (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
-    : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
+val t_Shake128StateX2:Type
+
+val t_Shake128StateX3:Type
+
+val t_Shake128StateX4:Type
+
+val shake128_absorb_final_x2 (st: t_Shake128StateX2) (data0 data1: t_Slice u8)
+    : Prims.Pure t_Shake128StateX2 Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_absorb_final_x3 (st: t_Shake128StateX3) (data0 data1 data2: t_Slice u8)
+    : Prims.Pure t_Shake128StateX3 Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_absorb_final_x4 (st: t_Shake128StateX4) (data0 data1 data2 data3: t_Slice u8)
+    : Prims.Pure t_Shake128StateX4 Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_free_x2 (st: t_Shake128StateX2)
+    : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_free_x3 (st: t_Shake128StateX3)
+    : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_free_x4 (st: t_Shake128StateX4)
+    : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_init_x2: Prims.unit
+  -> Prims.Pure t_Shake128StateX2 Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_init_x3: Prims.unit
+  -> Prims.Pure t_Shake128StateX3 Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_init_x4: Prims.unit
+  -> Prims.Pure t_Shake128StateX4 Prims.l_True (fun _ -> Prims.l_True)
+
+val shake128_squeeze_nblocks_x2 (v_OUTPUT_BYTES: usize) (st: t_Shake128StateX2)
+    : Prims.Pure (t_Shake128StateX2 & t_Array (t_Array u8 v_OUTPUT_BYTES) (sz 2))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val shake128x4_256_ (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
-    : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
+val shake128_squeeze_nblocks_x3 (v_OUTPUT_BYTES: usize) (st: t_Shake128StateX3)
+    : Prims.Pure (t_Shake128StateX3 & t_Array (t_Array u8 v_OUTPUT_BYTES) (sz 3))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val shake128x4 (v_LEN: usize) (data0 data1 data2 data3: t_Slice u8)
-    : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
+val shake128_squeeze_nblocks_x4 (v_OUTPUT_BYTES: usize) (st: t_Shake128StateX4)
+    : Prims.Pure (t_Shake128StateX4 & t_Array (t_Array u8 v_OUTPUT_BYTES) (sz 4))
       Prims.l_True
       (fun _ -> Prims.l_True)

proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fsti

@@ -17,6 +17,4 @@ let v_FIELD_MODULUS: i32 = 3329l
 
 let v_H_DIGEST_SIZE: usize = sz 32
 
-let v_REJECTION_SAMPLING_SEED_SIZE: usize = sz 168 *! sz 5
-
 let v_SHARED_SECRET_SIZE: usize = sz 32