Merge branch 'main' into jonas/ml-dsa-target-feature

cryspen · Nov 5, 2024 · 5f88703 · 5f88703
2 parents 5c005e0 + 5ddbf9e
commit 5f88703
Show file tree

Hide file tree

Showing 10 changed files with 442 additions and 167 deletions.
diff --git a/.github/workflows/c.yml b/.github/workflows/c.yml
@@ -118,7 +118,7 @@ jobs:
 
       - name: 🔨 Build
         run: |
-          cmake -B build
+          LIBCRUX_BENCHMARKS=1 cmake -B build
           cmake --build build
 
       - name: 🏃🏻‍♀️ Test
@@ -132,7 +132,7 @@ jobs:
       - name: 🔨 Build Release
         run: |
           rm -rf build
-          cmake -B build -DCMAKE_BUILD_TYPE=Release
+          LIBCRUX_BENCHMARKS=1 cmake -B build -DCMAKE_BUILD_TYPE=Release
           cmake --build build --config Release
         if: ${{ matrix.os != 'windows-latest' }}
 
@@ -159,13 +159,6 @@ jobs:
           cmake -B build
           cmake --build build
       # FIXME: Benchmark build for cg on Windows CI is not working right now.
-        if: ${{ matrix.os != 'windows-latest' }}
-
-      # FIXME: Benchmark build for cg on Windows CI are not working right now.
-      # - name: 🏃🏻‍♀️ Test (cg)
-      #   working-directory: libcrux-ml-kem/cg
-      #   run: ./build/Debug/ml_kem_test
-      #   if: ${{ matrix.os == 'windows-latest' }}
 
       - name: 🏃🏻‍♀️ Test
         run: ./build/ml_kem_test

diff --git a/.github/workflows/s390x.yml b/.github/workflows/s390x.yml
@@ -0,0 +1,44 @@
+name: s390x - Build & Test
+
+on:
+  push:
+  pull_request:
+    branches: ["main", "dev"]
+  workflow_dispatch:
+  merge_group:
+
+env:
+  CARGO_TERM_COLOR: always
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  s390x:
+    runs-on: ubuntu-latest
+    name: Build on ubuntu-22.04 s390x
+    steps:
+      - uses: actions/checkout@v4
+      - uses: uraimo/run-on-arch-action@v2
+        name: Run
+        id: runcmd
+        with:
+          arch: s390x
+          distro: ubuntu22.04
+
+          # Speed up builds by storing container images in
+          # a GitHub package registry.
+          githubToken: ${{ github.token }}
+
+          run: |
+            apt-get -y update
+            apt-get install -y curl gcc g++ make cmake ninja-build git
+            cd libcrux-ml-kem/c
+            cmake -B build -G"Ninja Multi-Config"
+            cmake --build build
+            ./build/Debug/ml_kem_test
+            cd ../cg
+            cmake -B build -G"Ninja Multi-Config"
+            cmake --build build
+            ./build/Debug/ml_kem_test
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti
@@ -24,19 +24,19 @@ val shake256_x4
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_block_x4 (x: t_Shake256x4)
+val squeeze_first_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_five_blocks (x: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
+val squeeze_first_five_blocks (state: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
     : Prims.Pure
       (t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
         t_Array u8 (sz 840)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_next_block (x: t_Shake128x4)
+val squeeze_next_block (state: t_Shake128x4)
     : Prims.Pure
       (t_Shake128x4 &
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
@@ -140,7 +140,7 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
-val squeeze_next_block_x4 (x: t_Shake256x4)
+val squeeze_next_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti
@@ -21,6 +21,9 @@ val t_Shake256Absorb:Type0
 
 val t_Shake256Squeeze:Type0
 
+val init_absorb__init_absorb (input: t_Slice u8)
+    : Prims.Pure Libcrux_sha3.Portable.t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
+
 val init_absorb (input0 input1 input2 input3: t_Slice u8)
     : Prims.Pure t_Shake128X4 Prims.l_True (fun _ -> Prims.l_True)
 
@@ -69,22 +72,22 @@ val shake256_init: Prims.unit -> Prims.Pure t_Shake256Absorb Prims.l_True (fun _
 val shake256_squeeze (st: t_Shake256Squeeze) (out: t_Slice u8)
     : Prims.Pure (t_Shake256Squeeze & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_first_block_shake256 (x: t_Shake256)
+val squeeze_first_block_shake256 (state: t_Shake256)
     : Prims.Pure (t_Shake256 & t_Array u8 (sz 136)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_first_block_x4 (x: t_Shake256X4)
+val squeeze_first_block_x4 (state: t_Shake256X4)
     : Prims.Pure
       (t_Shake256X4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_five_blocks (x: t_Shake128X4) (out0 out1 out2 out3: t_Array u8 (sz 840))
+val squeeze_first_five_blocks (state: t_Shake128X4) (out0 out1 out2 out3: t_Array u8 (sz 840))
     : Prims.Pure
       (t_Shake128X4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
         t_Array u8 (sz 840)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_next_block (x: t_Shake128X4)
+val squeeze_next_block (state: t_Shake128X4)
     : Prims.Pure
       (t_Shake128X4 &
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
@@ -188,7 +191,7 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128X4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
-val squeeze_next_block_shake256 (x: t_Shake256)
+val squeeze_next_block_shake256 (state: t_Shake256)
     : Prims.Pure (t_Shake256 & t_Array u8 (sz 136)) Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
@@ -238,7 +241,7 @@ let impl_2: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof t_Shake256 =
       self, hax_temp_output <: (t_Shake256 & t_Array u8 (sz 136))
   }
 
-val squeeze_next_block_x4 (x: t_Shake256X4)
+val squeeze_next_block_x4 (state: t_Shake256X4)
     : Prims.Pure
       (t_Shake256X4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
@@ -27,19 +27,19 @@ val shake256_x4
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_block_x4 (x: t_Shake256x4)
+val squeeze_first_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_five_blocks (x: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
+val squeeze_first_five_blocks (state: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
     : Prims.Pure
       (t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
         t_Array u8 (sz 840)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_next_block (x: t_Shake128x4)
+val squeeze_next_block (state: t_Shake128x4)
     : Prims.Pure
       (t_Shake128x4 &
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
@@ -143,7 +143,7 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
-val squeeze_next_block_x4 (x: t_Shake256x4)
+val squeeze_next_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))