From 3631be66363899bc6fd65542f46c83ce852075f6 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Mon, 23 Sep 2024 11:17:53 +0200 Subject: [PATCH] removed typeclass _super constraint --- .../Libcrux_ml_kem.Vector.Traits.fst | 14 ++++---------- .../Libcrux_ml_kem.Vector.Traits.fsti | 8 ++++---- libcrux-ml-kem/src/vector/traits.rs | 18 +++++++++--------- 3 files changed, 17 insertions(+), 23 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 1c6967d6d..485013065 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 @@ -11,25 +11,19 @@ let decompress_1_ (vec: v_T) = let z:v_T = f_ZERO #v_T #FStar.Tactics.Typeclasses.solve () in - let _:Prims.unit = - assert (forall i. Seq.index (i1._super_8706949974463268012.f_repr z) i == 0s) - in + let _:Prims.unit = assert (forall i. Seq.index (i1.f_repr z) i == 0s) in let _:Prims.unit = assert (forall i. - let x = Seq.index (i1._super_8706949974463268012.f_repr vec) i in + let x = Seq.index (i1.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))) + i < 16 ==> Spec.Utils.is_intb (pow2 15 - 1) (0 - v (Seq.index (i1.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 == (-1s)) + assert (forall i. Seq.index (i1.f_repr s) i == 0s \/ Seq.index (i1.f_repr s) i == (-1s)) in 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 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 e5599b2b3..0a54ddd5f 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 @@ -399,7 +399,7 @@ val decompress_1_ (#v_T: Type0) {| i1: t_Operations v_T |} (vec: v_T) : Prims.Pure v_T (requires forall i. - let x = Seq.index (i1._super_8706949974463268012.f_repr vec) i in + let x = Seq.index (i1.f_repr vec) i in (x == 0s \/ x == 1s)) (fun _ -> Prims.l_True) @@ -411,11 +411,11 @@ 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)) + (requires Spec.Utils.is_i16b_array 3328 (i1.f_repr a)) (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 + (let x = Seq.index (i1.f_repr a) i in + let y = Seq.index (i1.f_repr result) i in (v y >= 0 /\ v y <= 3328 /\ (v y % 3329 == v x % 3329)))) diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index aa0434e85..6cff1d585 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -214,10 +214,10 @@ pub fn to_standard_domain(v: T) -> T { #[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::requires(fstar!("Spec.Utils.is_i16b_array 3328 (i1.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 + (let x = Seq.index (i1.f_repr ${a}) i in + let y = Seq.index (i1.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); @@ -226,20 +226,20 @@ pub fn to_unsigned_representative(a: T) -> T { } #[hax_lib::fstar::options("--z3rlimit 100")] -#[hax_lib::requires(fstar!("forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in +#[hax_lib::requires(fstar!("forall i. let x = Seq.index (i1.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 + hax_lib::fstar!("assert(forall i. Seq.index (i1.f_repr ${z}) i == 0s)"); + hax_lib::fstar!("assert(forall i. let x = Seq.index (i1.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)))"); + (0 - v (Seq.index (i1.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(forall i. Seq.index (i1.f_repr ${s}) i == 0s \\/ + Seq.index (i1.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); res