CI for ML-DSA C code

.docker/c/ext-tools.sh

@@ -4,23 +4,23 @@ set -v -e -x
 
 source $HOME/.profile
 
-curl -L https://github.com/AeneasVerif/charon/archive/45f5a34f336e35c6cc2253bc90cbdb8d812cefa9.zip \
+curl -L https://github.com/AeneasVerif/charon/archive/db4e045d4597d06d854ce7a2c10e8dcfda6ecd25.zip \
     --output charon.zip
 unzip charon.zip
 rm -rf charon.zip
-mv charon-45f5a34f336e35c6cc2253bc90cbdb8d812cefa9/ charon
+mv charon-db4e045d4597d06d854ce7a2c10e8dcfda6ecd25/ charon
 
-curl -L https://github.com/FStarLang/karamel/archive/8c3612018c25889288da6857771be3ad03b75bcd.zip \
+curl -L https://github.com/FStarLang/karamel/archive/3823e3d82fa0b271d799b61c59ffb4742ddc1e65.zip \
     --output karamel.zip
 unzip karamel.zip
 rm -rf karamel.zip
-mv karamel-8c3612018c25889288da6857771be3ad03b75bcd/ karamel
+mv karamel-3823e3d82fa0b271d799b61c59ffb4742ddc1e65/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/83ab5654d49df0603797bf510475d52d67ca24d8.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20/ eurydice
+mv eurydice-83ab5654d49df0603797bf510475d52d67ca24d8/ eurydice
 
 echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
@@ -39,7 +39,7 @@ cd -
 
 cd eurydice/lib
 rm -f charon
-ln -s $CHARON_HOME/charon-ml charon
+ln -s $CHARON_HOME charon
 rm -f krml
 ln -s $KRML_HOME/lib krml
 cd ../

.docker/c/install.sh

@@ -9,7 +9,7 @@ opam init --bare --disable-sandboxing --shell-setup --yes
 opam switch create 4.14.1
 
 # Get F*, HACL*, Charon, Karamel, Eurydice for running proofs and extraction
-curl -L https://github.com/FStarLang/FStar/releases/download/v2024.09.05/fstar_2024.09.05_Linux_x86_64.tar.gz \
+curl -L https://github.com/FStarLang/FStar/releases/download/v2024.12.03/fstar_2024.12.03_Linux_x86_64.tar.gz \
     --output Fstar.tar.gz
 tar --extract --file Fstar.tar.gz
 rm -f Fstar.tar.gz
@@ -32,5 +32,5 @@ echo "export PATH=\"${PATH}:$HOME/fstar/bin:$HOME/z3/bin\"" >>$HOME/.profile
 echo "[[ ! -r /home/$USER/.opam/opam-init/init.sh ]] || source /home/$USER/.opam/opam-init/init.sh  > /dev/null 2> /dev/null" >>$HOME/.profile
 
 source $HOME/.profile
-opam install --yes ocamlfind visitors menhir ppx_deriving_yojson core_unix sedlex wasm fix process pprint zarith yaml easy_logging terminal
+opam install --yes ocamlfind visitors menhir ppx_deriving_yojson core_unix sedlex wasm fix process pprint zarith yaml easy_logging terminal unionFind
 eval $(opam env)

.github/workflows/c.yml

@@ -35,7 +35,7 @@ jobs:
           include-hidden-files: true
           if-no-files-found: error
 
-  extract-header-only:
+  extract-header-only-ml-kem:
     runs-on: ubuntu-latest
     container: franziskus/libcrux-c:latest
     defaults:
@@ -52,11 +52,34 @@ jobs:
       - name: Upload header only C extraction
         uses: actions/upload-artifact@v4
         with:
-          name: header-only-c-extraction
+          name: header-only-c-extraction-ml-kem
           path: libcrux-ml-kem/cg/
           include-hidden-files: true
           if-no-files-found: error
 
+
+  extract-header-only-ml-dsa:
+    runs-on: ubuntu-latest
+    container: franziskus/libcrux-c:latest
+    defaults:
+      run:
+        working-directory: libcrux-ml-dsa
+        shell: bash
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Extract C (header only)
+        run: |
+          ./boring.sh --no-clean
+
+      - name: Upload header only C extraction
+        uses: actions/upload-artifact@v4
+        with:
+          name: header-only-c-extraction-ml-dsa
+          path: libcrux-ml-dsa/cg/
+          include-hidden-files: true
+          if-no-files-found: error
+
   diff:
     needs: [extract]
     runs-on: ubuntu-latest
@@ -77,25 +100,46 @@ jobs:
           libcrux-ml-kem/headers_kill_revs.sh ~/c-extraction
           diff -r libcrux-ml-kem/c ~/c-extraction
 
-  diff-header-only:
-    needs: [extract-header-only]
+  diff-header-only-ml-kem:
+    needs: [extract-header-only-ml-kem]
     runs-on: ubuntu-latest
     defaults:
       run:
         shell: bash
     steps:
       - uses: actions/download-artifact@v4
         with:
-          name: header-only-c-extraction
-          path: ~/c-extraction
+          name: header-only-c-extraction-ml-kem
+          path: ~/mlkem-c-extraction
 
       - uses: actions/checkout@v4
 
       - name: Diff Extraction
         run: |
           libcrux-ml-kem/headers_kill_revs.sh libcrux-ml-kem/cg
-          libcrux-ml-kem/headers_kill_revs.sh ~/c-extraction
-          diff -r libcrux-ml-kem/cg ~/c-extraction
+          libcrux-ml-kem/headers_kill_revs.sh ~/mlkem-c-extraction
+          diff -r libcrux-ml-kem/cg ~/mlkem-c-extraction
+
+  diff-header-only-ml-dsa:
+    needs: [extract-header-only-ml-dsa]
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: header-only-c-extraction-ml-dsa
+          path: ~/mldsa-c-extraction
+
+      - uses: actions/checkout@v4
+
+      - name: Diff Extraction
+        run: |
+          libcrux-ml-kem/headers_kill_revs.sh libcrux-ml-dsa/cg
+          libcrux-ml-kem/headers_kill_revs.sh ~/mldsa-c-extraction
+          diff -r libcrux-ml-dsa/cg ~/mldsa-c-extraction
+
 
   build:
     needs: [extract]
@@ -136,8 +180,8 @@ jobs:
           cmake --build build --config Release
         if: ${{ matrix.os != 'windows-latest' }}
 
-  build-header-only:
-    needs: [extract-header-only]
+  build-header-only-ml-kem:
+    needs: [extract-header-only-ml-kem]
     strategy:
       fail-fast: false
       matrix:
@@ -152,7 +196,7 @@ jobs:
     steps:
       - uses: actions/download-artifact@v4
         with:
-          name: header-only-c-extraction
+          name: header-only-c-extraction-ml-kem
 
       - name: 🔨 Build
         run: |
@@ -163,3 +207,38 @@ jobs:
       - name: 🏃🏻‍♀️ Test
         run: ./build/ml_kem_test
         if: ${{ matrix.os != 'windows-latest' }}
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/Debug/ml_kem_test
+        if: ${{ matrix.os == 'windows-latest' }}
+
+  build-header-only-ml-dsa:
+    needs: [extract-header-only-ml-dsa]
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+          - windows-latest
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: header-only-c-extraction-ml-dsa
+
+      - name: 🔨 Build
+        run: |
+          cmake -B build
+          cmake --build build
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/ml_dsa_test
+        if: ${{ matrix.os != 'windows-latest' }}
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/Debug/ml_dsa_test
+        if: ${{ matrix.os == 'windows-latest' }}

.github/workflows/hax.yml

@@ -34,7 +34,7 @@ jobs:
       - uses: DeterminateSystems/magic-nix-cache-action@main
 
       - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/v2024.09.05
+        run: nix profile install github:FStarLang/FStar/v2024.12.03
 
       - name: ⤵ Clone HACL-star repository
         uses: actions/checkout@v4

libcrux-intrinsics/src/avx2_extract.rs

@@ -1,7 +1,7 @@
 //! This file does not contain correct function signatures!
 //! Replace with a hand-written file after extraction.
 
-#![allow(unused_variables, non_camel_case_types)]
+#![allow(unused_variables, non_camel_case_types, dead_code)]
 
 #[cfg(hax)]
 #[derive(Clone, Copy)]

libcrux-ml-dsa/cg/CMakeLists.txt

@@ -18,6 +18,7 @@ if(NOT MSVC)
         -Wall
         -fstack-usage
         -Wunused-function
+        # -Wno-unused-function
         $<$<CONFIG:DEBUG>:-g>
         $<$<CONFIG:DEBUG>:-Og>
         $<$<CONFIG:RELEASE>:-g>

libcrux-ml-dsa/cg/code_gen.txt

@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
-Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
-Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
 F*: b0961063393215ca65927f017720cb365a193833-dirty
-Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e

libcrux-ml-dsa/cg/eurydice_glue.h

@@ -149,6 +149,14 @@ static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) {
 #endif
 }
 
+static inline uint32_t core_num__i32_2__count_ones(int32_t x0) {
+#ifdef _MSC_VER
+  return __popcnt(x0);
+#else
+  return __builtin_popcount(x0);
+#endif
+}
+
 // unsigned overflow wraparound semantics in C
 static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x, uint16_t y) {
   return x + y;

libcrux-ml-dsa/cg/header.txt

@@ -4,9 +4,9 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */