rename-everything

12 files changed, 1314 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.
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
new file mode 100644
index 000000000..721908a6a
--- /dev/null
+++ b/src/Curves/Montgomery/Affine.v
@@ -0,0 +1,67 @@
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.GlobalSettings.
+Require Import Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    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}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "- x" := (Fopp x).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
+    Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "'∞'" := unit : type_scope.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+    Local Open Scope core_scope.
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+
+    Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b :=
+      match P return F*F+∞ with
+      | (x, y) => (x, -y)
+      | ∞ => ∞
+      end.
+    Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+
+    Local Notation add := (M.add(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+
+    Section MontgomeryWeierstrass.
+      Local Notation "2" := (1+1).
+      Local Notation "3" := (1+2).
+      Local Notation "4" := (1+3).
+      Local Notation "16" := (4*4).
+      Local Notation "9" := (3*3).
+      Local Notation "27" := (3*9).
+      Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+
+
+      Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
+      Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
+      Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
+      Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
+      Program Definition to_Weierstrass (P:@point) : Wpoint :=
+        match M.coordinates P return F*F+∞ with
+        | (x, y) => ((x + a/3)/b, y/b)
+        | _ => ∞
+        end.
+      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+
+      Program Definition of_Weierstrass (P:Wpoint) : point :=
+        match W.coordinates P return F*F+∞ with
+        | (x,y) => (b*x-a/3, b*y)
+        | _ => ∞
+        end.
+      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+    End MontgomeryWeierstrass.
+  End MontgomeryCurve.
+End M.
\ No newline at end of file
diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v
new file mode 100644
index 000000000..a83109a55
--- /dev/null
+++ b/src/Curves/Montgomery/AffineProofs.v
@@ -0,0 +1,83 @@
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.GlobalSettings.
+Require Import Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine.
+Require Import Crypto.Curves.Weierstrass.AffineProofs.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    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}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+    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.
+      
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "- x" := (Fopp x).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
+    Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "2" := (1+1). Local Notation "3" := (1+2).
+    Local Notation "9" := (3*3). Local Notation "27" := (3*9).
+    Local Notation "'∞'" := unit : type_scope.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+    Local Open Scope core_scope.
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+
+    Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
+    Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
+    Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
+    Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
+    Local Notation Wopp := (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec).
+
+    Ltac t :=
+      repeat
+        match goal with
+        | _ => solve [ 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 [M.coordinates M.add M.zero M.eq M.opp proj1_sig
+                             W.coordinates W.add W.zero W.eq W.opp
+                             M.of_Weierstrass M.to_Weierstrass] in *
+        | |- _ /\ _ => split | |- _ <-> _ => split
+        end.
+
+    Program Definition _MW (discr_nonzero:id _) : _ /\ _ /\ _ :=
+      @Group.group_from_redundant_representation
+        Wpoint W.eq Wadd W.zero Wopp
+        (Algebra.Hierarchy.abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero)))
+        (@M.point F Feq Fadd Fmul a b) M.eq (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero))
+        (M.of_Weierstrass(b_nonzero:=b_nonzero))
+        (M.to_Weierstrass(b_nonzero:=b_nonzero))
+        _ _ _ _ _
+    .
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+
+    Global Instance group discr_nonzero : Algebra.Hierarchy.group := proj1 (_MW discr_nonzero).
+    Global Instance homomorphism_of_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.of_Weierstrass) := proj1 (proj2 (_MW discr_nonzero)).
+    Global Instance homomorphism_to_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.to_Weierstrass) := proj2 (proj2 (_MW discr_nonzero)).
+  End MontgomeryCurve.
+End M.
diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v
new file mode 100644
index 000000000..60020827c
--- /dev/null
+++ b/src/Curves/Montgomery/XZ.v
@@ -0,0 +1,57 @@
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations.
+Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    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}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "x ^ 2" := (x*x).
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+    Local Notation add := (M.add(b_nonzero:=b_nonzero)).
+    Local Notation opp := (M.opp(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+
+    Program Definition to_xz (P:point) : F*F :=
+      match M.coordinates P with
+      | (x, y) => pair x 1
+      | ∞ => pair 1 0
+      end.
+
+    Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+
+    (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *)
+    Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
+    Definition xzladderstep (x1:F) (Q Q':F*F) : ((F*F)*(F*F)) :=
+      match Q, Q' with
+        pair x z, pair x' z' =>
+        dlet A := x+z in
+        dlet B := x-z in
+        dlet AA := A^2 in
+        dlet BB := B^2 in
+        dlet x2 := AA*BB in
+        dlet E := AA-BB in
+        dlet z2 := E*(AA + a24*E) in
+        dlet C := x'+z' in
+        dlet D := x'-z' in
+        dlet CB := C*B in
+        dlet DA := D*A in
+        dlet x3 := (DA+CB)^2 in
+        dlet z3 := x1*(DA-CB)^2 in
+        (pair (pair x2 z2) (pair x3 z3))
+      end.
+  End MontgomeryCurve.
+End M.
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v
new file mode 100644
index 000000000..d24d1398c
--- /dev/null
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -0,0 +1,58 @@
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+Require Import Crypto.Curves.Montgomery.XZ BinPos.
+
+Module M.
+  Section MontgomeryCurve.
+    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}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+
+    Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+    Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
+    Local Notation add := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)).
+    Local Notation opp := (M.opp(a:=a)(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+    Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
+
+    Ltac t :=
+      repeat
+        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 [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig M.xzladderstep M.to_xz Let_In] in *
+        | |- _ /\ _ => split
+        end.
+
+    Lemma xzladderstep_correct
+          (Q Q':point) x z x' z' x1 x2 z2 x3 z3
+          (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z')))
+          (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0  (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end)
+          (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end)
+          (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end):
+      match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\
+      match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end.
+    Proof using a24_correct char_ge_5. t; abstract fsatz. Qed.
+  End MontgomeryCurve.
+End M.
diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v
new file mode 100644
index 000000000..90bb3bdbc
--- /dev/null
+++ b/src/Curves/Weierstrass/Affine.v
@@ -0,0 +1,18 @@
+Require Import Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
+
+Module W.
+  Section W.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:DecidableRel Feq}.
+
+    Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b
+      := match W.coordinates P return F*F+_ with
+         | inl (x1, y1) => inl (x1, Fopp y1)
+         | _ => P
+         end.
+    Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed.
+  End W.
+End W.
\ No newline at end of file
diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v
new file mode 100644
index 000000000..81583d88f
--- /dev/null
+++ b/src/Curves/Weierstrass/AffineProofs.v
@@ -0,0 +1,196 @@
+Require Import Coq.Numbers.BinNums.
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine.
+Require Import Crypto.Algebra.Field Crypto.Algebra.Hierarchy.
+Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
+Require Import Coq.PArith.BinPos.
+
+Module W.
+  Section W.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:DecidableRel Feq}
+            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *)
+    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.
+    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 "-" := Fsub. Local Infix "*" := Fmul.
+    Local Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1).
+
+    Global Instance commutative_group {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : abelian_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp).
+    Proof using Type.
+      Time
+        repeat match goal with
+               | _ => solve [ contradiction | 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' @W.point
+               | _ => progress destruct_head' sum
+               | _ => progress destruct_head' prod
+               | _ => progress destruct_head' unit
+               | _ => progress destruct_head' and
+               | _ => progress cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig]in*
+               | _ => progress break_match
+               end.
+      (* Finished transaction in 2.098 secs (2.099u,0.s) (successful) *)
+      all:  try split.
+      (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *)
+
+      (* The [discriminant_nonzero] hypothesis makes [fsatz] slow but
+      is necessary in some cases. Thus, we wrap it in [id] by detault
+      to hide it from [nsatz] but unfold it when normal [fsatz] fails. *)
+      (* Variable re-ordering is a micro-optimization *)
+      (* TODO: why does par not work here? *)
+      Ltac s := abstract (
+                    match goal with [H:id _ |- _] => move H at bottom end;
+                    move b at bottom;
+                    move a at bottom;
+                    repeat match goal with [H: ?x = Fopp ?y |- _] => is_var x; is_var y; revert H end; intros;
+                    repeat match goal with [H: ?x = ?y |- _] => is_var x; is_var y; revert H end; intros;
+                    repeat split;
+                    solve
+                      [ fsatz
+                      | cbv [id] in *; fsatz]
+                  ).
+      Time s. (* Finished transaction in 0.099 secs (0.096u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 0.094 secs (0.093u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.48 secs (0.48u,0.s) (successful) *)
+      Time s. (* Finished transaction in 2.229 secs (2.226u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 3.164 secs (3.153u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 2.218 secs (2.199u,0.019s) (successful) *)
+      Time s. (* Finished transaction in 3.499 secs (3.486u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 1.164 secs (1.16u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.971 secs (1.953u,0.016s) (successful) *)
+      Time s. (* Finished transaction in 2.344 secs (2.343u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.287 secs (1.286u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.781 secs (1.783u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.497 secs (0.496u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.859 secs (1.856u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.499 secs (1.499u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.6 secs (1.6u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.446 secs (1.443u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.56 secs (1.563u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.62 secs (1.616u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.973 secs (1.966u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 7.66 secs (7.663u,0.s) (successful) *)
+      Time s. (* Finished transaction in 7.645 secs (7.643u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 5.956 secs (5.949u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 7.835 secs (7.803u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.893 secs (1.893u,0.s) (successful) *)
+      Time s. (* Finished transaction in 10.23 secs (10.229u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 11.059 secs (11.036u,0.02s) (successful) *)
+      Time s. (* Finished transaction in 8.965 secs (8.963u,0.s) (successful) *)
+      Time s. (* Finished transaction in 9.539 secs (9.539u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 2.019 secs (2.013u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 2.907 secs (2.9u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 1.622 secs (1.613u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 13.205 secs (13.203u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 14.689 secs (14.686u,0.s) (successful) *)
+      Time s. (* Finished transaction in 10.672 secs (10.673u,0.s) (successful) *)
+      Time s. (* Finished transaction in 13.509 secs (13.509u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.389 secs (1.386u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 10.331 secs (10.329u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 12.182 secs (12.176u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 9.826 secs (9.829u,0.s) (successful) *)
+      Time s. (* Finished transaction in 13.709 secs (13.703u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.059 secs (1.06u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.894 secs (1.896u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.358 secs (1.356u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.537 secs (1.536u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.342 secs (1.343u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.095 secs (1.096u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.157 secs (1.153u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.603 secs (1.603u,0.s) (successful) *)
+      Time s. (* Finished transaction in 6.196 secs (6.196u,0.s) (successful) *)
+      Time s. (* Finished transaction in 6.949 secs (6.949u,0.s) (successful) *)
+      Time s. (* Finished transaction in 4.685 secs (4.68u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 6.483 secs (6.483u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.451 secs (1.453u,0.s) (successful) *)
+      Time s. (* Finished transaction in 13.648 secs (13.646u,0.s) (successful) *)
+      Time s. (* Finished transaction in 18.053 secs (18.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 7.186 secs (7.186u,0.s) (successful) *)
+      Time s. (* Finished transaction in 8.817 secs (8.819u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.251 secs (1.25u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.569 secs (1.569u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.356 secs (1.356u,0.s) (successful) *)
+      Time s. (* Finished transaction in 11.45 secs (11.446u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 17.968 secs (17.969u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 12.418 secs (12.366u,0.046s) (successful) *)
+      Time s. (* Finished transaction in 15.323 secs (15.316u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 1.589 secs (1.586u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 10.22 secs (10.223u,0.s) (successful) *)
+      Time s. (* Finished transaction in 11.887 secs (11.889u,0.s) (successful) *)
+      Time s. (* Finished transaction in 7.284 secs (7.283u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 8.75 secs (8.753u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.291 secs (0.29u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.348 secs (0.346u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.222 secs (0.223u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.266 secs (0.266u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.296 secs (0.296u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.737 secs (0.736u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.227 secs (0.226u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.269 secs (0.269u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.054 secs (0.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.057 secs (0.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.308 secs (0.309u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.362 secs (0.363u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.226 secs (0.226u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.279 secs (0.279u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.057 secs (0.06u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.052 secs (0.049u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.053 secs (0.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.2 secs (0.203u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.21 secs (0.21u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.208 secs (0.206u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.162 secs (1.163u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.256 secs (1.256u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.994 secs (0.996u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.017 secs (1.016u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.186 secs (0.186u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.044 secs (1.043u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.123 secs (1.123u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.892 secs (0.889u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.961 secs (0.963u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.051 secs (0.05u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.085 secs (0.086u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.081 secs (0.08u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.12 secs (0.119u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.116 secs (0.12u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.074 secs (0.073u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.067 secs (0.066u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.07 secs (0.073u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.063 secs (0.063u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.084 secs (0.083u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.097 secs (0.096u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.108 secs (0.106u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.658 secs (0.66u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.775 secs (0.773u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.527 secs (0.526u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.625 secs (0.623u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.586 secs (0.586u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.687 secs (0.686u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.189 secs (0.189u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.21 secs (0.209u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.066 secs (0.066u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.078 secs (0.08u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.068 secs (0.066u,0.s) (successful) *)
+      (* Total: 414.396 seconds, roughly 7 minutes*)
+
+    Time Qed. (* Finished transaction in 390.998 secs (390.783u,0.276s) (successful) *)
+  End W.
+End W.
diff --git a/src/Curves/Weierstrass/Pre.v b/src/Curves/Weierstrass/Pre.v
new file mode 100644
index 000000000..6647d8e76
--- /dev/null
+++ b/src/Curves/Weierstrass/Pre.v
@@ -0,0 +1,62 @@
+Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Decidable.
+Import BinNums.
+
+Local Open Scope core_scope.
+
+Section Pre.
+  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))}
+          {eq_dec: DecidableRel Feq}.
+  Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)).
+  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" := (Fopp x).
+  Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
+  Local Notation "'∞'" := unit : type_scope.
+  Local Notation "'∞'" := (inr tt) : core_scope.
+  Local Notation "2" := (1+1). Local Notation "3" := (1+2).
+  Local Notation "( x , y )" := (inl (pair x y)).
+
+  Context {a:F}.
+  Context {b:F}.
+
+  (* the canonical definitions are in Spec *)
+  Let onCurve (P:F*F + ∞) := match P with
+                             | (x, y) => y^2 = x^3 + a*x + b
+                             | ∞ => True
+                             end.
+  Let add (P1' P2':F*F + ∞) : F*F + ∞ :=
+    match P1', P2' return _ with
+    | (x1, y1), (x2, y2) =>
+      if dec (x1 = x2)
+      then
+        if dec (y2 = -y1)
+        then ∞
+        else let k := (3*x1^2+a)/(2*y1) in
+             let x3 := k^2-x1-x1 in
+             let y3 := k*(x1-x3)-y1 in
+             (x3, y3)
+      else let k := (y2-y1)/(x2-x1) in
+           let x3 := k^2-x1-x2 in
+           let y3 := k*(x1-x3)-y1 in
+           (x3, y3)
+    | ∞, ∞ => ∞
+    | ∞, _ => P2'
+    | _, ∞ => P1'
+    end.
+
+  Lemma add_onCurve P1 P2 (_:onCurve P1) (_:onCurve P2) :
+    onCurve (add P1 P2).
+  Proof using a b char_ge_3 eq_dec field.
+    destruct_head' sum; destruct_head' prod;
+      cbv [onCurve add] in *; break_match; trivial; [|]; fsatz.
+  Qed.
+End Pre.
diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v
new file mode 100644
index 000000000..20866ca5d
--- /dev/null
+++ b/src/Curves/Weierstrass/Projective.v
@@ -0,0 +1,157 @@
+Require Import Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.Util.Decidable Crypto.Algebra.Field.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SetoidSubst.
+Require Import Crypto.Util.Notations Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.Sigma.
+
+Module Projective.
+  Section Projective.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
+            {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 "-" := Fsub.
+    Local Infix "*" := Fmul. Local Infix "/" := Fdiv.
+    Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
+    Local Notation Wpoint := (@W.point F Feq Fadd Fmul a b).
+
+    (* Originally from
+    <http://www.mat.uniroma3.it/users/pappa/CORSI/CR510_13_14/BosmaLenstra.pdf>
+    "Commplete Systems of Addition Laws" by Bosma and Lenstra;
+    optimized in <https://eprint.iacr.org/2015/1060.pdf> "Complete
+    addition formulas for prime order elliptic curves" Algorithm 1
+    "Complete, projective point addition for arbitrary prime order
+    short Weierstrass curves" by Joost Renes, Craig Costello, and
+    Lejla Batina. *)
+
+    Ltac t :=
+      repeat match goal with
+             | _ => solve [ contradiction | trivial ]
+             | _ => progress cbv zeta
+             | _ => progress intros
+             | _ => progress destruct_head' @W.point
+             | _ => progress destruct_head' sum
+             | _ => progress destruct_head' prod
+             | _ => progress destruct_head' unit
+             | _ => progress destruct_head' and
+             | _ => progress specialize_by assumption
+             | _ => progress cbv [W.eq W.add W.coordinates proj1_sig] in *
+             | _ => progress break_match_hyps
+             | _ => progress break_match
+             | |- _ /\ _ => split
+             end.
+
+    Definition point : Type := { P : F*F*F | let '(X,Y,Z) := P in Y^2*Z = X^3 + a*X*Z^2 + b*Z^3 /\ (Z = 0 -> Y <> 0) }.
+
+    Program Definition to_affine (P:point) : Wpoint :=
+      match proj1_sig P return F*F+_ with
+      | (X, Y, Z) =>
+        if dec (Z = 0) then inr tt
+        else inl (X/Z, Y/Z)
+      end.
+    Next Obligation. Proof. t. fsatz. Qed.
+
+    Program Definition of_affine (P:Wpoint) : point :=
+      match W.coordinates P return F*F*F with
+      | inl (x, y) => (x, y, 1)
+      | inr _ => (0, 1, 0)
+      end.
+    Next Obligation. Proof. t; fsatz. Qed.
+
+    Program Definition opp (P:point) : point :=
+      match proj1_sig P return F*F*F with
+      | (X, Y, Z) => (X, Fopp Y, Z)
+      end.
+    Next Obligation. Proof. t; fsatz. Qed.
+
+    Context (three_b:F) (three_b_correct: three_b = b+b+b).
+    Local Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1).
+    Context {discriminant_nonzero: id(4*a*a*a + 27*b*b <> 0)}.
+
+    Program Definition add (P Q:point)
+            (y_PmQ_nz: match W.coordinates (W.add (to_affine P) (to_affine (opp Q))) return Prop with
+                       | inr _ => True
+                       | inl (_, y) => y <> 0
+                       end) : point :=
+      match proj1_sig P, proj1_sig Q return F*F*F with (X1, Y1, Z1), (X2, Y2, Z2) =>
+        let t0 := X1*X2 in
+        let t1 := Y1*Y2 in
+        let t2 := Z1*Z2 in
+        let t3 := X1+Y1 in
+        let t4 := X2+Y2 in
+        let t3 := t3*t4 in
+        let t4 := t0+t1 in
+        let t3 := t3-t4 in
+        let t4 := X1+Z1 in
+        let t5 := X2+Z2 in
+        let t4 := t4*t5 in
+        let t5 := t0+t2 in
+        let t4 := t4-t5 in
+        let t5 := Y1+Z1 in
+        let X3 := Y2+Z2 in
+        let t5 := t5*X3 in
+        let X3 := t1+t2 in
+        let t5 := t5-X3 in
+        let Z3 := a*t4 in
+        let X3 := three_b*t2 in
+        let Z3 := X3+Z3 in
+        let X3 := t1-Z3 in
+        let Z3 := t1+Z3 in
+        let Y3 := X3*Z3 in
+        let t1 := t0+t0 in
+        let t1 := t1+t0 in
+        let t2 := a*t2 in
+        let t4 := three_b*t4 in
+        let t1 := t1+t2 in
+        let t2 := t0-t2 in
+        let t2 := a*t2 in
+        let t4 := t4+t2 in
+        let t0 := t1*t4 in
+        let Y3 := Y3+t0 in
+        let t0 := t5*t4 in
+        let X3 := t3*X3 in
+        let X3 := X3-t0 in
+        let t0 := t3*t1 in
+        let Z3 := t5*Z3 in
+        let Z3 := Z3+t0 in
+        (X3, Y3, Z3)
+      end.
+    Next Obligation.
+    Proof.
+      destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1].
+      destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2].
+      t.
+      all: try abstract fsatz.
+      (* FIXME: the final fsatz starts requiring 56 <> 0 if
+           - the next assert block is removed
+           - the assertion is changed to [Y2 = Fopp Y1] *)
+      assert (Y2 / Z2 = Fopp (Y1 / Z1)) by (
+        assert (forall pfP pfQ, match W.coordinates (W.add (to_affine (exist _ (X1,Y1,Z1) pfP)) (to_affine (exist _ (X2,Y2,Z2) pfQ))) with inl _ => False | _ => True end) by (cbv [to_affine]; t; fsatz); cbv [to_affine] in *; t; specialize_by (t;fsatz); t; fsatz).
+      unfold id in discriminant_nonzero; fsatz.
+    Qed.
+
+    Lemma to_affine_add P Q H :
+      W.eq
+        (to_affine (add P Q H))
+        (WeierstrassCurve.W.add (to_affine P) (to_affine Q)).
+    Proof using Type.
+      destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1].
+      destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2].
+      cbv [add opp to_affine] in *; t.
+      all: try abstract fsatz.
+
+      (* zero + P = P   -- cases for x and y *)
+      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+
+      (* P  + zero = P   -- cases for x and y *)
+      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+    Qed.
+  End Projective.
+End Projective.