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 *) 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: * * * *) 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 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. (* TODO: split module here? *) 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 M := CompleteTwistedEdwardsSpec ta td. Import M. 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" 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" 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. 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. 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. twisted. Qed. End CompleteTwistedEdwardsFacts. 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 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. Qed. Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP. trivialRep. 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 M := CompleteTwistedEdwardsSpec ta td. Module Format <: CompleteTwistedEdwardsPointFormat ta td. Module Spec := CompleteTwistedEdwardsSpec ta td. (** [projective] represents a point on an elliptic curve using projective * Edwards coordinates for twisted edwards curves with a=-1 (see * * ) *) 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. (* FIXME: this is copied from CompleteTwistedEdwardsFacts because I don't know how to get it to be in scope here *) Ltac twisted := autounfold; intros; repeat match goal with | [ x : Spec.point |- _ ] => destruct x end; simpl; repeat (ring || f_equal); field. twisted. Qed. (** [extended] represents a point on an elliptic curve using extended projective * Edwards coordinates with twist a=-1 (see ). *) 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). 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). 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. rep. Qed. Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP. rep. Qed. (** Second equation from section 3.1, also and *) 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: 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). split; rep. apply unifiedAddToTwisted; auto. apply unifiedAddCon; auto. Qed. End Format. End Minus1Twisted. (* (** [precomputed] represents a point on an elliptic curve using "precomputed" * Edwards coordinates, as used for fixed-base scalar multiplication * (see 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). *) (** [weierstrass] represents a point on an elliptic curve using Weierstrass * coordinates () 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. (** [montgomery] represents a point on an elliptic curve using Montgomery * coordinates (see ) *) 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. (** see section 13.2.3.c and *) 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'. 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... *) Abort. (* from *) 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). Definition montgomeryNegate P := mkMontgomery (montgomeryX P) (0-montgomeryY P). (** [montgomeryXFrac] represents a point on an elliptic curve using Montgomery x * coordinate stored as fraction as in * appendix B. *) Record montgomeryXFrac := mkMontgomeryXFrac {montgomeryXFracX : GF; montgomeryXFracZ : GF}. Definition montgomeryToMontgomeryXFrac P := mkMontgomeryXFrac (montgomeryX P) 1. Definition montgomeryXFracToMontgomeryX P : GF := (montgomeryXFracX P) / (montgomeryXFracZ P). (* from , * also appears in *) 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). (* (* 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 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.