Merge branch 'dev' into jonas/kem-crate

.github/workflows/c.yml

@@ -0,0 +1,61 @@
+name: Build & Test C
+
+on:
+  push:
+    branches: ["main", "dev"]
+  pull_request:
+    branches: ["main", "dev"]
+  workflow_dispatch:
+  merge_group:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+          - windows-latest
+
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+        working-directory: libcrux-ml-kem/c
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: 🔨 Build
+        run: |
+          cmake -B build
+          cmake --build build
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/Debug/ml_kem_test
+        if: ${{ matrix.os == 'windows-latest' }}
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/ml_kem_test
+        if: ${{ matrix.os != 'windows-latest' }}
+
+      - name: 🔨 Build Release
+        run: |
+          rm -rf build
+          cmake -B build -DCMAKE_BUILD_TYPE=Release
+          cmake --build build --config Release
+
+      # FIXME: Benchmarks on Windows CI are not working right now.
+      # - name: 🏃🏻‍♀️ Benchmark
+      #   run: ./build/Release/ml_kem_bench
+      #   if: ${{ matrix.os == 'windows-latest' }}
+
+      - name: 🏃🏻‍♀️ Benchmark
+        run: ./build/ml_kem_bench
+        if: ${{ matrix.os != 'windows-latest' }}
+

.github/workflows/hax.yml

@@ -52,70 +52,12 @@ jobs:
         run: |
           nix profile install ./hax
 
-      - name: 🏃 Extract the Kyber reference code
-        run: |
-          eval $(opam env)
-          (cd proofs/fstar/extraction/ && ./clean.sh)
-          rm -f sys/platform/proofs/fstar/extraction/*.fst*
-          ./hax-driver.py --kyber-reference
-
-      - name: 🏃 Regenerate `extraction-*` folders
-        run: ./proofs/fstar/patches.sh apply
-
-      - name: 🏃 Make sure snapshots are up-to-date
-        run: git diff --exit-code
-
-      - name: 🏃 Verify the Kyber reference code
-        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-driver.py --verify-extraction
-
-      - name: 🏃 Verify Kyber `extraction-edited` F* code
-        run: |
-          env FSTAR_HOME=${{ github.workspace }}/fstar \
-              HACL_HOME=${{ github.workspace }}/hacl-star \
-              HAX_HOME=${{ github.workspace }}/hax \
-              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
-              make -C proofs/fstar/extraction-edited
-
-      - name: 🏃 Verify Kyber `extraction-secret-independent` F* code
-        run: |
-          env FSTAR_HOME=${{ github.workspace }}/fstar \
-              HACL_HOME=${{ github.workspace }}/hacl-star \
-              HAX_HOME=${{ github.workspace }}/hax \
-              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
-              make -C proofs/fstar/extraction-secret-independent
-
-      - name: 🏃 Extract & Verify ML-KEM crate (lax)
+      - name: 🏃 Extract ML-KEM crate
         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 \
           #     PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
           #     ./hax.py prove --admit
-
-      - name: 🏃 Extract the Kyber specification
-        run: |
-          eval $(opam env)
-          # Extract the functions in the compress module individually to test
-            # the function-extraction code.
-          # Extract functions from the remaining modules to test the
-          # module-extraction code.
-          ./hax-driver.py --crate-path specs/kyber \
-            --functions hacspec_kyber::compress::compress \
-                        hacspec_kyber::compress::decompress \
-                        hacspec_kyber::compress::compress_d \
-                        hacspec::kyber::compress::decompress_d \
-            --modules ind_cpa \
-                      hacspec_kyber \
-                      matrix \
-                      ntt \
-                      parameters \
-                      sampling \
-                      serialize \
-            --exclude-modules libcrux::hacl::sha3 libcrux::digest

.github/workflows/mldsa.yml

@@ -41,6 +41,9 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      - name: Update dependencies
+        run: cargo update
+
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 

.github/workflows/mlkem.yml

@@ -41,6 +41,9 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      - name: Update dependencies
+        run: cargo update
+
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 
@@ -168,6 +171,9 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      - name: Update dependencies
+        run: cargo update
+
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 

.github/workflows/nix.yml

@@ -0,0 +1,20 @@
+name: Nix
+
+on:
+  push:
+    branches: [main, dev]
+  pull_request:
+
+jobs:
+  nix:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: DeterminateSystems/nix-installer-action@v12
+      - uses: DeterminateSystems/magic-nix-cache-action@v7
+      - name: Install & configure Cachix
+        shell: bash
+        run: |
+          nix-env --quiet -j8 -iA cachix -f https://cachix.org/api/v1/install
+          cachix use hax
+      - uses: actions/checkout@v4
+      - run: nix build -L .#ml-kem

.github/workflows/platform.yml

@@ -41,6 +41,9 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      - name: Update dependencies
+        run: cargo update
+
       - name: 🔨 Build
         run: cargo build --verbose
 

.github/workflows/rust.yml

@@ -40,6 +40,9 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      - name: Update dependencies
+        run: cargo update
+
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 

.github/workflows/specs.yml

@@ -41,6 +41,9 @@ jobs:
 
     - uses: actions/checkout@v3
 
+    - name: Update dependencies
+      run: cargo update
+
     - name: Build
       working-directory: specs
       run: cargo build --verbose

.gitignore

@@ -1,5 +1,4 @@
 /target
-/Cargo.lock
 .vscode
 .DS_Store
 benches/boringssl/build