diff --git a/libcrux-ml-dsa/cg/code_gen.txt b/libcrux-ml-dsa/cg/code_gen.txt
index 1990a3a8e..a636e3aa9 100644
--- a/libcrux-ml-dsa/cg/code_gen.txt
+++ b/libcrux-ml-dsa/cg/code_gen.txt
@@ -2,5 +2,5 @@ This code was generated with the following revisions:
 Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
 Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
 Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
-F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
-Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+F*: unset
+Libcrux: c9823353edf245785e103a69312b21cca741967a
diff --git a/libcrux-ml-dsa/cg/header.txt b/libcrux-ml-dsa/cg/header.txt
index 4004851e7..2f37f7aa7 100644
--- a/libcrux-ml-dsa/cg/header.txt
+++ b/libcrux-ml-dsa/cg/header.txt
@@ -7,6 +7,6 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
- * Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
diff --git a/libcrux-ml-dsa/cg/libcrux_core.h b/libcrux-ml-dsa/cg/libcrux_core.h
index f4c86a70d..5c9e4a5f2 100644
--- a/libcrux-ml-dsa/cg/libcrux_core.h
+++ b/libcrux-ml-dsa/cg/libcrux_core.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
- * Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_core_H
diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h
index b14980b0c..96f597fd7 100644
--- a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h
+++ b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
- * Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_mldsa65_avx2_H
diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h
index 73e831a9f..321590cbb 100644
--- a/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h
+++ b/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
- * Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_mldsa65_portable_H
@@ -2220,6 +2220,18 @@ libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
   }
 }
 
+static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(
+    libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re, size_t index,
+    size_t step_by, int32_t zeta) {
+  libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
+      re[index + step_by];
+  libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(&tmp,
+                                                                          zeta);
+  re[index + step_by] = re[index];
+  libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[index + step_by], &tmp);
+  libcrux_ml_dsa_simd_portable_arithmetic_add(&re[index], &tmp);
+}
+
 /**
 A monomorphic instance of libcrux_ml_dsa.simd.portable.ntt.outer_3_plus
 with const generics
@@ -2231,14 +2243,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_99(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)0U; i < (size_t)0U + (size_t)16U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)16U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)25847);
-    re[j + (size_t)16U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)16U],
-                                                     &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)16U,
+                                                        (int32_t)25847);
   }
 }
 
@@ -2258,13 +2264,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_990(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)0U; i < (size_t)0U + (size_t)8U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)8U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-2608894);
-    re[j + (size_t)8U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)8U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)8U,
+                                                        (int32_t)-2608894);
   }
 }
 
@@ -2279,13 +2280,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_7a(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)16U; i < (size_t)16U + (size_t)8U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)8U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-518909);
-    re[j + (size_t)8U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)8U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)8U,
+                                                        (int32_t)-518909);
   }
 }
 
@@ -2306,13 +2302,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_991(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)0U; i < (size_t)0U + (size_t)4U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)4U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)237124);
-    re[j + (size_t)4U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)4U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)4U,
+                                                        (int32_t)237124);
   }
 }
 
@@ -2327,13 +2318,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_a8(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)8U; i < (size_t)8U + (size_t)4U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)4U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-777960);
-    re[j + (size_t)4U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)4U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)4U,
+                                                        (int32_t)-777960);
   }
 }
 
@@ -2348,13 +2334,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_7a0(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)16U; i < (size_t)16U + (size_t)4U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)4U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-876248);
-    re[j + (size_t)4U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)4U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)4U,
+                                                        (int32_t)-876248);
   }
 }
 
@@ -2369,13 +2350,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_d9(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)24U; i < (size_t)24U + (size_t)4U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)4U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)466468);
-    re[j + (size_t)4U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)4U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)4U,
+                                                        (int32_t)466468);
   }
 }
 
@@ -2398,13 +2374,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_992(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)0U; i < (size_t)0U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)1826347);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)1826347);
   }
 }
 
@@ -2419,13 +2390,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_6b(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)4U; i < (size_t)4U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)2353451);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)2353451);
   }
 }
 
@@ -2440,13 +2406,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_a80(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)8U; i < (size_t)8U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-359251);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)-359251);
   }
 }
 
@@ -2461,13 +2422,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_95(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)12U; i < (size_t)12U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-2091905);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)-2091905);
   }
 }
 
@@ -2482,13 +2438,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_7a1(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)16U; i < (size_t)16U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)3119733);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)3119733);
   }
 }
 
@@ -2503,13 +2454,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_de(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)20U; i < (size_t)20U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-2884855);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)-2884855);
   }
 }
 
@@ -2524,13 +2470,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_d90(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)24U; i < (size_t)24U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)3111497);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)3111497);
   }
 }
 
@@ -2545,13 +2486,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_3b(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)28U; i < (size_t)28U + (size_t)2U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)2U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)2680103);
-    re[j + (size_t)2U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)2U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)2U,
+                                                        (int32_t)2680103);
   }
 }
 
@@ -2578,13 +2514,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_993(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)0U; i < (size_t)0U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)2725464);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)2725464);
   }
 }
 
@@ -2599,13 +2530,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_1c(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)2U; i < (size_t)2U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)1024112);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)1024112);
   }
 }
 
@@ -2620,13 +2546,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_6b0(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)4U; i < (size_t)4U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-1079900);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-1079900);
   }
 }
 
@@ -2641,13 +2562,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_44(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)6U; i < (size_t)6U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)3585928);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)3585928);
   }
 }
 
@@ -2662,13 +2578,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_a81(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)8U; i < (size_t)8U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-549488);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-549488);
   }
 }
 
@@ -2683,13 +2594,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_1f(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)10U; i < (size_t)10U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-1119584);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-1119584);
   }
 }
 
@@ -2704,13 +2610,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_950(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)12U; i < (size_t)12U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)2619752);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)2619752);
   }
 }
 
@@ -2725,13 +2626,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_3b0(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)14U; i < (size_t)14U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-2108549);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-2108549);
   }
 }
 
@@ -2746,13 +2642,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_7a2(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)16U; i < (size_t)16U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-2118186);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-2118186);
   }
 }
 
@@ -2767,13 +2658,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_e4(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)18U; i < (size_t)18U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-3859737);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-3859737);
   }
 }
 
@@ -2788,13 +2674,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_de0(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)20U; i < (size_t)20U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-1399561);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-1399561);
   }
 }
 
@@ -2809,13 +2690,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_05(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)22U; i < (size_t)22U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-3277672);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-3277672);
   }
 }
 
@@ -2830,13 +2706,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_d91(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)24U; i < (size_t)24U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)1757237);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)1757237);
   }
 }
 
@@ -2851,13 +2722,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_3a(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)26U; i < (size_t)26U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)-19422);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)-19422);
   }
 }
 
@@ -2872,13 +2738,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_3b1(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)28U; i < (size_t)28U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)4010497);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)4010497);
   }
 }
 
@@ -2893,13 +2754,8 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_a0(
     libcrux_ml_dsa_simd_portable_vector_type_Coefficients *re) {
   for (size_t i = (size_t)30U; i < (size_t)30U + (size_t)1U; i++) {
     size_t j = i;
-    libcrux_ml_dsa_simd_portable_vector_type_Coefficients tmp =
-        re[j + (size_t)1U];
-    libcrux_ml_dsa_simd_portable_arithmetic_montgomery_multiply_by_constant(
-        &tmp, (int32_t)280005);
-    re[j + (size_t)1U] = re[j];
-    libcrux_ml_dsa_simd_portable_arithmetic_subtract(&re[j + (size_t)1U], &tmp);
-    libcrux_ml_dsa_simd_portable_arithmetic_add(&re[j], &tmp);
+    libcrux_ml_dsa_simd_portable_ntt_outer_3_plus_round(re, j, (size_t)1U,
+                                                        (int32_t)280005);
   }
 }
 
diff --git a/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h b/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h
index 6a6115243..5fcf211c8 100644
--- a/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h
+++ b/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
- * Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_sha3_avx2_H
diff --git a/libcrux-ml-dsa/cg/libcrux_sha3_portable.h b/libcrux-ml-dsa/cg/libcrux_sha3_portable.h
index d08f2caa2..5e1a43ec1 100644
--- a/libcrux-ml-dsa/cg/libcrux_sha3_portable.h
+++ b/libcrux-ml-dsa/cg/libcrux_sha3_portable.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 4b3fc11774003a6ff7c09500ecb5f0145ca6d862
- * Libcrux: b54a2f8eacb847bfe456abe6b195dc94bf464dda
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_sha3_portable_H
diff --git a/libcrux-ml-dsa/src/simd/portable/ntt.rs b/libcrux-ml-dsa/src/simd/portable/ntt.rs
index 026ecb7a9..ed257b7a1 100644
--- a/libcrux-ml-dsa/src/simd/portable/ntt.rs
+++ b/libcrux-ml-dsa/src/simd/portable/ntt.rs
@@ -323,18 +323,6 @@ fn ntt_at_layer_2(re: &mut [Coefficients; SIMD_UNITS_IN_RING_ELEMENT]) {
 }
 
 #[inline(always)]
-#[hax_lib::fstar::before(
-    r#"
-let layer_bound_factor (step_by:usize) : n:nat{n <= 4} =
-    match step_by with
-    | MkInt 1 -> 4
-    | MkInt 2 -> 3
-    | MkInt 4 -> 2
-    | MkInt 8 -> 1
-    | MkInt 16 -> 0
-    | _ -> 0
-"#
-)]
 #[hax_lib::fstar::options("--z3rlimit 600 --split_queries always")]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 #[hax_lib::requires(fstar!(r#"
@@ -357,6 +345,61 @@ let layer_bound_factor (step_by:usize) : n:nat{n <= 4} =
 fn outer_3_plus<const OFFSET: usize, const STEP_BY: usize, const ZETA: i32>(
     re: &mut [Coefficients; SIMD_UNITS_IN_RING_ELEMENT],
 ) {
+    // Refactoring the code to have the loop body separately verified is good for proof performance.
+    // So we factor out the loop body in a `round` function similarly to the other NTT layers.
+    #[inline(always)]
+    #[hax_lib::fstar::before(
+        r#"
+    let layer_bound_factor (step_by:usize) : n:nat{n <= 4} =
+        match step_by with
+        | MkInt 1 -> 4
+        | MkInt 2 -> 3
+        | MkInt 4 -> 2
+        | MkInt 8 -> 1
+        | MkInt 16 -> 0
+        | _ -> 0
+    "#
+    )]
+    #[hax_lib::fstar::options("--z3rlimit 300 --split_queries always")]
+    #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
+    #[hax_lib::requires(fstar!(r#"
+        v $step_by > 0 /\
+        v $index + v $step_by < v $SIMD_UNITS_IN_RING_ELEMENT /\
+        Spec.Utils.is_i32b_array_opaque 
+                    (v $NTT_BASE_BOUND + ((layer_bound_factor $step_by) * v $FIELD_MAX)) 
+                    (Seq.index ${re} (v $index)).f_values /\
+        Spec.Utils.is_i32b_array_opaque 
+                    (v $NTT_BASE_BOUND + ((layer_bound_factor $step_by) * v $FIELD_MAX)) 
+                    (Seq.index ${re} (v $index + v $step_by)).f_values /\
+        Spec.Utils.is_i32b 4190208 $zeta
+    "#))]
+    #[hax_lib::ensures(|_| fstar!(r#"
+        Spec.Utils.modifies2_32 ${re} ${re}_future $index (${index + step_by}) /\
+        Spec.Utils.is_i32b_array_opaque 
+                    (v $NTT_BASE_BOUND + ((layer_bound_factor $step_by + 1) * v $FIELD_MAX)) 
+                    (Seq.index ${re}_future (v $index)).f_values /\
+        Spec.Utils.is_i32b_array_opaque 
+                    (v $NTT_BASE_BOUND + ((layer_bound_factor $step_by + 1) * v $FIELD_MAX)) 
+                    (Seq.index ${re}_future (v $index + v step_by)).f_values
+    "#))]
+    fn round(
+        re: &mut [Coefficients; SIMD_UNITS_IN_RING_ELEMENT],
+        index: usize,
+        step_by: usize,
+        zeta: i32,
+    ) {
+        hax_lib::fstar!(
+            "reveal_opaque (`%Spec.Utils.is_i32b_array_opaque) (Spec.Utils.is_i32b_array_opaque)"
+        );
+        let mut tmp = re[index + step_by];
+        montgomery_multiply_by_constant(&mut tmp, zeta);
+
+        re[index + step_by] = re[index];
+
+        arithmetic::subtract(&mut re[index + step_by], &tmp);
+        arithmetic::add(&mut re[index], &tmp);
+    }
+
     #[cfg(hax)]
     let orig_re = re.clone();
 
@@ -372,20 +415,7 @@ fn outer_3_plus<const OFFSET: usize, const STEP_BY: usize, const ZETA: i32>(
                     (Seq.index ${re} i).f_values))
         "#
         ));
-
-        let mut tmp = re[j + STEP_BY];
-        montgomery_multiply_by_constant(&mut tmp, ZETA);
-
-        re[j + STEP_BY] = re[j];
-
-        arithmetic::subtract(&mut re[j + STEP_BY], &tmp);
-        arithmetic::add(&mut re[j], &tmp);
-
-        hax_lib::fstar!(
-            r#"
-        assert ((v ${NTT_BASE_BOUND} + ((layer_bound_factor v_STEP_BY) * v $FIELD_MAX)) + (v $FIELD_MAX) 
-                == (v ${NTT_BASE_BOUND} + ((layer_bound_factor v_STEP_BY + 1) * v $FIELD_MAX)))"#
-        );
+        round(re, j, STEP_BY, ZETA);
     }
 }
 
diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt
index d2d199942..a636e3aa9 100644
--- a/libcrux-ml-kem/cg/code_gen.txt
+++ b/libcrux-ml-kem/cg/code_gen.txt
@@ -2,5 +2,5 @@ This code was generated with the following revisions:
 Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
 Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
 Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
-F*: 71d8221589d4d438af3706d89cb653cf53e18aab
-Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+F*: unset
+Libcrux: c9823353edf245785e103a69312b21cca741967a
diff --git a/libcrux-ml-kem/cg/header.txt b/libcrux-ml-kem/cg/header.txt
index c4a22e5a3..2f37f7aa7 100644
--- a/libcrux-ml-kem/cg/header.txt
+++ b/libcrux-ml-kem/cg/header.txt
@@ -7,6 +7,6 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h
index 4e4531cb8..71538e2ec 100644
--- a/libcrux-ml-kem/cg/libcrux_ct_ops.h
+++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_ct_ops_H
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
index fb49251eb..21e286c57 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_mlkem768_avx2_H
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
index 47064cace..b29da588a 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_mlkem768_portable_H
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem_core.h b/libcrux-ml-kem/cg/libcrux_mlkem_core.h
index 075898f33..5e6df5383 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem_core.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem_core.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_mlkem_core_H
diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
index afc95b31c..2b197f5b7 100644
--- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_sha3_avx2_H
diff --git a/libcrux-ml-kem/cg/libcrux_sha3_portable.h b/libcrux-ml-kem/cg/libcrux_sha3_portable.h
index 3a5e634d1..9eb110f81 100644
--- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h
@@ -7,8 +7,8 @@
  * Charon: bb62a9b39db4ea8c6d536fe61b7d26663751bf3c
  * Eurydice: 46cef5d58a855ed049fa89bfe99c959b5d9d0d4b
  * Karamel: 39cb85a718da8ae4a724d31b08f9134ca9311336
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: e74ed15b655f78c0fb80c8614a94c07932712e44
+ * F*: unset
+ * Libcrux: c9823353edf245785e103a69312b21cca741967a
  */
 
 #ifndef __libcrux_sha3_portable_H
diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fsti b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fsti
index 569a60969..c512e7e1d 100644
--- a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fsti
+++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fsti
@@ -599,7 +599,6 @@ let forall32 (p:(x:nat{x < 32} -> Type0)) =
 let modifies1_8 #t
     (a b: t_Array t (sz 8))
     (i:usize{v i < 8}) = 
-//    normalize_term (forall8 (fun j -> (v i <> j) ==> Seq.index a j == Seq.index b j))
     ((v i <> 0)  ==> Seq.index a 0 == Seq.index b 0) /\
     ((v i <> 1)  ==> Seq.index a 1 == Seq.index b 1) /\
     ((v i <> 2)  ==> Seq.index a 2 == Seq.index b 2) /\
@@ -621,6 +620,46 @@ let modifies2_8 #t
     ((v i <> 6 /\ v j <> 6)  ==> Seq.index a 6 == Seq.index b 6) /\
     ((v i <> 7 /\ v j <> 7)  ==> Seq.index a 7 == Seq.index b 7)
 
+let modifies1_16 #t
+    (a b: t_Array t (sz 16))
+    (i:usize{v i < 16}) = 
+    (v i <> 0  ==> Seq.index a 0 == Seq.index b 0) /\
+    (v i <> 1  ==> Seq.index a 1 == Seq.index b 1) /\
+    (v i <> 2  ==> Seq.index a 2 == Seq.index b 2) /\
+    (v i <> 3  ==> Seq.index a 3 == Seq.index b 3) /\
+    (v i <> 4  ==> Seq.index a 4 == Seq.index b 4) /\
+    (v i <> 5  ==> Seq.index a 5 == Seq.index b 5) /\
+    (v i <> 6  ==> Seq.index a 6 == Seq.index b 6) /\
+    (v i <> 7  ==> Seq.index a 7 == Seq.index b 7) /\
+    (v i <> 8  ==> Seq.index a 8 == Seq.index b 8) /\
+    (v i <> 9  ==> Seq.index a 9 == Seq.index b 9) /\
+    (v i <> 10 ==> Seq.index a 10 == Seq.index b 10) /\
+    (v i <> 11 ==> Seq.index a 11 == Seq.index b 11) /\
+    (v i <> 12 ==> Seq.index a 12 == Seq.index b 12) /\
+    (v i <> 13 ==> Seq.index a 13 == Seq.index b 13) /\
+    (v i <> 14 ==> Seq.index a 14 == Seq.index b 14) /\
+    (v i <> 15 ==> Seq.index a 15 == Seq.index b 15)
+
+let modifies2_16 #t
+    (a b: t_Array t (sz 16))
+    (i:usize{v i < 16}) (j:usize{v j < 16}) =
+    ((v i <> 0  /\ v j <> 0)  ==> Seq.index a 0 == Seq.index b 0) /\
+    ((v i <> 1  /\ v j <> 1)  ==> Seq.index a 1 == Seq.index b 1) /\
+    ((v i <> 2  /\ v j <> 2)  ==> Seq.index a 2 == Seq.index b 2) /\
+    ((v i <> 3  /\ v j <> 3)  ==> Seq.index a 3 == Seq.index b 3) /\
+    ((v i <> 4  /\ v j <> 4)  ==> Seq.index a 4 == Seq.index b 4) /\
+    ((v i <> 5  /\ v j <> 5)  ==> Seq.index a 5 == Seq.index b 5) /\
+    ((v i <> 6  /\ v j <> 6)  ==> Seq.index a 6 == Seq.index b 6) /\
+    ((v i <> 7  /\ v j <> 7)  ==> Seq.index a 7 == Seq.index b 7) /\
+    ((v i <> 8  /\ v j <> 8)  ==> Seq.index a 8 == Seq.index b 8) /\
+    ((v i <> 9  /\ v j <> 9)  ==> Seq.index a 9 == Seq.index b 9) /\
+    ((v i <> 10 /\ v j <> 10) ==> Seq.index a 10 == Seq.index b 10) /\
+    ((v i <> 11 /\ v j <> 11) ==> Seq.index a 11 == Seq.index b 11) /\
+    ((v i <> 12 /\ v j <> 12) ==> Seq.index a 12 == Seq.index b 12) /\
+    ((v i <> 13 /\ v j <> 13) ==> Seq.index a 13 == Seq.index b 13) /\
+    ((v i <> 14 /\ v j <> 14) ==> Seq.index a 14 == Seq.index b 14) /\
+    ((v i <> 15 /\ v j <> 15) ==> Seq.index a 15 == Seq.index b 15)
+
 let modifies1_32 #t
         (a b: t_Array t (mk_usize 32))
         (j:usize{v j < 32}) =
@@ -662,8 +701,6 @@ let modifies1_32 #t
 let modifies2_32 #t
         (a b: t_Array t (mk_usize 32))
         (i j:(n:usize{v n < 32})) =
-    // TODO: find some way to expand this from a smaller spec, e.g.:
-    // normalize_term (Spec.Utils.forall32 (fun x -> v j <> x ==> Seq.index a x == Seq.index b x))
     ((v i <> 0  /\ v j <> 0)  ==> Seq.index a 0 == Seq.index b 0) /\
     ((v i <> 1  /\ v j <> 1)  ==> Seq.index a 1 == Seq.index b 1) /\
     ((v i <> 2  /\ v j <> 2)  ==> Seq.index a 2 == Seq.index b 2) /\
@@ -700,7 +737,6 @@ let modifies2_32 #t
 let modifies_range_32 #t
         (a b: t_Array t (mk_usize 32))
         (i:usize{v i < 32}) (j:usize{v j <= 32 /\ v i <= v j}) =
-//    normalize_term (forall32 (fun k -> ((v i > k \/ k >= v j)   ==> Seq.index a k == Seq.index b k)))
     ((v i > 0 \/ 0 >= v j)   ==> Seq.index a 0 == Seq.index b 0) /\
     ((v i > 1 \/ 1 >= v j)   ==> Seq.index a 1 == Seq.index b 1) /\
     ((v i > 2 \/ 2 >= v j)   ==> Seq.index a 2 == Seq.index b 2) /\
diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs
index b14cab174..a6efa4354 100644
--- a/libcrux-ml-kem/src/ind_cca.rs
+++ b/libcrux-ml-kem/src/ind_cca.rs
@@ -805,6 +805,7 @@ pub(crate) mod unpacked {
     }
 
     #[hax_lib::fstar::options("--z3rlimit 200")]
+    #[hax_lib::fstar::before(r#"[@ "opaque_to_smt"]"#)]
     #[hax_lib::ensures(|result|
         fstar!(r#"forall (i: nat). i < v $K ==>
             (forall (j: nat). j < v $K ==>
@@ -852,7 +853,7 @@ pub(crate) mod unpacked {
 
     /// Generate Unpacked Keys
     #[inline(always)]
-    #[hax_lib::fstar::options("--z3rlimit 1500 --ext context_pruning --z3refresh")]
+    #[hax_lib::fstar::options("--z3rlimit 300 --ext context_pruning --split_queries always")]
     #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
         $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\
         $ETA1 == Spec.MLKEM.v_ETA1 $K /\
@@ -1012,7 +1013,7 @@ pub(crate) mod unpacked {
 
     // Decapsulate with Unpacked Private Key
     #[inline(always)]
-    #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning --z3refresh")]
+    #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")]
     #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
         $ETA1 == Spec.MLKEM.v_ETA1 $K /\
         $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\
diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
index 8650fcc0c..cd7f3a50a 100644
--- a/libcrux-ml-kem/src/ind_cpa.rs
+++ b/libcrux-ml-kem/src/ind_cpa.rs
@@ -127,7 +127,7 @@ pub(crate) fn serialize_public_key_mut<
 
 /// Call [`serialize_uncompressed_ring_element`] for each ring element.
 #[inline(always)]
-#[hax_lib::fstar::options("--z3rlimit 1000 --ext context_pruning --z3refresh")]
+#[hax_lib::fstar::options("--z3rlimit 1000 --ext context_pruning")]
 #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
     ${out.len()} == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\
     (forall (i:nat). i < v $K ==>
@@ -183,7 +183,7 @@ pub(crate) fn serialize_vector<const K: usize, Vector: Operations>(
 /// Sample a vector of ring elements from a centered binomial distribution.
 #[inline(always)]
 #[hax_lib::fstar::options(
-    "--max_fuel 15 --z3rlimit 1500 --ext context_pruning --z3refresh --split_queries always"
+    "--max_fuel 15 --z3rlimit 1500 --ext context_pruning --split_queries always"
 )]
 #[cfg_attr(
     hax,
@@ -301,7 +301,7 @@ fn sample_ring_element_cbd<
 /// convert them into their NTT representations.
 #[inline(always)]
 #[hax_lib::fstar::options(
-    "--max_fuel 25 --z3rlimit 2500 --ext context_pruning --z3refresh --split_queries always"
+    "--max_fuel 25 --z3rlimit 2500 --ext context_pruning --split_queries always"
 )]
 #[cfg_attr(hax, hax_lib::fstar::before(r#"let sample_vector_cbd_then_ntt_helper_2
       (v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)
@@ -450,7 +450,8 @@ fn sample_vector_cbd_then_ntt<
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
-#[hax_lib::fstar::options("--z3rlimit 500 --ext context_pruning --z3refresh")]
+#[hax_lib::fstar::before(r#"[@ "opaque_to_smt"]"#)]
+#[hax_lib::fstar::options("--z3rlimit 500 --ext context_pruning")]
 #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
     $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\
     $ETA1 == Spec.MLKEM.v_ETA1 $K /\
@@ -602,7 +603,7 @@ pub(crate) fn serialize_unpacked_secret_key<
 }
 
 /// Call [`compress_then_serialize_ring_element_u`] on each ring element.
-#[hax_lib::fstar::options("--z3rlimit 1500 --ext context_pruning --z3refresh")]
+#[hax_lib::fstar::options("--z3rlimit 1500 --ext context_pruning")]
 #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
     $OUT_LEN == Spec.MLKEM.v_C1_SIZE $K /\
     $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\
@@ -706,7 +707,7 @@ fn compress_then_serialize_u<
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
-#[hax_lib::fstar::options("--z3rlimit 800 --ext context_pruning --z3refresh")]
+#[hax_lib::fstar::options("--z3rlimit 800 --ext context_pruning")]
 #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
       $ETA1 == Spec.MLKEM.v_ETA1 $K /\
       $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\
diff --git a/libcrux-ml-kem/src/vector/portable/compress.rs b/libcrux-ml-kem/src/vector/portable/compress.rs
index b5739636d..c4be0130b 100644
--- a/libcrux-ml-kem/src/vector/portable/compress.rs
+++ b/libcrux-ml-kem/src/vector/portable/compress.rs
@@ -25,6 +25,7 @@ use libcrux_secrets::*;
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")]
+#[hax_lib::fstar::before(r#"[@ "opaque_to_smt"]"#)]
 #[cfg_attr(hax, hax_lib::requires(fe < (FIELD_MODULUS as u16)))]
 #[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"((833 <= v fe && v fe <= 2496) ==> v result == 1) /\
 						    (~(833 <=  v fe && v fe <= 2496) ==> v result == 0)"#)))]
@@ -93,6 +94,7 @@ pub(crate) fn compress_message_coefficient(fe: U16) -> U8 {
 }
 
 #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")]
+#[hax_lib::fstar::before(r#"[@ "opaque_to_smt"]"#)]
 #[cfg_attr(hax,
     hax_lib::requires(
         (coefficient_bits == 4 ||
@@ -102,7 +104,7 @@ pub(crate) fn compress_message_coefficient(fe: U16) -> U8 {
          fe < (FIELD_MODULUS as u16)))]
 #[cfg_attr(hax,
      hax_lib::ensures(
-     |result| result >= 0 && result < 2i16.pow(coefficient_bits as u32)))]
+     |result| fstar!(r#"v result >= 0 && v result < pow2 (v $coefficient_bits)"#)))]
 pub(crate) fn compress_ciphertext_coefficient(coefficient_bits: u8, fe: U16) -> FieldElement {
     // hax_debug_assert!(
     //     coefficient_bits == 4
@@ -137,7 +139,7 @@ let compress_message_coefficient_range_helper (fe: u16) : Lemma
 "#
     )
 )]
-#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 2000")]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 200")]
 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 16 ==> v (Seq.index ${a}.f_elements i) >= 0 /\
     v (Seq.index ${a}.f_elements i) < 3329"#))]
 #[hax_lib::ensures(|result| fstar!(r#"forall (i:nat). i < 16 ==> 
@@ -180,16 +182,17 @@ pub(crate) fn compress_1(mut a: PortableVector) -> PortableVector {
 }
 
 #[inline(always)]
-#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 2000")]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 500")]
 #[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/
         v $COEFFICIENT_BITS == 5 \/
         v $COEFFICIENT_BITS == 10 \/
         v $COEFFICIENT_BITS == 11) /\
-    (forall (i:nat). i < 16 ==> v (Seq.index ${a}.f_elements i) >= 0 /\
-        v (Seq.index ${a}.f_elements i) < 3329)"#))]
+    (forall (i:nat). i < 16 ==> 
+        (v (Seq.index ${a}.f_elements i) >= 0 /\
+         v (Seq.index ${a}.f_elements i) < 3329))"#))]
 #[hax_lib::ensures(|result| fstar!(r#"forall (i:nat). i < 16 ==> 
-    v (${result}.f_elements.[ sz i ] <: i16) >= 0 /\
-    v (${result}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS))"#))]
+    (v (${result}.f_elements.[ sz i ] <: i16) >= 0 /\
+     v (${result}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS)))"#))]
 pub(crate) fn compress<const COEFFICIENT_BITS: i32>(mut a: PortableVector) -> PortableVector {
     hax_lib::fstar!(
         "assert (v (cast ($COEFFICIENT_BITS) <: u8) == v $COEFFICIENT_BITS);
@@ -197,17 +200,18 @@ pub(crate) fn compress<const COEFFICIENT_BITS: i32>(mut a: PortableVector) -> Po
         assert (v (cast ($FIELD_MODULUS) <: u16) == 3329)"
     );
     hax_lib::fstar!(
-        "assert (forall (i:nat). i < 16 ==> (cast (${a}.f_elements.[ sz i ]) <: u16) <.
-        (cast ($FIELD_MODULUS) <: u16))"
+        "assert (forall (i:nat). i < 16 ==> 
+            (cast (${a}.f_elements.[ sz i ]) <: u16) <.
+            (cast ($FIELD_MODULUS) <: u16))"
     );
 
     for i in 0..FIELD_ELEMENTS_IN_VECTOR {
         hax_lib::loop_invariant!(|i: usize| {
             fstar!(
-                r#"(v $i < 16 ==> (forall (j:nat). (j >= v $i /\ j < 16) ==>
-            v (cast (${a}.f_elements.[ sz j ]) <: u16) < v (cast ($FIELD_MODULUS) <: u16))) /\
-            (forall (j:nat). j < v $i ==> v (${a}.f_elements.[ sz j ] <: i16) >= 0 /\
-                v (${a}.f_elements.[ sz j ] <: i16) < pow2 (v (cast ($COEFFICIENT_BITS) <: u32)))"#
+                r#"((forall (j:nat). (j >= v $i /\ j < 16) ==>
+                      v (cast (${a}.f_elements.[ sz j ]) <: u16) < v (cast ($FIELD_MODULUS) <: u16))) /\
+                    (forall (j:nat). j < v $i ==> v (${a}.f_elements.[ sz j ] <: i16) >= 0 /\
+                     v (${a}.f_elements.[ sz j ] <: i16) < pow2 (v $COEFFICIENT_BITS)))"#
             )
         });
 
@@ -217,12 +221,13 @@ pub(crate) fn compress<const COEFFICIENT_BITS: i32>(mut a: PortableVector) -> Po
 
         hax_lib::fstar!(
             r#"assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\
-            v (${a}.f_elements.[ $i ] <: i16) < pow2 (v (cast ($COEFFICIENT_BITS) <: u32)))"#
+            v (${a}.f_elements.[ $i ] <: i16) < pow2 (v $COEFFICIENT_BITS))"#
         );
     }
     hax_lib::fstar!(
-        r#"assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\
-        v (${a}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS))"#
+        r#"assert (forall (i:nat). i < 16 ==> 
+                    (v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\
+                     v (${a}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS)))"#
     );
 
     a
diff --git a/libcrux-ml-kem/src/vector/portable/ntt.rs b/libcrux-ml-kem/src/vector/portable/ntt.rs
index d3b03ec01..43765462b 100644
--- a/libcrux-ml-kem/src/vector/portable/ntt.rs
+++ b/libcrux-ml-kem/src/vector/portable/ntt.rs
@@ -3,7 +3,7 @@ use super::vector_type::*;
 use libcrux_secrets::*;
 
 #[inline(always)]
-#[hax_lib::fstar::before(interface, "[@@ \"opaque_to_smt\"]")]
+#[hax_lib::fstar::before("[@@ \"opaque_to_smt\"]")]
 #[hax_lib::requires(fstar!(r#"v i < 16 /\ v j < 16 /\ v i <> v j /\ 
                             Spec.Utils.is_i16b 1664 $zeta  /\
                             Spec.Utils.is_i16b_array (11207 + 6 * 3328) vec.f_elements /\
@@ -118,7 +118,7 @@ pub(crate) fn ntt_layer_3_step(mut vec: PortableVector, zeta: i16) -> PortableVe
 }
 
 #[inline(always)]
-#[hax_lib::fstar::before(interface, "[@@ \"opaque_to_smt\"]")]
+#[hax_lib::fstar::before("[@@ \"opaque_to_smt\"]")]
 #[hax_lib::requires(fstar!(r#"v i < 16 /\ v j < 16 /\  v i <> v j /\ 
                         Spec.Utils.is_i16b 1664 $zeta /\
                         Spec.Utils.is_i16b_array (4*3328) ${vec}.f_elements"#))]
@@ -267,23 +267,33 @@ pub(crate) fn inv_ntt_layer_3_step(mut vec: PortableVector, zeta: i16) -> Portab
 #[hax_lib::fstar::options(
     "--z3rlimit 250 --split_queries always --query_stats --ext context_prune"
 )]
-#[hax_lib::fstar::before(interface, "[@@ \"opaque_to_smt\"]")]
+#[hax_lib::fstar::before(
+    interface,
+    r#"
+    let ntt_multiply_binomials_post
+      (a b: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+      (zeta: i16)
+      (i: usize{v i < 8})
+      (out_future: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+            let ai = Seq.index a.f_elements (2 * v i) in
+            let aj = Seq.index a.f_elements (2 * v i + 1) in
+            let bi = Seq.index b.f_elements (2 * v i) in
+            let bj = Seq.index b.f_elements (2 * v i + 1) in
+            let oi = Seq.index out_future.f_elements (2 * v i) in
+            let oj = Seq.index out_future.f_elements (2 * v i + 1) in
+            ((v oi % 3329) == (((v ai * v bi + (v aj * v bj * v zeta * 169)) * 169) % 3329)) /\
+            ((v oj % 3329) == (((v ai * v bj + v aj * v bi) * 169) % 3329))
+"#
+)]
+#[hax_lib::fstar::before("[@@ \"opaque_to_smt\"]")]
 #[hax_lib::requires(fstar!(r#"v i < 8 /\ Spec.Utils.is_i16b 1664 $zeta /\
         Spec.Utils.is_i16b_array 3328 ${a}.f_elements /\
         Spec.Utils.is_i16b_array 3328 ${b}.f_elements /\
         Spec.Utils.is_i16b_array 3328 ${out}.f_elements "#))]
 #[hax_lib::ensures(|()| fstar!(r#"
         Spec.Utils.is_i16b_array 3328 ${out}_future.f_elements /\
-        (forall k. (k <> 2 * v $i /\ k <> 2 * v $i + 1) ==> 
-                    Seq.index ${out}_future.f_elements k == Seq.index ${out}.f_elements k) /\                 
-        (let ai = Seq.index ${a}.f_elements (2 * v $i) in
-         let aj = Seq.index ${a}.f_elements (2 * v $i + 1) in
-         let bi = Seq.index ${b}.f_elements (2 * v $i) in
-         let bj = Seq.index ${b}.f_elements (2 * v $i + 1) in
-         let oi = Seq.index out_future.f_elements (2 * v $i) in
-         let oj = Seq.index out_future.f_elements (2 * v $i + 1) in
-         ((v oi % 3329) == (((v ai * v bi + (v aj * v bj * v zeta * 169)) * 169) % 3329)) /\
-         ((v oj % 3329) == (((v ai * v bj + v aj * v bi) * 169) % 3329)))"#))]
+        Spec.Utils.modifies2_16 ${out}.f_elements ${out}_future.f_elements (sz 2 *! $i) ((sz 2 *! $i) +! sz 1) /\
+        ntt_multiply_binomials_post ${a} ${b} ${zeta} ${i} ${out}_future"#))]
 pub(crate) fn ntt_multiply_binomials(
     a: &PortableVector,
     b: &PortableVector,
@@ -400,24 +410,33 @@ pub(crate) fn ntt_multiply_binomials(
 }
 
 #[inline(always)]
-#[hax_lib::fstar::options("--z3rlimit 1000")]
+#[hax_lib::fstar::options("--z3rlimit 800 --split_queries always")]
 #[hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b 1664 $zeta0 /\
         Spec.Utils.is_i16b 1664 $zeta1 /\
         Spec.Utils.is_i16b 1664 $zeta2 /\
         Spec.Utils.is_i16b 1664 $zeta3 /\
         Spec.Utils.is_i16b_array 3328 ${lhs}.f_elements /\
         Spec.Utils.is_i16b_array 3328 ${rhs}.f_elements "#))]
-#[hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array 3328 ${result}.f_elements /\
-          (let zetas = Seq.seq_of_list [v zeta0; - v zeta0; v zeta1; - v zeta1; v zeta2; - v zeta2; v zeta3; - v zeta3] in
-          (forall (i:nat). i < 8 ==>
-           (let ai = Seq.index lhs.f_elements (2 * i) in
-            let aj = Seq.index lhs.f_elements (2 * i + 1) in
-            let bi = Seq.index rhs.f_elements (2 * i) in
-            let bj = Seq.index rhs.f_elements (2 * i + 1) in
-            let oi = Seq.index result.f_elements (2 * i) in
-            let oj = Seq.index result.f_elements (2 * i + 1) in
-            ((v oi % 3329) == (((v ai * v bi + (v aj * v bj * (Seq.index zetas i) * 169)) * 169) % 3329)) /\
-            ((v oj % 3329) == (((v ai * v bj + v aj * v bi) * 169) % 3329)))))"#))]
+#[hax_lib::ensures(|result| fstar!(r#"
+        Spec.Utils.is_i16b_array 3328 ${result}.f_elements /\
+        (let nzeta0:i16 = Core.Ops.Arith.f_neg zeta0 in
+         let nzeta1:i16 = Core.Ops.Arith.f_neg zeta1 in
+         let nzeta2:i16 = Core.Ops.Arith.f_neg zeta2 in
+         let nzeta3:i16 = Core.Ops.Arith.f_neg zeta3 in
+         let zetas =
+            Seq.seq_of_list [
+                zeta0;
+                nzeta0;
+                zeta1;
+                nzeta1;
+                zeta2;
+                nzeta2;
+                zeta3;
+                nzeta3
+            ]
+         in
+         Spec.Utils.forall8 (fun i -> ntt_multiply_binomials_post ${lhs} ${rhs} (Seq.index zetas i) (sz i) $result))
+"#))]
 pub(crate) fn ntt_multiply(
     lhs: &PortableVector,
     rhs: &PortableVector,