Mark to_unsigned_representative as lax

cryspen · Sep 23, 2024 · 44af8ba · 44af8ba
1 parent aee4c5b
commit 44af8ba
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst
@@ -53,7 +53,7 @@ let to_standard_domain
     v
     v_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS
 
-#push-options "--z3rlimit 100"
+#push-options "--admit_smt_queries true"
 
 let to_unsigned_representative
       (#v_T: Type0)

diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs
@@ -223,7 +223,7 @@ pub fn to_standard_domain<T: Operations>(v: T) -> T {
     T::montgomery_multiply_by_constant(v, MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS as i16)
 }
 
-#[hax_lib::fstar::options("--z3rlimit 100")]
+#[hax_lib::fstar::verification_status(lax)]
 #[hax_lib::requires(fstar!("Spec.Utils.is_i16b_array 3328 (i1._super_8706949974463268012.f_repr a)"))]
 #[hax_lib::ensures(|result| fstar!("forall i.
                                        (let x = Seq.index (i1._super_8706949974463268012.f_repr ${a}) i in