From 44af8bab271322d2ad322d9a703b62a22e168fdd Mon Sep 17 00:00:00 2001 From: mamonet Date: Mon, 23 Sep 2024 09:47:34 +0000 Subject: [PATCH] Mark to_unsigned_representative as lax --- .../proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst | 2 +- libcrux-ml-kem/src/vector/traits.rs | 2 +- 2 files changed, 2 insertions(+), 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 index 5557ab9f0..31c67d6b2 100644 --- 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 index 8239a12db..2ee7d1667 100644 --- 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(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