Merge pull request #1114 from cryspen/ci-fix

karthikbhargavan · web-flow · commit 7bf2ee9bb331 · 2025-08-25T18:13:58.000Z
Fixing proofs on CI
diff --git 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
@@ -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
@@ -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
@@ -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
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/libcrux-ml-kem/src/vector/portable/ntt.rs b/libcrux-ml-kem/src/vector/portable/ntt.rs
