Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ToBytes proved for both ref4 and mulx #31

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

ToBytes proved for both ref4 and mulx #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
097d3a2
ToBytes proved for both ref4 and mulx
JoaoDiogoDuarte Jan 4, 2025
b8830b2
Formatting fixes and added missing file
JoaoDiogoDuarte Jan 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 53 additions & 6 deletions proof/crypto_scalarmult/curve25519/amd64/mulx/CorrectnessProof_Mulx.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
require import Real Bool Int IntDiv.
from Jasmin require import JModel.
require import CorrectnessProof_Ref4 Curve25519_Procedures Ref4_scalarmult_s Mulx_scalarmult_s Zp_limbs Zp_25519.
require import CorrectnessProof_Ref4 Curve25519_Procedures Ref4_scalarmult_s Mulx_scalarmult_s Zp_limbs Zp_25519 CorrectnessProof_ToBytes.

import Zp Ring.IntID.

Expand Down Expand Up @@ -343,14 +343,61 @@ qed.
equiv eq_spec_impl_to_bytes_mulx : Ref4_scalarmult_s.M.__tobytes4 ~ Mulx_scalarmult_s.M.__tobytes4 :
={f} ==> ={res} by sim.

lemma h_to_bytes_mulx r:
hoare [M.__tobytes4 :
r = f
lemma equiv_to_bytes_mulx :
equiv[Mulx_scalarmult_s.M.__tobytes4 ~ ToBytesSpec.to_bytes :
f{1} = f{2}
==>
pack4 (to_list res) = (W256.of_int (asint (inzpRep4 r)))
valRep4 res{1} = valRep4 res{2}
].
proof.
symmetry.
transitivity
Ref4_scalarmult_s.M.__tobytes4
(={arg} ==> valRep4 res{1} = valRep4 res{2})
(={arg} ==> valRep4 res{1} = valRep4 res{2}). smt(). smt().
symmetry. proc *. call equiv_to_bytes. auto => />. smt().
proc *. call eq_spec_impl_to_bytes_mulx. auto => />.
qed.

lemma h_to_bytes_mulx _f:
hoare [Mulx_scalarmult_s.M.__tobytes4 :
_f = f
==>
pack4 (to_list res) = (W256.of_int (asint (inzpRep4 _f)))
].
proof.
admit.
have E: 0 <= valRep4 _f < W256.modulus. apply valRep4_cmp.
case (0 <= valRep4 _f < p) => C1.
conseq equiv_to_bytes_mulx (: _f = arg /\ 0 <= valRep4 _f < p ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_no_reduction _f).

case (p <= valRep4 _f < exp 2 255) => C2.
conseq equiv_to_bytes_mulx (: _f = arg /\ p <= valRep4 _f < exp 2 255 ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. exists _f. move: C2. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_cminusP_part1 _f).

case (exp 2 255 <= valRep4 _f < 2*p) => C3.
conseq equiv_to_bytes_mulx (: _f = arg /\ exp 2 255 <= valRep4 _f < 2*p ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. exists _f. move: C3. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_cminusP_part2 _f).

case (2*p <= valRep4 _f < W256.modulus) => C4.
conseq equiv_to_bytes_mulx (: _f = arg /\ 2*p <= valRep4 _f < W256.modulus ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. exists _f. move: C4. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_cminus2P _f). smt().
qed.

lemma ill_to_bytes_mulx : islossless M.__tobytes4 by islossless.
Expand Down
46 changes: 38 additions & 8 deletions proof/crypto_scalarmult/curve25519/amd64/ref4/CorrectnessProof_Ref4.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
require import Real Bool Int IntDiv.
from Jasmin require import JModel.
require import Curve25519_Procedures Ref4_scalarmult_s Zp_limbs Zp_25519.
from Jasmin require import JModel JUtils.
require import Curve25519_Procedures Ref4_scalarmult_s Zp_limbs Zp_25519 CorrectnessProof_ToBytes.

import Zp Ring.IntID.

Expand Down Expand Up @@ -448,15 +448,45 @@ proof.
qed.

(** to bytes **)
lemma h_to_bytes_ref4 r:
lemma h_to_bytes_ref4 _f:
hoare [M.__tobytes4 :
r = f
_f = f
==>
pack4 (to_list res) = (W256.of_int (asint (inzpRep4 r)))
pack4 (to_list res) = (W256.of_int (asint (inzpRep4 _f)))
].
proof.
proc.
admit.
have E: 0 <= valRep4 _f < W256.modulus. apply valRep4_cmp.
case (0 <= valRep4 _f < p) => C1.
conseq equiv_to_bytes (: _f = arg /\ 0 <= valRep4 _f < p ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_no_reduction _f).

case (p <= valRep4 _f < exp 2 255) => C2.
conseq equiv_to_bytes (: _f = arg /\ p <= valRep4 _f < exp 2 255 ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. exists _f. move: C2. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_cminusP_part1 _f).

case (exp 2 255 <= valRep4 _f < 2*p) => C3.
conseq equiv_to_bytes (: _f = arg /\ exp 2 255 <= valRep4 _f < 2*p ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. exists _f. move: C3. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_cminusP_part2 _f).

case (2*p <= valRep4 _f < W256.modulus) => C4.
conseq equiv_to_bytes (: _f = arg /\ 2*p <= valRep4 _f < W256.modulus ==>
(valRep4 res = asint (inzpRep4 _f))).
move => &1 [#] H. exists _f. move: C4. smt().
move => &1 &2 [#] H [#] H0. move: H. rewrite !H0. move => H1.
rewrite -H1 valRep4ToPack to_uintK //=.
apply (h_to_bytes_cminus2P _f). smt().
qed.

lemma ill_to_bytes_ref4 : islossless M.__tobytes4 by islossless.
Expand Down Expand Up @@ -639,7 +669,7 @@ proof.
rewrite (W64.and_mod 3 ctr{2}) //= (W64.and_mod 6 (of_int (to_uint ctr{2} %% 8))%W64) //= !to_uint_shr //= !shr_shrw.
smt(W64.to_uint_cmp W64.of_uintK W64.to_uintK).
rewrite /zeroextu64 /truncateu8 //= !of_uintK => />.
+ rewrite of_intE modz_small. apply bound_abs. smt(W8.to_uint_cmp JUtils.powS_minus JUtils.pow2_0).
+ rewrite of_intE modz_small. apply bound_abs. smt(W8.to_uint_cmp JUtils.powS_minus JUtils.pow2_0).
rewrite bits2wE /int2bs /mkseq -iotaredE => />.
auto => />.
rewrite (modz_small (to_uint ctr{2} %% 8) W64.modulus). apply bound_abs. smt(W64.to_uint_cmp).
Expand Down
Loading
Loading