c code update

cryspen · Jun 26, 2024 · a844017 · a844017
1 parent 4a55be9
commit a844017
Show file tree

Hide file tree

Showing 33 changed files with 13,364 additions and 4,588 deletions.
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -1,5 +1,5 @@
 This code was generated with the following tools:
 Charon: ae55966c01a1a4b185a1a34da7861ba5db74c8ad
 Eurydice: bbfd102bbfbc3e4c362953f093dbfd65e2fbc10c
-Karamel: 409fe4552f8f46351241cba1decfaa4d9fa6ffea
-F*: 
+Karamel: 018dcd1d71f37472c517822aa6bd275263a6dcaa
+F*: 0e2a116da266fbe1dbb81b414002d0afac6819b3
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 409fe455
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice
+  --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: 0e2a116d KaRaMeL version: 018dcd1d
  */
 
 #ifndef __internal_libcrux_core_H
@@ -23,7 +23,7 @@ extern core_fmt_Arguments core_fmt__core__fmt__Arguments__a__2__new_v1(
 
 #define CORE_NUM__U32_8__BITS (32U)
 
-static inline uint32_t core_num__u8_6__count_ones(uint8_t x0);
+static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t x0[4U]);
 
 #define LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE ((size_t)32U)
 
@@ -177,45 +177,6 @@ void libcrux_ml_kem_utils_into_padded_array___800size_t(Eurydice_slice slice,
 void libcrux_ml_kem_utils_into_padded_array___64size_t(Eurydice_slice slice,
                                                        uint8_t ret[64U]);
 
-typedef struct
-    core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_s {
-  core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag;
-  union {
-    uint8_t case_Ok[24U];
-    core_array_TryFromSliceError case_Err;
-  } val;
-} core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError;
-
-void core_result__core__result__Result_T__E___unwrap__uint8_t_24size_t__core_array_TryFromSliceError(
-    core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError self,
-    uint8_t ret[24U]);
-
-typedef struct
-    core_result_Result__uint8_t_20size_t__core_array_TryFromSliceError_s {
-  core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag;
-  union {
-    uint8_t case_Ok[20U];
-    core_array_TryFromSliceError case_Err;
-  } val;
-} core_result_Result__uint8_t_20size_t__core_array_TryFromSliceError;
-
-void core_result__core__result__Result_T__E___unwrap__uint8_t_20size_t__core_array_TryFromSliceError(
-    core_result_Result__uint8_t_20size_t__core_array_TryFromSliceError self,
-    uint8_t ret[20U]);
-
-typedef struct
-    core_result_Result__uint8_t_10size_t__core_array_TryFromSliceError_s {
-  core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag;
-  union {
-    uint8_t case_Ok[10U];
-    core_array_TryFromSliceError case_Err;
-  } val;
-} core_result_Result__uint8_t_10size_t__core_array_TryFromSliceError;
-
-void core_result__core__result__Result_T__E___unwrap__uint8_t_10size_t__core_array_TryFromSliceError(
-    core_result_Result__uint8_t_10size_t__core_array_TryFromSliceError self,
-    uint8_t ret[10U]);
-
 typedef struct core_option_Option__Eurydice_slice_uint8_t_s {
   core_option_Option__size_t_tags tag;
   Eurydice_slice f0;
@@ -235,10 +196,10 @@ void core_result__core__result__Result_T__E___unwrap__int16_t_16size_t__core_arr
     int16_t ret[16U]);
 
 typedef struct
-    K___Eurydice_slice_uint8_t_4size_t__Eurydice_slice_uint8_t_4size_t__s {
-  Eurydice_slice fst[4U];
-  Eurydice_slice snd[4U];
-} K___Eurydice_slice_uint8_t_4size_t__Eurydice_slice_uint8_t_4size_t_;
+    K___Eurydice_slice_uint8_t_2size_t__Eurydice_slice_uint8_t_2size_t__s {
+  Eurydice_slice fst[2U];
+  Eurydice_slice snd[2U];
+} K___Eurydice_slice_uint8_t_2size_t__Eurydice_slice_uint8_t_2size_t_;
 
 #if defined(__cplusplus)
 }

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_neon.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_neon.h
@@ -0,0 +1,74 @@
+/*
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice
+  --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: 0e2a116d KaRaMeL version: 018dcd1d
+ */
+
+#ifndef __internal_libcrux_mlkem_neon_H
+#define __internal_libcrux_mlkem_neon_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include "../libcrux_mlkem_neon.h"
+#include "eurydice_glue.h"
+#include "internal/libcrux_core.h"
+#include "internal/libcrux_mlkem_portable.h"
+
+bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_3size_t_1152size_t_1184size_t(
+    uint8_t *public_key);
+
+libcrux_ml_kem_mlkem768_MlKem768KeyPair
+libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t(
+    uint8_t randomness[64U]);
+
+K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
+libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_libcrux_ml_kem_ind_cca_MlKem_3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t(
+    libcrux_ml_kem_types_MlKemPublicKey____1184size_t *public_key,
+    uint8_t randomness[32U]);
+
+void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_libcrux_ml_kem_ind_cca_MlKem_3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t(
+    libcrux_ml_kem_types_MlKemPrivateKey____2400size_t *private_key,
+    libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]);
+
+bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_4size_t_1536size_t_1568size_t(
+    uint8_t *public_key);
+
+libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
+libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
+    uint8_t randomness[64U]);
+
+K___libcrux_ml_kem_types_MlKemCiphertext___1568size_t___uint8_t_32size_t_
+libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_libcrux_ml_kem_ind_cca_MlKem_4size_t_1568size_t_1568size_t_1536size_t_1408size_t_160size_t_11size_t_5size_t_352size_t_2size_t_128size_t_2size_t_128size_t(
+    libcrux_ml_kem_types_MlKemPublicKey____1568size_t *public_key,
+    uint8_t randomness[32U]);
+
+void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_libcrux_ml_kem_ind_cca_MlKem_4size_t_3168size_t_1536size_t_1568size_t_1568size_t_1536size_t_1408size_t_160size_t_11size_t_5size_t_352size_t_2size_t_128size_t_2size_t_128size_t_1600size_t(
+    libcrux_ml_kem_types_MlKemPrivateKey____3168size_t *private_key,
+    libcrux_ml_kem_mlkem1024_MlKem1024Ciphertext *ciphertext, uint8_t ret[32U]);
+
+bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_2size_t_768size_t_800size_t(
+    uint8_t *public_key);
+
+libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t
+libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_2size_t_768size_t_1632size_t_800size_t_768size_t_3size_t_192size_t(
+    uint8_t randomness[64U]);
+
+K___libcrux_ml_kem_types_MlKemCiphertext___768size_t___uint8_t_32size_t_
+libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_libcrux_ml_kem_ind_cca_MlKem_2size_t_768size_t_800size_t_768size_t_640size_t_128size_t_10size_t_4size_t_320size_t_3size_t_192size_t_2size_t_128size_t(
+    libcrux_ml_kem_types_MlKemPublicKey____800size_t *public_key,
+    uint8_t randomness[32U]);
+
+void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_libcrux_ml_kem_ind_cca_MlKem_2size_t_1632size_t_768size_t_800size_t_768size_t_768size_t_640size_t_128size_t_10size_t_4size_t_320size_t_3size_t_192size_t_2size_t_128size_t_800size_t(
+    libcrux_ml_kem_types_MlKemPrivateKey____1632size_t *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext____768size_t *ciphertext,
+    uint8_t ret[32U]);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_libcrux_mlkem_neon_H_DEFINED
+#endif
diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 409fe455
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice
+  --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: 0e2a116d KaRaMeL version: 018dcd1d
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H
@@ -23,51 +23,51 @@ extern const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U];
   (LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT / \
    LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_ELEMENTS_IN_VECTOR)
 
-bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_portable_PortableVector_4size_t_1536size_t_1568size_t(
+bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_portable_vector_type_PortableVector_4size_t_1536size_t_1568size_t(
     uint8_t *public_key);
 
 libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
-libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___4size_t___4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
+libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___4size_t___4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
     uint8_t randomness[64U]);
 
 K___libcrux_ml_kem_types_MlKemCiphertext___1568size_t___uint8_t_32size_t_
-libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___4size_t___libcrux_ml_kem_ind_cca_MlKem_4size_t_1568size_t_1568size_t_1536size_t_1408size_t_160size_t_11size_t_5size_t_352size_t_2size_t_128size_t_2size_t_128size_t(
+libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___4size_t___libcrux_ml_kem_ind_cca_MlKem_4size_t_1568size_t_1568size_t_1536size_t_1408size_t_160size_t_11size_t_5size_t_352size_t_2size_t_128size_t_2size_t_128size_t(
     libcrux_ml_kem_types_MlKemPublicKey____1568size_t *public_key,
     uint8_t randomness[32U]);
 
-void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___4size_t___libcrux_ml_kem_ind_cca_MlKem_4size_t_3168size_t_1536size_t_1568size_t_1568size_t_1536size_t_1408size_t_160size_t_11size_t_5size_t_352size_t_2size_t_128size_t_2size_t_128size_t_1600size_t(
+void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___4size_t___libcrux_ml_kem_ind_cca_MlKem_4size_t_3168size_t_1536size_t_1568size_t_1568size_t_1536size_t_1408size_t_160size_t_11size_t_5size_t_352size_t_2size_t_128size_t_2size_t_128size_t_1600size_t(
     libcrux_ml_kem_types_MlKemPrivateKey____3168size_t *private_key,
     libcrux_ml_kem_mlkem1024_MlKem1024Ciphertext *ciphertext, uint8_t ret[32U]);
 
-bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_portable_PortableVector_3size_t_1152size_t_1184size_t(
+bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_portable_vector_type_PortableVector_3size_t_1152size_t_1184size_t(
     uint8_t *public_key);
 
 libcrux_ml_kem_mlkem768_MlKem768KeyPair
-libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___3size_t___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t(
+libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___3size_t___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t(
     uint8_t randomness[64U]);
 
 K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
-libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___3size_t___libcrux_ml_kem_ind_cca_MlKem_3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t(
+libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___3size_t___libcrux_ml_kem_ind_cca_MlKem_3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t(
     libcrux_ml_kem_types_MlKemPublicKey____1184size_t *public_key,
     uint8_t randomness[32U]);
 
-void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___3size_t___libcrux_ml_kem_ind_cca_MlKem_3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t(
+void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___3size_t___libcrux_ml_kem_ind_cca_MlKem_3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t(
     libcrux_ml_kem_types_MlKemPrivateKey____2400size_t *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]);
 
-bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_portable_PortableVector_2size_t_768size_t_800size_t(
+bool libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_portable_vector_type_PortableVector_2size_t_768size_t_800size_t(
     uint8_t *public_key);
 
 libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t
-libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___2size_t___2size_t_768size_t_1632size_t_800size_t_768size_t_3size_t_192size_t(
+libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___2size_t___2size_t_768size_t_1632size_t_800size_t_768size_t_3size_t_192size_t(
     uint8_t randomness[64U]);
 
 K___libcrux_ml_kem_types_MlKemCiphertext___768size_t___uint8_t_32size_t_
-libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___2size_t___libcrux_ml_kem_ind_cca_MlKem_2size_t_768size_t_800size_t_768size_t_640size_t_128size_t_10size_t_4size_t_320size_t_3size_t_192size_t_2size_t_128size_t(
+libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___2size_t___libcrux_ml_kem_ind_cca_MlKem_2size_t_768size_t_800size_t_768size_t_640size_t_128size_t_10size_t_4size_t_320size_t_3size_t_192size_t_2size_t_128size_t(
     libcrux_ml_kem_types_MlKemPublicKey____800size_t *public_key,
     uint8_t randomness[32U]);
 
-void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___2size_t___libcrux_ml_kem_ind_cca_MlKem_2size_t_1632size_t_768size_t_800size_t_768size_t_768size_t_640size_t_128size_t_10size_t_4size_t_320size_t_3size_t_192size_t_2size_t_128size_t_800size_t(
+void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_vector_type_PortableVector_libcrux_ml_kem_hash_functions_portable_PortableHash___2size_t___libcrux_ml_kem_ind_cca_MlKem_2size_t_1632size_t_768size_t_800size_t_768size_t_768size_t_640size_t_128size_t_10size_t_4size_t_320size_t_3size_t_192size_t_2size_t_128size_t_800size_t(
     libcrux_ml_kem_types_MlKemPrivateKey____1632size_t *private_key,
     libcrux_ml_kem_types_MlKemCiphertext____768size_t *ciphertext,
     uint8_t ret[32U]);

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 409fe455
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice
+  --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: 0e2a116d KaRaMeL version: 018dcd1d
  */
 
 #ifndef __internal_libcrux_sha3_internal_H

diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 409fe455
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice
+  --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: 0e2a116d KaRaMeL version: 018dcd1d
  */
 
 #include "internal/libcrux_core.h"
@@ -338,48 +338,6 @@ void libcrux_ml_kem_utils_into_padded_array___64size_t(Eurydice_slice slice,
   memcpy(ret, out, (size_t)64U * sizeof(uint8_t));
 }
 
-void core_result__core__result__Result_T__E___unwrap__uint8_t_24size_t__core_array_TryFromSliceError(
-    core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError self,
-    uint8_t ret[24U]) {
-  if (self.tag == core_result_Ok) {
-    uint8_t f0[24U];
-    memcpy(f0, self.val.case_Ok, (size_t)24U * sizeof(uint8_t));
-    memcpy(ret, f0, (size_t)24U * sizeof(uint8_t));
-  } else {
-    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
-                      "unwrap not Ok");
-    KRML_HOST_EXIT(255U);
-  }
-}
-
-void core_result__core__result__Result_T__E___unwrap__uint8_t_20size_t__core_array_TryFromSliceError(
-    core_result_Result__uint8_t_20size_t__core_array_TryFromSliceError self,
-    uint8_t ret[20U]) {
-  if (self.tag == core_result_Ok) {
-    uint8_t f0[20U];
-    memcpy(f0, self.val.case_Ok, (size_t)20U * sizeof(uint8_t));
-    memcpy(ret, f0, (size_t)20U * sizeof(uint8_t));
-  } else {
-    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
-                      "unwrap not Ok");
-    KRML_HOST_EXIT(255U);
-  }
-}
-
-void core_result__core__result__Result_T__E___unwrap__uint8_t_10size_t__core_array_TryFromSliceError(
-    core_result_Result__uint8_t_10size_t__core_array_TryFromSliceError self,
-    uint8_t ret[10U]) {
-  if (self.tag == core_result_Ok) {
-    uint8_t f0[10U];
-    memcpy(f0, self.val.case_Ok, (size_t)10U * sizeof(uint8_t));
-    memcpy(ret, f0, (size_t)10U * sizeof(uint8_t));
-  } else {
-    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
-                      "unwrap not Ok");
-    KRML_HOST_EXIT(255U);
-  }
-}
-
 void core_result__core__result__Result_T__E___unwrap__int16_t_16size_t__core_array_TryFromSliceError(
     core_result_Result__int16_t_16size_t__core_array_TryFromSliceError self,
     int16_t ret[16U]) {

diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 409fe455
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice
+  --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: 0e2a116d KaRaMeL version: 018dcd1d
  */
 
 #ifndef __libcrux_core_H