Skip to content

Commit

Permalink
removed typeclass _super constraint
Browse files Browse the repository at this point in the history
  • Loading branch information
@karthikbhargavan
karthikbhargavan committed Sep 23, 2024
1 parent 57abb85 commit 3631be6
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 23 deletions.
14 changes: 4 additions & 10 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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))))
18 changes: 9 additions & 9 deletions libcrux-ml-kem/src/vector/traits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -214,10 +214,10 @@ pub fn to_standard_domain<T: Operations>(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<T: Operations>(a: T) -> T {
let t = T::shift_right::<15>(a);
Expand All @@ -226,20 +226,20 @@ pub fn to_unsigned_representative<T: Operations>(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<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
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
Expand Down

0 comments on commit 3631be6

Please sign in to comment.