traits

cryspen · Jan 27, 2025 · c958fae · c958fae
1 parent 0cf3560
commit c958fae
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 0 deletions.
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
@@ -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
@@ -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
@@ -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
@@ -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 ==>