Skip to content

Commit

Permalink
Optimize & fix Edwards XYZT operations
Browse files Browse the repository at this point in the history
  • Loading branch information
@andres-erbsen
andres-erbsen authored Oct 28, 2023
2 parents fba598d + fe162e0 commit dfc358d
Show file tree
Hide file tree
Showing 3 changed files with 133 additions and 129 deletions.
164 changes: 83 additions & 81 deletions src/Bedrock/End2End/X25519/EdwardsXYZT.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,32 +51,33 @@ Local Existing Instance field_parameters.
Local Instance frep25519 : Field.FieldRepresentation := field_representation n Field25519.s c.
Local Existing Instance frep25519_ok.

Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) {
Definition add_precomputed := func! (ox, oy, oz, ota, otb, X1, Y1, Z1, Ta1, Tb1, half_ypx, half_ymx, xyd) {
stackalloc 40 as YpX1;
fe25519_add(YpX1, Y1, X1);
stackalloc 40 as YmX1;
fe25519_sub(YmX1, Y1, X1);
stackalloc 40 as A;
fe25519_mul(A, YpX1, ypx2);
fe25519_mul(A, YmX1, half_ymx);
stackalloc 40 as B;
fe25519_mul(B, YmX1, ymx2);
fe25519_mul(B, YpX1, half_ypx);
stackalloc 40 as T1;
fe25519_mul(T1, Ta1, Tb1);
stackalloc 40 as C;
fe25519_mul(C, xy2d2, T1);
stackalloc 40 as D;
fe25519_carry_add(D, Z1, Z1);
fe25519_sub(ox, A, B);
fe25519_add(oy, A, B);
fe25519_add(oz, D, C);
fe25519_sub(ot, D, C);
fe25519_mul(ox, ox, ot);
fe25519_mul(oy, oy, oz);
fe25519_mul(oz, ot, oz);
fe25519_mul(ot, ox, oy)
fe25519_mul(C, xyd, T1);
fe25519_sub(ota, B, A);
stackalloc 40 as F;
fe25519_sub(F, Z1, C);
stackalloc 40 as G;
fe25519_add(G, Z1, C);
fe25519_add(otb, B, A);
fe25519_mul(ox, ota, F);
fe25519_mul(oy, G, otb);
fe25519_mul(oz, F, G)
}.

(* 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) {
(* Note: Ta/Tb are unused, but leaving in place in case we want to switch to a point struct in the future *)
Definition double := func! (ox, oy, oz, ota, otb, X, Y, Z, Ta, Tb) {
stackalloc 40 as trX;
fe25519_square(trX, X);
stackalloc 40 as trZ;
Expand All @@ -88,18 +89,15 @@ Definition double := func! (ox, oy, oz, ot, X, Y, Z, T) {
stackalloc 40 as rY;
fe25519_add(rY, X, Y);
fe25519_square(t0, rY);
stackalloc 40 as cY;
fe25519_carry_add(cY, trZ, trX);
fe25519_carry_add(otb, trZ, trX);
stackalloc 40 as cZ;
fe25519_carry_sub(cZ, trZ, trX);
stackalloc 40 as cX;
fe25519_sub(cX, t0, cY);
fe25519_sub(ota, t0, otb);
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)
fe25519_mul(ox, ota, cT);
fe25519_mul(oy, otb, cZ);
fe25519_mul(oz, cZ, cT)
}.

Section WithParameters.
Expand Down Expand Up @@ -133,47 +131,51 @@ Local Notation m1double :=

Global Instance spec_of_add_precomputed : spec_of "add_precomputed" :=
fnspec! "add_precomputed"
(oxK oyK ozK otK X1K Y1K Z1K T1K ypx2K ymx2K xy2d2K : word) /
(ox oy oz ot X1 Y1 Z1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop),
(oxK oyK ozK otaK otbK X1K Y1K Z1K Ta1K Tb1K half_ypxK half_ymxK xydK : word) /
(ox oy oz ota otb X1 Y1 Z1 Ta1 Tb1 half_ypx half_ymx xyd : felem) (R : _ -> Prop),
{ requires t m :=
bounded_by tight_bounds X1 /\
bounded_by tight_bounds Y1 /\
bounded_by tight_bounds Z1 /\
bounded_by loose_bounds T1 /\
bounded_by loose_bounds ypx2 /\
bounded_by loose_bounds ymx2 /\
bounded_by loose_bounds xy2d2 /\
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;
bounded_by loose_bounds Ta1 /\
bounded_by loose_bounds Tb1 /\
bounded_by loose_bounds half_ypx /\
bounded_by loose_bounds half_ymx /\
bounded_by loose_bounds xyd /\
m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem Ta1K Ta1) * (FElem Tb1K Tb1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otaK ota) * (FElem otbK otb) * R;
ensures t' m' :=
t = t' /\
exists ox' oy' oz' ot',
((feval ox'), (feval oy'), (feval oz'), (feval ot')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval T1)) ((feval ypx2), (feval ymx2), (feval xy2d2))) /\
exists ox' oy' oz' ota' otb',
((feval ox'), (feval oy'), (feval oz'), (feval ota'), (feval otb')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval Ta1), (feval Tb1)) ((feval half_ypx), (feval half_ymx), (feval xyd))) /\
bounded_by loose_bounds ox' /\
bounded_by loose_bounds oy' /\
bounded_by loose_bounds oz' /\
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 }.
bounded_by loose_bounds ota' /\
bounded_by loose_bounds otb' /\
m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem Ta1K Ta1) * (FElem Tb1K Tb1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otaK ota') * (FElem otbK otb') * 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),
(oxK oyK ozK otaK otbK XK YK ZK TaK TbK : word) /
(ox oy oz ota otb X Y Z Ta Tb : felem) (p : point) (R : _ -> Prop),
{ requires t m :=
coordinates p = ((feval X), (feval Y), (feval Z), (feval T)) /\
coordinates p = ((feval X), (feval Y), (feval Z), (feval Ta), (feval Tb)) /\
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;
bounded_by loose_bounds Ta /\
bounded_by loose_bounds Tb /\
m =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TaK Ta) * (FElem TbK Tb) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otaK ota) * (FElem otbK otb) * R;
ensures t' m' :=
t = t' /\
exists ox' oy' oz' ot',
((feval ox'), (feval oy'), (feval oz'), (feval ot')) = coordinates (@m1double p) /\
exists ox' oy' oz' ota' otb',
((feval ox'), (feval oy'), (feval oz'), (feval ota'), (feval otb')) = 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 }.
bounded_by loose_bounds ota' /\ (* could be tight_bounds if we need it, but I don't think we do *)
bounded_by tight_bounds otb' /\
m' =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TaK Ta) * (FElem TbK Tb) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otaK ota') * (FElem otbK otb') * R }.


Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square.
Expand Down Expand Up @@ -264,37 +266,37 @@ Proof.
(* 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_add(YpX1, Y1, X1) *)
single_step. (* fe25519_sub(YmX1, Y1, X1) *)
single_step. (* fe25519_mul(A, YpX1, ypx2) *)
single_step. (* fe25519_mul(B, YmX1, ymx2) *)
single_step. (* fe25519_mul(C, xy2d2, T1) *)
single_step. (* fe25519_carry_add(D, Z1, Z1) *)
single_step. (* fe25519_sub(ox, A, B) *)
single_step. (* fe25519_add(oy, A, B) *)
single_step. (* fe25519_add(oz, D, C) *)
single_step. (* fe25519_sub(ot, D, C) *)
single_step. (* fe25519_mul(ox, ox, ot) *)
single_step. (* fe25519_mul(oy, oy, oz) *)
single_step. (* fe25519_mul(oz, ot, oz) *)
single_step. (* fe25519_mul(ot, ox, oy) *)
single_step. (* fe25519_mul(A, YmX1, half_ymx) *)
single_step. (* fe25519_mul(B, YpX1, half_ypx) *)
single_step. (* fe25519_mul(T1, Ta1, Tb1) *)
single_step. (* fe25519_mul(C, xyd, T1) *)
single_step. (* fe25519_sub(ota, B, A) *)
single_step. (* fe25519_sub(F, Z1, C) *)
single_step. (* fe25519_add(G, Z1, C) *)
single_step. (* fe25519_add(otb, B, A) *)
single_step. (* fe25519_mul(ox, ota, F) *)
single_step. (* fe25519_mul(oy, G, otb) *)
single_step. (* fe25519_mul(oz, F, G) *)

(* Solve the postconditions *)
repeat straightline.
(* Rewrites the FElems for the stack (in H88) to be about bytes instead *)
(* Rewrites the FElems for the stack (in H93) 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 H88.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H88.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H88.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H88.
do 6 (seprewrite_in @Bignum.Bignum_to_bytes H88).
subst Pt Pz Py Px.
extract_ex1_and_emp_in H88.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H93.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H93.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H93.
remember (Bignum.Bignum felem_size_in_words otbK _) as Ptb in H93.
remember (Bignum.Bignum felem_size_in_words otaK _) as Pta in H93.
do 8 (seprewrite_in @Bignum.Bignum_to_bytes H93).
subst Pz Py Px Ptb Pta.
extract_ex1_and_emp_in H93.

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

(* Post-conditions *)
exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds.
exists x9,x10,x11,x5,x8; ssplit. 2,3,4,5,6:solve_bounds.
{ (* Correctness: result matches Gallina *)
cbv [bin_model bin_mul bin_add bin_carry_add bin_sub] in *.
cbv match beta delta [m1add_precomputed_coordinates].
Expand All @@ -317,38 +319,38 @@ Proof.
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_add(otb, trZ, trX) *)
single_step. (* fe25519_carry_sub(cZ, trZ, trX) *)
single_step. (* fe25519_sub(cX, t0, cY) *)
single_step. (* fe25519_sub(ota, t0, otb) *)
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(ox, ota, cT) *)
single_step. (* fe25519_mul(oy, otb, 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 *)
(* Rewrites the FElems for the stack (in H87) 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.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H87.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H87.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H87.
remember (Bignum.Bignum felem_size_in_words otaK _) as Pta in H87.
remember (Bignum.Bignum felem_size_in_words otbK _) as Ptb in H87.
do 7 (seprewrite_in @Bignum.Bignum_to_bytes H87).
subst Pz Py Px Pta Ptb.
extract_ex1_and_emp_in H87.

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

(* Post-conditions *)
exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds.
exists x9,x10,x11,x7,x5; ssplit. 2,3,4,5,6: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.
destruct p. cbv [coordinates proj1_sig] in H12.
rewrite H12.
rewrite F.pow_2_r in *.
congruence.
}
Expand Down
47 changes: 23 additions & 24 deletions src/Curves/Edwards/XYZT/Basic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,14 @@ Section ExtendedCoordinates.
Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
(** [Extended.point] represents a point on an elliptic curve using extended projective
* Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
Definition point := { P | let '(X,Y,Z,T) := P in
Definition point := { P | let '(X,Y,Z,Ta,Tb) := P in
a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2
/\ X * Y = Z * T
/\ X * Y = Z * Ta * Tb
/\ Z <> 0 }.
Definition coordinates (P:point) : F*F*F*F := proj1_sig P.
Definition coordinates (P:point) : F*F*F*F*F := proj1_sig P.
Definition eq (P1 P2:point) :=
let '(X1, Y1, Z1, _) := coordinates P1 in
let '(X2, Y2, Z2, _) := coordinates P2 in
let '(X1, Y1, Z1, _, _) := coordinates P1 in
let '(X2, Y2, Z2, _, _) := coordinates P2 in
Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.

Ltac t_step :=
Expand All @@ -58,14 +58,16 @@ Section ExtendedCoordinates.
Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined.

Program Definition from_twisted (P:Epoint) : point :=
let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy).
let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy, snd xy).
Next Obligation. t. Qed.
Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted.
Proof using Type. cbv [from_twisted]; t. Qed.

Program Definition to_twisted (P:point) : Epoint :=
let XYZT := coordinates P in let T := snd XYZT in
let XYZ := fst XYZT in let Z := snd XYZ in
let XYZTT := coordinates P in let Ta := snd XYZTT in
let XYZT := fst XYZTT in
let Tb := snd XYZT in
let XYZ := fst XYZT in let Z := snd XYZ in
let XY := fst XYZ in let Y := snd XY in
let X := fst XY in
let iZ := Finv Z in ((X*iZ), (Y*iZ)).
Expand All @@ -78,36 +80,35 @@ Section ExtendedCoordinates.
Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P.
Proof using Type. cbv [to_twisted from_twisted]; t. Qed.

Program Definition zero : point := (0, 1, 1, 0).
Program Definition zero : point := (0, 1, 1, 0, 1).
Next Obligation. t. Qed.

Program Definition opp P : point :=
match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end.
match coordinates P return F*F*F*F*F with (X,Y,Z,Ta,Tb) => (Fopp X, Y, Z, Fopp Ta, Tb) end.
Next Obligation. t. Qed.

Section TwistMinusOne.
Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}.
Program Definition m1add
(P1 P2:point) : point :=
match coordinates P1, coordinates P2 return F*F*F*F with
(X1, Y1, Z1, T1), (X2, Y2, Z2, T2) =>
match coordinates P1, coordinates P2 return F*F*F*F*F with
(X1, Y1, Z1, Ta1, Tb1), (X2, Y2, Z2, Ta2, Tb2) =>
let A := (Y1-X1)*(Y2-X2) in
let B := (Y1+X1)*(Y2+X2) in
let C := T1*twice_d*T2 in
let C := (Ta1*Tb1)*twice_d*(Ta2*Tb2) in
let D := Z1*(Z2+Z2) in
let E := B-A in
let F := D-C in
let G := D+C in
let H := B+A in
let X3 := E*F in
let Y3 := G*H in
let T3 := E*H in
let Z3 := F*G in
(X3, Y3, Z3, T3)
(X3, Y3, Z3, E, H)
end.
Next Obligation.
match goal with
| [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
| [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
=> pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2)))
end; t.
Qed.
Expand All @@ -134,8 +135,8 @@ Section ExtendedCoordinates.
Proof. pose proof isomorphic_commutative_group_m1 as H; destruct H as [ [] [] [] [] ]; trivial. Qed.

Program Definition m1double (P : point) : point :=
match coordinates P return F*F*F*F with
(X, Y, Z, _) =>
match coordinates P return F*F*F*F*F with
(X, Y, Z, _, _) =>
let trX := X^2 in
let trZ := Y^2 in
let trT := (let t0 := Z^2 in t0+t0) in
Expand All @@ -148,8 +149,7 @@ Section ExtendedCoordinates.
let X3 := cX*cT in
let Y3 := cY*cZ in
let Z3 := cZ*cT in
let T3 := cX*cY in
(X3, Y3, Z3, T3)
(X3, Y3, Z3, cX, cY)
end.
Next Obligation.
match goal with
Expand All @@ -167,8 +167,8 @@ Section ExtendedCoordinates.

(* https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#doubling-double-2008-hwcd *)
Program Definition double (P : point) : point :=
match coordinates P return F*F*F*F with
(X1, Y1, Z1, T1) =>
match coordinates P return F*F*F*F*F with
(X1, Y1, Z1, _, _) =>
let A := X1^2 in
let B := Y1^2 in
let t0 := Z1^2 in
Expand All @@ -183,9 +183,8 @@ Section ExtendedCoordinates.
let H := D-B in
let X3 := E*F in
let Y3 := G*H in
let T3 := E*H in
let Z3 := F*G in
(X3, Y3, Z3, T3)
(X3, Y3, Z3, E, H)
end.
Next Obligation.
match goal with
Expand Down
Loading

0 comments on commit dfc358d

Please sign in to comment.