[SHA3 / ML-KEM/ ML-DSA] C extraction

.github/workflows/build.yml

@@ -29,7 +29,7 @@ jobs:
           submodules: recursive
 
       - name: Install GNU ARM Toolchain
-        uses: carlosperate/arm-none-eabi-gcc-action@v1.8.0
+        uses: carlosperate/arm-none-eabi-gcc-action@v1
         with:
           release: 13.2.Rel1
 

.github/workflows/mldsa-c-extract-build-test.yml

@@ -0,0 +1,87 @@
+name: ML-DSA C - Extract, Build & Test
+
+on:
+  merge_group:
+  push:
+    branches: ["main"]
+  pull_request:
+    branches: ["main", "*"]
+  workflow_dispatch:
+
+env:
+  CARGO_TERM_COLOR: always
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  extract-c:
+    runs-on: ubuntu-latest
+    container:
+      image: ghcr.io/cryspen/libcrux-c:latest
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: Extract C
+        run: |
+          export HOME=/home/user
+          cd libcrux-iot
+          ../c/extract-mldsa.sh
+
+      - name: Upload C extraction
+        uses: actions/upload-artifact@v4
+        with:
+          name: c-extraction-mldsa-iot
+          path: c/ml-dsa/extracted
+          include-hidden-files: true
+          if-no-files-found: error
+
+  build-c:
+    needs: [extract-c]
+    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@v5
+        with:
+          name: c-extraction-mldsa-iot
+
+      - name: Set CC and CXX to Clang on Ubuntu
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          echo "CC=clang" >> $GITHUB_ENV
+          echo "CXX=clang++" >> $GITHUB_ENV
+
+      - name: 🔨 Build
+        run: |
+          cmake -B build
+          cmake --build build
+
+      - name: 🏃🏻‍♀️ Test ML-DSA 65
+        run: ./build/ml_dsa_test65
+        if: ${{ matrix.os != 'windows-latest' }}
+
+
+  mldsa-build-test-status:
+    if: ${{ always() }}
+    needs: [build-c]
+    runs-on: ubuntu-latest
+    steps:
+      - name: Successful
+        if: ${{ !(contains(needs.*.result, 'failure')) }}
+        run: exit 0
+      - name: Failing
+        if: ${{ (contains(needs.*.result, 'failure')) }}
+        run: exit 1

c/c.sh

@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-set -e
+set -ex
 set -o pipefail
 
 function fail() {
@@ -35,7 +35,8 @@ glue=$EURYDICE_HOME/include/eurydice_glue.h
 features=""
 eurydice_glue=1
 karamel_include=1
-unrolling=16
+# We want to avoid the `KRML_MAYBE_FOR*` unrolling macros, for now
+unrolling=0
 format=1
 cpp17=
 
@@ -55,8 +56,8 @@ while [ $# -gt 0 ]; do
             *) fail "invalid argument to --clean: $2" ;;
           esac
           ;;
-        -d | --dep) deps+=("$2") ; shift ;;
-        --libcrux-dep) libcrux_deps+=("$2") ; shift ;;
+        -d | --dep) deps+=("libcrux_iot_$2") ; shift ;;
+        --libcrux-dep) libcrux_deps+=("libcrux_$2") ; shift ;;
         --extract) extract="$2" ; shift ;;
         --config) config="$2"; shift ;;
         --out) out="$2"; shift ;;
@@ -100,75 +101,27 @@ if [[ "$clean_cargo" = 1 ]]; then
   (cd workspace_root; cargo clean -p $extract_crate)
 fi
 
-dep_llbcs=()
+dep_args=("--include $extract_crate_ --start-from $extract_crate_")
 for dep in "${deps[@]}"; do
-  dep_crate="libcrux-iot-$dep"
-  dep_crate_=$(sed s/-/_/g <<<$dep_crate)
-  dep_llbc_path=$workspace_root/${dep_crate_}.llbc
-  dep_llbcs+=("$dep_llbc_path")
+    dep_arg="--include $dep --start-from $dep"
+    dep_args+=("$dep_arg")
 done
+
 for dep in "${libcrux_deps[@]}"; do
-  dep_crate="libcrux-$dep"
-  dep_crate_=$(sed s/-/_/g <<<$dep_crate)
-  dep_llbc_path=$workspace_root/${dep_crate_}.llbc
-  dep_llbcs+=("$dep_llbc_path")
+    dep_arg="--include $dep --start-from $dep"
+    dep_args+=("$dep_arg")
 done
 
 if [[ "$no_charon" = 0 ]]; then
   rm -rf "${dep_llbcs[@]}"
 
-  for dep in ${libcrux_deps[@]}; do
-      dep_crate="libcrux-$dep"
-      dep_src=$(cargo metadata --format-version=1 --manifest-path=$pkg_root/Cargo.toml | jq -r ".packages[] | select(.name==\"$dep_crate\") | .targets[].src_path")
-      dep_src_root=$(dirname $(dirname $dep_src))
-      dep_crate_=$(sed s/-/_/g <<<$dep_crate)
-    # dep_pkg_root="$libcrux_workspace_root/$dep"
-    dep_llbc_path=$workspace_root/${dep_crate_}.llbc
-
-    # Because of a Charon bug we have to clean the dep crate.
-    (cd $dep_src_root ; cargo clean -p $dep_crate)
-    echo "Running charon (libcrux - $dep) ..."
-    ( cd $dep_src_root &&
-      RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon cargo \
-        --remove-associated-types '*' \
-        --rustc-arg=-Cdebug-assertions=no \
-        --dest-file=$dep_llbc_path)
-    if ! [[ -f $dep_llbc_path ]]; then
-        echo "😱😱😱 You are the victim of this bug: https://hacspec.zulipchat.com/#narrow/stream/433829-Circus/topic/charon.20declines.20to.20generate.20an.20llbc.20file"
-        echo "Suggestion: rm -rf $workspace_root/target or cargo clean"
-        echo "failed for libcrux dependency $dep: file $dep_llbc_path does not exist"
-        file $dep_llbc_path
-        exit 1
-    fi
-  done
-
-  for dep in ${deps[@]}; do
-    dep_crate="libcrux-iot-$dep"
-    dep_crate_=$(sed s/-/_/g <<<$dep_crate)
-    dep_pkg_root="$workspace_root/$dep"
-    dep_llbc_path=$workspace_root/${dep_crate_}.llbc
-
-    # Because of a Charon bug we have to clean the dep crate.
-    (cd $workspace_root ; cargo clean -p $dep_crate)
-    echo "Running charon ($dep) ..."
-    ( cd $dep_pkg_root &&
-      RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon cargo \
-        --remove-associated-types '*' \
-        --rustc-arg=-Cdebug-assertions=no )
-    if ! [[ -f $dep_llbc_path ]]; then
-        echo "😱😱😱 You are the victim of this bug: https://hacspec.zulipchat.com/#narrow/stream/433829-Circus/topic/charon.20declines.20to.20generate.20an.20llbc.20file"
-        echo "Suggestion: rm -rf $workspace_root/target or cargo clean"
-        echo "failed for dependency $dep: file $dep_llbc_path does not exist"
-        file $dep_llbc_path
-        exit 1
-    fi
-  done
-
   echo "Running charon ($extract) ..."
     ( cd $pkg_root &&
-      RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon cargo \
-        --remove-associated-types '*' \
-        --rustc-arg=-Cdebug-assertions=no \
+          RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon cargo \
+                   --preset eurydice \
+                   ${dep_args[@]} \
+                   --remove-associated-types '*' \
+                   --rustc-arg=-Cdebug-assertions=no \
         $features )
 else
     echo "Skipping charon"
@@ -230,7 +183,7 @@ echo $EURYDICE_HOME/eurydice \
 $EURYDICE_HOME/eurydice \
     --config "$config" -funroll-loops $unrolling \
     --header header.txt $cpp17 \
-    "${dep_llbcs[@]}" $extract_llbc_path
+    $extract_llbc_path
 
 if [[ "$eurydice_glue" = 1 ]]; then
     cp "$glue" .

c/extract-mldsa.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+
+repo_root=$(git rev-parse --show-toplevel)
+
+$repo_root/c/c.sh --extract ml-dsa --config $repo_root/c/mldsa.yml --no-glue --dep sha3 --libcrux-dep secrets --clean cfiles

c/ml-dsa/extracted/CMakeLists.txt

@@ -0,0 +1,94 @@
+# cmake -B build -G "Ninja Multi-Config"
+# cmake --build build
+# # For release (benchmarks)
+# cmake --build build --config Release
+
+cmake_minimum_required(VERSION 3.10..4.0)
+
+project(libcrux-ml-dsa
+    VERSION 0.1.0
+    LANGUAGES C CXX
+)
+
+set(CMAKE_C_STANDARD 11)
+set(CMAKE_CXX_STANDARD 20)
+
+if(NOT MSVC)
+    # TODO: Clean up
+    add_compile_options(
+        -Wall
+
+        # -Wextra
+        # -pedantic
+        # -Wconversion
+        # -Wsign-conversion
+        $<$<CONFIG:DEBUG>:-g>
+        $<$<CONFIG:DEBUG>:-Og>
+        $<$<CONFIG:RELEASE>:-g>
+        $<$<CONFIG:RELEASE>:-O3>
+    )
+endif(NOT MSVC)
+
+set(CMAKE_COLOR_DIAGNOSTICS "ON")
+
+# For LSP-based editors
+set(CMAKE_EXPORT_COMPILE_COMMANDS 1)
+include_directories(
+    ${PROJECT_SOURCE_DIR}
+    ${PROJECT_SOURCE_DIR}/internal
+    ${PROJECT_SOURCE_DIR}/karamel/include
+)
+file(GLOB SOURCES
+  ${PROJECT_SOURCE_DIR}/libcrux_iot_mldsa_core.c
+  ${PROJECT_SOURCE_DIR}/libcrux_iot_sha3.c
+  ${PROJECT_SOURCE_DIR}/libcrux_iot_mldsa65_portable.c
+)
+
+if(${CMAKE_SYSTEM_NAME} MATCHES Linux)
+    add_compile_options(
+        -fPIC
+    )
+endif(${CMAKE_SYSTEM_NAME} MATCHES Linux)
+
+# if(${CMAKE_SYSTEM_NAME} MATCHES Linux AND CMAKE_BUILD_TYPE MATCHES "Release")
+#     add_compile_options(
+#         -flto
+#     )
+#     add_link_options(-flto)
+# endif(${CMAKE_SYSTEM_NAME} MATCHES Linux AND CMAKE_BUILD_TYPE MATCHES "Release")
+
+add_library(ml_dsa SHARED ${SOURCES})
+add_library(ml_dsa_static STATIC ${SOURCES})
+
+# --- Tests
+if(DEFINED ENV{LIBCRUX_UNPACKED})
+    add_compile_definitions(LIBCRUX_UNPACKED)
+endif(DEFINED ENV{LIBCRUX_UNPACKED})
+
+# Get gtests
+include(FetchContent)
+FetchContent_Declare(googletest
+    GIT_REPOSITORY https://github.com/google/googletest.git
+    GIT_TAG v1.16.0
+)
+
+# For Windows: Prevent overriding the parent project's compiler/linker settings
+set(gtest_force_shared_crt ON CACHE BOOL "" FORCE)
+FetchContent_MakeAvailable(googletest)
+
+# Get nlohmann json
+FetchContent_Declare(json
+    GIT_REPOSITORY https://github.com/nlohmann/json.git
+    GIT_TAG v3.11.3
+)
+FetchContent_MakeAvailable(json)
+
+add_executable(ml_dsa_test65
+    ${PROJECT_SOURCE_DIR}/tests/mldsa65.cc
+)
+target_link_libraries(ml_dsa_test65 PRIVATE
+    ml_dsa_static
+    gtest_main
+    nlohmann_json::nlohmann_json
+)
+

c/ml-dsa/extracted/code_gen.txt

@@ -0,0 +1,6 @@
+This code was generated with the following revisions:
+Charon: 146b7dce58cb11ca8010b1c947c3437a959dcd88
+Eurydice: cdf02f9d8ed0d73f88c0a495c5b79359a51398fc
+Karamel: 8e7262955105599e91f3a99c9ab3d3387f7046f2
+F*: unset
+Libcrux: 0c7d13eb4d0117dce1ec2ef42fdb87d10cf78e2b