From 0a1e8feaa2b24978218a2b7f291cf8aae9210638 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 11:38:09 -0400 Subject: [PATCH 1/7] switch to halved variant of precomputed coordinates --- src/Curves/Edwards/XYZT/Precomputed.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Curves/Edwards/XYZT/Precomputed.v b/src/Curves/Edwards/XYZT/Precomputed.v index 6b925c020f..d36e8bd4cb 100644 --- a/src/Curves/Edwards/XYZT/Precomputed.v +++ b/src/Curves/Edwards/XYZT/Precomputed.v @@ -27,11 +27,11 @@ Section ExtendedCoordinates. Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). - Definition precomputed_point : Type := F*F*F. + Definition precomputed_point : Type := F*F*F. (* (y+x)/2, (y-x)/2, dxy *) Definition of_twisted (P:Epoint) := let '(x, y) := E.coordinates P in - (y+x, y-x, (let xy := x*y in xy+xy)*d). + ((y+x)/(1+1), (y-x)/(1+1), x*y*d). (* 1+1 ew *) Section TwistMinusOne. Context {a_eq_minus1:a = Fopp 1}. @@ -43,11 +43,10 @@ Section ExtendedCoordinates. let A := YpX1*ypx2 in let B := YmX1*ymx2 in let C := xy2d2*T1 in - let D := Z1+Z1 in let X3 := A-B in let Y3 := A+B in - let Z3 := D+C in - let T3 := D-C in + let Z3 := Z1+C in + let T3 := Z1-C in (* X/Z, Y/T = x, y *) let X3 := X3*T3 in let Y3 := Y3*Z3 in From 8bc54775d032caa2d431dfb09599599772fe015d Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 12:19:18 -0400 Subject: [PATCH 2/7] Extend variant coords to Bedrock E2E --- src/Bedrock/End2End/X25519/EdwardsXYZT.v | 57 +++++++++++------------- src/Curves/Edwards/XYZT/Precomputed.v | 8 ++-- 2 files changed, 31 insertions(+), 34 deletions(-) diff --git a/src/Bedrock/End2End/X25519/EdwardsXYZT.v b/src/Bedrock/End2End/X25519/EdwardsXYZT.v index 17fe942592..73b5977aa0 100644 --- a/src/Bedrock/End2End/X25519/EdwardsXYZT.v +++ b/src/Bedrock/End2End/X25519/EdwardsXYZT.v @@ -51,23 +51,21 @@ 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, ot, X1, Y1, Z1, T1, 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, YpX1, half_ypx); stackalloc 40 as B; - fe25519_mul(B, YmX1, ymx2); + fe25519_mul(B, YmX1, half_ymx); stackalloc 40 as C; - fe25519_mul(C, xy2d2, T1); - stackalloc 40 as D; - fe25519_carry_add(D, Z1, Z1); + fe25519_mul(C, xyd, T1); fe25519_sub(ox, A, B); fe25519_add(oy, A, B); - fe25519_add(oz, D, C); - fe25519_sub(ot, D, C); + fe25519_add(oz, Z1, C); + fe25519_sub(ot, Z1, C); fe25519_mul(ox, ox, ot); fe25519_mul(oy, oy, oz); fe25519_mul(oz, ot, oz); @@ -133,26 +131,26 @@ 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 otK X1K Y1K Z1K T1K half_ypxK half_ymxK xydK : word) / + (ox oy oz ot X1 Y1 Z1 T1 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 half_ypx /\ + bounded_by loose_bounds half_ymx /\ + bounded_by loose_bounds xyd /\ + m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (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')) = (@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))) /\ + ((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 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 }. + m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }. Global Instance spec_of_double : spec_of "double" := fnspec! "double" @@ -264,14 +262,13 @@ 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_mul(A, YpX1, half_ypx) *) + single_step. (* fe25519_mul(B, YmX1, half_ymx) *) + single_step. (* fe25519_mul(C, xyd, T1) *) 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_add(oz, Z1, C) *) + single_step. (* fe25519_sub(ot, Z1, C) *) single_step. (* fe25519_mul(ox, ox, ot) *) single_step. (* fe25519_mul(oy, oy, oz) *) single_step. (* fe25519_mul(oz, ot, oz) *) @@ -279,22 +276,22 @@ Proof. (* 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 H80) 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). + remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H80. + remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H80. + remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H80. + remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H80. + do 5 (seprewrite_in @Bignum.Bignum_to_bytes H80). subst Pt Pz Py Px. - extract_ex1_and_emp_in H88. + extract_ex1_and_emp_in H80. (* Solve stack/memory stuff *) repeat straightline. (* Post-conditions *) - exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds. + exists x8,x9,x10,x11; ssplit. 2,3,4,5: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]. diff --git a/src/Curves/Edwards/XYZT/Precomputed.v b/src/Curves/Edwards/XYZT/Precomputed.v index d36e8bd4cb..3340bfa4e2 100644 --- a/src/Curves/Edwards/XYZT/Precomputed.v +++ b/src/Curves/Edwards/XYZT/Precomputed.v @@ -37,12 +37,12 @@ Section ExtendedCoordinates. Context {a_eq_minus1:a = Fopp 1}. Definition m1add_precomputed_coordinates (P:F*F*F*F) (Q:precomputed_point) : F*F*F*F := let '(X1, Y1, Z1, T1) := P in - let '(ypx2, ymx2, xy2d2) := Q in + let '(half_ypx, half_ymx, xyd) := Q in let YpX1 := Y1+X1 in let YmX1 := Y1-X1 in - let A := YpX1*ypx2 in - let B := YmX1*ymx2 in - let C := xy2d2*T1 in + let A := YpX1*half_ypx in + let B := YmX1*half_ymx in + let C := xyd*T1 in let X3 := A-B in let Y3 := A+B in let Z3 := Z1+C in From b80db9d52c5d07947fff2163559353626b0786f3 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 15:20:51 -0400 Subject: [PATCH 3/7] Fix calculation of T in mixed addition We were previously overwriting the values used to calculate T. This corrects the logic, while still minimizing memory consumption. The result is a little messier in the order of statements, but not by much. --- src/Bedrock/End2End/X25519/EdwardsXYZT.v | 51 ++++++++++++------------ src/Curves/Edwards/XYZT/Precomputed.v | 29 ++++++++------ 2 files changed, 42 insertions(+), 38 deletions(-) diff --git a/src/Bedrock/End2End/X25519/EdwardsXYZT.v b/src/Bedrock/End2End/X25519/EdwardsXYZT.v index 73b5977aa0..4ee85fe98b 100644 --- a/src/Bedrock/End2End/X25519/EdwardsXYZT.v +++ b/src/Bedrock/End2End/X25519/EdwardsXYZT.v @@ -57,19 +57,20 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, half_ypx, h stackalloc 40 as YmX1; fe25519_sub(YmX1, Y1, X1); stackalloc 40 as A; - fe25519_mul(A, YpX1, half_ypx); + fe25519_mul(A, YmX1, half_ymx); stackalloc 40 as B; - fe25519_mul(B, YmX1, half_ymx); + fe25519_mul(B, YpX1, half_ypx); stackalloc 40 as C; fe25519_mul(C, xyd, T1); - fe25519_sub(ox, A, B); - fe25519_add(oy, A, B); + fe25519_sub(ox, B, A); + stackalloc 40 as F; + fe25519_sub(F, Z1, C); fe25519_add(oz, Z1, C); - fe25519_sub(ot, Z1, C); - fe25519_mul(ox, ox, ot); - fe25519_mul(oy, oy, oz); - fe25519_mul(oz, ot, oz); - fe25519_mul(ot, ox, oy) + fe25519_add(oy, B, A); + fe25519_mul(ot, ox, oy); + fe25519_mul(ox, ox, F); + fe25519_mul(oy, oz, oy); + fe25519_mul(oz, F, oz) }. (* Equivalent of m1double in src/Curves/Edwards/XYZT/Basic.v *) @@ -262,36 +263,36 @@ 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, half_ypx) *) - single_step. (* fe25519_mul(B, YmX1, half_ymx) *) + single_step. (* fe25519_mul(A, YmX1, half_ymx) *) + single_step. (* fe25519_mul(B, YpX1, half_ypx) *) single_step. (* fe25519_mul(C, xyd, T1) *) - single_step. (* fe25519_sub(ox, A, B) *) - single_step. (* fe25519_add(oy, A, B) *) + single_step. (* fe25519_sub(ox, B, A) *) + single_step. (* fe25519_sub(F, Z1, C) *) single_step. (* fe25519_add(oz, Z1, C) *) - single_step. (* fe25519_sub(ot, Z1, 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_add(oy, B, A) *) single_step. (* fe25519_mul(ot, ox, oy) *) + single_step. (* fe25519_mul(ox, ox, F) *) + single_step. (* fe25519_mul(oy, oy, oz) *) + single_step. (* fe25519_mul(oz, F, oz) *) (* Solve the postconditions *) repeat straightline. - (* Rewrites the FElems for the stack (in H80) to be about bytes instead *) + (* Rewrites the FElems for the stack (in H84) 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 H80. - remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H80. - remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H80. - remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H80. - do 5 (seprewrite_in @Bignum.Bignum_to_bytes H80). + remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H84. + remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H84. + remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H84. + remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H84. + do 6 (seprewrite_in @Bignum.Bignum_to_bytes H84). subst Pt Pz Py Px. - extract_ex1_and_emp_in H80. + extract_ex1_and_emp_in H84. (* Solve stack/memory stuff *) repeat straightline. (* Post-conditions *) - exists x8,x9,x10,x11; ssplit. 2,3,4,5:solve_bounds. + exists x9,x10,x11,x8; ssplit. 2,3,4,5: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]. diff --git a/src/Curves/Edwards/XYZT/Precomputed.v b/src/Curves/Edwards/XYZT/Precomputed.v index 3340bfa4e2..1b65320cec 100644 --- a/src/Curves/Edwards/XYZT/Precomputed.v +++ b/src/Curves/Edwards/XYZT/Precomputed.v @@ -15,7 +15,7 @@ Section ExtendedCoordinates. {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Notation "2" := (Fadd 1 1). Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x). @@ -31,27 +31,29 @@ Section ExtendedCoordinates. Definition of_twisted (P:Epoint) := let '(x, y) := E.coordinates P in - ((y+x)/(1+1), (y-x)/(1+1), x*y*d). (* 1+1 ew *) + ((y+x)/2, (y-x)/2, x*y*d). Section TwistMinusOne. Context {a_eq_minus1:a = Fopp 1}. + (* https://hyperelliptic.org/EFD/g1p/data/twisted/extended-1/addition/madd-2008-hwcd-3, + but with halved precomputed coordinates (making D unnecessary) *) Definition m1add_precomputed_coordinates (P:F*F*F*F) (Q:precomputed_point) : F*F*F*F := let '(X1, Y1, Z1, T1) := P in let '(half_ypx, half_ymx, xyd) := Q in let YpX1 := Y1+X1 in let YmX1 := Y1-X1 in - let A := YpX1*half_ypx in - let B := YmX1*half_ymx in - let C := xyd*T1 in - let X3 := A-B in - let Y3 := A+B in + let A := YmX1*half_ymx in + let B := YpX1*half_ypx in + let C := xyd*T1 in (* = T1*2d*T2, since Z2=1 so T2=X2*Y2 *) + let X3 := B-A in + let F := Z1-C in let Z3 := Z1+C in - let T3 := Z1-C in - (* X/Z, Y/T = x, y *) - let X3 := X3*T3 in - let Y3 := Y3*Z3 in - let Z3 := T3*Z3 in + let Y3 := B+A in + (* X/Z, Y/Z = x, y *) let T3 := X3*Y3 in + let X3 := X3*F in + let Y3 := Z3*Y3 in + let Z3 := F*Z3 in (X3, Y3, Z3, T3). Create HintDb points_as_coordinates discriminated. @@ -62,7 +64,7 @@ Section ExtendedCoordinates. Lemma m1add_precomputed_coordinates_correct P Q : let '(X1, Y1, Z1, T1) := m1add_precomputed_coordinates (XYZT.Basic.coordinates P) (of_twisted Q) in let '(X2, Y2, Z2, T2) := coordinates (m1add P (XYZT_of_twisted Q)) in - Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2. + Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2 /\ X1*Y1 = Z1*T1. Proof. repeat match goal with | _ => progress autounfold with points_as_coordinates in * @@ -73,5 +75,6 @@ Section ExtendedCoordinates. | |- _ /\ _ => split end; fsatz. Qed. + End TwistMinusOne. End ExtendedCoordinates. \ No newline at end of file From 9e666e0e05796a1e7c40ee54923b58db8afbacb9 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 16:14:58 -0400 Subject: [PATCH 4/7] Split T into parts to save a mul --- src/Curves/Edwards/XYZT/Basic.v | 47 ++++++++++++++++----------------- 1 file changed, 23 insertions(+), 24 deletions(-) diff --git a/src/Curves/Edwards/XYZT/Basic.v b/src/Curves/Edwards/XYZT/Basic.v index 9a1915a778..fc69464f30 100644 --- a/src/Curves/Edwards/XYZT/Basic.v +++ b/src/Curves/Edwards/XYZT/Basic.v @@ -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 ). *) - 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 := @@ -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)). @@ -78,22 +80,22 @@ 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 @@ -101,13 +103,12 @@ Section ExtendedCoordinates. 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. @@ -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 @@ -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 @@ -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 @@ -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 From 8c81ddfd05bc2f95d7924ab6f6fb8114fbc09efd Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 16:19:43 -0400 Subject: [PATCH 5/7] Extend split T to precomputed addition --- src/Curves/Edwards/XYZT/Precomputed.v | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/src/Curves/Edwards/XYZT/Precomputed.v b/src/Curves/Edwards/XYZT/Precomputed.v index 1b65320cec..fbec2081a8 100644 --- a/src/Curves/Edwards/XYZT/Precomputed.v +++ b/src/Curves/Edwards/XYZT/Precomputed.v @@ -37,24 +37,25 @@ Section ExtendedCoordinates. Context {a_eq_minus1:a = Fopp 1}. (* https://hyperelliptic.org/EFD/g1p/data/twisted/extended-1/addition/madd-2008-hwcd-3, but with halved precomputed coordinates (making D unnecessary) *) - Definition m1add_precomputed_coordinates (P:F*F*F*F) (Q:precomputed_point) : F*F*F*F := - let '(X1, Y1, Z1, T1) := P in + Definition m1add_precomputed_coordinates (P:F*F*F*F*F) (Q:precomputed_point) : F*F*F*F*F := + let '(X1, Y1, Z1, Ta, Tb) := P in let '(half_ypx, half_ymx, xyd) := Q in let YpX1 := Y1+X1 in let YmX1 := Y1-X1 in let A := YmX1*half_ymx in let B := YpX1*half_ypx in + let T1 := Ta*Tb in let C := xyd*T1 in (* = T1*2d*T2, since Z2=1 so T2=X2*Y2 *) - let X3 := B-A in + let E := B-A in let F := Z1-C in - let Z3 := Z1+C in - let Y3 := B+A in + let G := Z1+C in + let H := B+A in (* X/Z, Y/Z = x, y *) - let T3 := X3*Y3 in - let X3 := X3*F in - let Y3 := Z3*Y3 in - let Z3 := F*Z3 in - (X3, Y3, Z3, T3). + let X3 := E*F in + let Y3 := G*H in + let Z3 := F*G in + (* Leave T split in two parts *) + (X3, Y3, Z3, E, H). Create HintDb points_as_coordinates discriminated. Hint Unfold XYZT.Basic.point XYZT.Basic.coordinates XYZT.Basic.from_twisted XYZT.Basic.m1add @@ -62,9 +63,9 @@ Section ExtendedCoordinates. Local Notation m1add := (Basic.m1add(nonzero_a:=nonzero_a)(square_a:=square_a)(a_eq_minus1:=a_eq_minus1)(nonsquare_d:=nonsquare_d)(k_eq_2d:=reflexivity _)). Local Notation XYZT_of_twisted := (Basic.from_twisted(nonzero_a:=nonzero_a)(d:=d)). Lemma m1add_precomputed_coordinates_correct P Q : - let '(X1, Y1, Z1, T1) := m1add_precomputed_coordinates (XYZT.Basic.coordinates P) (of_twisted Q) in - let '(X2, Y2, Z2, T2) := coordinates (m1add P (XYZT_of_twisted Q)) in - Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2 /\ X1*Y1 = Z1*T1. + let '(X1, Y1, Z1, Ta1, Tb1) := m1add_precomputed_coordinates (XYZT.Basic.coordinates P) (of_twisted Q) in + let '(X2, Y2, Z2, _, _) := coordinates (m1add P (XYZT_of_twisted Q)) in + Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2 /\ X1*Y1 = Z1*Ta1*Tb1. Proof. repeat match goal with | _ => progress autounfold with points_as_coordinates in * From f157471f455b63e9b66368d9aa9142b819bfe3ce Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 16:55:10 -0400 Subject: [PATCH 6/7] Pipe split T through Bedrock code --- src/Bedrock/End2End/X25519/EdwardsXYZT.v | 138 ++++++++++++----------- 1 file changed, 71 insertions(+), 67 deletions(-) diff --git a/src/Bedrock/End2End/X25519/EdwardsXYZT.v b/src/Bedrock/End2End/X25519/EdwardsXYZT.v index 4ee85fe98b..67e865b9d9 100644 --- a/src/Bedrock/End2End/X25519/EdwardsXYZT.v +++ b/src/Bedrock/End2End/X25519/EdwardsXYZT.v @@ -51,7 +51,7 @@ 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, half_ypx, half_ymx, xyd) { +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; @@ -60,22 +60,24 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, half_ypx, h fe25519_mul(A, YmX1, half_ymx); stackalloc 40 as B; fe25519_mul(B, YpX1, half_ypx); + stackalloc 40 as T1; + fe25519_mul(T1, Ta1, Tb1); stackalloc 40 as C; fe25519_mul(C, xyd, T1); - fe25519_sub(ox, B, A); + fe25519_sub(ota, B, A); stackalloc 40 as F; fe25519_sub(F, Z1, C); - fe25519_add(oz, Z1, C); - fe25519_add(oy, B, A); - fe25519_mul(ot, ox, oy); - fe25519_mul(ox, ox, F); - fe25519_mul(oy, oz, oy); - fe25519_mul(oz, F, oz) + 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; @@ -87,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. @@ -132,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 half_ypxK half_ymxK xydK : word) / - (ox oy oz ot X1 Y1 Z1 T1 half_ypx half_ymx xyd : 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 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 T1K T1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otK ot) * R; + 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 half_ypx), (feval half_ymx), (feval xyd))) /\ + 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 half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (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. @@ -265,34 +268,35 @@ Proof. single_step. (* fe25519_sub(YmX1, Y1, X1) *) 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(ox, B, A) *) + single_step. (* fe25519_sub(ota, B, A) *) single_step. (* fe25519_sub(F, Z1, C) *) - single_step. (* fe25519_add(oz, Z1, C) *) - single_step. (* fe25519_add(oy, B, A) *) - single_step. (* fe25519_mul(ot, ox, oy) *) - single_step. (* fe25519_mul(ox, ox, F) *) - single_step. (* fe25519_mul(oy, oy, oz) *) - single_step. (* fe25519_mul(oz, F, oz) *) + 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 H84) 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 H84. - remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H84. - remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H84. - remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H84. - do 6 (seprewrite_in @Bignum.Bignum_to_bytes H84). - subst Pt Pz Py Px. - extract_ex1_and_emp_in H84. + 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,x8; 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]. @@ -315,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. } From fe162e0f6605ea9ac80f1de33eaca8b615e03ba3 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 27 Oct 2023 16:56:38 -0400 Subject: [PATCH 7/7] Newline at EOF --- src/Curves/Edwards/XYZT/Precomputed.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Curves/Edwards/XYZT/Precomputed.v b/src/Curves/Edwards/XYZT/Precomputed.v index fbec2081a8..1f9dd3431a 100644 --- a/src/Curves/Edwards/XYZT/Precomputed.v +++ b/src/Curves/Edwards/XYZT/Precomputed.v @@ -78,4 +78,4 @@ Section ExtendedCoordinates. Qed. End TwistMinusOne. -End ExtendedCoordinates. \ No newline at end of file +End ExtendedCoordinates.