Merge branch 'main' into keks/bench-chachapoly

cryspen · Feb 12, 2025 · 26e3056 · 26e3056
2 parents 639672c + cc29351
commit 26e3056
Show file tree

Hide file tree

Showing 57 changed files with 524 additions and 428 deletions.
diff --git a/.docker/c/Dockerfile b/.docker/c/Dockerfile
@@ -20,17 +20,18 @@ WORKDIR $HOME
 USER $USER
 COPY --chown=$USER:$USER . $HOME/$USER
 
-# Setup & install.
-ADD install.sh /tmp/install.sh
-RUN bash /tmp/install.sh
-ADD ext-tools.sh /tmp/ext-tools.sh
-RUN bash /tmp/ext-tools.sh
-
 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=97a06e07e7e423df192c40d5a88bf6c85fd4d278
+ENV EURYDICE_REV=b8ea420ccde8db516ced5db9c097d77fa558fb94
+ENV CHARON_REV=30cab88265206f4fa849736e704983e39a404d96
 ENV PATH="${PATH}:$HOME/fstar/bin:$HOME/z3/bin"
 
-
+# Setup & install.
+ADD install.sh /tmp/install.sh
+RUN bash /tmp/install.sh
+ADD ext-tools.sh /tmp/ext-tools.sh
+RUN bash /tmp/ext-tools.sh
diff --git a/.docker/c/ext-tools.sh b/.docker/c/ext-tools.sh
@@ -4,28 +4,32 @@ set -v -e -x
 
 source $HOME/.profile
 
-curl -L https://github.com/AeneasVerif/charon/archive/db4e045d4597d06d854ce7a2c10e8dcfda6ecd25.zip \
+curl -L https://github.com/AeneasVerif/charon/archive/$CHARON_REV.zip \
     --output charon.zip
 unzip charon.zip
 rm -rf charon.zip
-mv charon-db4e045d4597d06d854ce7a2c10e8dcfda6ecd25/ charon
+mv charon-$CHARON_REV/ charon
 
-curl -L https://github.com/FStarLang/karamel/archive/3823e3d82fa0b271d799b61c59ffb4742ddc1e65.zip \
+curl -L https://github.com/FStarLang/karamel/archive/$KRML_REV.zip \
     --output karamel.zip
 unzip karamel.zip
 rm -rf karamel.zip
-mv karamel-3823e3d82fa0b271d799b61c59ffb4742ddc1e65/ karamel
+mv karamel-$KRML_REV/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/83ab5654d49df0603797bf510475d52d67ca24d8.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/$EURYDICE_REV.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-83ab5654d49df0603797bf510475d52d67ca24d8/ eurydice
+mv eurydice-$EURYDICE_REV/ eurydice
 
 echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
 echo "export CHARON_HOME=$HOME/charon" >>$HOME/.profile
 
+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

diff --git a/.github/workflows/c.yml b/.github/workflows/c.yml
@@ -8,6 +8,11 @@ on:
   workflow_dispatch:
   merge_group:
 
+env:
+  REGISTRY: ghcr.io
+  IMAGE_NAME: ${{ github.repository }}-c
+  VERSION_TAG: latest
+
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
@@ -28,6 +33,7 @@ jobs:
     outputs:
       # only run if files in `.docker/c/` unchanged
       should-run: ${{ steps.changes.outputs.docker-c == 'false' }}
+      image: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.VERSION_TAG }}
 
   report-status-tests:
     runs-on: ubuntu-latest
@@ -56,7 +62,8 @@ jobs:
     needs: [setup]
     if: ${{ needs.setup.outputs.should-run == 'true' }}
     runs-on: ubuntu-latest
-    container: franziskus/libcrux-c:latest
+    container:
+      image: ${{ needs.setup.outputs.image }}
     defaults:
       run:
         working-directory: libcrux-ml-kem
@@ -80,7 +87,8 @@ jobs:
     needs: [setup]
     if: ${{ needs.setup.outputs.should-run == 'true' }}
     runs-on: ubuntu-latest
-    container: franziskus/libcrux-c:latest
+    container:
+      image: ${{ needs.setup.outputs.image }}
     defaults:
       run:
         working-directory: libcrux-ml-kem
@@ -105,7 +113,8 @@ jobs:
     needs: [setup]
     if: ${{ needs.setup.outputs.should-run == 'true' }}
     runs-on: ubuntu-latest
-    container: franziskus/libcrux-c:latest
+    container:
+      image: ${{ needs.setup.outputs.image }}
     defaults:
       run:
         working-directory: libcrux-ml-dsa

diff --git a/.github/workflows/docker-c-latest.yml b/.github/workflows/docker-c-latest.yml
@@ -0,0 +1,57 @@
+name: Publish latest Docker C extraction container
+
+on:
+  workflow_dispatch:
+  pull_request:
+    branches: ['main']
+    paths: ['.docker/c/**']
+    types:
+      - closed
+
+env:
+  REGISTRY: ghcr.io
+  IMAGE_NAME: ${{ github.repository }}-c
+  SOURCE_TAG: unstable
+  TARGET_TAG: latest
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  setup:
+    # Only run if PR merged
+    if: ${{ github.event.pull_request.merged == true }}
+    runs-on: ubuntu-latest
+    steps:
+      - name: Setup tag names
+        run: echo "Setting up tag names..."
+    outputs:
+      source_image: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.SOURCE_TAG }}
+      target_image: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.TARGET_TAG }}
+
+
+  publish:
+    needs: [setup]
+    runs-on: ubuntu-latest
+
+    # We need write access to packages
+    permissions:
+      contents: read
+      packages: write
+      id-token: write
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: Log in to the Container registry
+        uses: docker/login-action@v3
+        with:
+          registry: ${{ env.REGISTRY }}
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+      - name: Retag and push Docker image
+        id: push
+        run: |
+            docker pull ${{ needs.setup.outputs.source_image }}
+            docker tag ${{ needs.setup.outputs.source_image }} ${{ needs.setup.outputs.target_image }}
+            docker push ${{ needs.setup.outputs.target_image }}
diff --git a/benchmarks/Cargo.toml b/benchmarks/Cargo.toml
@@ -20,6 +20,7 @@ libcrux = { path = "../", features = ["rand", "tests"] }
 libcrux-chacha20poly1305 = { path = "../chacha20poly1305" }
 libcrux-kem = { path = "../libcrux-kem", features = ["tests"] }
 libcrux-ml-kem = { path = "../libcrux-ml-kem" }
+libcrux-sha2 = { path = "../sha2" }
 rand_core = { version = "0.6" }
 # Benchmarking "RustCrypto"
 chacha20poly1305 = "0.10"

diff --git a/benchmarks/benches/sha2.rs b/benchmarks/benches/sha2.rs
@@ -1,8 +1,6 @@
 #![allow(non_snake_case)]
 use criterion::{criterion_group, criterion_main, BatchSize, BenchmarkId, Criterion, Throughput};
 
-use libcrux::digest::{self, *};
-
 use benchmarks::util::*;
 
 macro_rules! impl_comp {
@@ -23,7 +21,7 @@ macro_rules! impl_comp {
                         b.iter_batched(
                             || randombytes(*payload_size),
                             |payload| {
-                                let _d = digest::hash($libcrux, &payload);
+                                let _d = $libcrux(&payload);
                             },
                             BatchSize::SmallInput,
                         )
@@ -87,28 +85,28 @@ macro_rules! impl_comp {
 
 impl_comp!(
     Sha2_224,
-    Algorithm::Sha224,
+    libcrux_sha2::sha224,
     None,
     sha2::Sha224,
     MessageDigest::sha224()
 );
 impl_comp!(
     Sha2_256,
-    Algorithm::Sha256,
+    libcrux_sha2::sha256,
     Some(&ring::digest::SHA256),
     sha2::Sha256,
     MessageDigest::sha256()
 );
 impl_comp!(
     Sha2_384,
-    Algorithm::Sha384,
+    libcrux_sha2::sha384,
     Some(&ring::digest::SHA384),
     sha2::Sha384,
     MessageDigest::sha384()
 );
 impl_comp!(
     Sha2_512,
-    Algorithm::Sha512,
+    libcrux_sha2::sha512,
     Some(&ring::digest::SHA512),
     sha2::Sha512,
     MessageDigest::sha512()

diff --git a/libcrux-ml-dsa/cg/code_gen.txt b/libcrux-ml-dsa/cg/code_gen.txt
@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
-Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
-Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
-F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
-Libcrux: 5c7517ad29733fa58f7764538c6c66db534763a6
+Charon: 30cab88265206f4fa849736e704983e39a404d96
+Eurydice: b8ea420ccde8db516ced5db9c097d77fa558fb94
+Karamel: 97a06e07e7e423df192c40d5a88bf6c85fd4d278
+F*: b0961063393215ca65927f017720cb365a193833-dirty
+Libcrux: 15b22d1beea1cc7052b8a68b653b012241724664
diff --git a/libcrux-ml-dsa/cg/eurydice_glue.h b/libcrux-ml-dsa/cg/eurydice_glue.h
@@ -20,6 +20,14 @@ extern "C" {
 #include "karamel/endianness.h"
 #include "karamel/target.h"
 
+#define EURYDICE_ASSERT(test, msg)                                            \
+  do {                                                                        \
+    if (!(test)) {                                                            \
+      fprintf(stderr, "assertion \"%s\" failed: file \"%s\", line %d\n", msg, \
+              __FILE__, __LINE__);                                            \
+    }                                                                         \
+  } while (0)
+
 // SLICES, ARRAYS, ETC.
 
 // The MSVC C++ compiler does not support compound literals.

diff --git a/libcrux-ml-dsa/cg/header.txt b/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: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
- * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
- * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
- * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
- * Libcrux: 5c7517ad29733fa58f7764538c6c66db534763a6
+ * Charon: 30cab88265206f4fa849736e704983e39a404d96
+ * Eurydice: b8ea420ccde8db516ced5db9c097d77fa558fb94
+ * Karamel: 97a06e07e7e423df192c40d5a88bf6c85fd4d278
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 15b22d1beea1cc7052b8a68b653b012241724664
  */
diff --git a/libcrux-ml-dsa/cg/libcrux_core.h b/libcrux-ml-dsa/cg/libcrux_core.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
- * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
- * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
- * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
- * Libcrux: 5c7517ad29733fa58f7764538c6c66db534763a6
+ * Charon: 30cab88265206f4fa849736e704983e39a404d96
+ * Eurydice: b8ea420ccde8db516ced5db9c097d77fa558fb94
+ * Karamel: 97a06e07e7e423df192c40d5a88bf6c85fd4d278
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 15b22d1beea1cc7052b8a68b653b012241724664
  */
 
 #ifndef __libcrux_core_H