diff options
Diffstat (limited to 'src/Curves/PointFormats.v')
-rw-r--r-- | src/Curves/PointFormats.v | 501 |
1 files changed, 240 insertions, 261 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 4c5572ea7..6db178aea 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -1,14 +1,14 @@ - Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Tactics.VerdiTactics. +Require Import Logic.Eqdep_dec. -Module TwistedEdwardsDefs (M : Modulus). +Module GaloisDefs (M : Modulus). Module Export GT := GaloisTheory M. Open Scope GF_scope. -End TwistedEdwardsDefs. +End GaloisDefs. Module Type TwistedEdwardsParams (M : Modulus). - Module Export Defs := TwistedEdwardsDefs M. + Module Export GFDefs := GaloisDefs M. Parameter a : GF. Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. @@ -22,304 +22,293 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> * <https://eprint.iacr.org/2015/677.pdf> *) - Record point := mkPoint {projX : GF; projY : GF}. - Notation "'(' x ',' y ')'" := (mkPoint x y). - Definition zero := (0, 1). - 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. - + Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition point := { P | onCurve P}. + Definition mkPoint := exist onCurve. + + Definition projX (P:point) := fst (proj1_sig P). + Definition projY (P:point) := snd (proj1_sig P). + + Definition checkOnCurve x y : if Zbool.Zeq_bool (a*x^2 + y^2) (1 + d*x^2*y^2) then point else True. + break_if. exists (x, y). exact (GFdecidable _ _ Heqb). trivial. + Defined. + Hint Unfold onCurve mkPoint. + + Definition zero : point. exists (0, 1). + abstract (unfold onCurve; ring). + Defined. + + Definition unifiedAdd' (P1' P2' : (GF*GF)) := + let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). + + Definition unifiedAdd (P1 P2 : point) : point. refine ( + let 'exist P1' pf1 := P1 in + let 'exist P2' pf2 := P2 in + mkPoint (unifiedAdd' P1' P2') _). + Proof. + destruct P1' as [x1 y1], P2' as [x2 y2]; unfold unifiedAdd', onCurve. + admit. (* field will likely work here, but I have not done this by hand *) + Defined. Local Infix "+" := unifiedAdd. - (* Naive implementation *) - Fixpoint scalarMultSpec (n:nat) (P : point) : point := + Fixpoint scalarMult (n:nat) (P : point) : point := match n with | O => zero - | S n' => P + scalarMultSpec n' P + | S n' => P + scalarMult n' P end . - - (* TODO: non-naive *) - Definition scalarMult := scalarMultSpec. - 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 encode : (GF*GF) -> point. + Parameter decode : point -> (GF*GF). Parameter unifiedAdd : point -> point -> point. - Parameter rep : point -> Curve.point -> Prop. + Parameter rep : point -> (GF*GF) -> 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 encode_rep: forall P, encode P ~= P. + Axiom decode_rep : forall P rP, P ~= rP -> decode P = rP. 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. + P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ). 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 + Lemma twistedAddCompletePlus : forall (P1 P2:point), + let '(x1, y1) := proj1_sig P1 in + let '(x2, y2) := proj1_sig 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 + Lemma twistedAddCompleteMinus : forall (P1 P2:point), + let '(x1, y1) := proj1_sig P1 in + let '(x2, y2) := proj1_sig P2 in (1 - d*x1*x2*y1*y2) <> 0. (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *) Admitted. + Lemma point_eq : forall x1 x2 y1 y2, + x1 = x2 -> y1 = y2 -> + forall p1 p2, + mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. + Proof. + intros; subst; f_equal. + apply (UIP_dec). (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) + admit. (* GF_eq_dec *) + Qed. + Hint Resolve point_eq. + Hint Unfold unifiedAdd onCurve. Ltac twisted := autounfold; intros; - repeat match goal with - | [ x : point |- _ ] => destruct x - end; simpl; repeat (ring || f_equal); field. + repeat (match goal with + | [ x : point |- _ ] => destruct x; unfold onCurve in * + | [ x : (GF*GF)%type |- _ ] => destruct x + | [ |- exist _ _ _ = exist _ _ _ ] => eapply point_eq + end; simpl; repeat (ring || f_equal)). 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). + Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C. Proof. - (* uh... I don't actually know where this is proven... *) + (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *) Admitted. - Lemma zeroOnCurve : onCurve (0, 1). - Proof. - twisted. - Qed. Lemma zeroIsIdentity : forall P, P + zero = P. Proof. - admit. - Qed. + twisted. + (* the denominators are 1 and numerators are equal *) + Admitted. End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. - Module Export Defs := TwistedEdwardsDefs M. + Module Export GFDefs := GaloisDefs M. Open Scope GF_scope. - Definition a := 0 - 1. + Definition a := inject (- 1). Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End Minus1Params. -Module Minus1Twisted (M : Modulus) (Import P : Minus1Params M). - Module Import Curve := CompleteTwistedEdwardsCurve M P. +Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P. + Module Import Facts := CompleteTwistedEdwardsFacts M P. + Module Import Curve := Facts.Curve. + (** [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 : (GF*GF)) : projective := + let '(x, y) := P in (x, y, 1). + + Definition projectiveToTwisted (P : projective) : GF * GF := + let 'mkProjective X Y Z := P in + pair (X/Z) (Y/Z). + Hint Unfold projectiveToTwisted twistedToProjective. + + Lemma GFdiv_1 : forall x, x/1 = x. + Admitted. + Hint Resolve GFdiv_1. + + Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P. + Proof. + twisted; eapply GFdiv_1. + 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}. + + 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 : (GF*GF)) : point := + let '(x, y) := P in (x, y, 1, x*y). + Definition encode P := let '(x, y) := P in twistedToExtended (x, y). + + Definition decode (P : point) := + projectiveToTwisted (extendedToProjective P). + Local Hint Unfold extendedValid twistedToExtended decode projectiveToTwisted Curve.unifiedAdd'. + + Lemma twistedExtendedInv : forall P, + decode (twistedToExtended P) = P. + Proof. + twisted; eapply GFdiv_1. + Qed. + + Lemma twistedToExtendedValid : forall P, extendedValid (twistedToExtended P). + Proof. + autounfold. + destruct P. + simpl. + rewrite GFdiv_1; reflexivity. + Qed. + + Definition rep (P:point) (rP:(GF*GF)) : Prop := + decode P = rP /\ extendedValid P. + Local Notation "P '~=' rP" := (rep P rP) (at level 70). + Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with + | [ x : rep ?a ?b |- _ ] => destruct x + end). + + Lemma encode_rep : forall P, encode P ~= P. + Proof. + split. + apply twistedExtendedInv. + apply twistedToExtendedValid. + Qed. - Module Minus1Format <: CompleteTwistedEdwardsPointFormat M P. - Module Import Facts := CompleteTwistedEdwardsFacts M P. - (** [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. - admit. - 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 : 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. - apply twistedProjectiveInv. - Qed. - - Lemma twistedToExtendedValid : forall (P : Curve.point), extendedValid (twistedToExtended P). - Proof. - autounfold. - destruct P. - simpl. - admit. - (* field. *) - Qed. - - 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. - split. - apply twistedExtendedInv. - apply twistedToExtendedValid. - Qed. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - Definition projX P := Curve.projX (extendedToTwisted P). - Definition projY P := Curve.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 = Curve.projX rP. - Proof. - rep. - Qed. - Lemma projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP. - Proof. - rep. - Qed. - - 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 : Curve.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 : 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. + Lemma decode_rep : forall P rP, P ~= rP -> decode P = rP. + Proof. + rep. + Qed. + + + 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 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 : Curve.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 + (P1con : extendedValid P1) (P1on : Curve.onCurve tP1) (P1rep : decode P1 = tP1) + (P2con : extendedValid P2) (P2on : Curve.onCurve tP2) (P2rep : decode P2 = tP2), + decode (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 *) + 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. +End Minus1Format. (* @@ -443,13 +432,3 @@ Module WeirstrassMontgomery (Import M : Modulus). *) 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. - |