diff options
Diffstat (limited to 'src/Curves/PointFormats.v')
-rw-r--r-- | src/Curves/PointFormats.v | 804 |
1 files changed, 388 insertions, 416 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 8ab81e0a8..6ec9aba68 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -2,436 +2,397 @@ Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Tactics.VerdiTactics. -(* FIXME: remove after [field] with modulus as a parameter (34d9f8a6e6a4be439d1c56a8b999d2c21ee12a46) is fixed *) -Require Import Zpower ZArith Znumtheory. -Definition two_255_19 := (two_p 255) - 19. -Lemma two_255_19_prime : prime two_255_19. Admitted. -Definition prime25519 := exist _ two_255_19 two_255_19_prime. -Module M <: Modulus. - Definition modulus := prime25519. -End M. - - -(** Theory of elliptic curves over prime fields for cryptographic applications, -with focus on the curves in <https://tools.ietf.org/html/draft-ladd-safecurves-04> *) -Module PointFormats. - Module F := ComputationalGaloisField M. - Export M F F.T. - Local Open Scope GF_scope. - Local Notation "2" := (1+1). - Local Notation "3" := (1+1+1). - Local Notation "4" := (1+1+1+1). - Local Notation "27" := (3*3*3). - - Module Type TwistedA. - Parameter a : GF. - Axiom a_nonzero : a <> 0. - Axiom a_square : exists sqrt_a, sqrt_a^2 = a. - End TwistedA. - - Module Type TwistedD. - Parameter d : GF. - Axiom d_nonsquare : forall not_sqrt_d, not_sqrt_d^2 <> d. - End TwistedD. - - Module CompleteTwistedEdwardsSpec (Import ta:TwistedA) (Import td:TwistedD). - (** Twisted Ewdwards curves with complete addition laws. References: - * <https://eprint.iacr.org/2008/013.pdf> - * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> - * <https://eprint.iacr.org/2015/677.pdf> - *) - Record point := mkPoint {projX : GF; projY : GF}. +Module Type TwistedEdwardsParams (Import M : Modulus). + Module Export GT := GaloisTheory M. + Open Scope GF_scope. + Definition twistedA := { a : GF | a <> 0 /\ exists sqrt_a, sqrt_a^2 = a }. + Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }. + + Parameter a : twistedA. + Parameter d : twistedD. + + Definition twistedAToGF (a : twistedA) := proj1_sig a. + Coercion twistedAToGF : twistedA >-> GF. + Definition twistedDToGF (d : twistedD) := proj1_sig d. + Coercion twistedDToGF : twistedD >-> GF. +End TwistedEdwardsParams. + +Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M). + (** Twisted Ewdwards curves with complete addition laws. References: + * <https://eprint.iacr.org/2008/013.pdf> + * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> + * <https://eprint.iacr.org/2015/677.pdf> + *) + Record point := mkPoint {projX : GF; projY : GF}. + + Definition unifiedAdd (P1 P2 : point) : point := + let x1 := projX P1 in + let y1 := projY P1 in + let x2 := projX P2 in + let y2 := projY P2 in + mkPoint + ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) + ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)) + . + + Definition onCurve : point -> Prop := fun P => + let x := projX P in + let y := projY P in + a*x^2 + y^2 = 1 + d*x^2*y^2. +End CompleteTwistedEdwardsCurve. + +Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M). + Module Curve := CompleteTwistedEdwardsCurve M P. + Parameter point : Type. + Parameter mkPoint : forall (x y:GF), point. + Parameter projX : point -> GF. + Parameter projY : point -> GF. + Parameter unifiedAdd : point -> point -> point. + + Parameter rep : point -> Curve.point -> Prop. + Local Notation "P '~=' rP" := (rep P rP) (at level 70). + Axiom mkPoint_rep: forall x y, mkPoint x y ~= Curve.mkPoint x y. + Axiom unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd rP rQ). + Axiom projX_rep : forall P rP, P ~= rP -> projX P = Curve.projX rP. + Axiom projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP. +End CompleteTwistedEdwardsPointFormat. + +Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). + Module Import Curve := CompleteTwistedEdwardsCurve M P. + Lemma twistedAddCompletePlus : forall (P1 P2:point) + (oc1:onCurve P1) (oc2:onCurve P2), + let x1 := projX P1 in + let y1 := projY P1 in + let x2 := projX P2 in + let y2 := projY P2 in + (1 + d*x1*x2*y1*y2) <> 0. + (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *) + Admitted. + Lemma twistedAddCompleteMinus : forall (P1 P2:point) + (oc1:onCurve P1) (oc2:onCurve P2), + let x1 := projX P1 in + let y1 := projY P1 in + let x2 := projX P2 in + let y2 := projY P2 in + (1 - d*x1*x2*y1*y2) <> 0. + (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *) + Admitted. + + Hint Unfold unifiedAdd onCurve. + Ltac twisted := autounfold; intros; + repeat match goal with + | [ x : point |- _ ] => destruct x + end; simpl; repeat (ring || f_equal); field. + Local Infix "+" := unifiedAdd. + Lemma twistedAddComm : forall A B, (A+B = B+A). + Proof. + twisted. + Qed. - Definition unifiedAdd (P1 P2 : point) : point := - let x1 := projX P1 in - let y1 := projY P1 in - let x2 := projX P2 in - let y2 := projY P2 in - mkPoint - ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) - ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)) - . - - Definition onCurve : point -> Prop := fun P => - let x := projX P in - let y := projY P in - a*x^2 + y^2 = 1 + d*x^2*y^2. - End CompleteTwistedEdwardsSpec. - - Module Type CompleteTwistedEdwardsPointFormat (ta:TwistedA) (td:TwistedD). - Module Spec := CompleteTwistedEdwardsSpec ta td. - Parameter point : Type. - Parameter mkPoint : forall (x y:GF), point. - Parameter projX : point -> GF. - Parameter projY : point -> GF. - Parameter unifiedAdd : point -> point -> point. - - Parameter rep : point -> Spec.point -> Prop. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - Axiom mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y. - Axiom unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ). - Axiom projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP. - Axiom projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP. - End CompleteTwistedEdwardsPointFormat. - - Module CompleteTwistedEdwardsFacts (Import ta:TwistedA) (Import td:TwistedD). - Module Import Spec := CompleteTwistedEdwardsSpec ta td. - - Lemma twistedAddCompletePlus : forall (P1 P2:point) - (oc1:onCurve P1) (oc2:onCurve P2), - let x1 := projX P1 in - let y1 := projY P1 in - let x2 := projX P2 in - let y2 := projY P2 in - (1 + d*x1*x2*y1*y2) <> 0. - (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *) - Admitted. - Lemma twistedAddCompleteMinus : forall (P1 P2:point) - (oc1:onCurve P1) (oc2:onCurve P2), - let x1 := projX P1 in - let y1 := projY P1 in - let x2 := projX P2 in - let y2 := projY P2 in - (1 - d*x1*x2*y1*y2) <> 0. - (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *) - Admitted. + Lemma twistedAddAssoc : forall A B C + (ocA:onCurve A) (ocB:onCurve B) (ocC:onCurve C), + (A+(B+C) = (A+B)+C). + Proof. + (* uh... I don't actually know where this is proven... *) + Admitted. - Hint Unfold unifiedAdd onCurve. - Ltac twisted := autounfold; intros; - repeat match goal with - | [ x : point |- _ ] => destruct x - end; simpl; repeat (ring || f_equal); field. - Local Infix "+" := unifiedAdd. - Lemma twistedAddComm : forall A B, (A+B = B+A). + Local Notation "'(' x ',' y ')'" := (mkPoint x y). + Definition zero := (0, 1). + Lemma zeroOnCurve : onCurve (0, 1). + Proof. + twisted. + Qed. + Lemma zeroIsIdentity : forall P, P + zero = P. + Proof. + admit. + Qed. +End CompleteTwistedEdwardsFacts. + +Module Minus1Twisted (Import M : Modulus). + Module Minus1Params <: TwistedEdwardsParams M. + Module Export GT := GaloisTheory M. + Open Scope GF_scope. + Definition isSquareAndNonzero (a : GF) := a <> 0 /\ exists sqrt_a, sqrt_a^2 = a. + Definition twistedA := { a : GF | isSquareAndNonzero a }. + Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }. + + Axiom minusOneIsSquareAndNonzero : isSquareAndNonzero (0 - 1). + Definition a : twistedA := exist _ _ minusOneIsSquareAndNonzero. + + Parameter d : twistedD. + + Definition twistedAToGF (a : twistedA) := proj1_sig a. + Coercion twistedAToGF : twistedA >-> GF. + Definition twistedDToGF (d : twistedD) := proj1_sig d. + Coercion twistedDToGF : twistedD >-> GF. + End Minus1Params. + Import Minus1Params. + + Module Import Curve := CompleteTwistedEdwardsCurve M Minus1Params. + + Module Minus1Format <: CompleteTwistedEdwardsPointFormat M Minus1Params. + Module Import Facts := CompleteTwistedEdwardsFacts M Minus1Params. + (** [projective] represents a point on an elliptic curve using projective + * Edwards coordinates for twisted edwards curves with a=-1 (see + * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html> + * <https://en.wikipedia.org/wiki/Edwards_curve#Projective_homogeneous_coordinates>) *) + Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}. + Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z). + + Definition twistedToProjective (P : Curve.point) : projective := + let x := Curve.projX P in + let y := Curve.projY P in + (x, y, 1). + + Local Notation "'(' X ',' Y ')'" := (Curve.mkPoint X Y). + Definition projectiveToTwisted (P : projective) : Curve.point := + let X := projectiveX P in + let Y := projectiveY P in + let Z := projectiveZ P in + (X/Z, Y/Z). + + Hint Unfold projectiveToTwisted twistedToProjective. + + Lemma twistedProjectiveInv : forall P, + projectiveToTwisted (twistedToProjective P) = P. Proof. - twisted. + admit. Qed. - Lemma twistedAddAssoc : forall A B C - (ocA:onCurve A) (ocB:onCurve B) (ocC:onCurve C), - (A+(B+C) = (A+B)+C). + (** [extended] represents a point on an elliptic curve using extended projective + * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) + Record extended := mkExtended {extendedToProjective : projective; extendedT : GF}. + (*Error: The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name.*) + + Definition point := extended. + Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T). + Definition extendedValid (P : point) : Prop := + let pP := extendedToProjective P in + let X := projectiveX pP in + let Y := projectiveY pP in + let Z := projectiveZ pP in + let T := extendedT P in + T = X*Y/Z. + + + Definition twistedToExtended (P : Curve.point) : point := + let x := Curve.projX P in + let y := Curve.projY P in + (x, y, 1, x*y). + Definition mkPoint x y := twistedToExtended (x, y). + + Definition extendedToTwisted (P : point) : Curve.point := + projectiveToTwisted (extendedToProjective P). + Local Hint Unfold extendedValid twistedToExtended extendedToTwisted projectiveToTwisted Curve.unifiedAdd mkPoint. + + Lemma twistedExtendedInv : forall P, + extendedToTwisted (twistedToExtended P) = P. Proof. - (* uh... I don't actually know where this is proven... *) - Admitted. + apply twistedProjectiveInv. + Qed. - Local Notation "'(' x ',' y ')'" := (mkPoint x y). - Definition zero := (0, 1). - Lemma zeroOnCurve : onCurve (0, 1). + Lemma twistedToExtendedValid : forall (P : Curve.point), extendedValid (twistedToExtended P). Proof. - twisted. + autounfold. + destruct P. + simpl. + admit. + (* field. *) Qed. - Lemma zeroIsIdentity : forall P, P + zero = P. + + Definition rep (P:point) (rP:Curve.point) : Prop := + extendedToTwisted P = rP /\ extendedValid P. + Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Curve.mkPoint x y). Proof. - twisted. + split. + apply twistedExtendedInv. + apply twistedToExtendedValid. Qed. - End CompleteTwistedEdwardsFacts. - + Local Notation "P '~=' rP" := (rep P rP) (at level 70). - Module CompleteTwistedEdwardsSpecPointFormat (ta:TwistedA) (td:TwistedD) - <: CompleteTwistedEdwardsPointFormat ta td. - Module Spec := CompleteTwistedEdwardsSpec ta td. - Definition point := Spec.point. - Definition mkPoint := Spec.mkPoint. - Definition projX := Spec.projX. - Definition projY := Spec.projY. - Definition unifiedAdd := Spec.unifiedAdd. + Definition projX P := Curve.projX (extendedToTwisted P). + Definition projY P := Curve.projY (extendedToTwisted P). - Definition rep : point -> point -> Prop := eq. - Local Hint Unfold rep. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - Local Ltac trivialRep := autounfold; intros; subst; auto. - Lemma mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y. - trivialRep. - Qed. - Lemma unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ). - trivialRep. - Qed. - Lemma projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP. - trivialRep. + Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with + | [ x : rep ?a ?b |- _ ] => destruct x + end). + Lemma projX_rep : forall P rP, P ~= rP -> projX P = Curve.projX rP. + Proof. + rep. Qed. - Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP. - trivialRep. + Lemma projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP. + Proof. + rep. Qed. - End CompleteTwistedEdwardsSpecPointFormat. - - Module Type Minus1IsSquare. - Axiom minusOneIsSquare : exists sqrt_a, sqrt_a^2 = 0 - 1. - End Minus1IsSquare. - - Module Minus1Twisted (m1s:Minus1IsSquare) (Import td:TwistedD). - Module ta <: TwistedA. - Definition a : GF := 0 - 1. - Lemma a_square : exists sqrt_a, sqrt_a^2 = a. - Proof. - apply m1s.minusOneIsSquare. - Qed. - Lemma a_nonzero : a <> 0. - Proof. - discriminate. - (* This result happens to be trivial in the concrete modulus! - * We probably want a generic [0 <> 1] fact to use when we parameterize more. *) - Qed. - End ta. - Import ta. - - Module Spec := CompleteTwistedEdwardsSpec ta td. - - Module Format <: CompleteTwistedEdwardsPointFormat ta td. - Module Import Facts := CompleteTwistedEdwardsFacts ta td. - - (** [projective] represents a point on an elliptic curve using projective - * Edwards coordinates for twisted edwards curves with a=-1 (see - * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html> - * <https://en.wikipedia.org/wiki/Edwards_curve#Projective_homogeneous_coordinates>) *) - Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}. - Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z). - - Definition twistedToProjective (P : Spec.point) : projective := - let x := Spec.projX P in - let y := Spec.projY P in - (x, y, 1). - - Local Notation "'(' X ',' Y ')'" := (Spec.mkPoint X Y). - Definition projectiveToTwisted (P : projective) : Spec.point := - let X := projectiveX P in - let Y := projectiveY P in - let Z := projectiveZ P in - (X/Z, Y/Z). - - Hint Unfold projectiveToTwisted twistedToProjective. - - Lemma twistedProjectiveInv : forall P, - projectiveToTwisted (twistedToProjective P) = P. - Proof. - twisted. - Qed. - - (** [extended] represents a point on an elliptic curve using extended projective - * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) - Record extended := mkExtended {extendedToProjective : projective; extendedT : GF}. - (*Error: The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name.*) - - Definition point := extended. - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T). - Definition extendedValid (P : point) : Prop := - let pP := extendedToProjective P in - let X := projectiveX pP in - let Y := projectiveY pP in - let Z := projectiveZ pP in - let T := extendedT P in - T = X*Y/Z. - - - Definition twistedToExtended (P : Spec.point) : point := - let x := Spec.projX P in - let y := Spec.projY P in - (x, y, 1, x*y). - Definition mkPoint x y := twistedToExtended (x, y). - - Definition extendedToTwisted (P : point) : Spec.point := - projectiveToTwisted (extendedToProjective P). - Local Hint Unfold extendedValid twistedToExtended extendedToTwisted projectiveToTwisted Spec.unifiedAdd mkPoint. - - Lemma twistedExtendedInv : forall P, - extendedToTwisted (twistedToExtended P) = P. - Proof. - apply twistedProjectiveInv. - Qed. - - Lemma twistedToExtendedValid : forall (P : Spec.point), extendedValid (twistedToExtended P). - Proof. - autounfold. - destruct P. - simpl. - field. - Qed. - - Definition rep (P:point) (rP:Spec.point) : Prop := - extendedToTwisted P = rP /\ extendedValid P. - Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Spec.mkPoint x y). - Proof. - split. - apply twistedExtendedInv. - apply twistedToExtendedValid. - Qed. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - Definition projX P := Spec.projX (extendedToTwisted P). - Definition projY P := Spec.projY (extendedToTwisted P). - - Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with - | [ x : rep ?a ?b |- _ ] => destruct x - end). - Lemma projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP. - Proof. - rep. - Qed. - Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP. - Proof. - rep. - Qed. - - (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) - Definition unifiedAdd (P1 P2 : point) : point := - let k := 2 * d in - let pP1 := extendedToProjective P1 in - let X1 := projectiveX pP1 in - let Y1 := projectiveY pP1 in - let Z1 := projectiveZ pP1 in - let T1 := extendedT P1 in - let pP2 := extendedToProjective P2 in - let X2 := projectiveX pP2 in - let Y2 := projectiveY pP2 in - let Z2 := projectiveZ pP2 in - let T2 := extendedT P2 in - let A := (Y1-X1)*(Y2-X2) in - let B := (Y1+X1)*(Y2+X2) in - let C := T1*k*T2 in - let D := Z1*2*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 - mkExtended (mkProjective X3 Y3 Z3) T3. - - Delimit Scope extendedM1_scope with extendedM1. - Infix "+" := unifiedAdd : extendedM1_scope. - - Lemma unifiedAddCon : forall (P1 P2:point) - (hv1:extendedValid P1) (hv2:extendedValid P2), - extendedValid (P1 + P2)%extendedM1. - Proof. - intros. - remember ((P1+P2)%extendedM1) as P3. - destruct P1 as [[X1 Y1 Z1] T1]. - destruct P2 as [[X2 Y2 Z2] T2]. - destruct P3 as [[X3 Y3 Z3] T3]. - unfold extendedValid, extendedToProjective, projectiveToTwisted, Spec.projX, Spec.projY in *. - invcs HeqP3. - subst. - (* field. -- fails. but it works in sage: + + Local Notation "2" := (1+1). + (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) + Definition unifiedAdd (P1 P2 : point) : point := + let k := 2 * d in + let pP1 := extendedToProjective P1 in + let X1 := projectiveX pP1 in + let Y1 := projectiveY pP1 in + let Z1 := projectiveZ pP1 in + let T1 := extendedT P1 in + let pP2 := extendedToProjective P2 in + let X2 := projectiveX pP2 in + let Y2 := projectiveY pP2 in + let Z2 := projectiveZ pP2 in + let T2 := extendedT P2 in + let A := (Y1-X1)*(Y2-X2) in + let B := (Y1+X1)*(Y2+X2) in + let C := T1*k*T2 in + let D := Z1*2*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 + mkExtended (mkProjective X3 Y3 Z3) T3. + + Delimit Scope extendedM1_scope with extendedM1. + Infix "+" := unifiedAdd : extendedM1_scope. + + Lemma unifiedAddCon : forall (P1 P2:point) + (hv1:extendedValid P1) (hv2:extendedValid P2), + extendedValid (P1 + P2)%extendedM1. + Proof. + intros. + remember ((P1+P2)%extendedM1) as P3. + destruct P1 as [[X1 Y1 Z1] T1]. + destruct P2 as [[X2 Y2 Z2] T2]. + destruct P3 as [[X3 Y3 Z3] T3]. + unfold extendedValid, extendedToProjective, projectiveToTwisted, Curve.projX, Curve.projY in *. + invcs HeqP3. + subst. + (* field. -- fails. but it works in sage: sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2"); print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) == ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * (2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * ((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * - ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) / - ((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * - (2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))' - Outputs: - True - *) - Admitted. - - Ltac extended0 := repeat progress (autounfold; simpl); intros; - repeat match goal with - | [ x : Spec.point |- _ ] => destruct x - | [ x : point |- _ ] => destruct x - | [ x : projective |- _ ] => destruct x - end; simpl in *; subst. - - Ltac extended := extended0; repeat (ring || f_equal)(*; field*). - - Lemma unifiedAddToTwisted : forall (P1 P2 : point) (tP1 tP2 : Spec.point) - (P1con : extendedValid P1) (P1on : Spec.onCurve tP1) (P1rep : extendedToTwisted P1 = tP1) - (P2con : extendedValid P2) (P2on : Spec.onCurve tP2) (P2rep : extendedToTwisted P2 = tP2), - extendedToTwisted (P1 + P2)%extendedM1 = Spec.unifiedAdd tP1 tP2. - Proof. - extended0. - apply f_equal2. - (* case 1 verified by hand: follows from field and completeness of edwards addition *) - (* field should work here *) - Admitted. - - Lemma unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ). - Proof. - split; rep. - apply unifiedAddToTwisted; auto. - apply unifiedAddCon; auto. - Qed. - - Module Spec := Spec. - End Format. - End Minus1Twisted. + ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) / + ((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * + (2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))' + Outputs: + True + *) + Admitted. + Ltac extended0 := repeat progress (autounfold; simpl); intros; + repeat match goal with + | [ x : Curve.point |- _ ] => destruct x + | [ x : point |- _ ] => destruct x + | [ x : projective |- _ ] => destruct x + end; simpl in *; subst. - (* - (** [precomputed] represents a point on an elliptic curve using "precomputed" - * Edwards coordinates, as used for fixed-base scalar multiplication - * (see <http://ed25519.cr.yp.to/ed25519-20110926.pdf> section 4: addition). *) - Record precomputed := mkPrecomputed {precomputedSum : GF; - precomputedDifference : GF; - precomputed2dxy : GF}. - Definition twistedToPrecomputed (d:GF) (P : twisted) : precomputed := - let x := twistedX P in - let y := twistedY P in - mkPrecomputed (y+x) (y-x) (2*d*x*y). - *) + Ltac extended := extended0; repeat (ring || f_equal)(*; field*). + Lemma unifiedAddToTwisted : forall (P1 P2 : point) (tP1 tP2 : Curve.point) + (P1con : extendedValid P1) (P1on : Curve.onCurve tP1) (P1rep : extendedToTwisted P1 = tP1) + (P2con : extendedValid P2) (P2on : Curve.onCurve tP2) (P2rep : extendedToTwisted P2 = tP2), + extendedToTwisted (P1 + P2)%extendedM1 = Curve.unifiedAdd tP1 tP2. + Proof. + extended0. + apply f_equal2. + (* case 1 verified by hand: follows from field and completeness of edwards addition *) + (* field should work here *) + Admitted. + Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd rP rQ). + Proof. + split; rep. + apply unifiedAddToTwisted; auto. + apply unifiedAddCon; auto. + Qed. + + Module Curve := Curve. + End Minus1Format. + +End Minus1Twisted. + + +(* +(** [precomputed] represents a point on an elliptic curve using "precomputed" +* Edwards coordinates, as used for fixed-base scalar multiplication +* (see <http://ed25519.cr.yp.to/ed25519-20110926.pdf> section 4: addition). *) +Record precomputed := mkPrecomputed {precomputedSum : GF; + precomputedDifference : GF; + precomputed2dxy : GF}. +Definition twistedToPrecomputed (d:GF) (P : twisted) : precomputed := +let x := twistedX P in +let y := twistedY P in +mkPrecomputed (y+x) (y-x) (2*d*x*y). +*) + +Module WeirstrassMontgomery (Import M : Modulus). + Module Import GT := GaloisTheory M. + Local Open Scope GF_scope. + Local Notation "2" := (1+1). + Local Notation "3" := (1+1+1). + Local Notation "4" := (1+1+1+1). + Local Notation "27" := (3*3*3). (** [weierstrass] represents a point on an elliptic curve using Weierstrass * coordinates (<http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf>) definition 13.1*) Record weierstrass := mkWeierstrass {weierstrassX : GF; weierstrassY : GF}. Definition weierstrassOnCurve (a1 a2 a3 a4 a5 a6:GF) (P : weierstrass) : Prop := - let x := weierstrassX P in - let y := weierstrassY P in - y^2 + a1*x*y + a3*y = x^3 + a2*x^2 + a4*x + a6. + let x := weierstrassX P in + let y := weierstrassY P in + y^2 + a1*x*y + a3*y = x^3 + a2*x^2 + a4*x + a6. (** [montgomery] represents a point on an elliptic curve using Montgomery * coordinates (see <https://en.wikipedia.org/wiki/Montgomery_curve>) *) Record montgomery := mkMontgomery {montgomeryX : GF; montgomeryY : GF}. Definition montgomeryOnCurve (B A:GF) (P : montgomery) : Prop := - let x := montgomeryX P in - let y := montgomeryY P in - B*y^2 = x^3 + A*x^2 + x. + let x := montgomeryX P in + let y := montgomeryY P in + B*y^2 = x^3 + A*x^2 + x. (** see <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> section 13.2.3.c and <https://en.wikipedia.org/wiki/Montgomery_curve#Equivalence_with_Weierstrass_curves> *) Definition montgomeryToWeierstrass (B A:GF) (P : montgomery) : weierstrass := - let x := montgomeryX P in - let y := montgomeryY P in - mkWeierstrass (x/B + A/(3*B)) (y/B). - - Lemma montgomeryToWeierstrassOnCurve : forall (B A:GF) (P:montgomery), - let a4 := 1/B^2 - A^2/(3*B^2) in - let a6 := 0- A^3/(27*B^3) - a4*A/(3*B) in - let P' := montgomeryToWeierstrass B A P in - montgomeryOnCurve B A P -> weierstrassOnCurve 0 0 0 a4 0 a6 P'. + let x := montgomeryX P in + let y := montgomeryY P in + mkWeierstrass (x/B + A/(3*B)) (y/B). + + Lemma montgomeryToWeierstrassOnCurve : forall (B A:GF) (P:montgomery), + let a4 := 1/B^2 - A^2/(3*B^2) in + let a6 := 0- A^3/(27*B^3) - a4*A/(3*B) in + let P' := montgomeryToWeierstrass B A P in + montgomeryOnCurve B A P -> weierstrassOnCurve 0 0 0 a4 0 a6 P'. Proof. - intros. - unfold montgomeryToWeierstrass, montgomeryOnCurve, weierstrassOnCurve in *. - remember (weierstrassY P') as y in *. - remember (weierstrassX P') as x in *. - remember (montgomeryX P) as u in *. - remember (montgomeryY P) as v in *. - clear Hequ Heqv Heqy Heqx P'. - (* This is not currently important and makes field run out of memory. Maybe - * because I transcribed it incorrectly... *) + intros. + unfold montgomeryToWeierstrass, montgomeryOnCurve, weierstrassOnCurve in *. + remember (weierstrassY P') as y in *. + remember (weierstrassX P') as x in *. + remember (montgomeryX P) as u in *. + remember (montgomeryY P) as v in *. + clear Hequ Heqv Heqy Heqx P'. + (* This is not currently important and makes field run out of memory. Maybe + * because I transcribed it incorrectly... *) Abort. (* from <http://www.hyperelliptic.org/EFD/g1p/auto-montgom.html> *) - Definition montgomeryAddDistinct (B A:GF) (P1 P2:montgomery) : montgomery := - let x1 := montgomeryX P1 in - let y1 := montgomeryY P1 in - let x2 := montgomeryX P2 in - let y2 := montgomeryY P2 in - mkMontgomery - (B*(y2-y1)^2/(x2-x1)^2-A-x1-x2) - ((2*x1+x2+A)*(y2-y1)/(x2-x1)-B*(y2-y1)^3/(x2-x1)^3-y1). + Definition montgomeryAddDistinct (B A:GF) (P1 P2:montgomery) : montgomery := + let x1 := montgomeryX P1 in + let y1 := montgomeryY P1 in + let x2 := montgomeryX P2 in + let y2 := montgomeryY P2 in + mkMontgomery + (B*(y2-y1)^2/(x2-x1)^2-A-x1-x2) + ((2*x1+x2+A)*(y2-y1)/(x2-x1)-B*(y2-y1)^3/(x2-x1)^3-y1). Definition montgomeryDouble (B A:GF) (P1:montgomery) : montgomery := - let x1 := montgomeryX P1 in - let y1 := montgomeryY P1 in - mkMontgomery - (B*(3*x1^2+2*A*x1+1)^2/(2*B*y1)^2-A-x1-x1) - ((2*x1+x1+A)*(3*x1^2+2*A*x1+1)/(2*B*y1)-B*(3*x1^2+2*A*x1+1)^3/(2*B*y1)^3-y1). + let x1 := montgomeryX P1 in + let y1 := montgomeryY P1 in + mkMontgomery + (B*(3*x1^2+2*A*x1+1)^2/(2*B*y1)^2-A-x1-x1) + ((2*x1+x1+A)*(3*x1^2+2*A*x1+1)/(2*B*y1)-B*(3*x1^2+2*A*x1+1)^3/(2*B*y1)^3-y1). Definition montgomeryNegate P := mkMontgomery (montgomeryX P) (0-montgomeryY P). (** [montgomeryXFrac] represents a point on an elliptic curve using Montgomery x @@ -442,38 +403,49 @@ Module PointFormats. Definition montgomeryXFracToMontgomeryX P : GF := (montgomeryXFracX P) / (montgomeryXFracZ P). (* from <http://www.hyperelliptic.org/EFD/g1p/auto-montgom-xz.html#ladder-mladd-1987-m>, - * also appears in <https://tools.ietf.org/html/draft-josefsson-tls-curve25519-06#appendix-A.1.3> *) + * also appears in <https://tools.ietf.org/html/draft-josefsson-tls-curve25519-06#appendix-A.1.3> *) Definition montgomeryDifferentialDoubleAndAdd (a : GF) - (X1 : GF) (P2 P3 : montgomeryXFrac) : (montgomeryXFrac * montgomeryXFrac) := - let X2 := montgomeryXFracX P2 in - let Z2 := montgomeryXFracZ P2 in - let X3 := montgomeryXFracX P3 in - let Z3 := montgomeryXFracZ P3 in - let A := X2 + Z2 in - let AA := A^2 in - let B := X2 - Z2 in - let BB := B^2 in - let E := AA - BB in - let C := X3 + Z3 in - let D := X3 - Z3 in - let DA := D * A in - let CB := C * B in - let X5 := (DA + CB)^2 in - let Z5 := X1 * (DA - CB)^2 in - let X4 := AA * BB in - let Z4 := E * (BB + (a-2)/4 * E) in - (mkMontgomeryXFrac X4 Z4, mkMontgomeryXFrac X5 Z5). + (X1 : GF) (P2 P3 : montgomeryXFrac) : (montgomeryXFrac * montgomeryXFrac) := + let X2 := montgomeryXFracX P2 in + let Z2 := montgomeryXFracZ P2 in + let X3 := montgomeryXFracX P3 in + let Z3 := montgomeryXFracZ P3 in + let A := X2 + Z2 in + let AA := A^2 in + let B := X2 - Z2 in + let BB := B^2 in + let E := AA - BB in + let C := X3 + Z3 in + let D := X3 - Z3 in + let DA := D * A in + let CB := C * B in + let X5 := (DA + CB)^2 in + let Z5 := X1 * (DA - CB)^2 in + let X4 := AA * BB in + let Z4 := E * (BB + (a-2)/4 * E) in + (mkMontgomeryXFrac X4 Z4, mkMontgomeryXFrac X5 Z5). (* (* <https://eprint.iacr.org/2008/013.pdf> Theorem 3.2. *) (* TODO: exceptional points *) - Definition twistedToMontfomery (a d:GF) (P : twisted) : montgomery := - let x := twistedX P in - let y := twistedY P in - mkMontgomery ((1+y)/(1-y)) ((1+y)/((1-y)*x)). + Definition twistedToMontfomery (a d:GF) (P : twisted) : montgomery := + let x := twistedX P in + let y := twistedY P in + mkMontgomery ((1+y)/(1-y)) ((1+y)/((1-y)*x)). Definition montgomeryToTwisted (B A:GF) (P : montgomery) : twisted := - let X := montgomeryX P in - let Y := montgomeryY P in - mkTwisted (X/Y) ((X-1)/(X+1)). - *) -End PointFormats. + let X := montgomeryX P in + let Y := montgomeryY P in + mkTwisted (X/Y) ((X-1)/(X+1)). + *) + +End WeirstrassMontgomery. + +(* FIXME: remove after [field] with modulus as a parameter (34d9f8a6e6a4be439d1c56a8b999d2c21ee12a46) is fixed *) +Require Import Zpower ZArith Znumtheory. +Definition two_255_19 := (two_p 255) - 19. +Lemma two_255_19_prime : prime two_255_19. Admitted. +Definition prime25519 := exist _ two_255_19 two_255_19_prime. +Module M <: Modulus. + Definition modulus := prime25519. +End M. + |