diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst index 6ae69f3d3..787fb7d16 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst @@ -241,6 +241,8 @@ let invert_ntt_at_layer_3_ #pop-options +#push-options "--admit_smt_queries true" + let inv_ntt_layer_int_vec_step_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -267,6 +269,8 @@ let inv_ntt_layer_int_vec_step_reduce let b:v_Vector = Libcrux_ml_kem.Vector.Traits.montgomery_multiply_fe #v_Vector a_minus_b zeta_r in a, b <: (v_Vector & v_Vector) +#pop-options + #push-options "--admit_smt_queries true" let invert_ntt_at_layer_4_plus diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst index c12f474cf..ff5e40a44 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst @@ -246,6 +246,8 @@ let ntt_at_layer_3_ #pop-options +#push-options "--admit_smt_queries true" + let ntt_layer_int_vec_step (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -269,6 +271,8 @@ let ntt_layer_int_vec_step in a, b <: (v_Vector & v_Vector) +#pop-options + #push-options "--admit_smt_queries true" let ntt_at_layer_4_plus diff --git a/libcrux-ml-kem/src/invert_ntt.rs b/libcrux-ml-kem/src/invert_ntt.rs index 29011756a..f4e6295b4 100644 --- a/libcrux-ml-kem/src/invert_ntt.rs +++ b/libcrux-ml-kem/src/invert_ntt.rs @@ -160,6 +160,7 @@ pub(crate) fn invert_ntt_at_layer_3<Vector: Operations>( } #[inline(always)] +#[hax_lib::fstar::verification_status(lax)] #[hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b 1664 $zeta_r /\ (forall i. i < 16 ==> Spec.Utils.is_intb (pow2 15 - 1) diff --git a/libcrux-ml-kem/src/ntt.rs b/libcrux-ml-kem/src/ntt.rs index a8273ac3f..2ab38bd80 100644 --- a/libcrux-ml-kem/src/ntt.rs +++ b/libcrux-ml-kem/src/ntt.rs @@ -182,6 +182,7 @@ pub(crate) fn ntt_at_layer_3<Vector: Operations>( } #[inline(always)] +#[hax_lib::fstar::verification_status(lax)] #[hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b 1664 $zeta_r /\ (let t = ${montgomery_multiply_fe::<Vector>} $b $zeta_r in (forall i. i < 16 ==>