From a0fca270d6aa1b87baad440858a9ec8bd88b14fa Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 18 Sep 2024 21:48:57 +0200 Subject: [PATCH 1/3] trait --- .../Libcrux_ml_kem.Vector.Portable.fsti | 2 +- .../Libcrux_ml_kem.Vector.Traits.fst | 17 ++++++-- .../proofs/fstar/spec/Spec.Utils.fst | 41 ++++++++++++++++--- libcrux-ml-kem/src/vector/traits.rs | 12 ++++-- 4 files changed, 59 insertions(+), 13 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti index 1ab0710b5..6800ca944 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti +++ b/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 "--z3rlimit 200" [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_1: Libcrux_ml_kem.Vector.Traits.t_Operations 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 a4328b6ad..fa3af71db 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 @@ -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,6 +14,17 @@ let decompress_1_ let _:Prims.unit = assert (forall i. Seq.index (i1._super_8706949974463268012.f_repr z) i == 0s) in + let _:Prims.unit = + assert (forall i. + 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 (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. @@ -24,8 +35,8 @@ let decompress_1_ let res:v_T = f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve s 1665s 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 res) i == 0s \/ + Seq.index (i1._super_8706949974463268012.f_repr res) i == 1665s) in res diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst index 7af93a429..cb1f38eb1 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst +++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst @@ -209,9 +209,25 @@ 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.modulo_lemma (v+p) p; + assert ((v + p) % p == v % p); + Math.Lemmas.lemma_mod_plus v 1 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 +251,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 +441,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() diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index c26d49382..6b9aa17f5 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -219,19 +219,25 @@ pub fn to_unsigned_representative(a: T) -> T { 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(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)"); + hax_lib::fstar!("assert (forall i. Seq.index (i1._super_8706949974463268012.f_repr ${res}) i == 0s \\/ + Seq.index (i1._super_8706949974463268012.f_repr ${res}) i == 1665s)"); res } From d16265c8a01d35ce78101bcc7103a9c017d64b63 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Thu, 19 Sep 2024 12:17:13 +0200 Subject: [PATCH 2/3] arith --- .../Libcrux_ml_kem.Vector.Portable.fsti | 2 +- .../extraction/Libcrux_ml_kem.Vector.Traits.fst | 16 +++++++++------- .../extraction/Libcrux_ml_kem.Vector.Traits.fsti | 8 +++++++- libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst | 12 ++++++++++-- libcrux-ml-kem/src/vector/portable.rs | 2 +- libcrux-ml-kem/src/vector/traits.rs | 8 ++++++-- 6 files changed, 34 insertions(+), 14 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti index 6800ca944..d7a0d3f21 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti +++ b/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 200" +#push-options "--admit_smt_queries true" [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_1: Libcrux_ml_kem.Vector.Traits.t_Operations 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 fa3af71db..1c6967d6d 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 @@ -32,13 +32,7 @@ let decompress_1_ Seq.index (i1._super_8706949974463268012.f_repr s) i == (-1s)) 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. - Seq.index (i1._super_8706949974463268012.f_repr res) i == 0s \/ - Seq.index (i1._super_8706949974463268012.f_repr res) i == 1665s) - in - res + f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve s 1665s #pop-options @@ -59,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) @@ -69,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 diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti index 9e1d121d7..222c69504 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti +++ b/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)))) diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst index cb1f38eb1..bfa2fcd9a 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst +++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst @@ -214,9 +214,11 @@ let lemma_range_at_percent (v:int) (p:int{p>0/\ p%2=0 /\ v < p/2 /\ v >= -p / 2} Lemma (v @% p == v) = let m = v % p in if v < 0 then ( - Math.Lemmas.modulo_lemma (v+p) p; - assert ((v + p) % p == v % p); 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); @@ -460,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); + () diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs index 65c12806c..6f9ca5d53 100644 --- a/libcrux-ml-kem/src/vector/portable.rs +++ b/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 { diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index 6b9aa17f5..32effc445 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -212,7 +212,13 @@ 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::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(a: T) -> T { let t = T::shift_right::<15>(a); let fm = T::bitwise_and_with_constant(t, FIELD_MODULUS); @@ -236,8 +242,6 @@ pub fn decompress_1(vec: T) -> T { 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 ${res}) i == 0s \\/ - Seq.index (i1._super_8706949974463268012.f_repr ${res}) i == 1665s)"); res } From 2f27e118b652d3afc053d7249ef30637f4dce816 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Thu, 19 Sep 2024 12:35:37 +0200 Subject: [PATCH 3/3] spec --- libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst index dabcb0f5c..0fba37313 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst +++ b/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 =