C update

cryspen · Jun 11, 2024 · ad7b9cb · ad7b9cb
1 parent 496e7bf
commit ad7b9cb
Show file tree

Hide file tree

Showing 34 changed files with 151 additions and 120 deletions.
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -0,0 +1,5 @@
+This code was generated with the following tools:
+Charon: 0b8b7a82c2a18f65ab9df16f222d52594c17f59c
+Eurydice: f5a2305081d09f3b45ed272e5388e542f4c4a7c1
+Karamel: 22425a93c68d9e3794909f98854aaffdc0560510
+F*: 
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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __internal_libcrux_core_H
@@ -44,20 +44,20 @@ void libcrux_ml_kem_constant_time_ops_select_shared_secret_in_constant_time(
 
 #define LIBCRUX_ML_KEM_CONSTANTS_H_DIGEST_SIZE ((size_t)32U)
 
-typedef struct libcrux_ml_kem_utils_Keypair1024_s {
+typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair1024_s {
   uint8_t fst[1536U];
   uint8_t snd[1568U];
-} libcrux_ml_kem_utils_Keypair1024;
+} libcrux_ml_kem_utils_extraction_helper_Keypair1024;
 
-typedef struct libcrux_ml_kem_utils_Keypair512_s {
+typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair512_s {
   uint8_t fst[768U];
   uint8_t snd[800U];
-} libcrux_ml_kem_utils_Keypair512;
+} libcrux_ml_kem_utils_extraction_helper_Keypair512;
 
-typedef struct libcrux_ml_kem_utils_Keypair768_s {
+typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair768_s {
   uint8_t fst[1152U];
   uint8_t snd[1184U];
-} libcrux_ml_kem_utils_Keypair768;
+} libcrux_ml_kem_utils_extraction_helper_Keypair768;
 
 libcrux_ml_kem_types_MlKemPublicKey____1568size_t
 libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1568size_t(

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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #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
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem1024_portable_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem512_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #include "libcrux_mlkem512_avx2.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem512_avx2_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #include "libcrux_mlkem512_portable.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem512_portable_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem768_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #include "libcrux_mlkem768_avx2.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem768_avx2_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #include "libcrux_mlkem768_portable.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #ifndef __libcrux_mlkem768_portable_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
-  version: 6bb7cd3e
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
+  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
+  KaRaMeL version: 22425a93
  */
 
 #include "internal/libcrux_mlkem_avx2.h"
@@ -2612,7 +2612,7 @@ compute_As_plus_e__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-static libcrux_ml_kem_utils_Keypair768
+static libcrux_ml_kem_utils_extraction_helper_Keypair768
 generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t(
     Eurydice_slice key_generation_seed) {
   uint8_t hashed[64U];
@@ -2687,7 +2687,7 @@ generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_f
   memcpy(uu____6, secret_key_serialized, (size_t)1152U * sizeof(uint8_t));
   uint8_t uu____7[1184U];
   memcpy(uu____7, public_key_serialized, (size_t)1184U * sizeof(uint8_t));
-  libcrux_ml_kem_utils_Keypair768 lit;
+  libcrux_ml_kem_utils_extraction_helper_Keypair768 lit;
   memcpy(lit.fst, uu____6, (size_t)1152U * sizeof(uint8_t));
   memcpy(lit.snd, uu____7, (size_t)1184U * sizeof(uint8_t));
   return lit;
@@ -2774,7 +2774,7 @@ libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vecto
       (size_t)64U, randomness,
       LIBCRUX_ML_KEM_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE, uint8_t,
       size_t, Eurydice_slice);
-  libcrux_ml_kem_utils_Keypair768 uu____0 =
+  libcrux_ml_kem_utils_extraction_helper_Keypair768 uu____0 =
       generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t(
           ind_cpa_keypair_randomness);
   uint8_t ind_cpa_private_key[1152U];
@@ -5057,7 +5057,7 @@ compute_As_plus_e__libcrux_ml_kem_vector_avx2_SIMD256Vector_4size_t(
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-static libcrux_ml_kem_utils_Keypair1024
+static libcrux_ml_kem_utils_extraction_helper_Keypair1024
 generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_4size_t_1536size_t_1568size_t_1536size_t_2size_t_128size_t(
     Eurydice_slice key_generation_seed) {
   uint8_t hashed[64U];
@@ -5132,7 +5132,7 @@ generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_f
   memcpy(uu____6, secret_key_serialized, (size_t)1536U * sizeof(uint8_t));
   uint8_t uu____7[1568U];
   memcpy(uu____7, public_key_serialized, (size_t)1568U * sizeof(uint8_t));
-  libcrux_ml_kem_utils_Keypair1024 lit;
+  libcrux_ml_kem_utils_extraction_helper_Keypair1024 lit;
   memcpy(lit.fst, uu____6, (size_t)1536U * sizeof(uint8_t));
   memcpy(lit.snd, uu____7, (size_t)1568U * sizeof(uint8_t));
   return lit;
@@ -5219,7 +5219,7 @@ libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vecto
       (size_t)64U, randomness,
       LIBCRUX_ML_KEM_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE, uint8_t,
       size_t, Eurydice_slice);
-  libcrux_ml_kem_utils_Keypair1024 uu____0 =
+  libcrux_ml_kem_utils_extraction_helper_Keypair1024 uu____0 =
       generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_4size_t_1536size_t_1568size_t_1536size_t_2size_t_128size_t(
           ind_cpa_keypair_randomness);
   uint8_t ind_cpa_private_key[1536U];
@@ -6571,7 +6571,7 @@ compute_As_plus_e__libcrux_ml_kem_vector_avx2_SIMD256Vector_2size_t(
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-static libcrux_ml_kem_utils_Keypair512
+static libcrux_ml_kem_utils_extraction_helper_Keypair512
 generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_2size_t_768size_t_800size_t_768size_t_3size_t_192size_t(
     Eurydice_slice key_generation_seed) {
   uint8_t hashed[64U];
@@ -6646,7 +6646,7 @@ generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_f
   memcpy(uu____6, secret_key_serialized, (size_t)768U * sizeof(uint8_t));
   uint8_t uu____7[800U];
   memcpy(uu____7, public_key_serialized, (size_t)800U * sizeof(uint8_t));
-  libcrux_ml_kem_utils_Keypair512 lit;
+  libcrux_ml_kem_utils_extraction_helper_Keypair512 lit;
   memcpy(lit.fst, uu____6, (size_t)768U * sizeof(uint8_t));
   memcpy(lit.snd, uu____7, (size_t)800U * sizeof(uint8_t));
   return lit;
@@ -6733,7 +6733,7 @@ libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vecto
       (size_t)64U, randomness,
       LIBCRUX_ML_KEM_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE, uint8_t,
       size_t, Eurydice_slice);
-  libcrux_ml_kem_utils_Keypair512 uu____0 =
+  libcrux_ml_kem_utils_extraction_helper_Keypair512 uu____0 =
       generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_2size_t_768size_t_800size_t_768size_t_3size_t_192size_t(
           ind_cpa_keypair_randomness);
   uint8_t ind_cpa_private_key[768U];