diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
index 2e22eab77..652ce941a 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
-Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
 Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
 F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
-Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
index a0381ed6a..028032211 100644
--- a/libcrux-ml-kem/c/internal/libcrux_core.h
+++ b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 92522b699..0a996c9fb 100644
--- a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
+++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 a90a7b18d..7bd8b40cd 100644
--- a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
+++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 003fbd8ee..8be31ea17 100644
--- a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 c23f5a0f3..267174f80 100644
--- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
+++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 fe23b8463..e98fb186d 100644
--- a/libcrux-ml-kem/c/libcrux_core.c
+++ b/libcrux-ml-kem/c/libcrux_core.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "internal/libcrux_core.h"
diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h
index a76feeeaa..899850336 100644
--- a/libcrux-ml-kem/c/libcrux_core.h
+++ b/libcrux-ml-kem/c/libcrux_core.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #ifndef __libcrux_core_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h
index e4c7008f7..7ec8206d4 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 38597d472..bce2c367d 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "libcrux_mlkem1024_avx2.h"
@@ -205,7 +205,12 @@ libcrux_ml_kem_mlkem1024_avx2_generate_key_pair(uint8_t randomness[64U]) {
 }
 
 /**
- 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,
@@ -265,7 +270,12 @@ bool libcrux_ml_kem_mlkem1024_avx2_validate_private_key_only(
 }
 
 /**
- 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);
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
index 8ca7a9720..f0664f5c8 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 f799f3dfd..efbf1c6cd 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "libcrux_mlkem1024_portable.h"
@@ -146,7 +146,7 @@ generics
 - SECRET_KEY_SIZE= 3168
 - CIPHERTEXT_SIZE= 1568
 */
-static bool validate_private_key_6b(
+static KRML_MUSTINLINE 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_b5(private_key,
@@ -200,7 +200,7 @@ generics
 - RANKED_BYTES_PER_RING_ELEMENT= 1536
 - PUBLIC_KEY_SIZE= 1568
 */
-static bool validate_public_key_6b(uint8_t *public_key) {
+static KRML_MUSTINLINE bool validate_public_key_6b(uint8_t *public_key) {
   return libcrux_ml_kem_ind_cca_validate_public_key_00(public_key);
 }
 
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
index 45f8bcfd4..c0cc37f0f 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #ifndef __libcrux_mlkem1024_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h
index 6e717878f..f5f8e52cd 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 3b8425a60..189f6fe8e 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "libcrux_mlkem512_avx2.h"
@@ -205,7 +205,12 @@ libcrux_ml_kem_mlkem512_avx2_generate_key_pair(uint8_t randomness[64U]) {
 }
 
 /**
- 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,
@@ -265,7 +270,12 @@ bool libcrux_ml_kem_mlkem512_avx2_validate_private_key_only(
 }
 
 /**
- 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);
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
index 669e98b4e..fb012491b 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 e9b85aecf..617386bb8 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "libcrux_mlkem512_portable.h"
@@ -146,7 +146,7 @@ generics
 - SECRET_KEY_SIZE= 1632
 - CIPHERTEXT_SIZE= 768
 */
-static bool validate_private_key_1c(
+static KRML_MUSTINLINE 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_fb(private_key,
@@ -200,7 +200,7 @@ generics
 - RANKED_BYTES_PER_RING_ELEMENT= 768
 - PUBLIC_KEY_SIZE= 800
 */
-static bool validate_public_key_1c(uint8_t *public_key) {
+static KRML_MUSTINLINE bool validate_public_key_1c(uint8_t *public_key) {
   return libcrux_ml_kem_ind_cca_validate_public_key_86(public_key);
 }
 
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
index 35a235896..ca114ecc1 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #ifndef __libcrux_mlkem512_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h
index afd2ddfb5..ac85b1f42 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 46d7d26b5..f9451ab9e 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "libcrux_mlkem768_avx2.h"
@@ -205,7 +205,12 @@ libcrux_ml_kem_mlkem768_avx2_generate_key_pair(uint8_t randomness[64U]) {
 }
 
 /**
- 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,
@@ -265,7 +270,12 @@ bool libcrux_ml_kem_mlkem768_avx2_validate_private_key_only(
 }
 
 /**
- 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);
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
index ac6658417..620eb7623 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 5b8ba054c..eeafd72f8 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "libcrux_mlkem768_portable.h"
@@ -146,7 +146,7 @@ generics
 - SECRET_KEY_SIZE= 2400
 - CIPHERTEXT_SIZE= 1088
 */
-static bool validate_private_key_31(
+static KRML_MUSTINLINE 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_37(private_key,
@@ -200,7 +200,7 @@ generics
 - RANKED_BYTES_PER_RING_ELEMENT= 1152
 - PUBLIC_KEY_SIZE= 1184
 */
-static bool validate_public_key_31(uint8_t *public_key) {
+static KRML_MUSTINLINE bool validate_public_key_31(uint8_t *public_key) {
   return libcrux_ml_kem_ind_cca_validate_public_key_6c(public_key);
 }
 
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
index 4af44382a..d964d45a3 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 75edc4e9b..a9323eaac 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "internal/libcrux_mlkem_avx2.h"
@@ -3737,8 +3737,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 =
       build_unpacked_public_key_fa1(public_key);
   IndCpaPublicKeyUnpacked_63 *uu____0 = &unpacked_public_key;
@@ -6213,8 +6215,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 =
       build_unpacked_public_key_fa0(public_key);
   IndCpaPublicKeyUnpacked_39 *uu____0 = &unpacked_public_key;
@@ -8277,8 +8281,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 =
       build_unpacked_public_key_fa(public_key);
   IndCpaPublicKeyUnpacked_94 *uu____0 = &unpacked_public_key;
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
index fcbeafcf4..ddd1f6c68 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 326a50675..d99545eff 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #include "internal/libcrux_mlkem_portable.h"
@@ -4886,8 +4886,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 =
       build_unpacked_public_key_3f1(public_key);
   IndCpaPublicKeyUnpacked_af *uu____0 = &unpacked_public_key;
@@ -7316,8 +7318,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 =
       build_unpacked_public_key_3f0(public_key);
   IndCpaPublicKeyUnpacked_d4 *uu____0 = &unpacked_public_key;
@@ -9330,8 +9334,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 =
       build_unpacked_public_key_3f(public_key);
   IndCpaPublicKeyUnpacked_a0 *uu____0 = &unpacked_public_key;
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h
index 323ba861a..240fddd8f 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #ifndef __libcrux_mlkem_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h
index 002ce6b2b..eb87a427c 100644
--- a/libcrux-ml-kem/c/libcrux_sha3.h
+++ b/libcrux-ml-kem/c/libcrux_sha3.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 337305c5b..e0f18f191 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 1e2f53358..f4164e3b8 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 14985c821..8e28a4374 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_internal.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 aae5027cd..b7c0ab441 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_neon.c
+++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #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 f32a3a0a2..57377f60d 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_neon.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h
@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 76be5813ea48977a7e122f6af350f1a5324b2cb6
+ * Libcrux: 150df2319c18ad9912639a9541adddd0d0e40015
  */
 
 #ifndef __libcrux_sha3_neon_H