Skip to content

Commit

Permalink
hiding ghost state needed only in proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@karthikbhargavan
karthikbhargavan committed Feb 2, 2025
1 parent 0180398 commit 122f914
Show file tree
Hide file tree
Showing 6 changed files with 22 additions and 19 deletions.
2 changes: 1 addition & 1 deletion libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fst
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Libcrux_intrinsics.Arm64_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
open Core
open FStar.Mul

Expand Down
2 changes: 1 addition & 1 deletion libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Libcrux_intrinsics.Arm64_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
open Core
open FStar.Mul

Expand Down
2 changes: 1 addition & 1 deletion libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fst
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Libcrux_intrinsics.Avx2_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
open Core
open FStar.Mul

Expand Down
2 changes: 1 addition & 1 deletion libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Libcrux_intrinsics.Avx2_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
open Core
open FStar.Mul

Expand Down
29 changes: 14 additions & 15 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Arithmetic.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ let _ =
#push-options "--z3rlimit 150"

let add (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) =
let v__lhs0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
let e_lhs0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
Core.Clone.f_clone #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients
#FStar.Tactics.Typeclasses.solve
lhs
Expand All @@ -29,8 +29,8 @@ let add (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) =
(forall j.
j < v i ==>
(Seq.index lhs.f_values j) ==
(Seq.index v__lhs0.f_values j) +! (Seq.index rhs.f_values j)) /\
(forall j. j >= v i ==> (Seq.index lhs.f_values j) == (Seq.index v__lhs0.f_values j)))
(Seq.index e_lhs0.f_values j) +! (Seq.index rhs.f_values j)) /\
(forall j. j >= v i ==> (Seq.index lhs.f_values j) == (Seq.index e_lhs0.f_values j)))
lhs
(fun lhs i ->
let lhs:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = lhs in
Expand All @@ -56,7 +56,7 @@ let add (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) =
let _:Prims.unit =
assert (forall i.
v (Seq.index lhs.f_values i) ==
v (Seq.index v__lhs0.f_values i) + v (Seq.index rhs.f_values i))
v (Seq.index e_lhs0.f_values i) + v (Seq.index rhs.f_values i))
in
lhs

Expand All @@ -65,7 +65,7 @@ let add (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) =
#push-options "--z3rlimit 150"

let subtract (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) =
let v__lhs0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
let e_lhs0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
Core.Clone.f_clone #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients
#FStar.Tactics.Typeclasses.solve
lhs
Expand All @@ -82,8 +82,8 @@ let subtract (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients)
(forall j.
j < v i ==>
(Seq.index lhs.f_values j) ==
(Seq.index v__lhs0.f_values j) -! (Seq.index rhs.f_values j)) /\
(forall j. j >= v i ==> (Seq.index lhs.f_values j) == (Seq.index v__lhs0.f_values j)))
(Seq.index e_lhs0.f_values j) -! (Seq.index rhs.f_values j)) /\
(forall j. j >= v i ==> (Seq.index lhs.f_values j) == (Seq.index e_lhs0.f_values j)))
lhs
(fun lhs i ->
let lhs:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = lhs in
Expand All @@ -109,7 +109,7 @@ let subtract (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients)
let _:Prims.unit =
assert (forall i.
v (Seq.index lhs.f_values i) ==
v (Seq.index v__lhs0.f_values i) - v (Seq.index rhs.f_values i))
v (Seq.index e_lhs0.f_values i) - v (Seq.index rhs.f_values i))
in
lhs

Expand Down Expand Up @@ -246,7 +246,7 @@ let montgomery_multiply_by_constant
(simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients)
(c: i32)
=
let v__simd_unit0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
let e_simd_unit0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
Core.Clone.f_clone #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients
#FStar.Tactics.Typeclasses.solve
simd_unit
Expand All @@ -265,10 +265,9 @@ let montgomery_multiply_by_constant
(let vecj = Seq.index simd_unit.f_values j in
(Spec.Utils.is_i32b 8380416 vecj /\
v vecj % 8380417 ==
(v (Seq.index v__simd_unit0.f_values j) * v c * 8265825) % 8380417))) /\
(v (Seq.index e_simd_unit0.f_values j) * v c * 8265825) % 8380417))) /\
(forall j.
j >= v i ==> (Seq.index simd_unit.f_values j) == (Seq.index v__simd_unit0.f_values j))
)
j >= v i ==> (Seq.index simd_unit.f_values j) == (Seq.index e_simd_unit0.f_values j)))
simd_unit
(fun simd_unit i ->
let simd_unit:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = simd_unit in
Expand Down Expand Up @@ -305,7 +304,7 @@ let montgomery_multiply_by_constant
#push-options "--z3rlimit 150"

let montgomery_multiply (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) =
let v__lhs0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
let e_lhs0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
Core.Clone.f_clone #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients
#FStar.Tactics.Typeclasses.solve
lhs
Expand All @@ -324,9 +323,9 @@ let montgomery_multiply (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coe
(let vecj = Seq.index lhs.f_values j in
(Spec.Utils.is_i32b 8380416 vecj /\
v vecj % 8380417 ==
(v (Seq.index v__lhs0.f_values j) * v (Seq.index rhs.f_values j) * 8265825) %
(v (Seq.index e_lhs0.f_values j) * v (Seq.index rhs.f_values j) * 8265825) %
8380417))) /\
(forall j. j >= v i ==> (Seq.index lhs.f_values j) == (Seq.index v__lhs0.f_values j)))
(forall j. j >= v i ==> (Seq.index lhs.f_values j) == (Seq.index e_lhs0.f_values j)))
lhs
(fun lhs i ->
let lhs:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = lhs in
Expand Down
4 changes: 4 additions & 0 deletions libcrux-ml-dsa/src/simd/portable/arithmetic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ pub(crate) const MONTGOMERY_SHIFT: u8 = 32;
(v (Seq.index ${lhs}_future.f_values i) ==
v (Seq.index ${lhs}.f_values i) + v (Seq.index ${rhs}.f_values i))"#))]
pub fn add(lhs: &mut Coefficients, rhs: &Coefficients) {
#[cfg(hax)]
let _lhs0 = lhs.clone();
for i in 0..lhs.values.len() {
hax_lib::loop_invariant!(|i: usize| {
Expand All @@ -42,6 +43,7 @@ pub fn add(lhs: &mut Coefficients, rhs: &Coefficients) {
(v (Seq.index ${lhs}_future.f_values i) ==
v (Seq.index ${lhs}.f_values i) - v (Seq.index ${rhs}.f_values i))"#))]
pub fn subtract(lhs: &mut Coefficients, rhs: &Coefficients) {
#[cfg(hax)]
let _lhs0 = lhs.clone();
for i in 0..lhs.values.len() {
hax_lib::loop_invariant!(|i: usize| {
Expand Down Expand Up @@ -198,6 +200,7 @@ Spec.Utils.is_i32b_array 8380416 ${simd_unit}_future.f_values /\
(v (Seq.index ${simd_unit}_future.f_values i) % 8380417 ==
(v (Seq.index ${simd_unit}.f_values i) * v $c * 8265825) % 8380417))"#))]
pub(crate) fn montgomery_multiply_by_constant(simd_unit: &mut Coefficients, c: i32) {
#[cfg(hax)]
let _simd_unit0 = simd_unit.clone();
for i in 0..simd_unit.values.len() {
hax_lib::loop_invariant!(|i: usize| {
Expand Down Expand Up @@ -227,6 +230,7 @@ Spec.Utils.is_i32b_array 8380416 ${lhs}_future.f_values /\
(v (Seq.index ${lhs}_future.f_values i) % 8380417 ==
(v (Seq.index ${lhs}.f_values i) * v (Seq.index ${rhs}.f_values i) * 8265825) % 8380417))"#))]
pub(crate) fn montgomery_multiply(lhs: &mut Coefficients, rhs: &Coefficients) {
#[cfg(hax)]
let _lhs0 = lhs.clone();
for i in 0..lhs.values.len() {
hax_lib::loop_invariant!(|i: usize| {
Expand Down

0 comments on commit 122f914

Please sign in to comment.