pinned versions

cryspen · Sep 24, 2024 · 6758f5c · 6758f5c
1 parent ff16b9e
commit 6758f5c
Show file tree

Hide file tree

Showing 43 changed files with 716 additions and 664 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: b351338f6a84c7a1afc27433eb0ffdc668b3581d
-Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46
-Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0
+Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
+Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
+Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
 F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd
-Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d
+Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127
diff --git a/libcrux-ml-kem/c/eurydice_glue.h b/libcrux-ml-kem/c/eurydice_glue.h
@@ -18,6 +18,13 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 
 #define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e)
+#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.
 
@@ -130,13 +137,18 @@ static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) {
   memcpy(dst, &x, 4);
 }
 
+static inline void core_num__u32_8__to_le_bytes(uint32_t src, uint8_t dst[4]) {
+  store32_le(dst, src);
+}
+
 static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) {
   return load32_le(buf);
 }
 
 static inline void core_num__u64_9__to_le_bytes(uint64_t v, uint8_t buf[8]) {
   store64_le(buf, v);
 }
+
 static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) {
   return load64_le(buf);
 }
@@ -188,6 +200,9 @@ static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) {
 static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
   return (*p) >> v;
 }
+static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) {
+  return x < y ? x : y;
+}
 
 #define core_num_nonzero_private_NonZeroUsizeInner size_t
 static inline core_num_nonzero_private_NonZeroUsizeInner
@@ -210,6 +225,9 @@ core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__N
 #define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next \
   Eurydice_range_iter_next
 
+#define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next \
+  Eurydice_range_iter_next
+
 // See note in karamel/lib/Inlining.ml if you change this
 #define Eurydice_into_iter(x, t, _ret_t) (x)
 #define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter \

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: b351338f6a84c7a1afc27433eb0ffdc668b3581d
- * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46
- * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0
+ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
+ * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
+ * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
  * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd
- * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d
+ * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127
  */
 
 #ifndef __internal_libcrux_core_H
@@ -291,14 +291,15 @@ typedef struct core_result_Result_00_s {
 } core_result_Result_00;
 
 /**
-This function found in impl {core::result::Result<T, E>}
+This function found in impl {core::result::Result<T, E>[TraitClause@0,
+TraitClause@1]}
 */
 /**
-A monomorphic instance of core.result.unwrap_41
+A monomorphic instance of core.result.unwrap_26
 with types uint8_t[32size_t], core_array_TryFromSliceError
 
 */
-void core_result_unwrap_41_33(core_result_Result_00 self, uint8_t ret[32U]);
+void core_result_unwrap_26_33(core_result_Result_00 self, uint8_t ret[32U]);
 
 /**
  Pad the `slice` with `0`s at the end.
@@ -382,14 +383,15 @@ typedef struct core_result_Result_6f_s {
 } core_result_Result_6f;
 
 /**
-This function found in impl {core::result::Result<T, E>}
+This function found in impl {core::result::Result<T, E>[TraitClause@0,
+TraitClause@1]}
 */
 /**
-A monomorphic instance of core.result.unwrap_41
+A monomorphic instance of core.result.unwrap_26
 with types uint8_t[24size_t], core_array_TryFromSliceError
 
 */
-void core_result_unwrap_41_76(core_result_Result_6f self, uint8_t ret[24U]);
+void core_result_unwrap_26_76(core_result_Result_6f self, uint8_t ret[24U]);
 
 /**
 A monomorphic instance of core.result.Result
@@ -405,14 +407,15 @@ typedef struct core_result_Result_7a_s {
 } core_result_Result_7a;
 
 /**
-This function found in impl {core::result::Result<T, E>}
+This function found in impl {core::result::Result<T, E>[TraitClause@0,
+TraitClause@1]}
 */
 /**
-A monomorphic instance of core.result.unwrap_41
+A monomorphic instance of core.result.unwrap_26
 with types uint8_t[20size_t], core_array_TryFromSliceError
 
 */
-void core_result_unwrap_41_ea(core_result_Result_7a self, uint8_t ret[20U]);
+void core_result_unwrap_26_ea(core_result_Result_7a self, uint8_t ret[20U]);
 
 /**
 A monomorphic instance of core.result.Result
@@ -428,14 +431,15 @@ typedef struct core_result_Result_cd_s {
 } core_result_Result_cd;
 
 /**
-This function found in impl {core::result::Result<T, E>}
+This function found in impl {core::result::Result<T, E>[TraitClause@0,
+TraitClause@1]}
 */
 /**
-A monomorphic instance of core.result.unwrap_41
+A monomorphic instance of core.result.unwrap_26
 with types uint8_t[10size_t], core_array_TryFromSliceError
 
 */
-void core_result_unwrap_41_07(core_result_Result_cd self, uint8_t ret[10U]);
+void core_result_unwrap_26_07(core_result_Result_cd self, uint8_t ret[10U]);
 
 /**
 A monomorphic instance of core.result.Result
@@ -451,14 +455,15 @@ typedef struct core_result_Result_c0_s {
 } core_result_Result_c0;
 
 /**
-This function found in impl {core::result::Result<T, E>}
+This function found in impl {core::result::Result<T, E>[TraitClause@0,
+TraitClause@1]}
 */
 /**
-A monomorphic instance of core.result.unwrap_41
+A monomorphic instance of core.result.unwrap_26
 with types int16_t[16size_t], core_array_TryFromSliceError
 
 */
-void core_result_unwrap_41_30(core_result_Result_c0 self, int16_t ret[16U]);
+void core_result_unwrap_26_30(core_result_Result_c0 self, int16_t ret[16U]);
 
 typedef struct Eurydice_slice_uint8_t_4size_t__x2_s {
   Eurydice_slice fst[4U];

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: b351338f6a84c7a1afc27433eb0ffdc668b3581d
- * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46
- * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0
+ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
+ * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
+ * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
  * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd
- * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d
+ * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127
  */
 
 #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: b351338f6a84c7a1afc27433eb0ffdc668b3581d
- * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46
- * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0
+ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
+ * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
+ * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
  * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd
- * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d
+ * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127
  */
 
 #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: b351338f6a84c7a1afc27433eb0ffdc668b3581d
- * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46
- * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0
+ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
+ * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
+ * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
  * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd
- * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d
+ * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H