Merge pull request #662 from cryspen/dev-merge-main

Merging main into dev
cryspen · Dec 1, 2024 · 5a621c7 · 5a621c7
2 parents 0eabf66 + 0a935fe
commit 5a621c7
Show file tree

Hide file tree

Showing 471 changed files with 62,150 additions and 7,428 deletions.
diff --git a/.docker/c/ext-tools.sh b/.docker/c/ext-tools.sh
@@ -16,11 +16,11 @@ unzip karamel.zip
 rm -rf karamel.zip
 mv karamel-8c3612018c25889288da6857771be3ad03b75bcd/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c/ eurydice
+mv eurydice-e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20/ eurydice
 
 echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile

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/hax.yml b/.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
diff --git a/.github/workflows/mlkem.yml b/.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
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/.gitignore b/.gitignore
@@ -15,6 +15,6 @@ kyber-crate/
 # F*
 .fstar-cache
 .depend
-**/proofs/fstar/*/#*#
-**/proofs/fstar/*/.#*
+/proofs/fstar/*/#*#
+/proofs/fstar/*/.#*
 hax.fst.config.json