Merging main into dev

.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

.github/workflows/hax.yml

@@ -68,4 +68,13 @@ jobs:
 
       - name: 🏃 Extract ML-DSA crate
         working-directory: libcrux-ml-dsa
-        run: cargo hax into fstar
+        run: ./hax.py extract
+
+      - name: 🏃 Lax ML-DSA crate
+        working-directory: libcrux-ml-dsa
+        run: |
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_HOME=${{ github.workspace }}/hax \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+              ./hax.py prove --admit

.github/workflows/mlkem.yml

@@ -87,11 +87,6 @@ jobs:
           rustc --print=cfg
           cargo build --verbose $RUST_TARGET_FLAG --features pre-verification
 
-      - name: 🔨 Build unpacked
-        run: |
-          rustc --print=cfg
-          cargo build --verbose $RUST_TARGET_FLAG --features pre-verification,unpacked
-
       - name: 🔨 Build Release
         run: cargo build --verbose --release $RUST_TARGET_FLAG --features pre-verification
 
@@ -173,3 +168,37 @@ jobs:
         run: |
           cargo clean
           cargo hack test --each-feature $EXCLUDE_FEATURES --verbose $RUST_TARGET_FLAG
+
+  fuzz:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest # macos-14 m1
+          - ubuntu-latest
+
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+        working-directory: libcrux-ml-kem
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: 🛠️ Setup Rust Nightly
+        run: |
+          rustup toolchain install nightly
+          cargo install cargo-fuzz
+
+      - name: 🛠️ Update dependencies
+        run: cargo update
+
+      - name: 🏃🏻‍♀️ Decaps
+        run: CARGO_PROFILE_RELEASE_LTO=false cargo +nightly fuzz run decaps -- -runs=100000
+
+      - name: 🏃🏻‍♀️ Encaps
+        run: CARGO_PROFILE_RELEASE_LTO=false cargo +nightly fuzz run encaps -- -runs=100000
+
+      - name: 🏃🏻‍♀️ KeyGen
+        run: CARGO_PROFILE_RELEASE_LTO=false cargo +nightly fuzz run keygen -- -runs=1000000

.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

.gitignore

@@ -15,6 +15,6 @@ kyber-crate/
 # F*
 .fstar-cache
 .depend
-**/proofs/fstar/*/#*#
-**/proofs/fstar/*/.#*
+/proofs/fstar/*/#*#
+/proofs/fstar/*/.#*
 hax.fst.config.json

Cargo.toml

@@ -8,6 +8,7 @@ members = [
     "benchmarks",
     "fuzz",
     "libcrux-ml-kem",
+    "libcrux-ml-kem/fuzz",
     "libcrux-sha3",
     "libcrux-ml-dsa",
     "libcrux-intrinsics",
@@ -74,13 +75,7 @@ log = { version = "0.4", optional = true }
 # WASM API
 wasm-bindgen = { version = "0.2.87", optional = true }
 getrandom = { version = "0.2", features = ["js"], optional = true }
-
-# When using the hax toolchain, we have more dependencies.
-# This is only required when doing proofs.
-#[target.'cfg(hax)'.dependencies]
-[workspace.dependencies]
-hax-lib-macros = { git = "https://github.com/hacspec/hax", branch = "main" }
-hax-lib = { git = "https://github.com/hacspec/hax/", branch = "main" }
+hax-lib = { version = "0.1.0-alpha.1", git = "https://github.com/hacspec/hax/", branch = "main" }
 
 [dev-dependencies]
 libcrux = { path = ".", features = ["rand", "tests"] }

benchmarks/benches/kyber768.rs

@@ -80,7 +80,7 @@ pub fn comparisons_pk_validation(c: &mut Criterion) {
         b.iter_batched(
             || libcrux_kem::deterministic::mlkem768_generate_keypair_derand(seed),
             |key_pair| {
-                let _valid = libcrux_kem::ml_kem768_validate_public_key(key_pair.into_parts().1);
+                let _valid = libcrux_kem::ml_kem768_validate_public_key(&key_pair.into_parts().1);
             },
             BatchSize::SmallInput,
         )

fstar-helpers/Makefile.base

@@ -1,5 +1,5 @@
 # Base Makefile for F* in libcrux.
-# This inherits from Makefile.generic, and adds the `specs` folder from HACL and the `libcrux-ml-kem/proofs/fstar/spec` folder. 
+# This inherits from Makefile.generic, and adds the `specs` folder from HACL.
 
 VERIFY_SLOW_MODULES ?= no
 ifeq (${VERIFY_SLOW_MODULES},no)
@@ -10,5 +10,5 @@ EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n";
 EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.';
 EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`';
 
-FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
+FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic

libcrux-intrinsics/Cargo.toml

@@ -11,7 +11,7 @@ description = "Libcrux intrinsics crate"
 exclude = ["/proofs"]
 
 [dependencies]
-hax-lib.workspace = true
+hax-lib = { version = "0.1.0-alpha.1", git = "https://github.com/hacspec/hax/" }
 
 [features]
 simd128 = []

libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti

@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Arm64_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul