Merge pull request #591 from cryspen/dev-arithmetic-proofs

Making Spec proofs more robust (for new F* versions)

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti

@@ -30,7 +30,7 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
       Libcrux_ml_kem.Vector.Portable.Vector_type.to_i16_array x
   }
 
-#push-options "--z3rlimit 400"
+#push-options "--admit_smt_queries true"
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1: Libcrux_ml_kem.Vector.Traits.t_Operations

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst

@@ -3,7 +3,7 @@ module Libcrux_ml_kem.Vector.Traits
 open Core
 open FStar.Mul
 
-#push-options "--z3rlimit 50"
+#push-options "--z3rlimit 100"
 
 let decompress_1_
       (#v_T: Type0)
@@ -14,20 +14,25 @@ let decompress_1_
   let _:Prims.unit =
     assert (forall i. Seq.index (i1._super_8706949974463268012.f_repr z) i == 0s)
   in
-  let s:v_T = f_sub #v_T #FStar.Tactics.Typeclasses.solve z vec in
   let _:Prims.unit =
     assert (forall i.
-          Seq.index (i1._super_8706949974463268012.f_repr s) i == 0s \/
-          Seq.index (i1._super_8706949974463268012.f_repr s) i == (-1s))
+          let x = Seq.index (i1._super_8706949974463268012.f_repr vec) i in
+          ((0 - v x) == 0 \/ (0 - v x) == - 1))
   in
-  let _:Prims.unit = assert (i1.f_bitwise_and_with_constant_pre s 1665s) in
-  let res:v_T = f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve s 1665s in
+  let _:Prims.unit =
+    assert (forall i.
+          i < 16 ==>
+          Spec.Utils.is_intb (pow2 15 - 1)
+            (0 - v (Seq.index (i1._super_8706949974463268012.f_repr vec) i)))
+  in
+  let s:v_T = f_sub #v_T #FStar.Tactics.Typeclasses.solve z vec in
   let _:Prims.unit =
     assert (forall i.
           Seq.index (i1._super_8706949974463268012.f_repr s) i == 0s \/
-          Seq.index (i1._super_8706949974463268012.f_repr s) i == 1665s)
+          Seq.index (i1._super_8706949974463268012.f_repr s) i == (-1s))
   in
-  res
+  let _:Prims.unit = assert (i1.f_bitwise_and_with_constant_pre s 1665s) in
+  f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve s 1665s
 
 #pop-options
 
@@ -48,6 +53,10 @@ 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)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Operations v_T)
@@ -58,3 +67,7 @@ let to_unsigned_representative
     f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve t v_FIELD_MODULUS
   in
   f_add #v_T #FStar.Tactics.Typeclasses.solve a fm
+
+#pop-options
+
+#pop-options

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti

@@ -422,4 +422,10 @@ val to_standard_domain (#v_T: Type0) {| i1: t_Operations v_T |} (v: v_T)
 val to_unsigned_representative (#v_T: Type0) {| i1: t_Operations v_T |} (a: v_T)
     : Prims.Pure v_T
       (requires Spec.Utils.is_i16b_array 3328 (i1._super_8706949974463268012.f_repr a))
-      (fun _ -> Prims.l_True)
+      (ensures
+        fun result ->
+          let result:v_T = result in
+          forall i.
+            (let x = Seq.index (i1._super_8706949974463268012.f_repr a) i in
+              let y = Seq.index (i1._super_8706949974463268012.f_repr result) i in
+              (v y >= 0 /\ v y <= 3328 /\ (v y % 3329 == v x % 3329))))

libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst

@@ -1,5 +1,5 @@
 module Spec.MLKEM.Math
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 30"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 
 open FStar.Mul
 open Core
@@ -94,6 +94,7 @@ let poly_ntt_step (a:field_element) (b:field_element) (i:nat{i < 128}) =
   let a = field_add a t in
   (a,b)
 
+#push-options "--split_queries always"
 let poly_ntt_layer (p:polynomial) (l:nat{l > 0 /\ l < 8}) : polynomial =
   let len = pow2 l in
   let k = (128 / len) - 1 in
@@ -103,6 +104,7 @@ let poly_ntt_layer (p:polynomial) (l:nat{l > 0 /\ l < 8}) : polynomial =
     let (idx0, idx1) = if idx < len then (idx, idx+len) else (idx-len,idx) in
     let (a_ntt, b_ntt) = poly_ntt_step p.[sz idx0] p.[sz idx1] (round + k) in
     if idx < len then a_ntt else b_ntt)
+#pop-options
 
 val poly_ntt: polynomial -> polynomial
 let poly_ntt p =

libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst

@@ -209,9 +209,27 @@ val lemma_add_i16b (b1 b2:nat) (n1 n2:i16) :
 let lemma_add_i16b (b1 b2:nat) (n1 n2:i16) = ()
 
 
-#push-options "--z3rlimit 250"
+#push-options "--z3rlimit 100 --split_queries always"
 let lemma_range_at_percent (v:int) (p:int{p>0/\ p%2=0 /\ v < p/2 /\ v >= -p / 2}):
-  Lemma (v @% p == v) = ()
+  Lemma (v @% p == v) =
+    let m = v % p in
+    if v < 0 then (
+      Math.Lemmas.lemma_mod_plus v 1 p;
+      assert ((v + p) % p == v % p);
+      assert (v + p >= 0);
+      assert (v + p < p);
+      Math.Lemmas.modulo_lemma (v+p) p;
+      assert (m == v + p);
+      assert (m >= p/2);
+      assert (v @% p == m - p);
+      assert (v @% p == v))
+    else (
+      assert (v >= 0 /\ v < p);
+      Math.Lemmas.modulo_lemma v p;
+      assert (v % p == v);
+      assert (m < p/2);
+      assert (v @% p == v)
+    )
 #pop-options
 
 val lemma_sub_i16b (b1 b2:nat) (n1 n2:i16) :
@@ -235,9 +253,22 @@ let mont_red_i32 (x:i32) : i16 =
   let vhigh = cast (x >>! 16l) <: i16 in
   vhigh -. k_times_modulus
 
-#push-options "--z3rlimit 250"
+#push-options "--z3rlimit 100"
 let lemma_at_percent_mod (v:int) (p:int{p>0/\ p%2=0}):
-  Lemma ((v @% p) % p == v % p) = ()
+  Lemma ((v @% p) % p == v % p) =
+  let m = v % p in
+  assert (m >= 0 /\ m < p);
+  if m >= p/2 then (
+    assert ((v @%p) % p == (m - p) %p);
+    Math.Lemmas.lemma_mod_plus m (-1) p;
+    assert ((v @%p) % p == m %p);
+    Math.Lemmas.lemma_mod_mod m v p;
+    assert ((v @%p) % p == v % p)
+  ) else (
+    assert ((v @%p) % p == m%p);
+    Math.Lemmas.lemma_mod_mod m v p;
+    assert ((v @%p) % p == v % p)
+  ) 
 #pop-options
 
 let lemma_div_at_percent (v:int) (p:int{p>0/\ p%2=0 /\ (v/p) < p/2 /\ (v/p) >= -p / 2}):
@@ -412,9 +443,9 @@ let barrett_red (x:i16) =
   x -. qm
 
 let lemma_barrett_red (x:i16) : Lemma
-   (requires (Spec.Utils.is_i16b 28296 x))
+   (requires (is_i16b 28296 x))
    (ensures (let result = barrett_red x in
-             Spec.Utils.is_i16b 3328 result /\
+             is_i16b 3328 result /\
              v result % 3329 == v x % 3329)) 
    [SMTPat (barrett_red x)]
    = admit()
@@ -431,3 +462,9 @@ let lemma_cond_sub x:
         [SMTPat (cond_sub x)]
   = admit()
 
+
+let lemma_shift_right_15_i16 (x:i16):
+  Lemma (if v x >= 0 then (x >>! 15l) == 0s else (x >>! 15l) == -1s) =
+  Rust_primitives.Integers.mk_int_v_lemma #i16_inttype 0s;
+  Rust_primitives.Integers.mk_int_v_lemma #i16_inttype (-1s);
+  ()

libcrux-ml-kem/src/vector/portable.rs

@@ -22,7 +22,7 @@ impl crate::vector::traits::Repr for PortableVector {
     }
 }
 
-#[hax_lib::fstar::before(interface, r#"#push-options "--z3rlimit 200""#)]
+#[hax_lib::fstar::before(interface, r#"#push-options "--admit_smt_queries true""#)]
 #[hax_lib::fstar::after(interface, r#"#pop-options"#)]
 #[hax_lib::attributes] 
 impl Operations for PortableVector {

libcrux-ml-kem/src/vector/traits.rs

@@ -212,26 +212,36 @@ 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::verification_status(lax)]
+#[hax_lib::fstar::options("--z3rlimit 100")]
 #[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
+                                        let y = Seq.index (i1._super_8706949974463268012.f_repr ${result}) i in
+                                        (v y >= 0 /\\ v y <= 3328 /\\ (v y % 3329 == v x % 3329)))"))]
 pub fn to_unsigned_representative<T: Operations>(a: T) -> T {
     let t = T::shift_right::<15>(a);
     let fm = T::bitwise_and_with_constant(t, FIELD_MODULUS);
     T::add(a, &fm)
 }
 
-#[hax_lib::fstar::options("--z3rlimit 50")]
+#[hax_lib::fstar::options("--z3rlimit 100")]
 #[hax_lib::requires(fstar!("forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in 
                                       (x == 0s \\/ x == 1s)"))]
 pub fn decompress_1<T: Operations>(vec: T) -> T {
     let z = T::ZERO();
     hax_lib::fstar!("assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${z}) i == 0s)");
+    hax_lib::fstar!("assert(forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in 
+                                      ((0 - v x) == 0 \\/ (0 - v x) == -1))"); 
+    hax_lib::fstar!("assert(forall i. i < 16 ==>
+                                      Spec.Utils.is_intb (pow2 15 - 1) 
+                                        (0 - v (Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i)))");                               
+
     let s = T::sub(z, &vec);
     hax_lib::fstar!("assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == 0s \\/ 
                                       Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == -1s)");
     hax_lib::fstar!("assert (i1.f_bitwise_and_with_constant_pre ${s} 1665s)");
     let res = T::bitwise_and_with_constant(s, 1665);
-    hax_lib::fstar!("assert (forall i. Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == 0s \\/ 
-                                       Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == 1665s)");
     res
 }