SIMD SHA-3 and memory usage optimizations

.github/workflows/hax.yml

@@ -92,7 +92,7 @@ jobs:
       - name: 🏃 Extract & Verify ML-KEM crate (lax)
         run: |
           cd libcrux-ml-kem
-          ./hax.py extract
+          # ./hax.py extract
           # env FSTAR_HOME=${{ github.workspace }}/fstar \
           #     HACL_HOME=${{ github.workspace }}/hacl-star \
           #     HAX_HOME=${{ github.workspace }}/hax \

.github/workflows/mlkem.yml

@@ -4,7 +4,7 @@ on:
   push:
     branches: ["main", "dev"]
   pull_request:
-    branches: ["main", "dev"]
+    branches: ["main", "dev", "*"]
   workflow_dispatch:
   merge_group:
 
@@ -22,15 +22,15 @@ jobs:
       matrix:
         bits: [32, 64]
         os:
-          - macos-latest
+          - macos-13 # Intel mac
+          - macos-latest # macos-14 m1
           - ubuntu-latest
           - windows-latest
         exclude:
           - bits: 32
             os: "macos-latest"
-          # FIXME: Linking isn't working here yet for hacl #42
           - bits: 32
-            os: "windows-latest"
+            os: "macos-13"
 
     runs-on: ${{ matrix.os }}
     defaults:
@@ -44,23 +44,21 @@ jobs:
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 
-      - name: ⚙️ Setup Ubuntu x86
+      - name: 🛠️ Setup Rust Nightly
+        run: rustup toolchain install nightly
+
+      - name: 🛠️ Setup Ubuntu x86
         if: ${{ matrix.bits == 32 &&  matrix.os == 'ubuntu-latest' }}
         run: |
           rustup target add i686-unknown-linux-gnu
           sudo apt-get update
           sudo apt-get install -y gcc-multilib g++-multilib
 
-      - name: ⚙️ Setup Ubuntu x64
+      - name: 🛠️ Setup Ubuntu x64
         if: ${{ matrix.bits == 64 &&  matrix.os == 'ubuntu-latest' }}
         run: |
           rustup target add aarch64-unknown-linux-gnu
 
-      - name: ⚙️ Setup macOS
-        if: ${{  matrix.os == 'macos-latest' }}
-        run: |
-          rustup target add aarch64-apple-darwin
-
       # Set up 32 bit systems
 
       - name: 🛠️ Config Windows x86
@@ -72,60 +70,90 @@ jobs:
           echo "RUST_TARGET_FLAG=--target=i686-unknown-linux-gnu" > $GITHUB_ENV
         if: ${{ matrix.bits == 32 && matrix.os == 'ubuntu-latest' }}
 
-      # Set up windows
-
-      - name: ⚙️ Setup Windows x86
-        if: ${{ matrix.bits == 32 && matrix.os == 'windows-latest' }}
-        shell: pwsh
-        run: |
-          echo "VCPKG_ROOT=$env:VCPKG_INSTALLATION_ROOT" | Out-File -FilePath $env:GITHUB_ENV -Append
-          vcpkg install openssl:x86-windows-static-md
-
-      - name: ⚙️ Setup Windows x64
-        if: ${{ matrix.bits == 64 && matrix.os == 'windows-latest' }}
-        shell: pwsh
-        run: |
-          echo "VCPKG_ROOT=$env:VCPKG_INSTALLATION_ROOT" | Out-File -FilePath $env:GITHUB_ENV -Append
-          vcpkg install openssl:x64-windows-static-md
-
       # Build ...
 
       - name: 🔨 Build
-        run: cargo build --verbose $RUST_TARGET_FLAG
+        run: |
+          rustc --print=cfg
+          cargo build --verbose $RUST_TARGET_FLAG
 
       - name: 🔨 Build Release
         run: cargo build --verbose --release $RUST_TARGET_FLAG
 
-      # Cross compilation
-
-      - name: 🔨 Build aarch64 macOS
+      - name: 🏃🏻 Asan MacOS
         if: ${{ matrix.os == 'macos-latest' }}
-        run: cargo build --verbose --target aarch64-apple-darwin
+        run: RUSTDOCFLAGS=-Zsanitizer=address RUSTFLAGS=-Zsanitizer=address cargo +nightly test --release --target aarch64-apple-darwin
+
+      # We get false positives here.
+      # TODO: Figure out what is going on here
+      # - name: 🏃🏻 Asan Linux
+      #   if: ${{ matrix.bits == 64 && matrix.os == 'ubuntu-latest' }}
+      #   run: RUSTDOCFLAGS=-Zsanitizer=address RUSTFLAGS=-Zsanitizer=address cargo +nightly test --release --target x86_64-unknown-linux-gnu
+
+      # Test SHA3
+      - name: 🏃🏻‍♀️ SHA3 Test
+        working-directory: libcrux-sha3
+        run: |
+          cargo clean
+          cargo test --verbose $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ SHA3 Test Release
+        working-directory: libcrux-sha3
+        run: |
+          cargo clean
+          cargo test --release --verbose $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ SHA3 Test Portable
+        working-directory: libcrux-sha3
+        run: |
+          cargo clean
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ SHA3 Test Portable Release
+        working-directory: libcrux-sha3
+        run: |
+          cargo clean
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose --release $RUST_TARGET_FLAG
 
       # Test ...
 
       - name: 🏃🏻‍♀️ Test
-        run: cargo test --verbose $RUST_TARGET_FLAG
+        run: |
+          cargo clean
+          cargo test --verbose $RUST_TARGET_FLAG
 
       - name: 🏃🏻‍♀️ Test Release
-        run: cargo test --verbose --release $RUST_TARGET_FLAG
+        if: ${{ matrix.os != 'macos-latest' }}
+        run: |
+          cargo clean
+          cargo test --verbose --release $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ Test Portable
+        run: |
+          cargo clean
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ Test Portable Release
+        run: |
+          cargo clean
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose --release $RUST_TARGET_FLAG
 
   benchmarks:
     strategy:
       fail-fast: true
       matrix:
         bits: [32, 64]
         os:
+          - macos-13
           - macos-latest
           - ubuntu-latest
           - windows-latest
         exclude:
           # There's no such thing as 32-bit macOS
           - bits: 32
             os: "macos-latest"
-          # FIXME: Linking isn't working here yet for hacl #42
           - bits: 32
-            os: "windows-latest"
+            os: "macos-13"
 
     runs-on: ${{ matrix.os }}
     defaults:
@@ -139,19 +167,19 @@ jobs:
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 
-      - name: ⚙️ Setup Ubuntu x86
+      - name: 🛠️ Setup Ubuntu x86
         if: ${{ matrix.bits == 32 &&  matrix.os == 'ubuntu-latest' }}
         run: |
           rustup target add i686-unknown-linux-gnu
           sudo apt-get update
           sudo apt-get install -y gcc-multilib g++-multilib
 
-      - name: ⚙️ Setup Ubuntu x64
+      - name: 🛠️ Setup Ubuntu x64
         if: ${{ matrix.bits == 64 &&  matrix.os == 'ubuntu-latest' }}
         run: |
           rustup target add aarch64-unknown-linux-gnu
 
-      - name: ⚙️ Setup macOS
+      - name: 🛠️ Setup macOS
         if: ${{  matrix.os == 'macos-latest' }}
         run: |
           rustup target add aarch64-apple-darwin
@@ -167,28 +195,12 @@ jobs:
           echo "RUST_TARGET_FLAG=--target=i686-unknown-linux-gnu" > $GITHUB_ENV
         if: ${{ matrix.bits == 32 && matrix.os == 'ubuntu-latest' }}
 
-      # Set up windows
-
-      - name: ⚙️ Setup Windows x86
-        if: ${{ matrix.bits == 32 && matrix.os == 'windows-latest' }}
-        shell: pwsh
-        run: |
-          echo "VCPKG_ROOT=$env:VCPKG_INSTALLATION_ROOT" | Out-File -FilePath $env:GITHUB_ENV -Append
-          vcpkg install openssl:x86-windows-static-md
-
-      - name: ⚙️ Setup Windows x64
-        if: ${{ matrix.bits == 64 && matrix.os == 'windows-latest' }}
-        shell: pwsh
-        run: |
-          echo "VCPKG_ROOT=$env:VCPKG_INSTALLATION_ROOT" | Out-File -FilePath $env:GITHUB_ENV -Append
-          vcpkg install openssl:x64-windows-static-md
-
       # Benchmarks ...
 
-      - name: 🏃🏻‍♀️ Benchmarks Windows
-        if: ${{ matrix.os == 'windows-latest' }}
+      - name: 🏃🏻‍♀️ Benchmarks
         run: cargo bench --verbose $RUST_TARGET_FLAG
-
-      - name: 🏃🏻‍♀️ Benchmarks Clang
-        if: ${{ matrix.os != 'windows-latest' }}
-        run: CC=clang cargo bench --verbose $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ Benchmarks Portable
+        run: |
+          cargo clean
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo bench --verbose $RUST_TARGET_FLAG

.github/workflows/platform.yml

@@ -0,0 +1,74 @@
+name: Platform
+
+on:
+  push:
+    branches: ["main", "dev"]
+  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:
+  platform:
+    strategy:
+      fail-fast: false
+      matrix:
+        bits: [32, 64]
+        os:
+          - macos-13 # Intel mac
+          - macos-latest # macos-14 m1
+          - ubuntu-latest
+          - windows-latest
+        exclude:
+          - bits: 32
+            os: "macos-latest"
+          - bits: 32
+            os: "macos-13"
+
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+        working-directory: sys/platform
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: 🔨 Build
+        run: cargo build --verbose
+
+      - name: 🏃🏻‍♀️ Test
+        run: cargo test --verbose -- --nocapture
+
+      - name: 🏃🏻‍♀️ Test Release
+        run: cargo test --verbose --release -- --nocapture
+
+      - name: 🛠️ Setup Linux x86
+        if: ${{ matrix.bits == 32 &&  matrix.os == 'ubuntu-latest' }}
+        run: |
+          rustup target add i686-unknown-linux-gnu
+          sudo apt-get update
+          sudo apt-get install -y gcc-multilib g++-multilib
+
+      - name: 🏃🏻‍♀️ Test Linux x86
+        if: ${{ matrix.bits == 32 &&  matrix.os == 'ubuntu-latest' }}
+        run: cargo test --verbose --target i686-unknown-linux-gnu -- --nocapture
+
+      - name: 🏃🏻‍♀️ Test Release Linux x86
+        if: ${{ matrix.bits == 32 &&  matrix.os == 'ubuntu-latest' }}
+        run: cargo test --verbose --release --target i686-unknown-linux-gnu -- --nocapture
+
+      - name: 🏃🏻‍♀️ Test Windows x86
+        if: ${{ matrix.bits == 32 &&  matrix.os == 'windows-latest' }}
+        run: cargo test --verbose --target i686-pc-windows-msvc -- --nocapture
+
+      - name: 🏃🏻‍♀️ Test Release Windows x86
+        if: ${{ matrix.bits == 32 &&  matrix.os == 'windows-latest' }}
+        run: cargo test --verbose --release --target i686-pc-windows-msvc -- --nocapture

libcrux-ml-kem/build.rs

@@ -16,11 +16,13 @@ fn main() {
         // We enable simd128 on all aarch64 builds.
         println!("cargo:rustc-cfg=feature=\"simd128\"");
     }
-    if (target_arch == "x86" || target_arch == "x86_64") && !disable_simd256 {
-        // We enable simd256 on all x86 and x86_64 builds.
+    if target_arch == "x86_64" && !disable_simd256 {
+        // We enable simd256 on all x86_64 builds.
         // Note that this doesn't mean the required CPU features are available.
         // But the compiler will support them and the runtime checks ensure that
         // it's only used when available.
+        //
+        // We don't enable this on x86 because it seems to generate invalid code.
         println!("cargo:rustc-cfg=feature=\"simd256\"");
     }
 }

libcrux-ml-kem/src/constants.rs

@@ -32,4 +32,7 @@ pub(crate) const CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = 32;
 
 // XXX: Eurydice can't handle this.
 // digest_size(Algorithm::Sha3_256);
+/// SHA3 256 digest size
 pub(crate) const H_DIGEST_SIZE: usize = 32;
+/// SHA3 512 digest size
+pub(crate) const G_DIGEST_SIZE: usize = 64;