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

Edwards point doubling for X25519 #1642

Merged
merged 6 commits into from
Sep 12, 2023
Merged

Edwards point doubling for X25519 #1642

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
a965e2f
Initial double spec and proof
bMacSwigg Aug 25, 2023
2d606ef
Rename AddPrecomputed to be more general
bMacSwigg Aug 25, 2023
6b72541
Integrate point doubling into Edwards file
bMacSwigg Aug 25, 2023
cf7377f
Add TODO in comment
bMacSwigg Aug 25, 2023
26eba55
Switch to carry_sub and complete proof
bMacSwigg Sep 8, 2023
e1bf093
Update TODO comment
bMacSwigg Sep 8, 2023
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
124 changes: 122 additions & 2 deletions src/Bedrock/End2End/X25519/AddPrecomputed.v → src/Bedrock/End2End/X25519/EdwardsXYZT.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@ Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.
Require Import Crypto.Bedrock.End2End.X25519.Field25519.
Require Import Crypto.Bedrock.Specs.Field.
Require Import Crypto.Spec.Curve25519.
Require Import Crypto.Util.Decidable.
Require Import Curves.Edwards.XYZT.Basic.
Require Import Curves.Edwards.XYZT.Precomputed.
Require Import Lia.
Require Crypto.Bedrock.Field.Synthesis.New.Signature.
Expand Down Expand Up @@ -72,8 +74,44 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2,
fe25519_mul(ot, ox, oy)
}.

(* Equivalent of m1double in src/Curves/Edwards/XYZT/Basic.v *)
(* Note: T is unused, but leaving in place in case we want to switch to a point struct in the future *)
Definition double := func! (ox, oy, oz, ot, X, Y, Z, T) {
stackalloc 40 as trX;
fe25519_square(trX, X);
stackalloc 40 as trZ;
fe25519_square(trZ, Y);
stackalloc 40 as t0;
fe25519_square(t0, Z);
stackalloc 40 as trT;
fe25519_carry_add(trT, t0, t0);
stackalloc 40 as rY;
fe25519_add(rY, X, Y);
fe25519_square(t0, rY);
stackalloc 40 as cY;
fe25519_carry_add(cY, trZ, trX);
stackalloc 40 as cZ;
fe25519_carry_sub(cZ, trZ, trX);
stackalloc 40 as cX;
fe25519_sub(cX, t0, cY);
stackalloc 40 as cT;
fe25519_sub(cT, trT, cZ);
fe25519_mul(ox, cX, cT);
fe25519_mul(oy, cY, cZ);
fe25519_mul(oz, cZ, cT);
fe25519_mul(ot, cX, cY)
}.

Section WithParameters.
Context {two_lt_M: 2 < M_pos}.
(* TODO: Can we provide actual values/proofs for these, rather than just sticking them in the context? *)
Context {char_ge_3 : (@Ring.char_ge (F M_pos) Logic.eq F.zero F.one F.opp F.add F.sub F.mul (BinNat.N.succ_pos BinNat.N.two))}.
bMacSwigg marked this conversation as resolved.
Show resolved Hide resolved
Context {field:@Algebra.Hierarchy.field (F M_pos) Logic.eq F.zero F.one F.opp F.add F.sub F.mul F.inv F.div}.
Context {a d: F M_pos}
{nonzero_a : a <> F.zero}
{square_a : exists sqrt_a, (F.mul sqrt_a sqrt_a) = a}
{nonsquare_d : forall x, (F.mul x x) <> d}.
Context {a_eq_minus1:a = F.opp F.one} {twice_d} {k_eq_2d:twice_d = (F.add d d)}.

Local Coercion F.to_Z : F >-> Z.
Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing).
Expand All @@ -83,6 +121,14 @@ Local Notation FElem := (FElem(FieldRepresentation:=frep25519)).
Local Notation bounded_by := (bounded_by(FieldRepresentation:=frep25519)).
Local Notation word := (Naive.word 32).
Local Notation felem := (felem(FieldRepresentation:=frep25519)).
Local Notation point := (point(Fzero:=F.zero)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(d:=d)).
Local Notation coordinates := (coordinates(Feq:=Logic.eq)).
Local Notation m1double :=
(m1double(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one)
(Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div)
(field:=field)(char_ge_3:=char_ge_3)(Feq_dec:=F.eq_dec)
(a:=a)(d:=d)(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)
(a_eq_minus1:=a_eq_minus1)(twice_d:=twice_d)(k_eq_2d:=k_eq_2d)).


Global Instance spec_of_add_precomputed : spec_of "add_precomputed" :=
Expand All @@ -108,12 +154,34 @@ Global Instance spec_of_add_precomputed : spec_of "add_precomputed" :=
bounded_by loose_bounds ot' /\
m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }.

Global Instance spec_of_double : spec_of "double" :=
fnspec! "double"
(oxK oyK ozK otK XK YK ZK TK : word) /
(ox oy oz ot X Y Z T : felem) (p : point) (R : _ -> Prop),
{ requires t m :=
coordinates p = ((feval X), (feval Y), (feval Z), (feval T)) /\
bounded_by tight_bounds X /\
bounded_by tight_bounds Y /\
bounded_by loose_bounds Z /\
bounded_by loose_bounds T /\
m =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TK T) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otK ot) * R;
ensures t' m' :=
t = t' /\
exists ox' oy' oz' ot',
((feval ox'), (feval oy'), (feval oz'), (feval ot')) = coordinates (@m1double p) /\
bounded_by tight_bounds ox' /\
bounded_by tight_bounds oy' /\
bounded_by tight_bounds oz' /\
bounded_by tight_bounds ot' /\
m' =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TK T) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }.


Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square.
Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul.
Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add.
Local Instance spec_of_fe25519_carry_add : spec_of "fe25519_carry_add" := Field.spec_of_BinOp bin_carry_add.
Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub.
Local Instance spec_of_fe25519_carry_sub : spec_of "fe25519_carry_sub" := Field.spec_of_BinOp bin_carry_sub.
Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word.

Local Arguments word.rep : simpl never.
Expand All @@ -122,8 +190,8 @@ Local Arguments word.unsigned : simpl never.
Local Arguments word.of_Z : simpl never.

Local Ltac cbv_bounds H :=
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds] in H;
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds].
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds] in H;
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds].

Local Ltac solve_bounds :=
repeat match goal with
Expand Down Expand Up @@ -236,4 +304,56 @@ Proof.
ecancel_assumption.
Qed.

Lemma double_ok : program_logic_goal_for_function! double.
Proof.
(* Without this, resolution of cbv stalls out Qed. *)
Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds].

(* Unwrap each call in the program. *)
(* Each binop produces 2 memory goals on the inputs, 2 bounds goals on the inputs, and 1 memory goal on the output. *)
single_step. (* fe25519_square(trX, X) *)
single_step. (* fe25519_square(trZ, Y) *)
single_step. (* fe25519_square(t0, Z) *)
single_step. (* fe25519_carry_add(trT, t0, t0) *)
single_step. (* fe25519_add(rY, X, Y) *)
single_step. (* fe25519_square(t0, rY) *)
single_step. (* fe25519_carry_add(cY, trZ, trX) *)
single_step. (* fe25519_carry_sub(cZ, trZ, trX) *)
single_step. (* fe25519_sub(cX, t0, cY) *)
single_step. (* fe25519_sub(cT, trT, cZ) *)
single_step. (* fe25519_mul(ox, cX, cT) *)
single_step. (* fe25519_mul(oy, cY, cZ) *)
single_step. (* fe25519_mul(oz, cZ, cT) *)
single_step. (* fe25519_mul(ot, cX, cY) *)

(* Solve the postconditions *)
repeat straightline.
(* Rewrites the FElems for the stack (in H98) to be about bytes instead *)
cbv [FElem] in *.
(* Prevent output from being rewritten by seprewrite_in *)
remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H98.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H98.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H98.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H98.
do 9 (seprewrite_in @Bignum.Bignum_to_bytes H98).
subst Pt Pz Py Px.
extract_ex1_and_emp_in H98.

(* Solve stack/memory stuff *)
repeat straightline.

(* Post-conditions *)
exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds.
{ (* Correctness: result matches Gallina *)
cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *.
cbv match beta delta [m1double coordinates proj1_sig].
destruct p. cbv [coordinates proj1_sig] in H13.
rewrite H13.
rewrite F.pow_2_r in *.
congruence.
}
(* Safety: memory is what it should be *)
ecancel_assumption.
Qed.

End WithParameters.