Merge pull request #328 from cryspen/dev_vector_restruct

Restructure Vector code in ML-KEM to split functionality
cryspen · Jun 27, 2024 · 2ebae74 · 2ebae74
2 parents 7d40ffc + d3ca0bd
commit 2ebae74
Show file tree

Hide file tree

Showing 61 changed files with 12,574 additions and 4,034 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: 42a431696cd32d41155d7e484720eb71fd5dc7b1
+F*: f09228ef9a64ac4ef383ee0e10656ccb612db2ee
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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #ifndef __internal_libcrux_core_H
@@ -15,12 +15,6 @@ extern "C" {
 #include "../libcrux_core.h"
 #include "eurydice_glue.h"
 
-extern void core_fmt_rt__core__fmt__rt__Argument__a__1__none(
-    core_fmt_rt_Argument *x0);
-
-extern core_fmt_Arguments core_fmt__core__fmt__Arguments__a__2__new_v1(
-    Eurydice_slice x0, Eurydice_slice x1);
-
 #define CORE_NUM__U32_8__BITS (32U)
 
 static inline uint32_t core_num__u8_6__count_ones(uint8_t x0);
@@ -216,11 +210,6 @@ void core_result__core__result__Result_T__E___unwrap__uint8_t_10size_t__core_arr
     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;
-} core_option_Option__Eurydice_slice_uint8_t;
-
 typedef struct
     core_result_Result__int16_t_16size_t__core_array_TryFromSliceError_s {
   core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag;

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H

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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #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_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #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
@@ -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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #include "internal/libcrux_core.h"

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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #ifndef __libcrux_core_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #ifndef __libcrux_mlkem1024_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #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
@@ -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: /home/karthik/eurydice/eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
+  version: 42a43169
  */
 
 #ifndef __libcrux_mlkem1024_avx2_H