aboutsummaryrefslogtreecommitdiff
path: root/src/Curves/Edwards
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2017-04-06 22:53:07 -0400
committerGravatar Andres Erbsen <andreser@mit.edu>2017-04-06 22:53:07 -0400
commitc9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch)
treedb7187f6984acff324ca468e7b33d9285806a1eb /src/Curves/Edwards
parent21198245dab432d3c0ba2bb8a02254e7d0594382 (diff)
rename-everything
Diffstat (limited to 'src/Curves/Edwards')
-rw-r--r--src/Curves/Edwards/AffineProofs.v316
-rw-r--r--src/Curves/Edwards/Montgomery.v114
-rw-r--r--src/Curves/Edwards/Pre.v46
-rw-r--r--src/Curves/Edwards/XYZT.v140
4 files changed, 616 insertions, 0 deletions
diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v
new file mode 100644
index 000000000..2d1db7126
--- /dev/null
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -0,0 +1,316 @@
+Require Export Crypto.Spec.CompleteEdwardsCurve.
+
+Require Import Crypto.Algebra.Hierarchy Crypto.Util.Decidable.
+Require Import Coq.Logic.Eqdep_dec.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Crypto.Util.Tuple Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SetoidSubst.
+Require Export Crypto.Util.FixCoqMistakes.
+
+Module E.
+ Import Group ScalarMult Ring Field CompleteEdwardsCurve.E.
+
+ Notation onCurve_zero := Pre.onCurve_zero.
+ Notation denominator_nonzero := Pre.denominator_nonzero.
+ Notation denominator_nonzero_x := Pre.denominator_nonzero_x.
+ Notation denominator_nonzero_y := Pre.denominator_nonzero_y.
+ Notation onCurve_add := Pre.onCurve_add.
+
+ Section CompleteEdwardsCurveTheorems.
+ Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+ {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 Infix "+" := Fadd. Local Infix "*" := Fmul.
+ Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+ Local Notation "x ^ 2" := (x*x).
+
+ Context {a d: F}
+ {nonzero_a : a <> 0}
+ {square_a : exists sqrt_a, sqrt_a^2 = a}
+ {nonsquare_d : forall x, x^2 <> d}.
+
+ Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
+ Local Notation point := (@E.point F Feq Fone Fadd Fmul a d).
+ Local Notation eq := (@E.eq F Feq Fone Fadd Fmul a d).
+ Local Notation zero := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
+ Local Notation add := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+ Local Notation mul := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+
+ Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)).
+ Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed.
+
+ Ltac t_step :=
+ match goal with
+ | _ => solve [trivial | exact _ ]
+ | _ => intro
+ | |- Equivalence _ => split
+ | |- abelian_group => split | |- group => split | |- monoid => split
+ | |- is_associative => split | |- is_commutative => split
+ | |- is_left_inverse => split | |- is_right_inverse => split
+ | |- is_left_identity => split | |- is_right_identity => split
+ | _ => progress destruct_head' @E.point
+ | _ => progress destruct_head' prod
+ | _ => progress destruct_head' and
+ | |- context[E.add ?P ?Q] =>
+ unique pose proof (Pre.denominator_nonzero_x _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q));
+ unique pose proof (Pre.denominator_nonzero_y _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q))
+ | _ => progress cbv [opp E.zero E.eq E.add E.coordinates proj1_sig fieldwise fieldwise'] in *
+ (* [_gather_nonzeros] must run before [fst_pair] or [simpl] but after splitting E.eq and unfolding [E.add] *)
+ | |- _ /\ _ => split | |- _ <-> _ => split
+ end.
+ Ltac t := repeat t_step; fsatz.
+
+ Global Instance associative_add : is_associative(eq:=E.eq)(op:=add).
+ Proof using Type.
+ (* [nsatz_compute] for a denominator runs out of 6GB of stack space *)
+ (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5359 *)
+ Add Field _field : (Algebra.Field.field_theory_for_stdlib_tactic (T:=F)).
+ Import Field_tac.
+ repeat t_step; (field_simplify_eq; [IntegralDomain.nsatz|]); repeat split; trivial.
+ { intro. eapply H3. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+ { intro. eapply H. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+ { intro. eapply H4. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+ { intro. eapply H0. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+ Qed.
+
+ Global Instance edwards_curve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
+ Proof using Type. t. Qed.
+
+ Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof using Type. repeat t_step. Qed.
+
+ Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
+ Proof using Type.
+ intros n n'; repeat intro; subst n'.
+ induction n; (reflexivity || eapply (_:Proper (eq==>eq==>eq) add); eauto).
+ Qed.
+
+ Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul.
+ Proof using Type. split; intros; (reflexivity || exact _). Qed.
+
+ Section PointCompression.
+ Local Notation "x ^ 2" := (x*x).
+
+ Lemma solve_correct x y : onCurve x y <-> (x^2 = (y^2-1) / (d*y^2-a)).
+ Proof using Feq_dec field nonsquare_d nonzero_a square_a. destruct square_a as [sqrt_a]; pose proof (nonsquare_d (sqrt_a/y));
+ split; intros; fsatz. Qed.
+
+ (* TODO: move *)
+ Definition exist_option {A} (P : A -> Prop) (x : option A)
+ : match x with Some v => P v | None => True end -> option { a : A | P a }.
+ destruct x; intros; [apply Some | apply None]; eauto. Defined.
+ Lemma exist_option_Some {A} P (x:option A) pf s
+ (H:Logic.eq (exist_option P x pf) (Some s))
+ : Logic.eq x (Some (proj1_sig s)).
+ Proof using Type. destruct x, s; cbv [exist_option proj1_sig] in *; congruence. Qed.
+ Lemma exist_option_None {A} P (x:option A) pf
+ (H:Logic.eq (exist_option P x pf) None)
+ : Logic.eq x None.
+ Proof using Type. destruct x; cbv [exist_option proj1_sig] in *; congruence. Qed.
+
+ Context
+ {sqrt_div:F -> F -> option F}
+ {sqrt_Some: forall u v r, Logic.eq (sqrt_div u v) (Some r) -> r^2 = u/v}
+ {sqrt_None: forall u v, Logic.eq (sqrt_div u v) None -> forall r, r^2 <> u/v}
+ {parity:F -> bool} {Proper_parity: Proper (Feq ==> Logic.eq) parity}
+ {parity_opp: forall x, x <> 0 -> Logic.eq (parity (Fopp x)) (negb (parity x)) }.
+
+ Definition compress (P:point) : (bool*F) :=
+ let (x, y) := coordinates P in pair (parity x) y.
+ Definition set_sign r p : option F :=
+ if dec (Logic.eq (parity r) p)
+ then Some r
+ else
+ let r' := Fopp r in
+ if dec (Logic.eq (parity r') p)
+ then Some r'
+ else None.
+ Lemma set_sign_None r p s (H:Logic.eq (set_sign r p) (Some s))
+ : s^2 = r^2 /\ Logic.eq (parity s) p.
+ Proof using Feq_dec field nonzero_a.
+ repeat match goal with
+ | _ => progress subst
+ | _ => progress cbv [set_sign] in *
+ | _ => progress break_match_hyps
+ | _ => progress Option.inversion_option
+ | _ => split
+ | _ => solve [ trivial | fsatz ]
+ end.
+ Qed.
+ Lemma set_sign_Some r p (H:Logic.eq (set_sign r p) None)
+ : forall s, s^2 = r^2 -> not (Logic.eq (parity s) p).
+ repeat match goal with
+ | _ => progress intros
+ | _ => progress subst
+ | _ => progress cbv [set_sign] in *
+ | _ => progress break_match_hyps
+ | _ => progress Option.inversion_option
+ end.
+ destruct (dec (r = 0)).
+ assert (s = 0); [|solve[setoid_subst_rel Feq; trivial] ].
+ admit.
+ progress rewrite parity_opp in * by assumption.
+ destruct (parity r), p; cbv [negb] in *; congruence.
+ Admitted.
+
+ Local Ltac t_step :=
+ match goal with
+ | _ => progress subst
+ | _ => progress destruct_head' @E.point
+ | _ => progress destruct_head' and
+ | _ => progress break_match
+ | _ => progress break_match_hyps
+ | _ => progress Option.inversion_option
+ | _ => progress Prod.inversion_prod
+ | H:_ |- _ => unique pose proof (sqrt_Some _ _ _ H); clear H
+ | H:_ |- _ => unique pose proof (sqrt_None _ _ H); clear H
+ | H:_ |- _ => unique pose proof (set_sign_None _ _ _ H); clear H
+ | H:_ |- _ => unique pose proof (set_sign_Some _ _ H); clear H
+ | H:_ |- _ => unique pose proof (exist_option_Some _ _ _ _ H); clear H
+ | H:_ |- _ => unique pose proof (exist_option_None _ _ _ H); clear H
+ | _ => solve [trivial | eapply solve_correct; fsatz]
+ end.
+ Local Ltac t := repeat t_step.
+
+ Program Definition decompress (b:bool*F) : option point :=
+ exist_option _
+ match b return option (F*F) with
+ (p, y) =>
+ match sqrt_div (y^2 - 1) (d*y^2 - a) return option (F*F) with
+ | None => None
+ | Some r =>
+ match set_sign r p return option (F*F) with
+ | Some x => Some (x, y)
+ | None => None
+ end
+ end
+ end _.
+ Next Obligation. t. Qed.
+
+ Lemma decompress_Some b P (H:Logic.eq (decompress b) (Some P))
+ : Logic.eq (compress P) b.
+ Proof using Type. cbv [compress decompress] in *; t. Qed.
+
+ Lemma decompress_None b (H:Logic.eq (decompress b) None)
+ : forall P, not (Logic.eq (compress P) b).
+ Proof.
+ cbv [compress decompress exist_option coordinates] in *; intros.
+ t.
+ intro.
+ apply (H0 f); [|congruence].
+ admit.
+ intro. Prod.inversion_prod; subst.
+ rewrite solve_correct in y.
+ eapply H. eapply y.
+ Admitted.
+ End PointCompression.
+ End CompleteEdwardsCurveTheorems.
+ Section Homomorphism.
+ Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {Fchar_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+ {Feq_dec:DecidableRel Feq}.
+
+ Context {Fa Fd: F}
+ {nonzero_a : not (Feq Fa Fzero)}
+ {square_a : exists sqrt_a, Feq (Fmul sqrt_a sqrt_a) Fa}
+ {nonsquare_d : forall x, not (Feq (Fmul x x) Fd)}.
+
+ Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
+ {fieldK: @Algebra.Hierarchy.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
+ {Keq_dec:DecidableRel Keq}.
+ Context {FtoK:F->K} {HFtoK:@Ring.is_homomorphism F Feq Fone Fadd Fmul
+ K Keq Kone Kadd Kmul FtoK}.
+ Context {KtoF:K->F} {HKtoF:@Ring.is_homomorphism K Keq Kone Kadd Kmul
+ F Feq Fone Fadd Fmul KtoF}.
+ Context {HisoF:forall x, Feq (KtoF (FtoK x)) x}.
+ Context {Ka} {Ha:Keq (FtoK Fa) Ka} {Kd} {Hd:Keq (FtoK Fd) Kd}.
+
+ Lemma nonzero_Ka : ~ Keq Ka Kzero.
+ Proof using Feq_dec HFtoK HKtoF Ha HisoF Keq_dec field fieldK nonzero_a.
+ rewrite <-Ha.
+ Ring.pull_homomorphism FtoK.
+ intro X.
+ eapply (Monoid.is_homomorphism_phi_proper(phi:=KtoF)) in X.
+ rewrite 2HisoF in X.
+ auto.
+ Qed.
+
+ Lemma square_Ka : exists sqrt_a, Keq (Kmul sqrt_a sqrt_a) Ka.
+ Proof using Feq_dec HFtoK Ha Keq_dec field fieldK square_a.
+ destruct square_a as [sqrt_a]. exists (FtoK sqrt_a).
+ Ring.pull_homomorphism FtoK. rewrite <-Ha.
+ eapply Monoid.is_homomorphism_phi_proper; assumption.
+ Qed.
+
+ Lemma nonsquare_Kd : forall x, not (Keq (Kmul x x) Kd).
+ Proof using Feq_dec HKtoF Hd HisoF Keq_dec field fieldK nonsquare_d.
+ intros x X. apply (nonsquare_d (KtoF x)).
+ Ring.pull_homomorphism KtoF. rewrite X. rewrite <-Hd, HisoF.
+ reflexivity.
+ Qed.
+
+ (* TODO: character respects isomorphism *)
+ Global Instance Kchar_ge_2 :
+ @char_ge K Keq Kzero Kone Kopp Kadd Ksub Kmul (BinNat.N.succ_pos BinNat.N.two).
+ Proof.
+ intros p Hp X; apply (Fchar_ge_3 p Hp).
+ eapply Monoid.is_homomorphism_phi_proper in X.
+ rewrite (homomorphism_zero(zero:=Fzero)(phi:=KtoF)) in X.
+ etransitivity; [|eexact X]; clear X.
+ (* TODO: Ring.of_Z of isomorphism *)
+ Admitted.
+
+ Local Notation Fpoint := (@E.point F Feq Fone Fadd Fmul Fa Fd).
+ Local Notation Kpoint := (@E.point K Keq Kone Kadd Kmul Ka Kd).
+ Local Notation FzeroP := (E.zero(nonzero_a:=nonzero_a)(d:=Fd)).
+ Local Notation KzeroP := (E.zero(nonzero_a:=nonzero_Ka)(d:=Kd)).
+ Local Notation FaddP := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+ Local Notation KaddP := (E.add(nonzero_a:=nonzero_Ka)(square_a:=square_Ka)(nonsquare_d:=nonsquare_Kd)).
+
+ Obligation Tactic := idtac.
+ Program Definition point_phi (P:Fpoint) : Kpoint := exist _ (
+ let (x, y) := coordinates P in (FtoK x, FtoK y)) _.
+ Next Obligation.
+ destruct P as [ [? ?] ?]; cbv.
+ rewrite <-!Ha, <-!Hd; pull_homomorphism FtoK.
+ eapply Monoid.is_homomorphism_phi_proper; assumption.
+ Qed.
+
+ Lemma Proper_point_phi : Proper (eq==>eq) point_phi.
+ Proof using Type.
+ intros P Q H.
+ destruct P as [ [? ?] ?], Q as [ [? ?] ?], H as [Hl Hr]; cbv.
+ rewrite !Hl, !Hr. split; reflexivity.
+ Qed.
+
+ Lemma lift_ismorphism : @Monoid.is_homomorphism Fpoint eq FaddP
+ Kpoint eq KaddP point_phi.
+ Proof using Type.
+ repeat match goal with
+ | |- _ => intro
+ | |- Monoid.is_homomorphism => split
+ | _ => progress destruct_head' @E.point
+ | _ => progress destruct_head' prod
+ | _ => progress destruct_head' and
+ | |- context[E.add ?P ?Q] =>
+ unique pose proof (Pre.denominator_nonzero_x _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q));
+ unique pose proof (Pre.denominator_nonzero_y _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q))
+ | _ => progress cbv [eq add point_phi coordinates] in *
+ | |- _ /\ _ => split
+ | _ => rewrite !(homomorphism_div(phi:=FtoK)) by assumption
+ | _ => rewrite !Ha
+ | _ => rewrite !Hd
+ | _ => Ring.push_homomorphism FtoK
+ | |- _ ?x ?x => reflexivity
+ | _ => eapply Monoid.is_homomorphism_phi_proper; assumption
+ end.
+ Qed.
+ End Homomorphism.
+End E.
diff --git a/src/Curves/Edwards/Montgomery.v b/src/Curves/Edwards/Montgomery.v
new file mode 100644
index 000000000..d274356c9
--- /dev/null
+++ b/src/Curves/Edwards/Montgomery.v
@@ -0,0 +1,114 @@
+Require Import Crypto.Curves.Edwards.AffineProofs.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.AffineProofs.
+Require Import Crypto.Curves.Montgomery.Affine.
+
+Require Import Crypto.Util.Notations Crypto.Util.Decidable.
+Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Algebra.Field.
+Import BinNums.
+
+Module E.
+ Section EdwardsMontgomery.
+ Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}
+ {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 Infix "+" := Fadd. Local Infix "*" := Fmul.
+ Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+ Local Notation "x ^ 2" := (x*x).
+
+ Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
+ Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
+ Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
+ Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
+
+ Context {a d: F}
+ {nonzero_a : a <> 0}
+ {square_a : exists sqrt_a, sqrt_a^2 = a}
+ {nonsquare_d : forall x, x^2 <> d}.
+ Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
+ Local Notation Ezero := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
+ Local Notation Eadd := (E.add(char_ge_3:=char_ge_3)(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+ Local Notation Eopp := (E.opp(nonzero_a:=nonzero_a)(d:=d)).
+
+ Let a_neq_d : a <> d.
+ Proof. intro X.
+ edestruct square_a. eapply nonsquare_d.
+ rewrite <-X. eassumption. Qed.
+
+
+ Local Notation "2" := (1+1). Local Notation "4" := (1+1+1+1).
+ Local Notation MontgomeryA := (2*(a+d)/(a-d)).
+ Local Notation MontgomeryB := (4/(a-d)).
+
+ Let b_nonzero : MontgomeryB <> 0. Proof. fsatz. Qed.
+
+ Local Notation Mpoint := (@M.point F Feq Fadd Fmul MontgomeryA MontgomeryB).
+ Local Notation Madd := (@M.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 MontgomeryA MontgomeryB b_nonzero).
+ Local Notation "'∞'" := (inr tt) : core_scope.
+
+ Ltac t_step :=
+ match goal with
+ | _ => solve [ contradiction | trivial ]
+ | _ => progress intros
+ | _ => progress subst
+ | _ => progress Tactics.DestructHead.destruct_head' @M.point
+ | _ => progress Tactics.DestructHead.destruct_head' @prod
+ | _ => progress Tactics.DestructHead.destruct_head' @sum
+ | _ => progress Tactics.DestructHead.destruct_head' @and
+ | _ => progress Sum.inversion_sum
+ | _ => progress Prod.inversion_prod
+ | _ => progress Tactics.BreakMatch.break_match_hyps
+ | _ => progress Tactics.BreakMatch.break_match
+ | _ => progress cbv [E.coordinates M.coordinates E.add M.add E.zero M.zero E.eq M.eq E.opp M.opp proj1_sig fst snd] in *
+ | |- _ /\ _ => split
+ end.
+ Ltac t := repeat t_step.
+
+ Program Definition to_Montgomery (P:Epoint) : Mpoint :=
+ match E.coordinates P return F*F+_ with
+ | (x, y) =>
+ if dec (y <> 1 /\ x <> 0)
+ then inl ((1+y)/(1-y), (1+y)/(x-x*y))
+ else ∞
+ end.
+ Next Obligation. Proof. t. fsatz. Qed.
+
+ (* The exceptional cases are tricky. *)
+ (* See https://eprint.iacr.org/2008/013.pdf page 5 before continuing *)
+
+ Program Definition of_Montgomery (P:Mpoint) : Epoint :=
+ match M.coordinates P return F*F with
+ | inl (x,y) =>
+ if dec (y = 0)
+ then (0, Fopp 1)
+ else (x/y, (x-1)/(x+1))
+ | ∞ => pair 0 1
+ end.
+ Next Obligation.
+ Proof.
+ t; try fsatz.
+ assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz.
+ Admitted.
+
+ Program Definition _EM (discr_nonzero:id _) : _ /\ _ /\ _ :=
+ @Group.group_from_redundant_representation
+ Mpoint M.eq Madd M.zero M.opp
+ (M.group discr_nonzero)
+ Epoint E.eq Eadd Ezero Eopp
+ of_Montgomery
+ to_Montgomery
+ _ _ _ _ _
+ .
+ Next Obligation. Proof. Admitted. (* M->E->M *)
+ Next Obligation. Proof. Admitted. (* equivalences match *)
+ Next Obligation. Proof. Admitted. (* add *)
+ Next Obligation. Proof. Admitted. (* opp *)
+ Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed.
+
+ Global Instance homomorphism_of_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 (_EM discr_nonzero)).
+ Global Instance homomorphism_to_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 (_EM discr_nonzero)).
+ End EdwardsMontgomery.
+End E.
diff --git a/src/Curves/Edwards/Pre.v b/src/Curves/Edwards/Pre.v
new file mode 100644
index 000000000..244acc9b5
--- /dev/null
+++ b/src/Curves/Edwards/Pre.v
@@ -0,0 +1,46 @@
+Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid Crypto.Util.Relations.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.Field.
+Require Import Crypto.Util.Notations Crypto.Util.Decidable (*Crypto.Util.Tactics*).
+Require Import Coq.PArith.BinPos.
+
+Section Edwards.
+ Context {F eq zero one opp add sub mul inv div}
+ {field:@Algebra.Hierarchy.field F eq zero one opp add sub mul inv div}
+ {eq_dec:DecidableRel eq}.
+
+ Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
+ Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+ Local Notation "0" := zero. Local Notation "1" := one.
+ Local Infix "+" := add. Local Infix "*" := mul.
+ Local Infix "-" := sub. Local Infix "/" := div.
+ Local Notation "x ^ 2" := (x*x).
+
+ Context (a:F) (a_nonzero : a<>0) (a_square : exists sqrt_a, sqrt_a^2 = a).
+ Context (d:F) (d_nonsquare : forall sqrt_d, sqrt_d^2 <> d).
+ Context {char_ge_3:@Ring.char_ge F eq zero one opp add sub mul 3}.
+
+ Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
+ Lemma onCurve_zero : onCurve 0 1.
+ Proof using a_nonzero eq_dec field.
+ fsatz. Qed.
+
+ Section Addition.
+ Context (x1 y1:F) (P1onCurve: onCurve x1 y1).
+ Context (x2 y2:F) (P2onCurve: onCurve x2 y2).
+ Lemma denominator_nonzero : (d*x1*x2*y1*y2)^2 <> 1.
+ Proof using Type*.
+ destruct a_square as [sqrt_a], (dec(sqrt_a*x2+y2 = 0)), (dec(sqrt_a*x2-y2 = 0));
+ try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ]
+ => pose proof (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
+ /(f (sqrt_a * x2) y2 * x1 * y1 )))
+ end; Field.fsatz.
+ Qed.
+
+ Lemma denominator_nonzero_x : 1 + d*x1*x2*y1*y2 <> 0.
+ Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed.
+ Lemma denominator_nonzero_y : 1 - d*x1*x2*y1*y2 <> 0.
+ Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed.
+ Lemma onCurve_add : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)).
+ Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed.
+ End Addition.
+End Edwards. \ No newline at end of file
diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v
new file mode 100644
index 000000000..160866b64
--- /dev/null
+++ b/src/Curves/Edwards/XYZT.v
@@ -0,0 +1,140 @@
+Require Import Coq.Classes.Morphisms.
+
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.AffineProofs.
+
+Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings.
+Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.UniquePose.
+
+Module Extended.
+ Section ExtendedCoordinates.
+ Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+ {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+ {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 Infix "+" := Fadd. Local Infix "*" := Fmul.
+ Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+ Local Notation "x ^ 2" := (x*x).
+
+ Context {a d: F}
+ {nonzero_a : a <> 0}
+ {square_a : exists sqrt_a, sqrt_a^2 = a}
+ {nonsquare_d : forall x, x^2 <> d}.
+ 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).
+ (** [Extended.point] represents a point on an elliptic curve using extended projective
+ * Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
+ Definition point := { P | let '(X,Y,Z,T) := P in
+ a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2
+ /\ X * Y = Z * T
+ /\ Z <> 0 }.
+ Definition coordinates (P:point) : 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
+ Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.
+
+ Ltac t_step :=
+ match goal with
+ | |- Proper _ _ => intro
+ | _ => progress intros
+ | _ => progress destruct_head' prod
+ | _ => progress destruct_head' @E.point
+ | _ => progress destruct_head' point
+ | _ => progress destruct_head' and
+ | _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in *
+ | |- _ /\ _ => split | |- _ <-> _ => split
+ end.
+ Ltac t := repeat t_step; Field.fsatz.
+
+ Global Instance Equivalence_eq : Equivalence eq.
+ Proof using Feq_dec field nonzero_a. split; repeat intro; t. Qed.
+ Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
+ 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).
+ 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 XY := fst XYZ in let Y := snd XY in
+ let X := fst XY in
+ let iZ := Finv Z in ((X*iZ), (Y*iZ)).
+ Next Obligation. t. Qed.
+ Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted.
+ Proof using Type. cbv [to_twisted]; t. Qed.
+
+ Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P.
+ Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
+ 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).
+ 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.
+ 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) =>
+ let A := (Y1-X1)*(Y2-X2) in
+ let B := (Y1+X1)*(Y2+X2) in
+ let C := T1*twice_d*T2 in
+ let D := Z1*(Z2+Z2) in
+ let E := B-A in
+ let F := D-C in
+ let G := D+C in
+ let H := B+A in
+ let X3 := E*F in
+ let Y3 := G*H in
+ let T3 := E*H in
+ let Z3 := F*G in
+ (X3, Y3, Z3, T3)
+ end.
+ Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))); t. Qed.
+
+ Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : Algebra.Hierarchy.group /\ _ /\ _ :=
+ @Group.group_from_redundant_representation
+ _ _ _ _ _
+ ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a')
+ (nonsquare_d:=nonsquare_d')).(Algebra.Hierarchy.abelian_group_group))
+ _
+ eq
+ m1add
+ zero
+ opp
+ from_twisted
+ to_twisted
+ to_twisted_from_twisted
+ _ _ _ _.
+ Next Obligation. cbv [to_twisted]. t. Qed.
+ Next Obligation.
+ match goal with
+ | |- context[E.add ?P ?Q] =>
+ unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q))
+ end. cbv [to_twisted m1add]. t. Qed.
+ Next Obligation. cbv [to_twisted opp]. t. Qed.
+ Next Obligation. cbv [to_twisted zero]. t. Qed.
+ Global Instance group x y z
+ : Algebra.Hierarchy.group := proj1 (_group_proof x y z).
+ Global Instance homomorphism_from_twisted x y z :
+ Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)).
+ Global Instance homomorphism_to_twisted x y z :
+ Monoid.is_homomorphism := proj2 (proj2 (_group_proof x y z)).
+ End TwistMinusOne.
+ End ExtendedCoordinates.
+End Extended.