Merge pull request #1237 from cryspen/franziskus/single-eurydice

Update Eurydice

Author: jschneider-bensch

.docker/c/Dockerfile

@@ -22,13 +22,13 @@ COPY --chown=$USER:$USER . $HOME/$USER
 
 ENV FSTAR_HOME=$HOME/fstar
 ENV HACL_HOME=$HOME/hacl-star
-ENV KRML_HOME=$HOME/karamel
 ENV EURYDICE_HOME=$HOME/eurydice
-ENV CHARON_HOME=$HOME/charon
-ENV KRML_REV=80f5435f2fc505973c469a4afcc8d875cddd0d8b
-ENV EURYDICE_REV=2381cbc416ef2ad0b561c362c500bc84f36b6785
-ENV CHARON_REV=667d2fc98984ff7f3df989c2367e6c1fa4a000e7
+ENV KRML_HOME=$HOME/eurydice/karamel
+ENV CHARON_HOME=$HOME/eurydice/charon
+ENV EURYDICE_REV=cdf02f9d8ed0d73f88c0a495c5b79359a51398fc
 ENV PATH="${PATH}:$HOME/fstar/bin:$HOME/z3/bin"
+ENV CC=clang
+ENV CXX=clang++
 
 # Setup & install.
 ADD install.sh /tmp/install.sh

.docker/c/ext-tools.sh

@@ -4,48 +4,31 @@ set -v -e -x
 
 source $HOME/.profile
 
-curl -L https://github.com/AeneasVerif/charon/archive/$CHARON_REV.zip \
-    --output charon.zip
-unzip charon.zip
-rm -rf charon.zip
-mv charon-$CHARON_REV/ charon
-
-curl -L https://github.com/FStarLang/karamel/archive/$KRML_REV.zip \
-    --output karamel.zip
-unzip karamel.zip
-rm -rf karamel.zip
-mv karamel-$KRML_REV/ karamel
-
-curl -L https://github.com/AeneasVerif/eurydice/archive/$EURYDICE_REV.zip \
-    --output eurydice.zip
-unzip eurydice.zip
-rm -rf eurydice.zip
-mv eurydice-$EURYDICE_REV/ eurydice
-
-echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
+git clone https://github.com/AeneasVerif/eurydice.git
+cd eurydice
+git checkout $EURYDICE_REV
+
+make setup-karamel
+make setup-charon
+make setup-libcrux
+
+make test
+
+# Remove Charon build files, since the binary has been generated
+cd charon/charon
+cargo clean
+cd -
+
+echo "export KRML_HOME=$HOME/eurydice/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
-echo "export CHARON_HOME=$HOME/charon" >>$HOME/.profile
+echo "export CHARON_HOME=$HOME/eurydice/charon" >>$HOME/.profile
+
+CHARON_REV="$(jq -r ".nodes.charon.locked.rev" flake.lock)"
+KRML_REV="$(jq -r ".nodes.karamel.locked.rev" flake.lock)"
 
 echo "export KRML_REV=$KRML_REV" >>$HOME/.profile
 echo "export EURYDICE_REV=$EURYDICE_REV" >>$HOME/.profile
 echo "export CHARON_REV=$CHARON_REV" >>$HOME/.profile
 
 source $HOME/.profile
 
-# Build everything
-cd charon
-make build-charon-rust -j
-cd -
-
-cd karamel
-make -j
-cd -
-
-cd eurydice/lib
-rm -f charon
-ln -s $CHARON_HOME charon
-rm -f krml
-ln -s $KRML_HOME/lib krml
-cd ../
-make -j
-cd ../

.docker/c/install.sh

@@ -35,5 +35,5 @@ echo "[[ ! -r /home/$USER/.opam/opam-init/init.sh ]] || source /home/$USER/.opam
 
 source $HOME/.profile
 opam install --yes ocamlfind visitors menhir ppx_deriving_yojson core_unix \
-    sedlex wasm fix process pprint zarith yaml easy_logging terminal unionFind
+    sedlex wasm fix process pprint zarith yaml easy_logging terminal unionFind ocamlformat.0.27.0
 eval $(opam env)

.docker/c/setup.sh

@@ -9,10 +9,14 @@ apt-get install -y \
     build-essential \
     opam \
     jq \
+    git \
+    clang \
+    ninja-build \
     libgmp-dev \
     locales \
     pkg-config \
     clang-format\
+    cmake \
     curl \
     time
 curl -fsSL https://deb.nodesource.com/setup_21.x | bash -

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

@@ -136,11 +136,11 @@ jobs:
           cmake --build build
 
       - name: 🏃🏻‍♀️ Test
-        run: ./build/Debug/ml_kem_test
+        run: ./build/Debug/ml_kem_test768
         if: ${{ matrix.os == 'windows-latest' }}
 
       - name: 🏃🏻‍♀️ Test
-        run: ./build/ml_kem_test
+        run: ./build/ml_kem_test768
         if: ${{ matrix.os != 'windows-latest' }}
 
       - name: 🔨 Build Release
@@ -174,11 +174,11 @@ jobs:
       # FIXME: Benchmark build for cg on Windows CI is not working right now.
 
       - name: 🏃🏻‍♀️ Test
-        run: ./build/ml_kem_test
+        run: ./build/ml_kem_test768
         if: ${{ matrix.os != 'windows-latest' }}
 
       - name: 🏃🏻‍♀️ Test
-        run: ./build/Debug/ml_kem_test
+        run: ./build/Debug/ml_kem_test768
         if: ${{ matrix.os == 'windows-latest' }}
 
   test-build-ml-dsa-header-only:

libcrux-ml-dsa/c.sh

@@ -16,6 +16,9 @@ if [[ -z "$KRML_HOME" ]]; then
     exit 1
 fi
 
+mldsa_root=$(pwd)
+repo_root=$(realpath ../)
+
 portable_only=0
 no_hacl=0
 no_charon=0
@@ -58,16 +61,26 @@ fi
 if [[ "$no_charon" = 0 ]]; then
     # Because of a Charon bug we have to clean the sha3 crate.
     cargo clean -p libcrux-sha3
-    rm -rf ../libcrux_ml_dsa.llbc ../libcrux_sha3.llbc
-    echo "Running charon (sha3) ..."
-    (cd ../libcrux-sha3 && RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon --remove-associated-types '*' --rustc-arg=-Cdebug-assertions=no)
-    if ! [[ -f ../libcrux_sha3.llbc ]]; then
+    rm -rf $repo_root/libcrux_ml_dsa.llbc $repo_root/libcrux_sha3.llbc
+
+    flags=
+    if [[ $(uname -m) == "arm64" ]]; then
+        flags+="-- --target=x86_64-apple-darwin"
+    fi
+
+    echo "Running charon (all) ..."
+    RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon cargo \
+                                    $features \
+                                    --preset eurydice \
+                                    --include 'libcrux_sha3' \
+                                    --start-from libcrux_ml_dsa --start-from libcrux_sha3 \
+                                    --include 'core::num::*::BITS' --include 'core::num::*::MAX' \
+                                    --rustc-arg=-Cdebug-assertions=no $flags
+    if ! [[ -f $repo_root/libcrux_ml_dsa.llbc ]]; then
         echo "😱😱😱 You are the victim of a bug."
         echo "Suggestion: rm -rf ../target or cargo clean"
         exit 1
     fi
-    echo "Running charon (ml-dsa) with $features ..."
-    RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon --remove-associated-types '*' --rustc-arg=-Cdebug-assertions=no $features
 else
     echo "Skipping charon"
 fi
@@ -114,10 +127,10 @@ echo " */" >> header.txt
 # Run eurydice to extract the C code
 echo "Running eurydice ..."
 echo $EURYDICE_HOME/eurydice --config ../$config -funroll-loops $unrolling \
---header header.txt $cpp17 ../../libcrux_ml_dsa.llbc ../../libcrux_sha3.llbc
+--header header.txt $cpp17 ../../libcrux_ml_dsa.llbc --keep-going
 
-$EURYDICE_HOME/eurydice --debug "-dast" --config ../$config -funroll-loops $unrolling \
---header header.txt $cpp17 ../../libcrux_ml_dsa.llbc ../../libcrux_sha3.llbc
+$EURYDICE_HOME/eurydice --config ../$config -funroll-loops $unrolling \
+--header header.txt $cpp17 ../../libcrux_ml_dsa.llbc --keep-going
 
 if [[ "$eurydice_glue" = 1 ]]; then
     cp $EURYDICE_HOME/include/eurydice_glue.h .
@@ -130,6 +143,7 @@ if [[ "$karamel_include" = 1 ]]; then
 fi
 
 find . -type f -name '*.c' -and -not -path '*_deps*' -exec clang-format-18 --style=Google -i "{}" \;
+find . -type f -name '*.cc' -and -not -path '*_deps*' -exec clang-format-18 --style=Google -i "{}" \;
 find . -type f -name '*.h' -and -not -path '*_deps*' -exec clang-format-18 --style=Google -i "{}" \;
 if [ -d "internal" ]; then
     clang-format-18 --style=Google -i internal/*.h

libcrux-ml-dsa/cg.yaml

@@ -5,18 +5,43 @@ files:
     inline_static: true
     api:
       - [libcrux_intrinsics, avx2]
+    private:
+      monomorphizations_exact:
+        - [ Eurydice, arr_05]
+        - [ Eurydice, arr_c0]
 
-  # # Constant time ops
-  # - name: libcrux_ct_ops
-  #   inline_static: true
-  #   api:
-  #     - [libcrux_ml_kem, constant_time_ops]
+  # MLDSA: MISC NON-ARCHITECTURE SPECIFIC HEADERS
+  - name: libcrux_mldsa_core
+    inline_static: true
+    private:
+      monomorphizations_of:
+        - [libcrux_ml_dsa, types, "*"]
+      patterns:
+        - [core, "*"]
+        - [libcrux_ml_dsa, types, "*" ]
+      monomorphizations_exact:
+        - [libcrux_sha3, Sha3_512Digest]
+        - [ Eurydice_dst_ref_shared uint8_t size_t_x4]
+        - [ Eurydice_dst_ref_shared uint8_t size_t_x2]
+        - [ Eurydice_dst_ref uint8_t size_t_x4]
+        - [ Eurydice_dst_ref uint8_t size_t_x2]
+        - [ "Eurydice_slice uint8_t_x4" ]
+        - [ "Eurydice_slice uint8_t_x2" ]
+        - [ Eurydice, arr_88]
+        - [ Eurydice, arr_910]
+        - [ Eurydice, arr_6d]
+        - [ core, result, unwrap_26_ab ]
+        - [ core, result, Result_a4 ]
 
+    api:
+      - [Eurydice, "*"]
+      
   # SHA3 (no mention of libcrux_mlkem in this section, please)
-
   - name: libcrux_sha3_avx2
     inline_static: true
     target: "avx2"
+    include_in_h:
+      - '"intrinsics/libcrux_intrinsics_avx2.h"'
     api:
       patterns:
         - [libcrux_sha3, avx2, "*"]
@@ -32,8 +57,7 @@ files:
         - [libcrux_sha3, avx2, "*"]
         - [libcrux_sha3, simd, avx2, "*"]
         - [libcrux_sha3, generic_keccak, simd256, "*"]
-    include_in_h:
-      - '"intrinsics/libcrux_intrinsics_avx2.h"'
+
 
   # Portable SHA3
   - name: libcrux_sha3_portable
@@ -63,7 +87,6 @@ files:
         - [libcrux_sha3, generic_keccak, xof, "*"]
 
   # MLDSA-65
-
   - name: libcrux_mldsa65_avx2
     inline_static: true
     target: "avx2"
@@ -76,8 +99,6 @@ files:
         - [libcrux_ml_dsa, hash_functions, simd256, "*"]
         - [libcrux_ml_dsa, ml_dsa_65, avx2, "*"]
         - [libcrux_ml_dsa, ml_dsa_generic, instantiations, avx2, "*"]
-        # - [core, option, Option_c4]
-        # - [libcrux_ml_dsa, polynomial, "*" ]
       monomorphizations_of:
         - [libcrux_ml_dsa, simd, avx2, "*"]
         - [libcrux_ml_dsa, hash_functions, simd256, "*"]
@@ -86,8 +107,9 @@ files:
       monomorphizations_using:
         - [libcrux_ml_dsa, simd, avx2, "*"]
         - [libcrux_ml_dsa, hash_functions, simd256, "*"]
-      # monomorphizations_exact:
-      #   - [core, option, Option_c4]
+      monomorphizations_exact:
+        - [core, option, Option_e70]
+        - [ Eurydice, arr_f8]
 
   - name: libcrux_mldsa65_portable
     inline_static: true
@@ -99,48 +121,30 @@ files:
         - [libcrux_ml_dsa, hash_functions, portable, "*"]
         - [libcrux_ml_dsa, ml_dsa_65, portable, "*"]
         - [libcrux_ml_dsa, ml_dsa_generic, instantiations, portable, "*"]
-        # - [libcrux_ml_dsa, pre_hash, PreHashResult]
-        # - [core, option, Option_84]
       monomorphizations_of:
         - [libcrux_ml_dsa, polynomial, "*" ]
         - [libcrux_ml_dsa, simd, "*"]
         - [libcrux_ml_dsa, hash_functions, portable, "*"]
         - [libcrux_ml_dsa, ml_dsa_65, portable]
         - [libcrux_ml_dsa, ml_dsa_generic, instantiations, portable, "*"]
-        # - [libcrux_ml_dsa, pre_hash, PreHashResult]
-        # - [core, option, Option_84]
       monomorphizations_using:
         - [libcrux_ml_dsa, polynomial, "*" ]
         - [libcrux_ml_dsa, simd, "*"]
         - [libcrux_ml_dsa, hash_functions, portable, "*"]
         - [libcrux_ml_dsa, ml_dsa_generic, instantiations, portable, "*"]
-        # - [libcrux_ml_dsa, pre_hash, PreHashResult]
       monomorphizations_exact:
         - [libcrux_ml_dsa, pre_hash, PreHashResult]
         - [core, result, Result_a8]
         - [core, option, Option_84]
 
-
-  # MLKEM: MISC NON-ARCHITECTURE SPECIFIC HEADERS
-  - name: libcrux_core
+  # MLDSA: catch-all for things that have not matched earlier
+  - name: libcrux_mldsa_core
     inline_static: true
     private:
       monomorphizations_of:
-        - [core, "*"]
-        - [libcrux_ml_dsa, types, "*"]
-        - [libcrux_ml_dsa, utils, "*" ]
-      monomorphizations_using:
         - [Eurydice, "*" ]
-        - [libcrux_ml_dsa, types, "*"]
       patterns:
-        - [core, "*"]
-        - [libcrux_ml_dsa, types ]
-        - [libcrux_ml_dsa, constants ]
-        - [libcrux_ml_dsa, utils, "*" ]
-        # - [libcrux_ml_dsa, simd, traits ]
-    api:
-      - [Eurydice, "*"]
-
+        - [Eurydice, "*" ]
 naming:
   skip_prefix:
     - [ core, core_arch, arm_shared, neon ]

libcrux-ml-dsa/cg/code_gen.txt

@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: 667d2fc98984ff7f3df989c2367e6c1fa4a000e7
-Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
-Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
-F*: 71d8221589d4d438af3706d89cb653cf53e18aab
-Libcrux: 4433a17f91aab0789f083de6c7fe08493e5998c8
+Charon: 146b7dce58cb11ca8010b1c947c3437a959dcd88
+Eurydice: cdf02f9d8ed0d73f88c0a495c5b79359a51398fc
+Karamel: 8e7262955105599e91f3a99c9ab3d3387f7046f2
+F*: unset
+Libcrux: 927ad3614c662733d7c77b6cd4304177fbd390a8