Simplify config by relying on the fact that the various variants are now macro-generated into their own modules

libcrux-ml-kem/c.yaml

@@ -171,31 +171,17 @@ files:
 
   - name: libcrux_mlkem512_avx2
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem512, avx2]
-        - [libcrux_ml_kem, ind_cca, instantiations, avx2]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem512, avx2]
-        - [libcrux_ml_kem, ind_cca, instantiations, avx2]
+      - [libcrux_ml_kem, mlkem512, avx2]
 
   - name: libcrux_mlkem512_neon
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem512, neon]
-        - [libcrux_ml_kem, ind_cca, instantiations, neon]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem512, neon]
-        - [libcrux_ml_kem, ind_cca, instantiations, neon]
+      - [libcrux_ml_kem, mlkem512, neon]
 
   - name: libcrux_mlkem512_portable
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem512, portable]
-        - [libcrux_ml_kem, ind_cca, instantiations, portable]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem512, portable]
-        - [libcrux_ml_kem, ind_cca, instantiations, portable]
+      - [libcrux_ml_kem, mlkem512, portable]
 
+  # This one contains common definitions like types, etc.
   - name: libcrux_mlkem512
     api:
       - [libcrux_ml_kem, mlkem512]
@@ -204,31 +190,17 @@ files:
 
   - name: libcrux_mlkem768_avx2
     api:
-      patterns:  
-        - [libcrux_ml_kem, mlkem768, avx2]
-        - [libcrux_ml_kem, ind_cca, instantiations, avx2]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem768, avx2]
-        - [libcrux_ml_kem, ind_cca, instantiations, avx2]
+      - [libcrux_ml_kem, mlkem768, avx2]
 
   - name: libcrux_mlkem768_neon
     api:
-      patterns:  
-        - [libcrux_ml_kem, mlkem768, neon]
-        - [libcrux_ml_kem, ind_cca, instantiations, neon]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem768, neon]
-        - [libcrux_ml_kem, ind_cca, instantiations, neon]
+      - [libcrux_ml_kem, mlkem768, neon]
 
   - name: libcrux_mlkem768_portable
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem768, portable]
-        - [libcrux_ml_kem, ind_cca, instantiations, portable]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem768, portable]
-        - [libcrux_ml_kem, ind_cca, instantiations, portable]
+      - [libcrux_ml_kem, mlkem768, portable]
 
+  # This one contains common definitions like types, etc.
   - name: libcrux_mlkem768
     api:
       - [libcrux_ml_kem, mlkem768]
@@ -237,45 +209,24 @@ files:
 
   - name: libcrux_mlkem1024_avx2
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem1024, avx2]
-        - [libcrux_ml_kem, ind_cca, instantiations, avx2]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem1024, avx2]
-        - [libcrux_ml_kem, ind_cca, instantiations, avx2]
+      - [libcrux_ml_kem, mlkem1024, avx2]
 
   - name: libcrux_mlkem1024_neon
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem1024, neon]
-        - [libcrux_ml_kem, ind_cca, instantiations, neon]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem1024, neon]
-        - [libcrux_ml_kem, ind_cca, instantiations, neon]
+      - [libcrux_ml_kem, mlkem1024, neon]
 
   - name: libcrux_mlkem1024_portable
     api:
-      patterns:
-        - [libcrux_ml_kem, mlkem1024, portable]
-        - [libcrux_ml_kem, ind_cca, instantiations, portable]
-      monomorphizations_of:
-        - [libcrux_ml_kem, mlkem1024, portable]
-        - [libcrux_ml_kem, ind_cca, instantiations, portable]
+      - [libcrux_ml_kem, mlkem1024, portable]
 
+  # This one contains common definitions like types, etc.
   - name: libcrux_mlkem1024
     api:
       - [libcrux_ml_kem, mlkem1024]
 
-  # Multiplexing API.
-
-  - name: libcrux_mlkem_multiplexing
-    api:
-      patterns:
-        - [libcrux_ml_kem, ind_cca, multiplexing]
-    inline_static: true
-
-  # Just a few constants not caught by anything above. Most likely can go into
-  # core or polynomial (TODO: try it).
+  # We let monomorphization insert things at the right place in each one of the
+  # 9 variants above. Helpers that have not been assigned into any of the
+  # individual libcrux_mlkemXXX files end up in a catch-all.
   - name: libcrux_mlkem_common
     private:
       - [libcrux_ml_kem, "*"]

libcrux-ml-kem/c/code_gen.txt

@@ -1,5 +1,5 @@
 This code was generated with the following tools:
-Charon: aeeae1d46704810bf498db552a75dff15aa3abcc
+Charon: 4bc2a90d4dab2efeb7f6db3fb61f850440d1b9e8
 Eurydice: ffeb01ce4cf0646e5cadec836bc042f98b8a16a8
-Karamel: 42a431696cd32d41155d7e484720eb71fd5dc7b1
+Karamel: 285552497829dd57fc019f946dce21c70ab35a0b
 F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty

libcrux-ml-kem/c/internal/libcrux_core.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __internal_libcrux_core_H

libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H

libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H
@@ -39,22 +39,6 @@ void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_vector_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_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_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_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_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_vector_type_PortableVector_2size_t_768size_t_800size_t(
     uint8_t *public_key);
 
@@ -72,6 +56,22 @@ void libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_portable_vector_t
     libcrux_ml_kem_types_MlKemCiphertext____768size_t *ciphertext,
     uint8_t ret[32U]);
 
+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_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_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_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]);
+
 #if defined(__cplusplus)
 }
 #endif

libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H

libcrux-ml-kem/c/internal/libcrux_sha3_internal.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __internal_libcrux_sha3_internal_H
@@ -177,6 +177,37 @@ libcrux_sha3_portable_incremental_shake128_squeeze_first_five_blocks(
       s, buf);
 }
 
+static inline void libcrux_sha3_portable_incremental_shake256_absorb_final(
+    libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
+    Eurydice_slice data0) {
+  Eurydice_slice buf[1U] = {data0};
+  libcrux_sha3_generic_keccak_absorb_final__uint64_t_1size_t_136size_t_31uint8_t(
+      s, buf);
+}
+
+static inline libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t
+libcrux_sha3_portable_incremental_shake256_init(void) {
+  return libcrux_sha3_generic_keccak__libcrux_sha3__generic_keccak__KeccakState_T__N__TraitClause_0__1__new__uint64_t_1size_t();
+}
+
+static inline void
+libcrux_sha3_portable_incremental_shake256_squeeze_first_block(
+    libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
+    Eurydice_slice out0) {
+  Eurydice_slice buf[1U] = {out0};
+  libcrux_sha3_generic_keccak_squeeze_first_block__uint64_t_1size_t_136size_t(
+      s, buf);
+}
+
+static inline void
+libcrux_sha3_portable_incremental_shake256_squeeze_next_block(
+    libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
+    Eurydice_slice out0) {
+  Eurydice_slice buf[1U] = {out0};
+  libcrux_sha3_generic_keccak_squeeze_next_block__uint64_t_1size_t_136size_t(
+      s, buf);
+}
+
 static inline libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t
 libcrux_sha3_portable___core__clone__Clone_for_libcrux_sha3__portable__KeccakState___clone(
     libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *self) {

libcrux-ml-kem/c/libcrux_core.c

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #include "internal/libcrux_core.h"

libcrux-ml-kem/c/libcrux_core.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __libcrux_core_H

libcrux-ml-kem/c/libcrux_mlkem1024.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __libcrux_mlkem1024_H

libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c

@@ -2,47 +2,85 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #include "libcrux_mlkem1024_avx2.h"
 
+#include "internal/libcrux_mlkem_avx2.h"
+
+static void
+decapsulate___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]) {
+  uint8_t ret0[32U];
+  libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_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(
+      private_key, ciphertext, ret0);
+  memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
+}
+
 void libcrux_ml_kem_mlkem1024_avx2_decapsulate(
     libcrux_ml_kem_types_MlKemPrivateKey____3168size_t *private_key,
     libcrux_ml_kem_mlkem1024_MlKem1024Ciphertext *ciphertext,
     uint8_t ret[32U]) {
   uint8_t ret0[32U];
-  libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate___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(
+  decapsulate___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(
       private_key, ciphertext, ret0);
   memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
 }
 
+static K___libcrux_ml_kem_types_MlKemCiphertext___1568size_t___uint8_t_32size_t_
+encapsulate___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]) {
+  libcrux_ml_kem_types_MlKemPublicKey____1568size_t *uu____0 = public_key;
+  uint8_t uu____1[32U];
+  memcpy(uu____1, randomness, (size_t)32U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_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(
+      uu____0, uu____1);
+}
+
 K___libcrux_ml_kem_types_MlKemCiphertext___1568size_t___uint8_t_32size_t_
 libcrux_ml_kem_mlkem1024_avx2_encapsulate(
     libcrux_ml_kem_types_MlKemPublicKey____1568size_t *public_key,
     uint8_t randomness[32U]) {
   libcrux_ml_kem_types_MlKemPublicKey____1568size_t *uu____0 = public_key;
   uint8_t uu____1[32U];
   memcpy(uu____1, randomness, (size_t)32U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate___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(
+  return encapsulate___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(
       uu____0, uu____1);
 }
 
+static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
+generate_keypair___4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
+    uint8_t randomness[64U]) {
+  uint8_t uu____0[64U];
+  memcpy(uu____0, randomness, (size_t)64U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
+      uu____0);
+}
+
 libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
 libcrux_ml_kem_mlkem1024_avx2_generate_key_pair(uint8_t randomness[64U]) {
   uint8_t uu____0[64U];
   memcpy(uu____0, randomness, (size_t)64U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair___4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
+  return generate_keypair___4size_t_1536size_t_3168size_t_1568size_t_1536size_t_2size_t_128size_t(
       uu____0);
 }
 
+static bool validate_public_key___4size_t_1536size_t_1568size_t(
+    uint8_t *public_key) {
+  return libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_avx2_SIMD256Vector_4size_t_1536size_t_1568size_t(
+      public_key);
+}
+
 core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1568size_t__
 libcrux_ml_kem_mlkem1024_avx2_validate_public_key(
     libcrux_ml_kem_types_MlKemPublicKey____1568size_t public_key) {
   core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1568size_t__
       uu____0;
-  if (libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key___4size_t_1536size_t_1568size_t(
-          public_key.value)) {
+  if (validate_public_key___4size_t_1536size_t_1568size_t(public_key.value)) {
     uu____0 = (CLITERAL(
         core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1568size_t__){
         .tag = core_option_Some, .f0 = public_key});

libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h

@@ -2,7 +2,7 @@
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
   -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
-  version: <unknown> KaRaMeL version: 42a43169
+  version: <unknown> KaRaMeL version: 28555249
  */
 
 #ifndef __libcrux_mlkem1024_avx2_H
@@ -14,7 +14,6 @@ extern "C" {
 
 #include "eurydice_glue.h"
 #include "libcrux_core.h"
-#include "libcrux_mlkem512_avx2.h"
 
 void libcrux_ml_kem_mlkem1024_avx2_decapsulate(
     libcrux_ml_kem_types_MlKemPrivateKey____3168size_t *private_key,