Merge pull request #795 from cryspen/franziskus/update-c-ext-tools

Update C extraction tools
cryspen · Feb 11, 2025 · 464e733 · 464e733
2 parents f91f5cd + c9719eb
commit 464e733
Show file tree

Hide file tree

Showing 51 changed files with 367 additions and 418 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/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

diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.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_mldsa65_avx2_H
@@ -6035,11 +6035,7 @@ libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_internal_07(
       memcpy(signer_response, signer_response1,
              (size_t)5U *
                  sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_4b));
-      if (hint0.tag == None) {
-        uu____8 = (CLITERAL(Result_53){
-            .tag = Err,
-            .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError});
-      } else {
+      if (!(hint0.tag == None)) {
         int32_t hint1[6U][256U];
         memcpy(hint1, hint0.f0, (size_t)6U * sizeof(int32_t[256U]));
         int32_t hint[6U][256U];
@@ -6059,6 +6055,9 @@ libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_internal_07(
             Eurydice_array_to_slice((size_t)3309U, signature, uint8_t));
         return (CLITERAL(Result_53){.tag = Ok});
       }
+      uu____8 = (CLITERAL(Result_53){
+          .tag = Err,
+          .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError});
     }
   }
   return uu____8;
@@ -6500,33 +6499,31 @@ libcrux_ml_dsa_encoding_signature_deserialize_21(
     if (uu____3.tag == None) {
       for (size_t i = previous_true_hints_seen; i < max_ones_in_hint; i++) {
         size_t j = i;
-        if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) !=
-            0U) {
-          uu____2 = (CLITERAL(Result_41){
-              .tag = Err,
-              .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError});
-          break;
+        if (!(Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) !=
+              0U)) {
+          continue;
         }
+        uu____2 = (CLITERAL(Result_41){
+            .tag = Err,
+            .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError});
+        break;
       }
       return (CLITERAL(Result_41){.tag = Ok});
     } else {
-      size_t i0 = uu____3.f0;
+      size_t i = uu____3.f0;
       size_t current_true_hints_seen = (size_t)Eurydice_slice_index(
-          hint_serialized, max_ones_in_hint + i0, uint8_t, uint8_t *);
+          hint_serialized, max_ones_in_hint + i, uint8_t, uint8_t *);
+      libcrux_ml_dsa_types_VerificationError uu____4;
       if (current_true_hints_seen < previous_true_hints_seen) {
-        uu____2 = (CLITERAL(Result_41){
-            .tag = Err,
-            .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError});
-        break;
+        uu____4 = libcrux_ml_dsa_types_VerificationError_MalformedHintError;
+        uu____2 = (CLITERAL(Result_41){.tag = Err, .f0 = uu____4});
       } else if (previous_true_hints_seen > max_ones_in_hint) {
-        uu____2 = (CLITERAL(Result_41){
-            .tag = Err,
-            .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError});
-        break;
+        uu____4 = libcrux_ml_dsa_types_VerificationError_MalformedHintError;
+        uu____2 = (CLITERAL(Result_41){.tag = Err, .f0 = uu____4});
       } else {
-        for (size_t i = previous_true_hints_seen; i < current_true_hints_seen;
-             i++) {
-          size_t j = i;
+        for (size_t i0 = previous_true_hints_seen; i0 < current_true_hints_seen;
+             i0++) {
+          size_t j = i0;
           if (j > previous_true_hints_seen) {
             if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) <=
                 Eurydice_slice_index(hint_serialized, j - (size_t)1U, uint8_t,
@@ -6535,22 +6532,17 @@ libcrux_ml_dsa_encoding_signature_deserialize_21(
                   .tag = Err,
                   .f0 =
                       libcrux_ml_dsa_types_VerificationError_MalformedHintError});
-              break;
-            } else {
-              libcrux_ml_dsa_encoding_signature_set_hint(
-                  out_hint, i0,
-                  (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t,
-                                               uint8_t *));
             }
-          } else {
-            libcrux_ml_dsa_encoding_signature_set_hint(
-                out_hint, i0,
-                (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t,
-                                             uint8_t *));
           }
+          libcrux_ml_dsa_encoding_signature_set_hint(
+              out_hint, i,
+              (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t,
+                                           uint8_t *));
         }
         previous_true_hints_seen = current_true_hints_seen;
+        continue;
       }
+      break;
     }
   }
   return uu____2;