ML-KEM: Restructure C Extraction

use common c.sh, symlink

update documentation

ci: update needs names in C workflow

mlkem: drop c-nss extract scripts

ci: update more needs names

Revert "ci: update more needs names"

This reverts commit b2d6f85.

ci: update needs of mlkem c status, but correct this time

fix C/C++ extraction

add mlkem.cmake symlink, move around version header kill script files

ci: clean the right directory

Author: keks

.github/workflows/docker-c-build-test.yml

@@ -40,54 +40,54 @@ jobs:
           tags: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.VERSION_TAG }}
     outputs:
       image: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.VERSION_TAG }}
-  extract:
+  extract-ml-kem-c-header-only:
     needs: [build-and-push-image]
     runs-on: ubuntu-latest
     container:
       image: ${{ needs.build-and-push-image.outputs.image }}
     defaults:
       run:
-        working-directory: libcrux-ml-kem
+        working-directory: libcrux-ml-kem/extracts/c_header_only
         shell: bash
     steps:
       - uses: actions/checkout@v5
 
-      - name: Extract C
+      - name: Extract C (header only)
         run: |
           export HOME=/home/user
-          ./c.sh --config cg.yaml --mlkem768 --no-unrolling --out c --clean --no-glue
-      - name: Upload C extraction
+          ./extract.sh
+      - name: Upload header only C extraction
         uses: actions/upload-artifact@v4
         with:
-          name: c-extraction
-          path: libcrux-ml-kem/c
+          name: extraction-ml-kem-c-header-only
+          path: libcrux-ml-kem/extracts/c_header_only/generated
           include-hidden-files: true
           if-no-files-found: error
-  extract-header-only-ml-kem:
+  extract-ml-kem-cpp-header-only:
     needs: [build-and-push-image]
     runs-on: ubuntu-latest
     container:
       image: ${{ needs.build-and-push-image.outputs.image }}
     defaults:
       run:
-        working-directory: libcrux-ml-kem
+        working-directory: libcrux-ml-kem/extracts/cpp_header_only
         shell: bash
     steps:
       - uses: actions/checkout@v5
 
-      - name: Extract C (header only)
+      - name: Extract C++ (header only)
         run: |
           export HOME=/home/user
-          ./boring.sh --no-clean
+          ./extract.sh --no-clean
 
-      - name: Upload header only C extraction
+      - name: Upload header only C++ extraction
         uses: actions/upload-artifact@v4
         with:
-          name: header-only-c-extraction-ml-kem
-          path: libcrux-ml-kem/cg/
+          name: extraction-ml-kem-cpp-header-only
+          path: libcrux-ml-kem/extracts/cpp_header_only/generated
           include-hidden-files: true
           if-no-files-found: error
-  extract-header-only-ml-dsa:
+  extract-ml-dsa-header-only:
     needs: [build-and-push-image]
     runs-on: ubuntu-latest
     container:
@@ -107,12 +107,12 @@ jobs:
       - name: Upload header only C extraction
         uses: actions/upload-artifact@v4
         with:
-          name: header-only-c-extraction-ml-dsa
+          name: extraction-ml-dsa-header-only
           path: libcrux-ml-dsa/cg/
           include-hidden-files: true
           if-no-files-found: error
-  test-build:
-    needs: [extract]
+  test-build-ml-kem-c-header-only:
+    needs: [extract-ml-kem-c-header-only]
     strategy:
       fail-fast: false
       matrix:
@@ -128,7 +128,7 @@ jobs:
     steps:
       - uses: actions/download-artifact@v5
         with:
-          name: c-extraction
+          name: extraction-ml-kem-c-header-only
 
       - name: 🔨 Build
         run: |
@@ -149,8 +149,8 @@ jobs:
           LIBCRUX_BENCHMARKS=1 cmake -B build -DCMAKE_BUILD_TYPE=Release
           cmake --build build --config Release
         if: ${{ matrix.os != 'windows-latest' }}
-  test-build-header-only-ml-kem:
-    needs: [extract-header-only-ml-kem]
+  test-build-ml-kem-cpp-header-only:
+    needs: [extract-ml-kem-cpp-header-only]
     strategy:
       fail-fast: false
       matrix:
@@ -165,7 +165,7 @@ jobs:
     steps:
       - uses: actions/download-artifact@v5
         with:
-          name: header-only-c-extraction-ml-kem
+          name: extraction-ml-kem-cpp-header-only
 
       - name: 🔨 Build
         run: |
@@ -181,8 +181,8 @@ jobs:
         run: ./build/Debug/ml_kem_test
         if: ${{ matrix.os == 'windows-latest' }}
 
-  test-build-header-only-ml-dsa:
-    needs: [extract-header-only-ml-dsa]
+  test-build-ml-dsa-header-only:
+    needs: [extract-ml-dsa-header-only]
     strategy:
       fail-fast: false
       matrix:
@@ -197,7 +197,7 @@ jobs:
     steps:
       - uses: actions/download-artifact@v5
         with:
-          name: header-only-c-extraction-ml-dsa
+          name: extraction-ml-dsa-header-only
 
       - name: 🔨 Build
         run: |

.github/workflows/mlkem-c.yml

@@ -38,7 +38,8 @@ jobs:
     if: ${{ always() }}
     needs:
       - setup
-      - extract
+      - extract-c
+      - extract-cpp
       - diff
       - build-c
       - build-cpp
@@ -51,47 +52,61 @@ jobs:
         if: ${{ (contains(needs.*.result, 'failure')) }} 
         run: exit 1 
 
-  extract:
+  extract-c:
     needs: [setup]
     if: ${{ needs.setup.outputs.should-run == 'true' }}
     runs-on: ubuntu-latest
     container:
       image: ${{ needs.setup.outputs.image }}
     defaults:
       run:
-        working-directory: libcrux-ml-kem
+        working-directory: libcrux-ml-kem/extracts/c_header_only
         shell: bash
     steps:
       - uses: actions/checkout@v5
 
-      - name: Extract C++
-        run: |
-          export HOME=/home/user
-          ./boring.sh --no-clean
-
       - name: Extract C
         run: |
           export HOME=/home/user
-          ./c.sh --config cg.yaml --mlkem768 --no-unrolling --out c --clean --no-glue
+          ./extract.sh
 
-      - name: Upload C++ extraction
+      - name: Upload C extraction
         uses: actions/upload-artifact@v4
         with:
-          name: cpp-extraction-ml-kem
-          path: libcrux-ml-kem/cg/
+          name: c-extraction-ml-kem
+          path: libcrux-ml-kem/extracts/c_header_only/generated
           include-hidden-files: true
           if-no-files-found: error
 
-      - name: Upload C extraction
+  extract-cpp:
+    needs: [setup]
+    if: ${{ needs.setup.outputs.should-run == 'true' }}
+    runs-on: ubuntu-latest
+    container:
+      image: ${{ needs.setup.outputs.image }}
+    defaults:
+      run:
+        working-directory: libcrux-ml-kem/extracts/cpp_header_only
+        shell: bash
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: Extract C++
+        run: |
+          export HOME=/home/user
+          ./extract.sh --no-clean
+
+      - name: Upload C++ extraction
         uses: actions/upload-artifact@v4
         with:
-          name: c-extraction-ml-kem
-          path: libcrux-ml-kem/c/
+          name: cpp-extraction-ml-kem
+          path: libcrux-ml-kem/extracts/cpp_header_only/generated
           include-hidden-files: true
           if-no-files-found: error
 
+
   diff:
-    needs: [extract]
+    needs: [extract-c, extract-cpp]
     runs-on: ubuntu-latest
     defaults:
       run:
@@ -110,18 +125,18 @@ jobs:
 
       - name: Diff Extraction C++
         run: |
-          libcrux-ml-kem/headers_kill_revs.sh libcrux-ml-kem/cg
-          libcrux-ml-kem/headers_kill_revs.sh ~/mlkem-cpp-extraction
-          diff -r libcrux-ml-kem/cg ~/mlkem-cpp-extraction
+          libcrux-ml-kem/extracts/common/headers_kill_revs.sh libcrux-ml-kem/extracts/cpp_header_only/generated
+          libcrux-ml-kem/extracts/common/headers_kill_revs.sh ~/mlkem-cpp-extraction
+          diff -r libcrux-ml-kem/extracts/cpp_header_only/generated ~/mlkem-cpp-extraction
 
       - name: Diff Extraction C
         run: |
-          libcrux-ml-kem/headers_kill_revs.sh libcrux-ml-kem/c
-          libcrux-ml-kem/headers_kill_revs.sh ~/mlkem-c-extraction
-          diff -r libcrux-ml-kem/c ~/mlkem-c-extraction
+          libcrux-ml-kem/extracts/common/headers_kill_revs.sh libcrux-ml-kem/extracts/c_header_only/generated
+          libcrux-ml-kem/extracts/common/headers_kill_revs.sh ~/mlkem-c-extraction
+          diff -r libcrux-ml-kem/extracts/c_header_only/generated ~/mlkem-c-extraction
 
   build-c:
-    needs: [extract]
+    needs: [extract-c]
     strategy:
       fail-fast: false
       matrix:
@@ -158,7 +173,7 @@ jobs:
         if: ${{ matrix.os == 'windows-latest' }}
 
   build-cpp:
-    needs: [extract]
+    needs: [extract-cpp]
     strategy:
       fail-fast: false
       matrix:

CONTRIBUTING.md

@@ -47,7 +47,7 @@ Relative to the crate root, the structure we aim to use is:
 /extracts/
 /extracts/$name/extract.sh   -- the script that extracts the code
 /extracts/$name/extract.yaml -- the eurydice config for the extraction
-/extracts/$name/out/         -- the extracted code
+/extracts/$name/generated/   -- the extracted code
 /extracts/$name/...          -- per-extraction extra data
 ```
 

PUBLISHING.md

@@ -99,3 +99,8 @@ later update these as well.
 ### Running `cargo publish`
 
 This pushes the crate to crates.io. Before running the full push, do a dry run.
+
+### Tag the commit
+
+Create and push a git tag named `${crate name}-v${version}` for all published
+crates.

RELEASE.md

@@ -1,6 +1,6 @@
 # Extraction into C code
 
-The folders `./c` and `./cg` contain C code extracted from `libcrux-ml-kem`.
+The subfolders of `./extracts/` contain C code extracted from `libcrux-ml-kem`.
 
 The C code is generated from Rust using [Charon], [Eurydice] and
 [KaRaMeL]. Charon translates the Rust crate to Low-Level Borrow
@@ -17,22 +17,27 @@ opam install --yes ocamlfind visitors menhir ppx_deriving_yojson core_unix sedle
 ```
 
 Now you're ready to install the tools.
+
 ### Set tool directories
+
 Set the directories where tool repositories should be cloned and tools should be built in. Setting these environment variables is important for the extraction script `c.sh`.
+
 ```bash
 export CHARON_HOME=$HOME/charon
 export KRML_HOME=$HOME/karamel
 export EURYDICE_HOME=$HOME/eurydice
 ```
 
 ### Charon
+
 ```bash
 git clone https://github.com/AeneasVerif/charon.git $CHARON_HOME
 cd $CHARON_HOME
 make
 ```
 
 ### KaRaMeL
+
 ```bash
 git clone https://github.com/FStarLang/karamel.git $KRML_HOME
 cd $KRML_HOME
@@ -48,23 +53,29 @@ make
 
 ## Generating C code
 
-The [c.sh](../c.sh) bash script drives the extraction, using the
-[c.yaml](../c.yaml) configuration file, which configures the Eurydice
-translation.
-
-To generate a header-only version, use [boring.sh](../boring.sh)
-instead, which internally runs [c.sh](../c.sh) with a header-only
-configuration found in [cg.yaml](../cg.yaml).
+Each extraction has a script `extract.sh` for extracting the code. They all make
+use of the `extracts/common/c.sh` script, but use it with different arguments.
+Each extraction also comes with an `extract.yaml` configuration file, which
+configures the Eurydice translation.
 
 While running the commands separately is possible, it is not
 recommended because the script sets all necessary configuration flags.
 
+We maintain the following extraction configurations:
+
+- `c_header_only`: header-only C code
+- `cpp_header_only`: header-only C++ code
+
+For the `c_header_only` and `cpp_header_only` extractions we also keep the
+extracted code in the repository so users don't need to extract it themselves.
+
 ## Build
 
-Make sure to use `CC=clang CXX=clang++` when benchmarking on Linux to get full performance.
+Make sure to use `CC=clang CXX=clang++` when benchmarking on Linux to get full
+performance.
 
 ```bash
-cd ./c               # or ./cg, if you want to build header-only
+cd extracts/c_header_only # or extracts/cpp_header_only if you want to build C++
 cmake -B build
 cmake --build build
 ```

libcrux-ml-kem/C-CODE.md

@@ -11,15 +11,9 @@ description = "Libcrux ML-KEM & Kyber implementations"
 exclude = [
     "/tests",
     "/implementation_notes.pdf",
-    "/c",
+    "/extracts",
     "/proofs",
-    "/c.sh",
-    "/c.yaml",
     "/hax.py",
-    "/cg",
-    "/c-nss.sh",
-    "/c.sh",
-    "/boring.sh",
 ]
 
 [lib]