diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
index 5ec52d2d..3cf3ee96 100644
--- 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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
 Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
-Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
-F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
-Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
index fe88ed86..e94e5270 100644
--- 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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __internal_libcrux_core_H
diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
index f5ebb270..5e6f4180 100644
--- 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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index 4619403c..bac4be01 100644
--- 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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index a2ad7982..79dc2be8 100644
--- 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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index b40b062f..10465c5b 100644
--- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
+++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __internal_libcrux_sha3_internal_H
diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c
index b0387843..67b4a83a 100644
--- a/libcrux-ml-kem/c/libcrux_core.c
+++ b/libcrux-ml-kem/c/libcrux_core.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "internal/libcrux_core.h"
diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h
index 558ada43..943c8179 100644
--- a/libcrux-ml-kem/c/libcrux_core.h
+++ b/libcrux-ml-kem/c/libcrux_core.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_core_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h
index f9c9eec0..7a8685cf 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem1024_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
index 7ea4e15c..148cc867 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_mlkem1024_avx2.h"
@@ -16,8 +16,31 @@
 #include "internal/libcrux_mlkem_avx2.h"
 
 /**
- Portable decapsulate
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.decapsulate_avx2 with const generics
+- K= 4
+- SECRET_KEY_SIZE= 3168
+- CPA_SECRET_KEY_SIZE= 1536
+- PUBLIC_KEY_SIZE= 1568
+- CIPHERTEXT_SIZE= 1568
+- T_AS_NTT_ENCODED_SIZE= 1536
+- C1_SIZE= 1408
+- C2_SIZE= 160
+- VECTOR_U_COMPRESSION_FACTOR= 11
+- VECTOR_V_COMPRESSION_FACTOR= 5
+- C1_BLOCK_SIZE= 352
+- ETA1= 2
+- ETA1_RANDOMNESS_SIZE= 128
+- ETA2= 2
+- ETA2_RANDOMNESS_SIZE= 128
+- IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1600
 */
+static void decapsulate_avx2_e0(
+    libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext_64 *ciphertext, uint8_t ret[32U]) {
+  libcrux_ml_kem_ind_cca_decapsulate_a10(private_key, ciphertext, ret);
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.instantiations.avx2.decapsulate
 with const generics
@@ -41,7 +64,7 @@ with const generics
 static void decapsulate_e0(libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key,
                            libcrux_ml_kem_types_MlKemCiphertext_64 *ciphertext,
                            uint8_t ret[32U]) {
-  libcrux_ml_kem_ind_cca_decapsulate_a10(private_key, ciphertext, ret);
+  decapsulate_avx2_e0(private_key, ciphertext, ret);
 }
 
 /**
@@ -57,6 +80,33 @@ void libcrux_ml_kem_mlkem1024_avx2_decapsulate(
   decapsulate_e0(private_key, ciphertext, ret);
 }
 
+/**
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.encapsulate_avx2 with const generics
+- K= 4
+- CIPHERTEXT_SIZE= 1568
+- PUBLIC_KEY_SIZE= 1568
+- T_AS_NTT_ENCODED_SIZE= 1536
+- C1_SIZE= 1408
+- C2_SIZE= 160
+- VECTOR_U_COMPRESSION_FACTOR= 11
+- VECTOR_V_COMPRESSION_FACTOR= 5
+- VECTOR_U_BLOCK_LEN= 352
+- ETA1= 2
+- ETA1_RANDOMNESS_SIZE= 128
+- ETA2= 2
+- ETA2_RANDOMNESS_SIZE= 128
+*/
+static tuple_fa encapsulate_avx2_8f(
+    libcrux_ml_kem_types_MlKemPublicKey_64 *public_key,
+    uint8_t randomness[32U]) {
+  libcrux_ml_kem_types_MlKemPublicKey_64 *uu____0 = public_key;
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[32U];
+  memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_encapsulate_700(uu____0, copy_of_randomness);
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.instantiations.avx2.encapsulate
 with const generics
@@ -81,7 +131,7 @@ static tuple_fa encapsulate_8f(
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[32U];
   memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_encapsulate_700(uu____0, copy_of_randomness);
+  return encapsulate_avx2_8f(uu____0, copy_of_randomness);
 }
 
 /**
@@ -104,6 +154,26 @@ tuple_fa libcrux_ml_kem_mlkem1024_avx2_encapsulate(
 /**
  Portable generate key pair.
 */
+/**
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair_avx2 with const
+generics
+- K= 4
+- CPA_PRIVATE_KEY_SIZE= 1536
+- PRIVATE_KEY_SIZE= 3168
+- PUBLIC_KEY_SIZE= 1568
+- BYTES_PER_RING_ELEMENT= 1536
+- ETA1= 2
+- ETA1_RANDOMNESS_SIZE= 128
+*/
+static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair generate_keypair_avx2_c9(
+    uint8_t randomness[64U]) {
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[64U];
+  memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_generate_keypair_d60(copy_of_randomness);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics
@@ -120,7 +190,7 @@ static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair generate_keypair_c9(
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[64U];
   memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_generate_keypair_d60(copy_of_randomness);
+  return generate_keypair_avx2_c9(copy_of_randomness);
 }
 
 /**
@@ -135,8 +205,20 @@ libcrux_ml_kem_mlkem1024_avx2_generate_key_pair(uint8_t randomness[64U]) {
 }
 
 /**
- Portable private key validation
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.validate_private_key_avx2 with const
+generics
+- K= 4
+- SECRET_KEY_SIZE= 3168
+- CIPHERTEXT_SIZE= 1568
 */
+static bool validate_private_key_avx2_6b(
+    libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext_64 *ciphertext) {
+  return libcrux_ml_kem_ind_cca_validate_private_key_b9(private_key,
+                                                        ciphertext);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.validate_private_key with const
@@ -145,11 +227,10 @@ generics
 - SECRET_KEY_SIZE= 3168
 - CIPHERTEXT_SIZE= 1568
 */
-static KRML_MUSTINLINE bool validate_private_key_6b(
+static bool validate_private_key_6b(
     libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key,
     libcrux_ml_kem_types_MlKemCiphertext_64 *ciphertext) {
-  return libcrux_ml_kem_ind_cca_validate_private_key_b9(private_key,
-                                                        ciphertext);
+  return validate_private_key_avx2_6b(private_key, ciphertext);
 }
 
 /**
@@ -164,8 +245,17 @@ bool libcrux_ml_kem_mlkem1024_avx2_validate_private_key(
 }
 
 /**
- Portable public key validation
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.validate_public_key_avx2 with const
+generics
+- K= 4
+- RANKED_BYTES_PER_RING_ELEMENT= 1536
+- PUBLIC_KEY_SIZE= 1568
 */
+static bool validate_public_key_avx2_6b(uint8_t *public_key) {
+  return libcrux_ml_kem_ind_cca_validate_public_key_1e(public_key);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.validate_public_key with const
@@ -174,8 +264,8 @@ generics
 - RANKED_BYTES_PER_RING_ELEMENT= 1536
 - PUBLIC_KEY_SIZE= 1568
 */
-static KRML_MUSTINLINE bool validate_public_key_6b(uint8_t *public_key) {
-  return libcrux_ml_kem_ind_cca_validate_public_key_1e(public_key);
+static bool validate_public_key_6b(uint8_t *public_key) {
+  return validate_public_key_avx2_6b(public_key);
 }
 
 /**
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
index 98e9899b..8af267ce 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index 8c8ddab2..abf29ae2 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_mlkem1024_portable.h"
@@ -38,9 +38,9 @@ libcrux_ml_kem.ind_cca.instantiations.portable.decapsulate with const generics
 - ETA2_RANDOMNESS_SIZE= 128
 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1600
 */
-static void decapsulate_e0(libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key,
-                           libcrux_ml_kem_types_MlKemCiphertext_64 *ciphertext,
-                           uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decapsulate_e0(
+    libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext_64 *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_ind_cca_decapsulate_621(private_key, ciphertext, ret);
 }
 
@@ -74,9 +74,9 @@ libcrux_ml_kem.ind_cca.instantiations.portable.encapsulate with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static tuple_fa encapsulate_8f(
-    libcrux_ml_kem_types_MlKemPublicKey_64 *public_key,
-    uint8_t randomness[32U]) {
+static KRML_MUSTINLINE tuple_fa
+encapsulate_8f(libcrux_ml_kem_types_MlKemPublicKey_64 *public_key,
+               uint8_t randomness[32U]) {
   libcrux_ml_kem_types_MlKemPublicKey_64 *uu____0 = public_key;
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[32U];
@@ -116,8 +116,8 @@ generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair generate_keypair_c9(
-    uint8_t randomness[64U]) {
+static KRML_MUSTINLINE libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
+generate_keypair_c9(uint8_t randomness[64U]) {
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[64U];
   memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
index 9c323c18..0f0340a3 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem1024_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h
index a0ed0868..d829c083 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem512_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
index b9a327fe..886edfd4 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_mlkem512_avx2.h"
@@ -16,8 +16,31 @@
 #include "internal/libcrux_mlkem_avx2.h"
 
 /**
- Portable decapsulate
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.decapsulate_avx2 with const generics
+- K= 2
+- SECRET_KEY_SIZE= 1632
+- CPA_SECRET_KEY_SIZE= 768
+- PUBLIC_KEY_SIZE= 800
+- CIPHERTEXT_SIZE= 768
+- T_AS_NTT_ENCODED_SIZE= 768
+- C1_SIZE= 640
+- C2_SIZE= 128
+- VECTOR_U_COMPRESSION_FACTOR= 10
+- VECTOR_V_COMPRESSION_FACTOR= 4
+- C1_BLOCK_SIZE= 320
+- ETA1= 3
+- ETA1_RANDOMNESS_SIZE= 192
+- ETA2= 2
+- ETA2_RANDOMNESS_SIZE= 128
+- IMPLICIT_REJECTION_HASH_INPUT_SIZE= 800
 */
+static void decapsulate_avx2_69(
+    libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext_1a *ciphertext, uint8_t ret[32U]) {
+  libcrux_ml_kem_ind_cca_decapsulate_a1(private_key, ciphertext, ret);
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.instantiations.avx2.decapsulate
 with const generics
@@ -41,7 +64,7 @@ with const generics
 static void decapsulate_69(libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key,
                            libcrux_ml_kem_types_MlKemCiphertext_1a *ciphertext,
                            uint8_t ret[32U]) {
-  libcrux_ml_kem_ind_cca_decapsulate_a1(private_key, ciphertext, ret);
+  decapsulate_avx2_69(private_key, ciphertext, ret);
 }
 
 /**
@@ -57,6 +80,33 @@ void libcrux_ml_kem_mlkem512_avx2_decapsulate(
   decapsulate_69(private_key, ciphertext, ret);
 }
 
+/**
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.encapsulate_avx2 with const generics
+- K= 2
+- CIPHERTEXT_SIZE= 768
+- PUBLIC_KEY_SIZE= 800
+- T_AS_NTT_ENCODED_SIZE= 768
+- C1_SIZE= 640
+- C2_SIZE= 128
+- VECTOR_U_COMPRESSION_FACTOR= 10
+- VECTOR_V_COMPRESSION_FACTOR= 4
+- VECTOR_U_BLOCK_LEN= 320
+- ETA1= 3
+- ETA1_RANDOMNESS_SIZE= 192
+- ETA2= 2
+- ETA2_RANDOMNESS_SIZE= 128
+*/
+static tuple_41 encapsulate_avx2_35(
+    libcrux_ml_kem_types_MlKemPublicKey_52 *public_key,
+    uint8_t randomness[32U]) {
+  libcrux_ml_kem_types_MlKemPublicKey_52 *uu____0 = public_key;
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[32U];
+  memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_encapsulate_70(uu____0, copy_of_randomness);
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.instantiations.avx2.encapsulate
 with const generics
@@ -81,7 +131,7 @@ static tuple_41 encapsulate_35(
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[32U];
   memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_encapsulate_70(uu____0, copy_of_randomness);
+  return encapsulate_avx2_35(uu____0, copy_of_randomness);
 }
 
 /**
@@ -104,6 +154,26 @@ tuple_41 libcrux_ml_kem_mlkem512_avx2_encapsulate(
 /**
  Portable generate key pair.
 */
+/**
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair_avx2 with const
+generics
+- K= 2
+- CPA_PRIVATE_KEY_SIZE= 768
+- PRIVATE_KEY_SIZE= 1632
+- PUBLIC_KEY_SIZE= 800
+- BYTES_PER_RING_ELEMENT= 768
+- ETA1= 3
+- ETA1_RANDOMNESS_SIZE= 192
+*/
+static libcrux_ml_kem_types_MlKemKeyPair_3e generate_keypair_avx2_a8(
+    uint8_t randomness[64U]) {
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[64U];
+  memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_generate_keypair_d6(copy_of_randomness);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics
@@ -120,7 +190,7 @@ static libcrux_ml_kem_types_MlKemKeyPair_3e generate_keypair_a8(
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[64U];
   memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_generate_keypair_d6(copy_of_randomness);
+  return generate_keypair_avx2_a8(copy_of_randomness);
 }
 
 /**
@@ -135,8 +205,20 @@ libcrux_ml_kem_mlkem512_avx2_generate_key_pair(uint8_t randomness[64U]) {
 }
 
 /**
- Portable private key validation
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.validate_private_key_avx2 with const
+generics
+- K= 2
+- SECRET_KEY_SIZE= 1632
+- CIPHERTEXT_SIZE= 768
 */
+static bool validate_private_key_avx2_1c(
+    libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext_1a *ciphertext) {
+  return libcrux_ml_kem_ind_cca_validate_private_key_ad(private_key,
+                                                        ciphertext);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.validate_private_key with const
@@ -145,11 +227,10 @@ generics
 - SECRET_KEY_SIZE= 1632
 - CIPHERTEXT_SIZE= 768
 */
-static KRML_MUSTINLINE bool validate_private_key_1c(
+static bool validate_private_key_1c(
     libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key,
     libcrux_ml_kem_types_MlKemCiphertext_1a *ciphertext) {
-  return libcrux_ml_kem_ind_cca_validate_private_key_ad(private_key,
-                                                        ciphertext);
+  return validate_private_key_avx2_1c(private_key, ciphertext);
 }
 
 /**
@@ -164,8 +245,17 @@ bool libcrux_ml_kem_mlkem512_avx2_validate_private_key(
 }
 
 /**
- Portable public key validation
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.validate_public_key_avx2 with const
+generics
+- K= 2
+- RANKED_BYTES_PER_RING_ELEMENT= 768
+- PUBLIC_KEY_SIZE= 800
 */
+static bool validate_public_key_avx2_1c(uint8_t *public_key) {
+  return libcrux_ml_kem_ind_cca_validate_public_key_ba(public_key);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.validate_public_key with const
@@ -174,8 +264,8 @@ generics
 - RANKED_BYTES_PER_RING_ELEMENT= 768
 - PUBLIC_KEY_SIZE= 800
 */
-static KRML_MUSTINLINE bool validate_public_key_1c(uint8_t *public_key) {
-  return libcrux_ml_kem_ind_cca_validate_public_key_ba(public_key);
+static bool validate_public_key_1c(uint8_t *public_key) {
+  return validate_public_key_avx2_1c(public_key);
 }
 
 /**
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
index 6b38fb88..e65b2304 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index 298c4f14..b0098dd8 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_mlkem512_portable.h"
@@ -38,9 +38,9 @@ libcrux_ml_kem.ind_cca.instantiations.portable.decapsulate with const generics
 - ETA2_RANDOMNESS_SIZE= 128
 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 800
 */
-static void decapsulate_69(libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key,
-                           libcrux_ml_kem_types_MlKemCiphertext_1a *ciphertext,
-                           uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decapsulate_69(
+    libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key,
+    libcrux_ml_kem_types_MlKemCiphertext_1a *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_ind_cca_decapsulate_620(private_key, ciphertext, ret);
 }
 
@@ -74,9 +74,9 @@ libcrux_ml_kem.ind_cca.instantiations.portable.encapsulate with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static tuple_41 encapsulate_35(
-    libcrux_ml_kem_types_MlKemPublicKey_52 *public_key,
-    uint8_t randomness[32U]) {
+static KRML_MUSTINLINE tuple_41
+encapsulate_35(libcrux_ml_kem_types_MlKemPublicKey_52 *public_key,
+               uint8_t randomness[32U]) {
   libcrux_ml_kem_types_MlKemPublicKey_52 *uu____0 = public_key;
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[32U];
@@ -116,8 +116,8 @@ generics
 - ETA1= 3
 - ETA1_RANDOMNESS_SIZE= 192
 */
-static libcrux_ml_kem_types_MlKemKeyPair_3e generate_keypair_a8(
-    uint8_t randomness[64U]) {
+static KRML_MUSTINLINE libcrux_ml_kem_types_MlKemKeyPair_3e
+generate_keypair_a8(uint8_t randomness[64U]) {
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[64U];
   memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
index 578f9f50..b3ec4caa 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem512_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h
index a2acef3f..8509367c 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem768_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
index 73864720..7db22d1a 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_mlkem768_avx2.h"
@@ -16,8 +16,31 @@
 #include "internal/libcrux_mlkem_avx2.h"
 
 /**
- Portable decapsulate
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.decapsulate_avx2 with const generics
+- K= 3
+- SECRET_KEY_SIZE= 2400
+- CPA_SECRET_KEY_SIZE= 1152
+- PUBLIC_KEY_SIZE= 1184
+- CIPHERTEXT_SIZE= 1088
+- T_AS_NTT_ENCODED_SIZE= 1152
+- C1_SIZE= 960
+- C2_SIZE= 128
+- VECTOR_U_COMPRESSION_FACTOR= 10
+- VECTOR_V_COMPRESSION_FACTOR= 4
+- C1_BLOCK_SIZE= 320
+- ETA1= 2
+- ETA1_RANDOMNESS_SIZE= 128
+- ETA2= 2
+- ETA2_RANDOMNESS_SIZE= 128
+- IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1120
 */
+static void decapsulate_avx2_35(
+    libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key,
+    libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) {
+  libcrux_ml_kem_ind_cca_decapsulate_a11(private_key, ciphertext, ret);
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.instantiations.avx2.decapsulate
 with const generics
@@ -41,7 +64,7 @@ with const generics
 static void decapsulate_35(
     libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) {
-  libcrux_ml_kem_ind_cca_decapsulate_a11(private_key, ciphertext, ret);
+  decapsulate_avx2_35(private_key, ciphertext, ret);
 }
 
 /**
@@ -57,6 +80,33 @@ void libcrux_ml_kem_mlkem768_avx2_decapsulate(
   decapsulate_35(private_key, ciphertext, ret);
 }
 
+/**
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.encapsulate_avx2 with const generics
+- K= 3
+- CIPHERTEXT_SIZE= 1088
+- PUBLIC_KEY_SIZE= 1184
+- T_AS_NTT_ENCODED_SIZE= 1152
+- C1_SIZE= 960
+- C2_SIZE= 128
+- VECTOR_U_COMPRESSION_FACTOR= 10
+- VECTOR_V_COMPRESSION_FACTOR= 4
+- VECTOR_U_BLOCK_LEN= 320
+- ETA1= 2
+- ETA1_RANDOMNESS_SIZE= 128
+- ETA2= 2
+- ETA2_RANDOMNESS_SIZE= 128
+*/
+static tuple_c2 encapsulate_avx2_cd(
+    libcrux_ml_kem_types_MlKemPublicKey_30 *public_key,
+    uint8_t randomness[32U]) {
+  libcrux_ml_kem_types_MlKemPublicKey_30 *uu____0 = public_key;
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[32U];
+  memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_encapsulate_701(uu____0, copy_of_randomness);
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.instantiations.avx2.encapsulate
 with const generics
@@ -81,7 +131,7 @@ static tuple_c2 encapsulate_cd(
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[32U];
   memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_encapsulate_701(uu____0, copy_of_randomness);
+  return encapsulate_avx2_cd(uu____0, copy_of_randomness);
 }
 
 /**
@@ -104,6 +154,26 @@ tuple_c2 libcrux_ml_kem_mlkem768_avx2_encapsulate(
 /**
  Portable generate key pair.
 */
+/**
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair_avx2 with const
+generics
+- K= 3
+- CPA_PRIVATE_KEY_SIZE= 1152
+- PRIVATE_KEY_SIZE= 2400
+- PUBLIC_KEY_SIZE= 1184
+- BYTES_PER_RING_ELEMENT= 1152
+- ETA1= 2
+- ETA1_RANDOMNESS_SIZE= 128
+*/
+static libcrux_ml_kem_mlkem768_MlKem768KeyPair generate_keypair_avx2_c6(
+    uint8_t randomness[64U]) {
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[64U];
+  memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
+  return libcrux_ml_kem_ind_cca_generate_keypair_d61(copy_of_randomness);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics
@@ -120,7 +190,7 @@ static libcrux_ml_kem_mlkem768_MlKem768KeyPair generate_keypair_c6(
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[64U];
   memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
-  return libcrux_ml_kem_ind_cca_generate_keypair_d61(copy_of_randomness);
+  return generate_keypair_avx2_c6(copy_of_randomness);
 }
 
 /**
@@ -135,8 +205,20 @@ libcrux_ml_kem_mlkem768_avx2_generate_key_pair(uint8_t randomness[64U]) {
 }
 
 /**
- Portable private key validation
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.validate_private_key_avx2 with const
+generics
+- K= 3
+- SECRET_KEY_SIZE= 2400
+- CIPHERTEXT_SIZE= 1088
 */
+static bool validate_private_key_avx2_31(
+    libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key,
+    libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext) {
+  return libcrux_ml_kem_ind_cca_validate_private_key_12(private_key,
+                                                        ciphertext);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.validate_private_key with const
@@ -145,11 +227,10 @@ generics
 - SECRET_KEY_SIZE= 2400
 - CIPHERTEXT_SIZE= 1088
 */
-static KRML_MUSTINLINE bool validate_private_key_31(
+static bool validate_private_key_31(
     libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext) {
-  return libcrux_ml_kem_ind_cca_validate_private_key_12(private_key,
-                                                        ciphertext);
+  return validate_private_key_avx2_31(private_key, ciphertext);
 }
 
 /**
@@ -164,8 +245,17 @@ bool libcrux_ml_kem_mlkem768_avx2_validate_private_key(
 }
 
 /**
- Portable public key validation
+A monomorphic instance of
+libcrux_ml_kem.ind_cca.instantiations.avx2.validate_public_key_avx2 with const
+generics
+- K= 3
+- RANKED_BYTES_PER_RING_ELEMENT= 1152
+- PUBLIC_KEY_SIZE= 1184
 */
+static bool validate_public_key_avx2_31(uint8_t *public_key) {
+  return libcrux_ml_kem_ind_cca_validate_public_key_ed(public_key);
+}
+
 /**
 A monomorphic instance of
 libcrux_ml_kem.ind_cca.instantiations.avx2.validate_public_key with const
@@ -174,8 +264,8 @@ generics
 - RANKED_BYTES_PER_RING_ELEMENT= 1152
 - PUBLIC_KEY_SIZE= 1184
 */
-static KRML_MUSTINLINE bool validate_public_key_31(uint8_t *public_key) {
-  return libcrux_ml_kem_ind_cca_validate_public_key_ed(public_key);
+static bool validate_public_key_31(uint8_t *public_key) {
+  return validate_public_key_avx2_31(public_key);
 }
 
 /**
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
index 07713cf5..c16b3e83 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index dbed46f8..53ed576c 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_mlkem768_portable.h"
@@ -38,7 +38,7 @@ libcrux_ml_kem.ind_cca.instantiations.portable.decapsulate with const generics
 - ETA2_RANDOMNESS_SIZE= 128
 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1120
 */
-static void decapsulate_35(
+static KRML_MUSTINLINE void decapsulate_35(
     libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_ind_cca_decapsulate_62(private_key, ciphertext, ret);
@@ -74,9 +74,9 @@ libcrux_ml_kem.ind_cca.instantiations.portable.encapsulate with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static tuple_c2 encapsulate_cd(
-    libcrux_ml_kem_types_MlKemPublicKey_30 *public_key,
-    uint8_t randomness[32U]) {
+static KRML_MUSTINLINE tuple_c2
+encapsulate_cd(libcrux_ml_kem_types_MlKemPublicKey_30 *public_key,
+               uint8_t randomness[32U]) {
   libcrux_ml_kem_types_MlKemPublicKey_30 *uu____0 = public_key;
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[32U];
@@ -116,8 +116,8 @@ generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static libcrux_ml_kem_mlkem768_MlKem768KeyPair generate_keypair_c6(
-    uint8_t randomness[64U]) {
+static KRML_MUSTINLINE libcrux_ml_kem_mlkem768_MlKem768KeyPair
+generate_keypair_c6(uint8_t randomness[64U]) {
   /* Passing arrays by value in Rust generates a copy in C */
   uint8_t copy_of_randomness[64U];
   memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t));
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
index df6ee6d4..fc5fdec2 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #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
index ded68248..ea4ebb6a 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "internal/libcrux_mlkem_avx2.h"
@@ -41,7 +41,7 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_zero(void) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_ZERO_ea(void) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ZERO_ea(void) {
   return libcrux_ml_kem_vector_avx2_zero();
 }
 
@@ -54,7 +54,8 @@ libcrux_ml_kem_vector_avx2_from_i16_array(Eurydice_slice array) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_from_i16_array_ea(Eurydice_slice array) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_from_i16_array_ea(Eurydice_slice array) {
   return libcrux_ml_kem_vector_avx2_from_i16_array(array);
 }
 
@@ -70,7 +71,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_to_i16_array(__m256i v,
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_to_i16_array_ea(__m256i x, int16_t ret[16U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_to_i16_array_ea(
+    __m256i x, int16_t ret[16U]) {
   libcrux_ml_kem_vector_avx2_to_i16_array(x, ret);
 }
 
@@ -83,7 +85,8 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_arithmetic_add(__m256i lhs,
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_add_ea(__m256i lhs, __m256i *rhs) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_add_ea(__m256i lhs,
+                                                          __m256i *rhs) {
   return libcrux_ml_kem_vector_avx2_arithmetic_add(lhs, rhs[0U]);
 }
 
@@ -96,7 +99,8 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_arithmetic_sub(__m256i lhs,
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_sub_ea(__m256i lhs, __m256i *rhs) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_sub_ea(__m256i lhs,
+                                                          __m256i *rhs) {
   return libcrux_ml_kem_vector_avx2_arithmetic_sub(lhs, rhs[0U]);
 }
 
@@ -110,8 +114,8 @@ libcrux_ml_kem_vector_avx2_arithmetic_multiply_by_constant(__m256i vector,
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_multiply_by_constant_ea(__m256i v,
-                                                           int16_t c) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_multiply_by_constant_ea(__m256i v, int16_t c) {
   return libcrux_ml_kem_vector_avx2_arithmetic_multiply_by_constant(v, c);
 }
 
@@ -125,7 +129,7 @@ libcrux_ml_kem_vector_avx2_arithmetic_bitwise_and_with_constant(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_bitwise_and_with_constant_ea(
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_bitwise_and_with_constant_ea(
     __m256i vector, int16_t constant) {
   return libcrux_ml_kem_vector_avx2_arithmetic_bitwise_and_with_constant(
       vector, constant);
@@ -152,7 +156,8 @@ libcrux_ml_kem_vector_avx2_arithmetic_cond_subtract_3329(__m256i vector) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_cond_subtract_3329_ea(__m256i vector) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_cond_subtract_3329_ea(__m256i vector) {
   return libcrux_ml_kem_vector_avx2_arithmetic_cond_subtract_3329(vector);
 }
 
@@ -176,7 +181,8 @@ libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(__m256i vector) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_barrett_reduce_ea(__m256i vector) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_barrett_reduce_ea(__m256i vector) {
   return libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(vector);
 }
 
@@ -200,7 +206,8 @@ libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constant(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_ea(
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_ea(
     __m256i vector, int16_t constant) {
   return libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constant(
       vector, constant);
@@ -225,7 +232,8 @@ libcrux_ml_kem_vector_avx2_compress_compress_message_coefficient(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_compress_1_ea(__m256i vector) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_compress_1_ea(__m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_compress_message_coefficient(
       vector);
 }
@@ -273,11 +281,9 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_ntt_layer_1_step(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_ntt_layer_1_step_ea(__m256i vector,
-                                                       int16_t zeta0,
-                                                       int16_t zeta1,
-                                                       int16_t zeta2,
-                                                       int16_t zeta3) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_layer_1_step_ea(
+    __m256i vector, int16_t zeta0, int16_t zeta1, int16_t zeta2,
+    int16_t zeta3) {
   return libcrux_ml_kem_vector_avx2_ntt_ntt_layer_1_step(vector, zeta0, zeta1,
                                                          zeta2, zeta3);
 }
@@ -299,9 +305,8 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_ntt_layer_2_step(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_ntt_layer_2_step_ea(__m256i vector,
-                                                       int16_t zeta0,
-                                                       int16_t zeta1) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_layer_2_step_ea(
+    __m256i vector, int16_t zeta0, int16_t zeta1) {
   return libcrux_ml_kem_vector_avx2_ntt_ntt_layer_2_step(vector, zeta0, zeta1);
 }
 
@@ -338,8 +343,8 @@ libcrux_ml_kem_vector_avx2_ntt_ntt_layer_3_step(__m256i vector, int16_t zeta) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_ntt_layer_3_step_ea(__m256i vector,
-                                                       int16_t zeta) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_ntt_layer_3_step_ea(__m256i vector, int16_t zeta) {
   return libcrux_ml_kem_vector_avx2_ntt_ntt_layer_3_step(vector, zeta);
 }
 
@@ -368,11 +373,9 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_1_step(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_inv_ntt_layer_1_step_ea(__m256i vector,
-                                                           int16_t zeta0,
-                                                           int16_t zeta1,
-                                                           int16_t zeta2,
-                                                           int16_t zeta3) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_inv_ntt_layer_1_step_ea(
+    __m256i vector, int16_t zeta0, int16_t zeta1, int16_t zeta2,
+    int16_t zeta3) {
   return libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_1_step(
       vector, zeta0, zeta1, zeta2, zeta3);
 }
@@ -400,9 +403,8 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_2_step(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_inv_ntt_layer_2_step_ea(__m256i vector,
-                                                           int16_t zeta0,
-                                                           int16_t zeta1) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_inv_ntt_layer_2_step_ea(
+    __m256i vector, int16_t zeta0, int16_t zeta1) {
   return libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_2_step(vector, zeta0,
                                                              zeta1);
 }
@@ -425,8 +427,8 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_3_step(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_inv_ntt_layer_3_step_ea(__m256i vector,
-                                                           int16_t zeta) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_inv_ntt_layer_3_step_ea(
+    __m256i vector, int16_t zeta) {
   return libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_3_step(vector, zeta);
 }
 
@@ -511,10 +513,9 @@ KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_ntt_multiply(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_ntt_multiply_ea(__m256i *lhs, __m256i *rhs,
-                                                   int16_t zeta0, int16_t zeta1,
-                                                   int16_t zeta2,
-                                                   int16_t zeta3) {
+KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_ntt_multiply_ea(
+    __m256i *lhs, __m256i *rhs, int16_t zeta0, int16_t zeta1, int16_t zeta2,
+    int16_t zeta3) {
   return libcrux_ml_kem_vector_avx2_ntt_ntt_multiply(lhs[0U], rhs[0U], zeta0,
                                                      zeta1, zeta2, zeta3);
 }
@@ -569,8 +570,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_1(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_serialize_1_ea(__m256i vector,
-                                               uint8_t ret[2U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_1_ea(
+    __m256i vector, uint8_t ret[2U]) {
   libcrux_ml_kem_vector_avx2_serialize_serialize_1(vector, ret);
 }
 
@@ -623,7 +624,8 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_deserialize_1_ea(Eurydice_slice bytes) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_deserialize_1_ea(Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_1(bytes);
 }
 
@@ -692,8 +694,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_4(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_serialize_4_ea(__m256i vector,
-                                               uint8_t ret[8U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_4_ea(
+    __m256i vector, uint8_t ret[8U]) {
   libcrux_ml_kem_vector_avx2_serialize_serialize_4(vector, ret);
 }
 
@@ -751,7 +753,8 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_deserialize_4_ea(Eurydice_slice bytes) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_deserialize_4_ea(Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_4(bytes);
 }
 
@@ -847,8 +850,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_5(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_serialize_5_ea(__m256i vector,
-                                               uint8_t ret[10U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_5_ea(
+    __m256i vector, uint8_t ret[10U]) {
   libcrux_ml_kem_vector_avx2_serialize_serialize_5(vector, ret);
 }
 
@@ -898,7 +901,8 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_deserialize_5_ea(Eurydice_slice bytes) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_deserialize_5_ea(Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_5(bytes);
 }
 
@@ -994,8 +998,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_serialize_10_ea(__m256i vector,
-                                                uint8_t ret[20U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_10_ea(
+    __m256i vector, uint8_t ret[20U]) {
   libcrux_ml_kem_vector_avx2_serialize_serialize_10(vector, ret);
 }
 
@@ -1029,7 +1033,8 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_deserialize_10_ea(Eurydice_slice bytes) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_deserialize_10_ea(Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_10(bytes);
 }
 
@@ -1050,8 +1055,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_11(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_serialize_11_ea(__m256i vector,
-                                                uint8_t ret[22U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_11_ea(
+    __m256i vector, uint8_t ret[22U]) {
   libcrux_ml_kem_vector_avx2_serialize_serialize_11(vector, ret);
 }
 
@@ -1069,7 +1074,8 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_11(Eurydice_slice bytes) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_deserialize_11_ea(Eurydice_slice bytes) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_deserialize_11_ea(Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_11(bytes);
 }
 
@@ -1121,8 +1127,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-void libcrux_ml_kem_vector_avx2_serialize_12_ea(__m256i vector,
-                                                uint8_t ret[24U]) {
+KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_12_ea(
+    __m256i vector, uint8_t ret[24U]) {
   libcrux_ml_kem_vector_avx2_serialize_serialize_12(vector, ret);
 }
 
@@ -1156,7 +1162,8 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_12(Eurydice_slice bytes) {
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-__m256i libcrux_ml_kem_vector_avx2_deserialize_12_ea(Eurydice_slice bytes) {
+KRML_MUSTINLINE __m256i
+libcrux_ml_kem_vector_avx2_deserialize_12_ea(Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_12(bytes);
 }
 
@@ -1243,8 +1250,8 @@ KRML_MUSTINLINE size_t libcrux_ml_kem_vector_avx2_sampling_rejection_sample(
 This function found in impl {(libcrux_ml_kem::vector::traits::Operations for
 libcrux_ml_kem::vector::avx2::SIMD256Vector)}
 */
-size_t libcrux_ml_kem_vector_avx2_rej_sample_ea(Eurydice_slice input,
-                                                Eurydice_slice output) {
+KRML_MUSTINLINE size_t libcrux_ml_kem_vector_avx2_rej_sample_ea(
+    Eurydice_slice input, Eurydice_slice output) {
   return libcrux_ml_kem_vector_avx2_sampling_rejection_sample(input, output);
 }
 
@@ -1387,7 +1394,7 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.shift_right_ea
 with const generics
 - SHIFT_BY= 15
 */
-static __m256i shift_right_ea_ef(__m256i vector) {
+static KRML_MUSTINLINE __m256i shift_right_ea_ef(__m256i vector) {
   return shift_right_ef(vector);
 }
 
@@ -1397,7 +1404,7 @@ libcrux_ml_kem.vector.traits.to_unsigned_representative with types
 libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
 
 */
-static __m256i to_unsigned_representative_79(__m256i a) {
+static KRML_MUSTINLINE __m256i to_unsigned_representative_79(__m256i a) {
   __m256i t = shift_right_ea_ef(a);
   __m256i fm = libcrux_ml_kem_vector_avx2_bitwise_and_with_constant_ea(
       t, LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS);
@@ -2344,7 +2351,8 @@ with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 
 */
-static __m256i montgomery_multiply_fe_79(__m256i v, int16_t fer) {
+static KRML_MUSTINLINE __m256i montgomery_multiply_fe_79(__m256i v,
+                                                         int16_t fer) {
   return libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_ea(v, fer);
 }
 
@@ -2678,7 +2686,7 @@ with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 
 */
-static __m256i to_standard_domain_79(__m256i v) {
+static KRML_MUSTINLINE __m256i to_standard_domain_79(__m256i v) {
   return libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_ea(
       v, LIBCRUX_ML_KEM_VECTOR_TRAITS_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS);
 }
@@ -2810,7 +2818,7 @@ with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static void generate_keypair_unpacked_221(
+static KRML_MUSTINLINE void generate_keypair_unpacked_221(
     Eurydice_slice key_generation_seed,
     IndCpaPrivateKeyUnpacked_63 *private_key,
     IndCpaPublicKeyUnpacked_63 *public_key) {
@@ -2869,8 +2877,8 @@ with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static libcrux_ml_kem_utils_extraction_helper_Keypair768 generate_keypair_bb1(
-    Eurydice_slice key_generation_seed) {
+static KRML_MUSTINLINE libcrux_ml_kem_utils_extraction_helper_Keypair768
+generate_keypair_bb1(Eurydice_slice key_generation_seed) {
   IndCpaPrivateKeyUnpacked_63 private_key = default_1a_ab();
   IndCpaPublicKeyUnpacked_63 public_key = default_8d_ab();
   generate_keypair_unpacked_221(key_generation_seed, &private_key, &public_key);
@@ -3348,7 +3356,7 @@ with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 
 */
-static __m256i decompress_1_79(__m256i v) {
+static KRML_MUSTINLINE __m256i decompress_1_79(__m256i v) {
   return libcrux_ml_kem_vector_avx2_bitwise_and_with_constant_ea(
       libcrux_ml_kem_vector_avx2_sub_ea(libcrux_ml_kem_vector_avx2_ZERO_ea(),
                                         &v),
@@ -3532,7 +3540,7 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_ea
 with const generics
 - COEFFICIENT_BITS= 10
 */
-static __m256i compress_ea_ef(__m256i vector) {
+static KRML_MUSTINLINE __m256i compress_ea_ef(__m256i vector) {
   return compress_ciphertext_coefficient_ef(vector);
 }
 
@@ -3642,7 +3650,7 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_ea
 with const generics
 - COEFFICIENT_BITS= 11
 */
-static __m256i compress_ea_c4(__m256i vector) {
+static KRML_MUSTINLINE __m256i compress_ea_c4(__m256i vector) {
   return compress_ciphertext_coefficient_c4(vector);
 }
 
@@ -3672,7 +3680,7 @@ with const generics
 - COMPRESSION_FACTOR= 10
 - BLOCK_LEN= 320
 */
-static void compress_then_serialize_u_8c(
+static KRML_MUSTINLINE void compress_then_serialize_u_8c(
     libcrux_ml_kem_polynomial_PolynomialRingElement_f6 input[3U],
     Eurydice_slice out) {
   for (size_t i = (size_t)0U;
@@ -3782,7 +3790,7 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_ea
 with const generics
 - COEFFICIENT_BITS= 4
 */
-static __m256i compress_ea_d1(__m256i vector) {
+static KRML_MUSTINLINE __m256i compress_ea_d1(__m256i vector) {
   return compress_ciphertext_coefficient_d1(vector);
 }
 
@@ -3895,7 +3903,7 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_ea
 with const generics
 - COEFFICIENT_BITS= 5
 */
-static __m256i compress_ea_f4(__m256i vector) {
+static KRML_MUSTINLINE __m256i compress_ea_f4(__m256i vector) {
   return compress_ciphertext_coefficient_f4(vector);
 }
 
@@ -3996,10 +4004,9 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_unpacked_741(IndCpaPublicKeyUnpacked_63 *public_key,
-                                 uint8_t message[32U],
-                                 Eurydice_slice randomness,
-                                 uint8_t ret[1088U]) {
+static KRML_MUSTINLINE void encrypt_unpacked_741(
+    IndCpaPublicKeyUnpacked_63 *public_key, uint8_t message[32U],
+    Eurydice_slice randomness, uint8_t ret[1088U]) {
   uint8_t prf_input[33U];
   libcrux_ml_kem_utils_into_padded_array_c8(/* for i from 0 to k−1 do r[i] :=
                                                CBD{η1}(PRF(r, N)) N := N + 1 end
@@ -4079,8 +4086,10 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_741(Eurydice_slice public_key, uint8_t message[32U],
-                        Eurydice_slice randomness, uint8_t ret[1088U]) {
+static KRML_MUSTINLINE void encrypt_741(Eurydice_slice public_key,
+                                        uint8_t message[32U],
+                                        Eurydice_slice randomness,
+                                        uint8_t ret[1088U]) {
   IndCpaPublicKeyUnpacked_63 unpacked_public_key = default_8d_ab();
   deserialize_ring_elements_reduced_98(
       Eurydice_slice_subslice_to(/* tˆ := Decode_12(pk) */
@@ -4320,7 +4329,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_ea with const
 generics
 - COEFFICIENT_BITS= 10
 */
-static __m256i decompress_ciphertext_coefficient_ea_ef(__m256i vector) {
+static KRML_MUSTINLINE __m256i
+decompress_ciphertext_coefficient_ea_ef(__m256i vector) {
   return decompress_ciphertext_coefficient_ef(vector);
 }
 
@@ -4415,7 +4425,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_ea with const
 generics
 - COEFFICIENT_BITS= 11
 */
-static __m256i decompress_ciphertext_coefficient_ea_c4(__m256i vector) {
+static KRML_MUSTINLINE __m256i
+decompress_ciphertext_coefficient_ea_c4(__m256i vector) {
   return decompress_ciphertext_coefficient_c4(vector);
 }
 
@@ -4583,7 +4594,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_ea with const
 generics
 - COEFFICIENT_BITS= 4
 */
-static __m256i decompress_ciphertext_coefficient_ea_d1(__m256i vector) {
+static KRML_MUSTINLINE __m256i
+decompress_ciphertext_coefficient_ea_d1(__m256i vector) {
   return decompress_ciphertext_coefficient_d1(vector);
 }
 
@@ -4678,7 +4690,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_ea with const
 generics
 - COEFFICIENT_BITS= 5
 */
-static __m256i decompress_ciphertext_coefficient_ea_f4(__m256i vector) {
+static KRML_MUSTINLINE __m256i
+decompress_ciphertext_coefficient_ea_f4(__m256i vector) {
   return decompress_ciphertext_coefficient_f4(vector);
 }
 
@@ -4826,8 +4839,9 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_unpacked_2f(IndCpaPrivateKeyUnpacked_63 *secret_key,
-                                uint8_t *ciphertext, uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_unpacked_2f(
+    IndCpaPrivateKeyUnpacked_63 *secret_key, uint8_t *ciphertext,
+    uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 u_as_ntt[3U];
   deserialize_then_decompress_u_ed(
       /* u := Decompress_q(Decode_{d_u}(c), d_u) */ ciphertext, u_as_ntt);
@@ -4854,8 +4868,8 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_2f(Eurydice_slice secret_key, uint8_t *ciphertext,
-                       uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_2f(Eurydice_slice secret_key,
+                                       uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 secret_as_ntt[3U];
   deserialize_secret_key_ab(/* sˆ := Decode_12(sk) */ secret_key,
                             secret_as_ntt);
@@ -5975,7 +5989,7 @@ with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static void generate_keypair_unpacked_22(
+static KRML_MUSTINLINE void generate_keypair_unpacked_22(
     Eurydice_slice key_generation_seed,
     IndCpaPrivateKeyUnpacked_39 *private_key,
     IndCpaPublicKeyUnpacked_39 *public_key) {
@@ -6034,8 +6048,8 @@ with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static libcrux_ml_kem_utils_extraction_helper_Keypair1024 generate_keypair_bb0(
-    Eurydice_slice key_generation_seed) {
+static KRML_MUSTINLINE libcrux_ml_kem_utils_extraction_helper_Keypair1024
+generate_keypair_bb0(Eurydice_slice key_generation_seed) {
   IndCpaPrivateKeyUnpacked_39 private_key = default_1a_42();
   IndCpaPublicKeyUnpacked_39 public_key = default_8d_42();
   generate_keypair_unpacked_22(key_generation_seed, &private_key, &public_key);
@@ -6425,7 +6439,7 @@ with const generics
 - COMPRESSION_FACTOR= 11
 - BLOCK_LEN= 352
 */
-static void compress_then_serialize_u_c9(
+static KRML_MUSTINLINE void compress_then_serialize_u_c9(
     libcrux_ml_kem_polynomial_PolynomialRingElement_f6 input[4U],
     Eurydice_slice out) {
   for (size_t i = (size_t)0U;
@@ -6523,9 +6537,9 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_unpacked_74(IndCpaPublicKeyUnpacked_39 *public_key,
-                                uint8_t message[32U], Eurydice_slice randomness,
-                                uint8_t ret[1568U]) {
+static KRML_MUSTINLINE void encrypt_unpacked_74(
+    IndCpaPublicKeyUnpacked_39 *public_key, uint8_t message[32U],
+    Eurydice_slice randomness, uint8_t ret[1568U]) {
   uint8_t prf_input[33U];
   libcrux_ml_kem_utils_into_padded_array_c8(/* for i from 0 to k−1 do r[i] :=
                                                CBD{η1}(PRF(r, N)) N := N + 1 end
@@ -6605,8 +6619,10 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_740(Eurydice_slice public_key, uint8_t message[32U],
-                        Eurydice_slice randomness, uint8_t ret[1568U]) {
+static KRML_MUSTINLINE void encrypt_740(Eurydice_slice public_key,
+                                        uint8_t message[32U],
+                                        Eurydice_slice randomness,
+                                        uint8_t ret[1568U]) {
   IndCpaPublicKeyUnpacked_39 unpacked_public_key = default_8d_42();
   deserialize_ring_elements_reduced_3c(
       Eurydice_slice_subslice_to(/* tˆ := Decode_12(pk) */
@@ -6901,8 +6917,9 @@ with const generics
 - U_COMPRESSION_FACTOR= 11
 - V_COMPRESSION_FACTOR= 5
 */
-static void decrypt_unpacked_37(IndCpaPrivateKeyUnpacked_39 *secret_key,
-                                uint8_t *ciphertext, uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_unpacked_37(
+    IndCpaPrivateKeyUnpacked_39 *secret_key, uint8_t *ciphertext,
+    uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 u_as_ntt[4U];
   deserialize_then_decompress_u_1e(
       /* u := Decompress_q(Decode_{d_u}(c), d_u) */ ciphertext, u_as_ntt);
@@ -6929,8 +6946,8 @@ with const generics
 - U_COMPRESSION_FACTOR= 11
 - V_COMPRESSION_FACTOR= 5
 */
-static void decrypt_37(Eurydice_slice secret_key, uint8_t *ciphertext,
-                       uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_37(Eurydice_slice secret_key,
+                                       uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 secret_as_ntt[4U];
   deserialize_secret_key_42(/* sˆ := Decode_12(sk) */ secret_key,
                             secret_as_ntt);
@@ -8017,7 +8034,7 @@ with const generics
 - ETA1= 3
 - ETA1_RANDOMNESS_SIZE= 192
 */
-static void generate_keypair_unpacked_220(
+static KRML_MUSTINLINE void generate_keypair_unpacked_220(
     Eurydice_slice key_generation_seed,
     IndCpaPrivateKeyUnpacked_94 *private_key,
     IndCpaPublicKeyUnpacked_94 *public_key) {
@@ -8076,8 +8093,8 @@ with const generics
 - ETA1= 3
 - ETA1_RANDOMNESS_SIZE= 192
 */
-static libcrux_ml_kem_utils_extraction_helper_Keypair512 generate_keypair_bb(
-    Eurydice_slice key_generation_seed) {
+static KRML_MUSTINLINE libcrux_ml_kem_utils_extraction_helper_Keypair512
+generate_keypair_bb(Eurydice_slice key_generation_seed) {
   IndCpaPrivateKeyUnpacked_94 private_key = default_1a_89();
   IndCpaPublicKeyUnpacked_94 public_key = default_8d_89();
   generate_keypair_unpacked_220(key_generation_seed, &private_key, &public_key);
@@ -8475,7 +8492,7 @@ with const generics
 - COMPRESSION_FACTOR= 10
 - BLOCK_LEN= 320
 */
-static void compress_then_serialize_u_2d(
+static KRML_MUSTINLINE void compress_then_serialize_u_2d(
     libcrux_ml_kem_polynomial_PolynomialRingElement_f6 input[2U],
     Eurydice_slice out) {
   for (size_t i = (size_t)0U;
@@ -8561,9 +8578,9 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_unpacked_740(IndCpaPublicKeyUnpacked_94 *public_key,
-                                 uint8_t message[32U],
-                                 Eurydice_slice randomness, uint8_t ret[768U]) {
+static KRML_MUSTINLINE void encrypt_unpacked_740(
+    IndCpaPublicKeyUnpacked_94 *public_key, uint8_t message[32U],
+    Eurydice_slice randomness, uint8_t ret[768U]) {
   uint8_t prf_input[33U];
   libcrux_ml_kem_utils_into_padded_array_c8(/* for i from 0 to k−1 do r[i] :=
                                                CBD{η1}(PRF(r, N)) N := N + 1 end
@@ -8643,8 +8660,10 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_74(Eurydice_slice public_key, uint8_t message[32U],
-                       Eurydice_slice randomness, uint8_t ret[768U]) {
+static KRML_MUSTINLINE void encrypt_74(Eurydice_slice public_key,
+                                       uint8_t message[32U],
+                                       Eurydice_slice randomness,
+                                       uint8_t ret[768U]) {
   IndCpaPublicKeyUnpacked_94 unpacked_public_key = default_8d_89();
   deserialize_ring_elements_reduced_09(
       Eurydice_slice_subslice_to(/* tˆ := Decode_12(pk) */
@@ -8898,8 +8917,9 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_unpacked_4b(IndCpaPrivateKeyUnpacked_94 *secret_key,
-                                uint8_t *ciphertext, uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_unpacked_4b(
+    IndCpaPrivateKeyUnpacked_94 *secret_key, uint8_t *ciphertext,
+    uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 u_as_ntt[2U];
   deserialize_then_decompress_u_ba(
       /* u := Decompress_q(Decode_{d_u}(c), d_u) */ ciphertext, u_as_ntt);
@@ -8926,8 +8946,8 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_4b(Eurydice_slice secret_key, uint8_t *ciphertext,
-                       uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_4b(Eurydice_slice secret_key,
+                                       uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 secret_as_ntt[2U];
   deserialize_secret_key_89(/* sˆ := Decode_12(sk) */ secret_key,
                             secret_as_ntt);
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
index e2801fb3..8adb2224 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
+++ b/libcrux-ml-kem/c/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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.c b/libcrux-ml-kem/c/libcrux_mlkem_portable.c
index 97d4af08..ff63cfb8 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "internal/libcrux_mlkem_portable.h"
@@ -2427,7 +2427,7 @@ libcrux_ml_kem.vector.traits.to_unsigned_representative with types
 libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics
 
 */
-static libcrux_ml_kem_vector_portable_vector_type_PortableVector
+static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector
 to_unsigned_representative_8c(
     libcrux_ml_kem_vector_portable_vector_type_PortableVector a) {
   libcrux_ml_kem_vector_portable_vector_type_PortableVector t =
@@ -3371,7 +3371,7 @@ with types libcrux_ml_kem_vector_portable_vector_type_PortableVector
 with const generics
 
 */
-static libcrux_ml_kem_vector_portable_vector_type_PortableVector
+static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector
 montgomery_multiply_fe_8c(
     libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t fer) {
   return libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_0d(v,
@@ -3727,7 +3727,7 @@ with types libcrux_ml_kem_vector_portable_vector_type_PortableVector
 with const generics
 
 */
-static libcrux_ml_kem_vector_portable_vector_type_PortableVector
+static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector
 to_standard_domain_8c(
     libcrux_ml_kem_vector_portable_vector_type_PortableVector v) {
   return libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_0d(
@@ -3864,7 +3864,7 @@ libcrux_ml_kem_variant_MlKem with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static void generate_keypair_unpacked_1c(
+static KRML_MUSTINLINE void generate_keypair_unpacked_1c(
     Eurydice_slice key_generation_seed,
     IndCpaPrivateKeyUnpacked_af *private_key,
     IndCpaPublicKeyUnpacked_af *public_key) {
@@ -3923,8 +3923,8 @@ libcrux_ml_kem_variant_MlKem with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static libcrux_ml_kem_utils_extraction_helper_Keypair1024 generate_keypair_151(
-    Eurydice_slice key_generation_seed) {
+static KRML_MUSTINLINE libcrux_ml_kem_utils_extraction_helper_Keypair1024
+generate_keypair_151(Eurydice_slice key_generation_seed) {
   IndCpaPrivateKeyUnpacked_af private_key = default_1a_d0();
   IndCpaPublicKeyUnpacked_af public_key = default_8d_d0();
   generate_keypair_unpacked_1c(key_generation_seed, &private_key, &public_key);
@@ -4413,7 +4413,7 @@ with types libcrux_ml_kem_vector_portable_vector_type_PortableVector
 with const generics
 
 */
-static libcrux_ml_kem_vector_portable_vector_type_PortableVector
+static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector
 decompress_1_8c(libcrux_ml_kem_vector_portable_vector_type_PortableVector v) {
   libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
       libcrux_ml_kem_vector_portable_ZERO_0d();
@@ -4637,7 +4637,7 @@ with const generics
 - COMPRESSION_FACTOR= 11
 - BLOCK_LEN= 352
 */
-static void compress_then_serialize_u_2f(
+static KRML_MUSTINLINE void compress_then_serialize_u_2f(
     libcrux_ml_kem_polynomial_PolynomialRingElement_1d input[4U],
     Eurydice_slice out) {
   for (size_t i = (size_t)0U;
@@ -4854,9 +4854,9 @@ generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_unpacked_2a(IndCpaPublicKeyUnpacked_af *public_key,
-                                uint8_t message[32U], Eurydice_slice randomness,
-                                uint8_t ret[1568U]) {
+static KRML_MUSTINLINE void encrypt_unpacked_2a(
+    IndCpaPublicKeyUnpacked_af *public_key, uint8_t message[32U],
+    Eurydice_slice randomness, uint8_t ret[1568U]) {
   uint8_t prf_input[33U];
   libcrux_ml_kem_utils_into_padded_array_c8(/* for i from 0 to k−1 do r[i] :=
                                                CBD{η1}(PRF(r, N)) N := N + 1 end
@@ -4937,8 +4937,10 @@ generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_2a1(Eurydice_slice public_key, uint8_t message[32U],
-                        Eurydice_slice randomness, uint8_t ret[1568U]) {
+static KRML_MUSTINLINE void encrypt_2a1(Eurydice_slice public_key,
+                                        uint8_t message[32U],
+                                        Eurydice_slice randomness,
+                                        uint8_t ret[1568U]) {
   IndCpaPublicKeyUnpacked_af unpacked_public_key = default_8d_d0();
   deserialize_ring_elements_reduced_0d(
       Eurydice_slice_subslice_to(/* tˆ := Decode_12(pk) */
@@ -5566,8 +5568,9 @@ with const generics
 - U_COMPRESSION_FACTOR= 11
 - V_COMPRESSION_FACTOR= 5
 */
-static void decrypt_unpacked_7d(IndCpaPrivateKeyUnpacked_af *secret_key,
-                                uint8_t *ciphertext, uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_unpacked_7d(
+    IndCpaPrivateKeyUnpacked_af *secret_key, uint8_t *ciphertext,
+    uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_1d u_as_ntt[4U];
   deserialize_then_decompress_u_00(
       /* u := Decompress_q(Decode_{d_u}(c), d_u) */ ciphertext, u_as_ntt);
@@ -5594,8 +5597,8 @@ with const generics
 - U_COMPRESSION_FACTOR= 11
 - V_COMPRESSION_FACTOR= 5
 */
-static void decrypt_7d(Eurydice_slice secret_key, uint8_t *ciphertext,
-                       uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_7d(Eurydice_slice secret_key,
+                                       uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_1d secret_as_ntt[4U];
   deserialize_secret_key_d0(/* sˆ := Decode_12(sk) */ secret_key,
                             secret_as_ntt);
@@ -6688,7 +6691,7 @@ libcrux_ml_kem_variant_MlKem with const generics
 - ETA1= 3
 - ETA1_RANDOMNESS_SIZE= 192
 */
-static void generate_keypair_unpacked_1c0(
+static KRML_MUSTINLINE void generate_keypair_unpacked_1c0(
     Eurydice_slice key_generation_seed,
     IndCpaPrivateKeyUnpacked_d4 *private_key,
     IndCpaPublicKeyUnpacked_d4 *public_key) {
@@ -6747,8 +6750,8 @@ libcrux_ml_kem_variant_MlKem with const generics
 - ETA1= 3
 - ETA1_RANDOMNESS_SIZE= 192
 */
-static libcrux_ml_kem_utils_extraction_helper_Keypair512 generate_keypair_150(
-    Eurydice_slice key_generation_seed) {
+static KRML_MUSTINLINE libcrux_ml_kem_utils_extraction_helper_Keypair512
+generate_keypair_150(Eurydice_slice key_generation_seed) {
   IndCpaPrivateKeyUnpacked_d4 private_key = default_1a_a0();
   IndCpaPublicKeyUnpacked_d4 public_key = default_8d_a0();
   generate_keypair_unpacked_1c0(key_generation_seed, &private_key, &public_key);
@@ -7171,7 +7174,7 @@ with const generics
 - COMPRESSION_FACTOR= 10
 - BLOCK_LEN= 320
 */
-static void compress_then_serialize_u_6d(
+static KRML_MUSTINLINE void compress_then_serialize_u_6d(
     libcrux_ml_kem_polynomial_PolynomialRingElement_1d input[2U],
     Eurydice_slice out) {
   for (size_t i = (size_t)0U;
@@ -7270,9 +7273,9 @@ generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_unpacked_2a0(IndCpaPublicKeyUnpacked_d4 *public_key,
-                                 uint8_t message[32U],
-                                 Eurydice_slice randomness, uint8_t ret[768U]) {
+static KRML_MUSTINLINE void encrypt_unpacked_2a0(
+    IndCpaPublicKeyUnpacked_d4 *public_key, uint8_t message[32U],
+    Eurydice_slice randomness, uint8_t ret[768U]) {
   uint8_t prf_input[33U];
   libcrux_ml_kem_utils_into_padded_array_c8(/* for i from 0 to k−1 do r[i] :=
                                                CBD{η1}(PRF(r, N)) N := N + 1 end
@@ -7354,8 +7357,10 @@ generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_2a0(Eurydice_slice public_key, uint8_t message[32U],
-                        Eurydice_slice randomness, uint8_t ret[768U]) {
+static KRML_MUSTINLINE void encrypt_2a0(Eurydice_slice public_key,
+                                        uint8_t message[32U],
+                                        Eurydice_slice randomness,
+                                        uint8_t ret[768U]) {
   IndCpaPublicKeyUnpacked_d4 unpacked_public_key = default_8d_a0();
   deserialize_ring_elements_reduced_5f(
       Eurydice_slice_subslice_to(/* tˆ := Decode_12(pk) */
@@ -7650,8 +7655,9 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_unpacked_d1(IndCpaPrivateKeyUnpacked_d4 *secret_key,
-                                uint8_t *ciphertext, uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_unpacked_d1(
+    IndCpaPrivateKeyUnpacked_d4 *secret_key, uint8_t *ciphertext,
+    uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_1d u_as_ntt[2U];
   deserialize_then_decompress_u_86(
       /* u := Decompress_q(Decode_{d_u}(c), d_u) */ ciphertext, u_as_ntt);
@@ -7678,8 +7684,8 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_d1(Eurydice_slice secret_key, uint8_t *ciphertext,
-                       uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_d1(Eurydice_slice secret_key,
+                                       uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_1d secret_as_ntt[2U];
   deserialize_secret_key_a0(/* sˆ := Decode_12(sk) */ secret_key,
                             secret_as_ntt);
@@ -8755,7 +8761,7 @@ libcrux_ml_kem_variant_MlKem with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static void generate_keypair_unpacked_1c1(
+static KRML_MUSTINLINE void generate_keypair_unpacked_1c1(
     Eurydice_slice key_generation_seed,
     IndCpaPrivateKeyUnpacked_a0 *private_key,
     IndCpaPublicKeyUnpacked_a0 *public_key) {
@@ -8814,8 +8820,8 @@ libcrux_ml_kem_variant_MlKem with const generics
 - ETA1= 2
 - ETA1_RANDOMNESS_SIZE= 128
 */
-static libcrux_ml_kem_utils_extraction_helper_Keypair768 generate_keypair_15(
-    Eurydice_slice key_generation_seed) {
+static KRML_MUSTINLINE libcrux_ml_kem_utils_extraction_helper_Keypair768
+generate_keypair_15(Eurydice_slice key_generation_seed) {
   IndCpaPrivateKeyUnpacked_a0 private_key = default_1a_1b();
   IndCpaPublicKeyUnpacked_a0 public_key = default_8d_1b();
   generate_keypair_unpacked_1c1(key_generation_seed, &private_key, &public_key);
@@ -9168,7 +9174,7 @@ with const generics
 - COMPRESSION_FACTOR= 10
 - BLOCK_LEN= 320
 */
-static void compress_then_serialize_u_43(
+static KRML_MUSTINLINE void compress_then_serialize_u_43(
     libcrux_ml_kem_polynomial_PolynomialRingElement_1d input[3U],
     Eurydice_slice out) {
   for (size_t i = (size_t)0U;
@@ -9255,10 +9261,9 @@ generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_unpacked_2a1(IndCpaPublicKeyUnpacked_a0 *public_key,
-                                 uint8_t message[32U],
-                                 Eurydice_slice randomness,
-                                 uint8_t ret[1088U]) {
+static KRML_MUSTINLINE void encrypt_unpacked_2a1(
+    IndCpaPublicKeyUnpacked_a0 *public_key, uint8_t message[32U],
+    Eurydice_slice randomness, uint8_t ret[1088U]) {
   uint8_t prf_input[33U];
   libcrux_ml_kem_utils_into_padded_array_c8(/* for i from 0 to k−1 do r[i] :=
                                                CBD{η1}(PRF(r, N)) N := N + 1 end
@@ -9340,8 +9345,10 @@ generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-static void encrypt_2a(Eurydice_slice public_key, uint8_t message[32U],
-                       Eurydice_slice randomness, uint8_t ret[1088U]) {
+static KRML_MUSTINLINE void encrypt_2a(Eurydice_slice public_key,
+                                       uint8_t message[32U],
+                                       Eurydice_slice randomness,
+                                       uint8_t ret[1088U]) {
   IndCpaPublicKeyUnpacked_a0 unpacked_public_key = default_8d_1b();
   deserialize_ring_elements_reduced_b3(
       Eurydice_slice_subslice_to(/* tˆ := Decode_12(pk) */
@@ -9595,8 +9602,9 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_unpacked_42(IndCpaPrivateKeyUnpacked_a0 *secret_key,
-                                uint8_t *ciphertext, uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_unpacked_42(
+    IndCpaPrivateKeyUnpacked_a0 *secret_key, uint8_t *ciphertext,
+    uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_1d u_as_ntt[3U];
   deserialize_then_decompress_u_6c(
       /* u := Decompress_q(Decode_{d_u}(c), d_u) */ ciphertext, u_as_ntt);
@@ -9623,8 +9631,8 @@ with const generics
 - U_COMPRESSION_FACTOR= 10
 - V_COMPRESSION_FACTOR= 4
 */
-static void decrypt_42(Eurydice_slice secret_key, uint8_t *ciphertext,
-                       uint8_t ret[32U]) {
+static KRML_MUSTINLINE void decrypt_42(Eurydice_slice secret_key,
+                                       uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement_1d secret_as_ntt[3U];
   deserialize_secret_key_1b(/* sˆ := Decode_12(sk) */ secret_key,
                             secret_as_ntt);
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h
index bdb63414..9e3758ce 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h
+++ b/libcrux-ml-kem/c/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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_mlkem_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h
index 4c9cc754..e8b660ff 100644
--- a/libcrux-ml-kem/c/libcrux_sha3.h
+++ b/libcrux-ml-kem/c/libcrux_sha3.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_sha3_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.c b/libcrux-ml-kem/c/libcrux_sha3_avx2.c
index 44399abd..2d8024a9 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "internal/libcrux_sha3_avx2.h"
diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/libcrux_sha3_avx2.h
index 8887556c..bba954e1 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/c/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: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_sha3_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3_internal.h b/libcrux-ml-kem/c/libcrux_sha3_internal.h
index a79a1389..aa770245 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_internal.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_sha3_internal_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.c b/libcrux-ml-kem/c/libcrux_sha3_neon.c
index 2ed7a6a1..7e1ef9a2 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_neon.c
+++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #include "libcrux_sha3_neon.h"
diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.h b/libcrux-ml-kem/c/libcrux_sha3_neon.h
index d0aad5d7..2ac25649 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_neon.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+ * Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102
+ * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
+ * F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
+ * Libcrux: de5cf36eb9ea4853d387d80f6b4385ce5275511b
  */
 
 #ifndef __libcrux_sha3_neon_H