refresh c code

cryspen · Jan 31, 2025 · d80ca0e · d80ca0e
1 parent 3ef33e0
commit d80ca0e
Show file tree

Hide file tree

Showing 41 changed files with 363 additions and 277 deletions.
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
-Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
-Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
-F*: b0961063393215ca65927f017720cb365a193833-dirty
-Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
diff --git a/libcrux-ml-kem/c/eurydice_glue.h b/libcrux-ml-kem/c/eurydice_glue.h
@@ -213,7 +213,7 @@ core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__N
 
 // ITERATORS
 #define Eurydice_range_iter_next(iter_ptr, t, ret_t) \
-  (((iter_ptr)->start >= (iter_ptr)->end)            \
+  (((iter_ptr)->start == (iter_ptr)->end)            \
        ? (CLITERAL(ret_t){.tag = core_option_None})  \
        : (CLITERAL(ret_t){.tag = core_option_Some,   \
                           .f0 = (iter_ptr)->start++}))

diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __internal_libcrux_core_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __internal_libcrux_sha3_internal_H
@@ -89,27 +89,42 @@ libcrux_sha3_portable_incremental_shake128_squeeze_next_block(
   libcrux_sha3_generic_keccak_squeeze_next_block_c6(s, buf);
 }
 
-#define libcrux_sha3_Algorithm_Sha224 1
-#define libcrux_sha3_Algorithm_Sha256 2
-#define libcrux_sha3_Algorithm_Sha384 3
-#define libcrux_sha3_Algorithm_Sha512 4
+#define libcrux_sha3_Sha224 0
+#define libcrux_sha3_Sha256 1
+#define libcrux_sha3_Sha384 2
+#define libcrux_sha3_Sha512 3
 
 typedef uint8_t libcrux_sha3_Algorithm;
 
 /**
  Returns the output size of a digest.
 */
 static inline size_t libcrux_sha3_digest_size(libcrux_sha3_Algorithm mode) {
-  if (!(mode == libcrux_sha3_Algorithm_Sha224)) {
-    if (mode == libcrux_sha3_Algorithm_Sha256) {
-      return (size_t)32U;
-    } else if (mode == libcrux_sha3_Algorithm_Sha384) {
-      return (size_t)48U;
-    } else {
-      return (size_t)64U;
+  size_t uu____0;
+  switch (mode) {
+    case libcrux_sha3_Sha224: {
+      uu____0 = (size_t)28U;
+      break;
+    }
+    case libcrux_sha3_Sha256: {
+      uu____0 = (size_t)32U;
+      break;
+    }
+    case libcrux_sha3_Sha384: {
+      uu____0 = (size_t)48U;
+      break;
+    }
+    case libcrux_sha3_Sha512: {
+      uu____0 = (size_t)64U;
+      break;
+    }
+    default: {
+      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
+                        __LINE__);
+      KRML_HOST_EXIT(253U);
     }
   }
-  return (size_t)28U;
+  return uu____0;
 }
 
 static const size_t libcrux_sha3_generic_keccak__PI[24U] = {
@@ -1381,43 +1396,63 @@ This function found in impl {(core::convert::From<libcrux_sha3::Algorithm> for
 u32)#1}
 */
 static inline uint32_t libcrux_sha3_from_eb(libcrux_sha3_Algorithm v) {
-  if (!(v == libcrux_sha3_Algorithm_Sha224)) {
-    if (v == libcrux_sha3_Algorithm_Sha256) {
-      return 2U;
-    } else if (v == libcrux_sha3_Algorithm_Sha384) {
-      return 3U;
-    } else {
-      return 4U;
+  uint32_t uu____0;
+  switch (v) {
+    case libcrux_sha3_Sha224: {
+      uu____0 = 1U;
+      break;
+    }
+    case libcrux_sha3_Sha256: {
+      uu____0 = 2U;
+      break;
+    }
+    case libcrux_sha3_Sha384: {
+      uu____0 = 3U;
+      break;
+    }
+    case libcrux_sha3_Sha512: {
+      uu____0 = 4U;
+      break;
+    }
+    default: {
+      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
+                        __LINE__);
+      KRML_HOST_EXIT(253U);
     }
   }
-  return 1U;
+  return uu____0;
 }
 
 /**
 This function found in impl {(core::convert::From<u32> for
 libcrux_sha3::Algorithm)}
 */
 static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
+  libcrux_sha3_Algorithm uu____0;
   switch (v) {
     case 1U: {
+      uu____0 = libcrux_sha3_Sha224;
       break;
     }
     case 2U: {
-      return libcrux_sha3_Algorithm_Sha256;
+      uu____0 = libcrux_sha3_Sha256;
+      break;
     }
     case 3U: {
-      return libcrux_sha3_Algorithm_Sha384;
+      uu____0 = libcrux_sha3_Sha384;
+      break;
     }
     case 4U: {
-      return libcrux_sha3_Algorithm_Sha512;
+      uu____0 = libcrux_sha3_Sha512;
+      break;
     }
     default: {
       KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
                         "panic!");
       KRML_HOST_EXIT(255U);
     }
   }
-  return libcrux_sha3_Algorithm_Sha224;
+  return uu____0;
 }
 
 typedef uint8_t libcrux_sha3_Sha3_512Digest[64U];

diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c
@@ -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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #include "internal/libcrux_core.h"
@@ -279,10 +279,10 @@ with const generics
 */
 uint8_t libcrux_ml_kem_utils_prf_input_inc_e0(uint8_t (*prf_inputs)[33U],
                                               uint8_t domain_separator) {
-  uint8_t _prf_inputs_init[3U][33U];
+  uint8_t ret[3U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)3U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[3U][33U], void *);
+      (size_t)3U, prf_inputs, ret, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(ret, uint8_t[3U][33U], void *);
   KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, size_t i0 = i;
                   prf_inputs[i0][32U] = domain_separator;
                   domain_separator = (uint32_t)domain_separator + 1U;);
@@ -412,10 +412,10 @@ with const generics
 */
 uint8_t libcrux_ml_kem_utils_prf_input_inc_fd(uint8_t (*prf_inputs)[33U],
                                               uint8_t domain_separator) {
-  uint8_t _prf_inputs_init[2U][33U];
+  uint8_t ret[2U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)2U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[2U][33U], void *);
+      (size_t)2U, prf_inputs, ret, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(ret, uint8_t[2U][33U], void *);
   KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, size_t i0 = i;
                   prf_inputs[i0][32U] = domain_separator;
                   domain_separator = (uint32_t)domain_separator + 1U;);
@@ -585,10 +585,10 @@ with const generics
 */
 uint8_t libcrux_ml_kem_utils_prf_input_inc_ac(uint8_t (*prf_inputs)[33U],
                                               uint8_t domain_separator) {
-  uint8_t _prf_inputs_init[4U][33U];
+  uint8_t ret[4U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)4U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[4U][33U], void *);
+      (size_t)4U, prf_inputs, ret, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(ret, uint8_t[4U][33U], void *);
   KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i;
                   prf_inputs[i0][32U] = domain_separator;
                   domain_separator = (uint32_t)domain_separator + 1U;);

diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __libcrux_core_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __libcrux_mlkem1024_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
@@ -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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #include "libcrux_mlkem1024_avx2.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __libcrux_mlkem1024_avx2_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
@@ -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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #include "libcrux_mlkem1024_portable.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.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*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
+ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Karamel: a02d57fc0ae585928e35464e9d806760aeccd5aa
+ * F*: 7cd06c5562fc47ec14cd35c38034d5558a5ff762
+ * Libcrux: 3ef33e0e7acecb3a0e0fec43e44a9e7ac766c01d
  */
 
 #ifndef __libcrux_mlkem1024_portable_H