Use hacl sha3 mb

Cargo.toml

@@ -9,7 +9,7 @@ members = [
 ]
 
 [workspace.package]
-version = "0.0.2-pre.1"
+version = "0.0.2-pre.2"
 authors = ["Cryspen"]
 license = "Apache-2.0"
 homepage = "https://github.com/cryspen/libcrux"
@@ -34,11 +34,11 @@ exclude = ["/tests", "/specs"]
 crate-type = ["staticlib", "cdylib", "lib"]
 
 [build-dependencies]
-libcrux-platform = { version = "=0.0.2-pre.1", path = "sys/platform" }
+libcrux-platform = { version = "=0.0.2-pre.2", path = "sys/platform" }
 
 [dependencies]
-libcrux-hacl = { version = "=0.0.2-pre.1", path = "sys/hacl" }
-libcrux-platform = { version = "=0.0.2-pre.1", path = "sys/platform" }
+libcrux-hacl = { version = "=0.0.2-pre.2", path = "sys/hacl" }
+libcrux-platform = { version = "=0.0.2-pre.2", path = "sys/platform" }
 rand = { version = "0.8" }
 log = { version = "0.4", optional = true }
 # WASM API
@@ -55,7 +55,7 @@ hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/ha
 getrandom = { version = "0.2", features = ["js"] }
 
 [target.'cfg(all(not(target_os = "windows"), target_arch = "x86_64"))'.dependencies]
-libjade-sys = { version = "=0.0.2-pre.1", path = "sys/libjade" }
+libjade-sys = { version = "=0.0.2-pre.2", path = "sys/libjade" }
 
 [dev-dependencies]
 libcrux = { path = ".", features = ["rand"] }

PUBLISHING.md

@@ -0,0 +1,9 @@
+# Release Management
+
+1. Update version in `Cargo.toml` and set all dependencies to that version. Always start with a prerelease version `-pre.A` before doing a full release.
+2. Tag the version `git tag vX.Y.Z` and `git push origin vX.Y.Z`.
+3. Release crates
+   1. libcrux-platform in `sys/platform`
+   2. libcrux-hacl in `sys/hacl`
+   3. libjade-sys in `sys/libjade`
+   4. libcrux

proofs/fstar/extraction/Libcrux.Digest.fsti

@@ -36,4 +36,6 @@ val sha3_512_ (payload: t_Slice u8) : t_Array u8 (sz 64)
 
 val shake128 (v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN
 
+val shake128x4 (v_LEN: usize) (data0: t_Slice u8) (data1: t_Slice u8) (data2: t_Slice u8) (data3: t_Slice u8): (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
+
 val shake256 (v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN

proofs/fstar/extraction/Libcrux.Kem.Kyber.Hash_functions.fst

@@ -10,31 +10,96 @@ let v_H (input: t_Slice u8) : t_Array u8 (sz 32) = Libcrux.Digest.sha3_256_ inpu
 let v_PRF (v_LEN: usize) (input: t_Slice u8) : t_Array u8 v_LEN =
   Libcrux.Digest.shake256 v_LEN input
 
-let v_XOFx4 (v_LEN v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K)
-    : t_Array (t_Array u8 v_LEN) v_K =
-  let out:t_Array (t_Array u8 v_LEN) v_K =
-    Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy v_LEN <: t_Array u8 v_LEN) v_K
+let v_XOFx4 (v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K)
+    : t_Array (t_Array u8 (sz 840)) v_K =
+  let out:t_Array (t_Array u8 (sz 840)) v_K =
+    Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy (sz 840) <: t_Array u8 (sz 840)) v_K
   in
-  let out:t_Array (t_Array u8 v_LEN) v_K =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = v_K
-            }
-            <:
-            Core.Ops.Range.t_Range usize)
-        <:
-        Core.Ops.Range.t_Range usize)
-      out
-      (fun out i ->
-          let out:t_Array (t_Array u8 v_LEN) v_K = out in
-          let i:usize = i in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
-            i
-            (Libcrux.Digest.shake128 v_LEN
-                (Rust_primitives.unsize (input.[ i ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+  let out:t_Array (t_Array u8 (sz 840)) v_K =
+    if ~.(Libcrux_platform.simd256_support <: bool) || ~.false
+    then
+      Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
+                Core.Ops.Range.f_start = sz 0;
+                Core.Ops.Range.f_end = v_K
+              }
               <:
-              t_Array u8 v_LEN)
+              Core.Ops.Range.t_Range usize)
           <:
-          t_Array (t_Array u8 v_LEN) v_K)
+          Core.Ops.Range.t_Range usize)
+        out
+        (fun out i ->
+            let out:t_Array (t_Array u8 (sz 840)) v_K = out in
+            let i:usize = i in
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
+              i
+              (Libcrux.Digest.shake128 (sz 840)
+                  (Rust_primitives.unsize (input.[ i ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+                <:
+                t_Array u8 (sz 840))
+            <:
+            t_Array (t_Array u8 (sz 840)) v_K)
+    else
+      let out:t_Array (t_Array u8 (sz 840)) v_K =
+        match cast (v_K <: usize) <: u8 with
+        | 2uy ->
+          let d0, d1, _, _:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
+            t_Array u8 (sz 840)) =
+            Libcrux.Digest.shake128x4 (sz 840)
+              (Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 0) d0
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 1) d1
+          in
+          out
+        | 3uy ->
+          let d0, d1, d2, _:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
+            t_Array u8 (sz 840)) =
+            Libcrux.Digest.shake128x4 (sz 840)
+              (Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 2 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 0) d0
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 1) d1
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 2) d2
+          in
+          out
+        | 4uy ->
+          let d0, d1, d2, d3:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
+            t_Array u8 (sz 840)) =
+            Libcrux.Digest.shake128x4 (sz 840)
+              (Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 2 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+              (Rust_primitives.unsize (input.[ sz 3 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 0) d0
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 1) d1
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 2) d2
+          in
+          let out:t_Array (t_Array u8 (sz 840)) v_K =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 3) d3
+          in
+          out
+        | _ -> out
+      in
+      out
   in
   out

proofs/fstar/extraction/Libcrux.Kem.Kyber.Matrix.fst

@@ -494,7 +494,7 @@ let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
                   seeds)
           in
           let xof_bytes:t_Array (t_Array u8 (sz 840)) v_K =
-            Libcrux.Kem.Kyber.Hash_functions.v_XOFx4 (sz 840) v_K seeds
+            Libcrux.Kem.Kyber.Hash_functions.v_XOFx4 v_K seeds
           in
           Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                     Core.Ops.Range.f_start = sz 0;

proofs/fstar/extraction/Libcrux_platform.fsti

@@ -0,0 +1,4 @@
+module Libcrux_platform
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+
+val simd256_support: bool

proofs/fstar/extraction/Makefile

@@ -49,6 +49,7 @@ all:
 
 
 VERIFIED = \
+	Libcrux_platform.fsti \
 	Libcrux.Kem.fst \
 	Libcrux.Kem.Kyber.Constants.fst \
 	Libcrux.Digest.fsti \

specs/kyber/Cargo.toml

@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-libcrux = { version = "=0.0.2-pre.1", path = "../../" }
+libcrux = { version = "=0.0.2-pre.2", path = "../../" }
 hacspec-lib = { version = "0.0.1", path = "../hacspec-lib" }
 
 [dev-dependencies]

specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Compress.fst

@@ -1,23 +1,29 @@
 module Hacspec_kyber.Compress
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
+open FStar.Mul
+
+let decompress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size: usize)
+    : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
+  let _:Prims.unit =
+    if ~.(to_bit_size <=. Hacspec_kyber.Parameters.v_BITS_PER_COEFFICIENT <: bool)
+    then
+      Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= parameters::BITS_PER_COEFFICIENT"
 
-let compress
-      (re:
-          Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
-            (sz 256))
-      (bits_per_compressed_coefficient: usize)
-    : Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
-      (sz 256) =
-  Hacspec_lib.Ring.impl_2__new (Core.Array.impl_23__map (Hacspec_lib.Ring.impl_2__coefficients re
           <:
-          t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
-        (fun coefficient ->
-            compress_d coefficient bits_per_compressed_coefficient
-            <:
-            Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+          Rust_primitives.Hax.t_Never)
+  in
+  let decompressed:u32 =
+    (((2ul *! (Core.Convert.f_from fe.Hacspec_lib.Field.f_value <: u32) <: u32) *!
+        (Core.Convert.f_from Hacspec_lib.Field.impl_2__MODULUS_1 <: u32)
+        <:
+        u32) +!
+      (1ul <<! to_bit_size <: u32)
       <:
-      t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+      u32) >>!
+    (to_bit_size +! sz 1 <: usize)
+  in
+  Core.Convert.f_into decompressed
 
 let decompress
       (re:
@@ -26,10 +32,13 @@ let decompress
       (bits_per_compressed_coefficient: usize)
     : Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       (sz 256) =
-  Hacspec_lib.Ring.impl_2__new (Core.Array.impl_23__map (Hacspec_lib.Ring.impl_2__coefficients re
+  Hacspec_lib.Ring.impl_2__new (sz 256)
+    (Core.Array.impl_23__map (sz 256)
+        (Hacspec_lib.Ring.impl_2__coefficients (sz 256) re
           <:
           t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
         (fun coefficient ->
+            let coefficient:Hacspec_lib.Field.t_PrimeFieldElement 3329us = coefficient in
             decompress_d coefficient bits_per_compressed_coefficient
             <:
             Hacspec_lib.Field.t_PrimeFieldElement 3329us)
@@ -51,7 +60,8 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
       (Core.Result.impl__unwrap_or_else (Core.Convert.f_try_into to_bit_size
             <:
             Core.Result.t_Result u32 Core.Num.Error.t_TryFromIntError)
-          (fun _ ->
+          (fun temp_0_ ->
+              let _:Core.Num.Error.t_TryFromIntError = temp_0_ in
               Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize
                             (let list =
                                 [
@@ -95,24 +105,22 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
   in
   Core.Convert.f_into (compressed %! two_pow_bit_size <: u32)
 
-let decompress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size: usize)
-    : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
-  let _:Prims.unit =
-    if ~.(to_bit_size <=. Hacspec_kyber.Parameters.v_BITS_PER_COEFFICIENT <: bool)
-    then
-      Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= parameters::BITS_PER_COEFFICIENT"
-
+let compress
+      (re:
+          Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+            (sz 256))
+      (bits_per_compressed_coefficient: usize)
+    : Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+      (sz 256) =
+  Hacspec_lib.Ring.impl_2__new (sz 256)
+    (Core.Array.impl_23__map (sz 256)
+        (Hacspec_lib.Ring.impl_2__coefficients (sz 256) re
           <:
-          Rust_primitives.Hax.t_Never)
-  in
-  let decompressed:u32 =
-    (((2ul *! (Core.Convert.f_from fe.Hacspec_lib.Field.f_value <: u32) <: u32) *!
-        (Core.Convert.f_from Hacspec_lib.Field.impl_2__MODULUS_1 <: u32)
-        <:
-        u32) +!
-      (1ul <<! to_bit_size <: u32)
+          t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+        (fun coefficient ->
+            let coefficient:Hacspec_lib.Field.t_PrimeFieldElement 3329us = coefficient in
+            compress_d coefficient bits_per_compressed_coefficient
+            <:
+            Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       <:
-      u32) >>!
-    (to_bit_size +! sz 1 <: usize)
-  in
-  Core.Convert.f_into decompressed
+      t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))