Merge branch 'spec' of github.mit.edu:plv/fiat-crypto

13 files changed, 1234 insertions, 52 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
new file mode 100644
index 000000000..b1be7dd63
--- /dev/null
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -0,0 +1,52 @@
+Require Export Crypto.Spec.CompleteEdwardsCurve.
+
+Require Import Crypto.CompleteEdwardsCurve.Pre.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Eqdep_dec.
+Require Import Crypto.Tactics.VerdiTactics.
+
+Section CompleteEdwardsCurveTheorems.
+  Context {prm:TwistedEdwardsParams}.
+  Existing Instance prime_q.
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [idtac],
+     postprocess [try exact Fq_1_neq_0; try assumption],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+
+  Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2,
+    mkPoint p1 pf1 = mkPoint p2 pf2.
+  Proof.
+    destruct p1, p2; intros; find_injection; intros; subst; apply f_equal.
+    apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) 
+  Qed.
+  Hint Resolve point_eq.
+
+  Ltac Edefn := unfold unifiedAdd, unifiedAdd', zero; intros;
+                  repeat match goal with
+                         | [ p : point |- _ ] =>
+                           let x := fresh "x" p in
+                           let y := fresh "y" p in
+                           let pf := fresh "pf" p in
+                           destruct p as [[x y] pf]; unfold onCurve in pf
+                  | _ => eapply point_eq, (f_equal2 pair)
+                  | _ => eapply point_eq
+  end.
+  Lemma twistedAddComm : forall A B, (A+B = B+A)%E.
+  Proof.
+    Edefn; apply f_equal2; ring.
+  Qed.
+
+  Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C.
+  Proof.
+    (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
+  Admitted.
+
+  Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
+  Proof.
+    Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
+           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl.
+  Qed.
+End CompleteEdwardsCurveTheorems.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
new file mode 100644
index 000000000..d2cd753fe
--- /dev/null
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -0,0 +1,130 @@
+Require Import Crypto.CompleteEdwardsCurve.Pre.
+Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Tactics.VerdiTactics.
+
+Section ExtendedCoordinates.
+  Local Open Scope F_scope.
+  Context {prm:TwistedEdwardsParams}.
+  Existing Instance prime_q.
+
+  Add Field GFfield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+
+
+  (** [extended] represents a point on an elliptic curve using extended projective
+  * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
+  Record extended := mkExtended {extendedX : F q;
+                                 extendedY : F q;
+                                 extendedZ : F q;
+                                 extendedT : F q}.
+  Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T).
+
+  Definition twistedToExtended (P : (F q*F q)) : extended :=
+    let '(x, y) := P in (x, y, 1, x*y).
+  Definition extendedToTwisted (P : extended) : F q * F q :=
+    let '(X, Y, Z, T) := P in ((X/Z), (Y/Z)).
+  Definition rep (P:extended) (rP:(F q*F q)) : Prop :=
+    let '(X, Y, Z, T) := P in
+    extendedToTwisted P = rP /\
+    Z <> 0 /\
+    T = X*Y/Z.
+  Local Hint Unfold twistedToExtended extendedToTwisted rep.
+  Local Notation "P '~=' rP" := (rep P rP) (at level 70).
+
+  Ltac extended_tac :=
+    repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros);
+    repeat match goal with
+      | [ p : (F q*F q)%type |- _ ] =>
+          let x := fresh "x" p in
+          let y := fresh "y" p in
+          destruct p as [x y]
+      | [ p : extended |- _ ] =>
+          let X := fresh "X" p in
+          let Y := fresh "Y" p in
+          let Z := fresh "Z" p in
+          let T := fresh "T" p in
+          destruct p as [X Y Z T]
+      | [ H: _ /\ _ |- _ ] => destruct H
+      | [ |- _ /\ _ ] => split
+      | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H
+      | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H
+      | [ |- @eq (F q * F q)%type _ _] => apply f_equal2
+      | _ => progress rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
+           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r
+      | _ => progress eauto using Fq_1_neq_0
+      | [ H: a = _ |- _ ] => rewrite H
+      | [ |- @eq (F q) _ _] => fail; field (*FIXME*)
+  end.
+
+  Lemma twistedToExtended_rep : forall P, twistedToExtended P ~= P.
+  Proof.
+    extended_tac.
+  Qed.
+
+  Lemma extendedToTwisted_rep : forall P rP, P ~= rP -> extendedToTwisted P = rP.
+  Proof.
+    extended_tac.
+  Qed.
+
+  Section TwistMinus1.
+    Context (a_eq_minus1 : a = opp 1).
+    (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
+    Definition unifiedAddM1 (P1 P2 : extended) : extended :=
+      let '(X1, Y1, Z1, T1) := P1 in
+      let '(X2, Y2, Z2, T2) := P2 in
+      let  A := (Y1-X1)*(Y2-X2) in
+      let  B := (Y1+X1)*(Y2+X2) in
+      let  C := T1*ZToField 2*d*T2 in
+      let  D := Z1*ZToField 2  *Z2 in
+      let  E := B-A in
+      let  F := D-C in
+      let  G := D+C in
+      let  H := B+A in
+      let X3 := E*F in
+      let Y3 := G*H in
+      let T3 := E*H in
+      let Z3 := F*G in
+      (X3, Y3, Z3, T3).
+    Local Hint Unfold unifiedAdd.
+
+    Lemma unifiedAdd_repM1: forall P Q rP rQ, onCurve rP -> onCurve rQ ->
+      P ~= rP -> Q ~= rQ -> (unifiedAddM1 P Q) ~= (unifiedAdd' rP rQ).
+    Proof.
+      intros P Q rP rQ HoP HoQ HrP HrQ.
+      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d) as HoR; simpl in HoR.
+      extended_tac.
+      field.
+
+      (* If we we had reasoning modulo associativity and commutativity,
+      *  the following tactic would probably solve all 10 goals here:
+      repeat match goal with [H1: @eq GF _ _, H2: @eq GF _ _ |- _ ] =>
+        let H := fresh "H" in ( 
+          pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H;
+          match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
+        ) || (
+          pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H;
+          match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
+        ); repeat apply mul_nonzero_nonzero; auto 10
+      end.
+      *)
+
+      - replace (Z0 * Z * Z0 * Z + d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * Z * Z0 * Z - d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * Z * Z0 * Z - d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto).
+      repeat apply mul_nonzero_nonzero.
+        + replace (Z0 * 2 * Z - X0 * Y0 / Z0 * 2 * d * (X * Y / Z)) with (2*Z*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+        + replace (Z0 * 2 * Z + X0 * Y0 / Z0 * 2 * d * (X * Y / Z)) with (2*Z*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+      - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10.
+    Qed.
+End ExtendedCoordinates.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v
new file mode 100644
index 000000000..8d24f2cd2
--- /dev/null
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v
@@ -0,0 +1,38 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Spec.CompleteEdwardsCurve.
+
+Section ExtendedCoordinates.
+  Local Open Scope F_scope.
+
+  Context {prm:TwistedEdwardsParams}.
+  Context {p:BinInt.Z} {p_eq_q:p = q}.
+  Lemma prime_p : Znumtheory.prime p.
+    rewrite p_eq_q; exact prime_q.
+  Qed.
+
+  Add Field Ffield_Z : (@Ffield_theory p prime_p)
+    (morphism (@Fring_morph p),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div (@Fmorph_div_theory p),
+     power_tac (@Fpower_theory p) [Fexp_tac]). 
+
+  Lemma biggerFraction : forall XP YP ZP XQ YQ ZQ d : F q, 
+   ZQ <> 0 ->
+   ZP <> 0 ->
+   ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
+   ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
+   ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
+
+   ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
+   (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) /
+   ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
+    (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) =
+   (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)).
+  Proof.
+    rewrite <-p_eq_q.
+    intros.
+    abstract (field; assumption).
+  Qed.
+End ExtendedCoordinates.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
new file mode 100644
index 000000000..e4dc140e1
--- /dev/null
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -0,0 +1,186 @@
+Require Import BinInt Znumtheory VerdiTactics.
+
+Require Import Crypto.Spec.ModularArithmetic.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Local Open Scope F_scope.
+  
+Section Pre.
+  Context {q : BinInt.Z}.
+  Context {a : F q}.
+  Context {d : F q}.
+  Context {prime_q : Znumtheory.prime q}.
+  Context {two_lt_q : 2 < q}.
+  Context {a_nonzero : a <> 0}.
+  Context {a_square : exists sqrt_a, sqrt_a^2 = a}.
+  Context {d_nonsquare : forall x, x^2 <> d}.
+
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+  
+  (* the canonical definitions are in Spec *)
+  Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
+  Local Notation unifiedAdd' P1' P2' := (
+    let '(x1, y1) := P1' in
+    let '(x2, y2) := P2' in
+    (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
+  ).
+  
+  Lemma char_gt_2 : ZToField 2 <> (0: F q).
+    intro; find_injection.
+    pose proof two_lt_q.
+    rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega.
+  Qed.
+
+  Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
+  Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
+  
+  Ltac whatsNotZero :=
+    repeat match goal with
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
+    | [H: (?a^?p)%F <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        let Y:=fresh in let Z:=fresh in try (
+          assert (p <> 0%N) as Z by (intro Y; inversion Y);
+          assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0);
+          clear Z)
+    | [H: (?a*?b)%F <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0)
+    | [H: (?a*?b)%F <> 0 |- _ ] =>
+        match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0)
+    end.
+
+  Lemma edwardsAddComplete' x1 y1 x2 y2 :
+    onCurve (x1, y1) ->
+    onCurve (x2, y2) ->
+    (d*x1*x2*y1*y2)^2 <> 1.
+  Proof.
+    intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
+  
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+    destruct a_square as [sqrt_a a_square'].
+    rewrite <-a_square' in *.
+  
+    (* Furthermore... *)
+    pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
+    rewrite Hc2 in Heqt at 2.
+    replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2))
+       with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field.
+    rewrite Hcontra in Heqt.
+    replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
+    rewrite <-Hc1 in Heqt.
+  
+    (* main equation for both potentially nonzero denominators *)
+    destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
+      try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
+        assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 =
+                 f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2)
+                   (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field;
+        rewrite Hcontra in Heqw1;
+        replace (1 * y1^2) with (y1^2) in * by field;
+        rewrite <- Heqt in *;
+        assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 /
+                                 (x1 * y1 * (f (sqrt_a * x2)  y2))^2)
+                                 by (rewriteAny; field; auto);
+        match goal with [H: d = (?n^2)/(?l^2) |- _ ] =>
+            destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
+        end
+      end.
+  
+    assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
+  
+    replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
+  
+    (* contradiction: product of nonzero things is zero *)
+    destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
+    destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
+    apply Ha_nonzero; field.
+  Qed.
+
+  Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
+    onCurve (x1, y1) ->
+    onCurve (x2, y2) ->
+    (1 + d*x1*x2*y1*y2) <> 0.
+  Proof.
+    intros Hc1 Hc2; simpl in Hc1, Hc2.
+    intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H].
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
+      intro Hz; rewrite Hz in H; intuition.
+  Qed.
+  
+  Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
+    onCurve (x1, y1) ->
+    onCurve (x2, y2) ->
+    (1 - d*x1*x2*y1*y2) <> 0.
+  Proof.
+    intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H].
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
+      intro Hz; rewrite Hz in H; apply H; field.
+  Qed.
+  
+  Definition zeroOnCurve : onCurve (0, 1).
+    simpl. field.
+  Qed.
+  
+  Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
+    (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
+    onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
+  Proof.
+    (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
+      * c=1 and an extra a in front of x^2 *) 
+  
+    injection H; clear H; intros.
+  
+    Ltac t x1 y1 x2 y2 :=
+      assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
+             = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
+      assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
+             = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
+    t x1 y1 x2 y2; t x2 y2 x1 y1.
+  
+    remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
+      (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
+    assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
+    assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +(
+    (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
+     y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
+    replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
+  
+    match goal with [ |- ?x = 1 ] => replace x with
+    ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
+     ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
+      d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
+    ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end.
+    - rewrite <-HT1, <-HT2; field; rewrite HT1.
+      replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
+      with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field.
+      auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
+        edwardsAddCompleteMinus, edwardsAddCompletePlus.
+    - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
+         with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
+           by field;
+      auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
+        edwardsAddCompleteMinus, edwardsAddCompletePlus.
+  Qed.
+  
+  Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
+    onCurve (unifiedAdd' P1 P2).
+  Proof.
+    intros; destruct P1, P2.
+    remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
+    eapply unifiedAdd'_onCurve'; eauto.
+  Qed.
+End Pre.
\ No newline at end of file
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 8137abc4c..2ea04cde5 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -137,56 +137,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
 
 
 
-  Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0.
-    intros.
-
-    induction p; inversion H.
-
-    revert H H1; generalize x; induction p; intros.
-
-    - simpl in H; apply mul_zero_why in H; destruct H; intuition.
-
-      + subst; intuition.
-
-      + apply IHp in H.
-        rewrite H1.
-        simpl in H1.
-        apply mul_zero_why in H1; destruct H1; intuition.
-        rewrite H0 in H.
-        apply mul_zero_why in H; destruct H; intuition.
-
-        simpl; intuition.
-
-    - simpl in H1; apply IHp in H1; simpl; intuition.
-      simpl in H; rewrite H in H1; rewrite H.
-      apply mul_zero_why in H1; destruct H1; intuition.
-
-    - simpl in H; subst; intuition.
-
-  Qed.
-
-  Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
-    intros; intuition.
-
-    induction p.
-
-    - apply H; intuition.
-
-    - apply H.
-      rewrite H1 in *.
-      induction p.
-
-      + simpl.
-        field.
-
-      + simpl in *.
-        replace (0 * 0) with 0 in * by field.
-        apply IHp; intuition.
-        induction p; inversion H2.
-
-      + simpl; intuition.
-
-  Qed.
+  Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. Admitted.
+  Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. Admitted.
 
   Lemma char_gt_2 : inject 2 <> 0.
     intro H; inversion H; clear H.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
new file mode 100644
index 000000000..6c79e6891
--- /dev/null
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -0,0 +1,422 @@
+Require Import Spec.ModularArithmetic.
+
+Require Import Eqdep_dec.
+Require Import Tactics.VerdiTactics.
+Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *)
+Require Import Coq.Classes.Morphisms Setoid.
+Require Export Ring_theory Field_theory Field_tac.
+
+Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
+Proof.
+  destruct x, y; intuition; simpl in *; try congruence.
+  subst_max.
+  f_equal.
+  eapply UIP_dec, Z.eq_dec.
+Qed.
+
+(* Fails iff the input term does some arithmetic with mod'd values. *)
+Ltac notFancy E :=
+match E with
+| - (_ mod _) => idtac
+| context[_ mod _] => fail 1
+| _ => idtac
+end.
+
+Lemma Zplus_neg : forall n m, n + -m = n - m.
+Proof.
+  auto.
+Qed.
+
+Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n.
+Proof.
+  intros; rewrite H; trivial.
+Qed.
+
+(* Remove redundant [mod] operations from the conclusion. *)
+Ltac demod :=
+  repeat match goal with
+         | [ |- context[(?x mod _ + _) mod _] ] =>
+           notFancy x; rewrite (Zplus_mod_idemp_l x)
+         | [ |- context[(_ + ?y mod _) mod _] ] =>
+           notFancy y; rewrite (Zplus_mod_idemp_r y)
+         | [ |- context[(?x mod _ - _) mod _] ] =>
+           notFancy x; rewrite (Zminus_mod_idemp_l x)
+         | [ |- context[(_ - ?y mod _) mod _] ] =>
+           notFancy y; rewrite (Zminus_mod_idemp_r _ y)
+         | [ |- context[(?x mod _ * _) mod _] ] =>
+           notFancy x; rewrite (Zmult_mod_idemp_l x)
+         | [ |- context[(_ * (?y mod _)) mod _] ] =>
+           notFancy y; rewrite (Zmult_mod_idemp_r y)
+         | [ |- context[(?x mod _) mod _] ] =>
+           notFancy x; rewrite (Zmod_mod x)
+         | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in *
+         end.
+
+(* Remove exists under equals: we do this a lot *)
+Ltac eq_remove_proofs := lazymatch goal with
+| [ |- @eq (F _) ?a ?b ] =>
+    assert (Q := F_eq a b);
+    simpl in *; apply Q; clear Q
+end.
+            
+Ltac Fdefn :=
+  intros;
+  unfold unfoldFm;
+  rewrite ?F_opp_spec;
+  repeat match goal with [ x : F _ |- _ ] => destruct x end;
+  try eq_remove_proofs;
+  demod;
+  rewrite ?Z.mul_1_l;
+  intuition; demod; try solve [ f_equal; intuition ].
+
+Local Open Scope F_scope.
+
+Section FEquality.
+  Context {m:Z}.
+
+  (** Equality **)
+  Definition F_eqb (x y : F m) : bool :=  Z.eqb x y.
+
+  Lemma F_eqb_eq x y : F_eqb x y = true -> x = y.
+  Proof.
+    unfold F_eqb; Fdefn; apply Z.eqb_eq; trivial.
+  Qed.
+
+  Lemma F_eqb_complete : forall x y: F m, x = y -> F_eqb x y = true.
+  Proof.
+    intros; subst; apply Z.eqb_refl.
+  Qed.
+
+  Lemma F_eqb_refl : forall x, F_eqb x x = true.
+  Proof.
+    intros; apply F_eqb_complete; trivial.
+  Qed.
+
+  Lemma F_eqb_neq x y : F_eqb x y = false -> x <> y.
+  Proof.
+    intuition; subst y.
+    pose proof (F_eqb_refl x).
+    congruence.
+  Qed.
+
+  Lemma F_eqb_neq_complete x y : x <> y -> F_eqb x y = false.
+  Proof.
+    intros.
+    case_eq (F_eqb x y); intros; trivial.
+    pose proof (F_eqb_eq x y); intuition.
+  Qed.
+
+  Lemma F_eq_dec : forall x y : F m, {x = y} + {x <> y}.
+  Proof.
+    intros; case_eq (F_eqb x y); [left|right]; auto using F_eqb_eq, F_eqb_neq.
+  Qed.
+
+  Lemma if_F_eq_dec_if_F_eqb : forall {T} x y (a b:T), (if F_eq_dec x y then a else b) = (if F_eqb x y then a else b).
+  Proof.
+    intros; intuition; break_if.
+    - rewrite F_eqb_complete; trivial.
+    - rewrite F_eqb_neq_complete; trivial.
+  Defined.
+End FEquality.
+
+Section FandZ.
+  Local Set Printing Coercions.
+  Context {m:Z}.
+
+  Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m).
+  Proof.
+    intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition.
+  Qed.
+
+  Lemma ZToField_0 : @ZToField m 0 = 0.
+  Proof.
+    Fdefn.
+  Qed.
+
+  Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m.
+  Proof.
+    Fdefn.
+  Qed.
+
+  Lemma mod_FieldToZ : forall x,  (@FieldToZ m x) mod m = FieldToZ x.
+  Proof.
+    Fdefn.
+  Qed.
+
+  (** ZToField distributes over operations **)
+  Lemma ZToField_add : forall (x y : Z),
+      @ZToField m (x + y) = ZToField x + ZToField y.
+  Proof.
+    Fdefn.
+  Qed.
+
+  Lemma FieldToZ_add : forall x y : F m,
+      FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z.
+  Proof.
+    Fdefn.
+  Qed.
+
+  Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m ->
+                                     b mod m =  (- a)  mod m.
+  Admitted.
+
+  Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m.
+  Proof.
+    intros.
+    pose proof (FieldToZ_add x (opp x)) as H.
+    rewrite F_opp_spec, FieldToZ_ZToField in H.
+    auto using mod_plus_zero_subproof.
+  Qed.
+
+  Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m.
+  Proof.
+    intros.
+    pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial.
+  Qed.
+
+  (* Compatibility between inject and subtraction *)
+  Lemma ZToField_sub : forall (x y : Z),
+      @ZToField m (x - y) = ZToField x - ZToField y.
+  Proof.
+    repeat progress Fdefn.
+    rewrite Zplus_mod, FieldToZ_opp', FieldToZ_ZToField.
+    demod; reflexivity.
+  Qed.
+
+  (* Compatibility between inject and multiplication *)
+  Lemma ZToField_mul : forall (x y : Z),
+      @ZToField m (x * y) = ZToField x * ZToField y.
+  Proof.
+    Fdefn.
+  Qed.
+
+  (* Compatibility between inject and GFtoZ *)
+  Lemma ZToField_idempotent : forall (x : F m), ZToField x = x.
+  Proof.
+    Fdefn.
+  Qed.
+
+  (* Compatibility between inject and mod *)
+  Lemma ZToField_mod : forall x, @ZToField m x = ZToField (x mod m).
+  Proof.
+    Fdefn.
+  Qed.
+End FandZ.
+
+Section RingModuloPre.
+  Context {m:Z}.
+  (* Substitution to prove all Compats *)
+  Ltac compat := repeat intro; subst; trivial.
+
+  Instance Fplus_compat : Proper (eq==>eq==>eq) (@add m).
+  Proof.
+    compat.
+  Qed.
+
+  Instance Fminus_compat : Proper (eq==>eq==>eq) (@sub m).
+  Proof.
+    compat.
+  Qed.
+
+  Instance Fmult_compat : Proper (eq==>eq==>eq) (@mul m).
+  Proof.
+    compat.
+  Qed.
+
+  Instance Fopp_compat : Proper (eq==>eq) (@opp m).
+  Proof.
+    compat.
+  Qed.
+
+  Instance Finv_compat : Proper (eq==>eq) (@inv m).
+  Proof.
+    compat.
+  Qed.
+
+  Instance Fdiv_compat : Proper (eq==>eq==>eq) (@div m).
+  Proof.
+    compat.
+  Qed.
+
+  (***** Ring Theory *****)
+  Definition Fring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq.
+  Proof.
+    constructor; Fdefn.
+  Qed.
+
+  Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
+  Proof.
+    destruct (F_pow_spec x) as [HO HS].
+  Admitted.
+
+  (***** Power theory *****)
+  Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m).
+  Proof.
+    constructor; apply pow_pow_N.
+  Qed.
+
+  (***** Division Theory *****)
+  Definition Fquotrem(a b: F m): F m * F m :=
+    let '(q, r) := (Z.quotrem a b) in (ZToField q, ZToField r).
+  Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem.
+  Proof.
+    constructor; intros; unfold Fquotrem, id.
+
+    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by
+      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+
+    Fdefn; rewrite <-Z.quot_rem'; trivial.
+  Qed.
+
+  Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m.
+  Admitted.
+
+  (* Define a "ring morphism" between GF and Z, i.e. an equivalence
+   * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
+   *
+   * Doing this allows us to do our coefficient manipulations in Z
+   * rather than GF, because we know it's equivalent to inject the
+   * result afterward.
+   *)
+  Lemma Fring_morph:
+      ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq
+                 0%Z 1%Z Z.add    Z.mul    Z.sub    Z.opp  Z.eqb
+                 (@ZToField m).
+  Proof.
+    constructor; intros; try Fdefn; unfold id, unfoldFm;
+      try (apply gf_eq; simpl; intuition).
+
+    - rewrite FieldToZ_opp, FieldToZ_ZToField; demod; trivial.
+    - rewrite FieldToZ_opp, FieldToZ_ZToField, Z_mod_opp; trivial.
+    - rewrite (proj1 (Z.eqb_eq x y)); trivial.
+  Qed.
+
+  (* Redefine our division theory under the ring morphism *)
+  Lemma Fmorph_div_theory: 
+      div_theory eq Zplus Zmult (@ZToField m) Z.quotrem.
+  Proof.
+    constructor; intros; intuition.
+    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
+      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+
+    eq_remove_proofs; demod;
+      rewrite <- (Z.quot_rem' a b);
+      destruct a; simpl; trivial.
+  Qed.
+
+  Lemma ZToField_1 : @ZToField m 1 = 1.
+  Proof.
+    Fdefn.
+  Qed.
+End RingModuloPre.
+  
+Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end.
+Ltac Fexp_tac t := Ncst t.
+Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1.
+Ltac Fpostprocess := repeat split;
+  repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] =>
+    change (exist a b (Pre.Z_mod_mod x q)) with (@ZToField q x%Z) end;
+  rewrite ?ZToField_0, ?ZToField_1.
+
+Module Type Modulus.
+  Parameter modulus : Z.
+End Modulus.
+
+(* Example of how to instantiate the ring tactic *)
+Module RingModulo (Export M : Modulus).
+  Definition ring_theory_modulo := @Fring_theory modulus.
+  Definition ring_morph_modulo := @Fring_morph modulus.
+  Definition morph_div_theory_modulo := @Fmorph_div_theory modulus.
+  Definition power_theory_modulo := @Fpower_theory modulus.
+  
+  Add Ring GFring_Z : ring_theory_modulo
+    (morphism ring_morph_modulo,
+     constants [Fconstant],
+     div morph_div_theory_modulo,
+     power_tac power_theory_modulo [Fexp_tac]). 
+End RingModulo.
+
+Section VariousModulo.
+  Context {m:Z}.
+  
+  Add Ring GFring_Z : (@Fring_theory m)
+    (morphism (@Fring_morph m),
+     constants [Fconstant],
+     div (@Fmorph_div_theory m),
+     power_tac (@Fpower_theory m) [Fexp_tac]). 
+
+  Lemma F_mul_0_l : forall x : F m, 0 * x = 0.
+  Proof.
+    intros; ring.
+  Qed.
+  
+  Lemma F_mul_0_r : forall x : F m, x * 0 = 0.
+  Proof.
+    intros; ring.
+  Qed.
+  
+  Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0.
+    intros; intuition; subst.
+    assert (0 * b = 0) by ring; intuition.
+  Qed.
+  
+  Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0.
+    intros; intuition; subst.
+    assert (a * 0 = 0) by ring; intuition.
+  Qed.
+  
+  Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N ->
+    (x ^ z) * (y ^ z) = (x * y) ^ z.
+  Proof.
+    intros.
+    replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
+    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | 
+      replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
+    intros z' z'_nonneg IHz'.
+    rewrite Z2N.inj_succ by auto.
+    rewrite <-N.add_1_l.
+    rewrite !(proj2 (@F_pow_spec m _) _).
+    rewrite <- IHz'.
+    ring.
+  Qed.
+  
+  Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y.
+  Proof.
+    split; intro; subst; ring.
+  Qed.
+
+  Lemma F_opp_involutive : forall x : F m, opp (opp x) = x.
+  Proof.
+    intros; ring.
+  Qed.
+
+  Lemma F_add_0_r : forall x : F m, (x + 0)%F = x.
+  Proof.
+    intros; ring.
+  Qed.
+
+  Lemma F_add_0_l : forall x : F m, (0 + x)%F = x.
+  Proof.
+    intros; ring.
+  Qed.
+
+  Lemma F_sub_0_r : forall x : F m, (x - 0)%F = x.
+  Proof.
+    intros; ring.
+  Qed.
+
+  Lemma F_sub_0_l : forall x : F m, (0 - x)%F = opp x.
+  Proof.
+    intros; ring.
+  Qed.
+
+  Lemma F_mul_1_r : forall x : F m, (x * 1)%F = x.
+  Proof.
+    intros; ring.
+  Qed.
+
+  Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x.
+  Proof.
+    intros; ring.
+  Qed.
+End VariousModulo.
\ No newline at end of file
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
new file mode 100644
index 000000000..2c111be32
--- /dev/null
+++ b/src/ModularArithmetic/Pre.v
@@ -0,0 +1,8 @@
+Require Import Znumtheory BinInt BinNums.
+
+Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
+  symmetry.
+  destruct (BinInt.Z.eq_dec m 0).
+  - subst; rewrite !Zdiv.Zmod_0_r; reflexivity.
+  - apply BinInt.Z.mod_mod; assumption.
+Qed.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
new file mode 100644
index 000000000..6a862fb3b
--- /dev/null
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -0,0 +1,147 @@
+Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems.
+Require Export Ring_theory Field_theory Field_tac.
+
+Require Import Tactics.VerdiTactics.
+Require Import Coq.Classes.Morphisms Setoid.
+Require Import BinInt BinNat ZArith Znumtheory NArith. (* import Zdiv before Znumtheory *)
+Require Import Eqdep_dec.
+
+Existing Class prime.
+
+Section FieldModuloPre.
+  Context {q:Z} {prime_q:prime q}.
+  Local Open Scope F_scope.
+
+  Lemma Fq_1_neq_0 : (1:F q) <> (0:F q).
+  Proof.
+    pose proof prime_ge_2 q _.
+    rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence.
+  Qed.
+
+  Lemma F_mul_inv_l : forall x : F q, inv x * x = 1.
+  Proof.
+    intros.
+    rewrite <-(proj1 (F_inv_spec _ x)).
+    Fdefn.
+  Qed.
+
+  (* Add an abstract field (without modifiers) *)
+  Definition Ffield_theory : field_theory 0%F 1%F (@add q) (@mul q) (@sub q) (@opp q) (@div q) (@inv q) eq.
+  Proof.
+    constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l.
+  Qed.
+End FieldModuloPre.
+
+Module Type PrimeModulus.
+  Parameter modulus : Z.
+  Parameter prime_modulus : prime modulus.
+End PrimeModulus.
+
+Module FieldModulo (Import M : PrimeModulus).
+  (* Add our field with all the fixin's *)
+  Module Import RingM := RingModulo M.
+  Definition field_theory_modulo := @Ffield_theory modulus prime_modulus.
+  Add Field Ffield_Z : field_theory_modulo
+    (morphism ring_morph_modulo,
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div morph_div_theory_modulo,
+     power_tac power_theory_modulo [Fexp_tac]). 
+End FieldModulo.
+
+Section VariousModPrime.
+  Context {q:Z} {prime_q:prime q}.
+  Local Open Scope F_scope.
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+  
+  Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y.
+  Proof.
+    intros ? ? ? z_nonzero mul_z_eq.
+    assert (x * z * inv z = y * z * inv z) as H by (rewrite mul_z_eq; reflexivity).
+    replace (x * z * inv z) with (x * (z * inv z)) in H by (field; trivial).
+    replace (y * z * inv z) with (y * (z * inv z)) in H by (field; trivial).
+    rewrite (proj1 (@F_inv_spec q _ _)) in H.
+    replace (x * 1) with x in H by field.
+    replace (y * 1) with y in H by field.
+    trivial.
+  Qed.
+  
+  Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0.
+    intros.
+    assert (Z := F_eq_dec a 0); destruct Z.
+  
+    - left; intuition.
+  
+    - assert (a * b / a = 0) by
+        ( rewrite H; field; intuition ).
+  
+      replace (a*b/a) with (b) in H0 by (field; trivial).
+      right; intuition.
+  Qed.
+  
+  Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0.
+    intros; intuition; subst.
+    apply Fq_mul_zero_why in H1.
+    destruct H1; subst; intuition.
+  Qed.
+  Hint Resolve Fq_mul_nonzero_nonzero.
+  
+  Lemma Fq_square_mul : forall x y z : F q, (y <> 0) ->
+    x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
+  Proof.
+    intros ? ? ? y_nonzero A.
+    exists (x / y).
+    assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div by (field; trivial).
+    assert (y ^ 2 <> 0) as y2_nonzero by (
+      change (2%N) with (1+(1+0))%N;
+      rewrite !(proj2 (@F_pow_spec q _) _), !(proj1 (@F_pow_spec q _));
+      auto 10 using Fq_mul_nonzero_nonzero, Fq_1_neq_0).
+    rewrite (Fq_mul_eq _ z (y ^ 2)); auto.
+    rewrite <- A.
+    field; trivial.
+  Qed.
+
+  Lemma Fq_root_zero : forall (x: F q) (p: N), x^p = 0 -> x = 0.
+    induction p using N.peano_ind;
+    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
+    - intros; destruct Fq_1_neq_0; auto.
+    - intro H; destruct (Fq_mul_zero_why x (x^p) H); auto.
+  Qed.
+
+  Lemma Fq_root_nonzero : forall (x:F q) p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
+    induction p using N.peano_ind;
+    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
+    - intuition.
+    - destruct (N.eq_dec p 0); intro H; intros; subst.
+      + rewrite (proj1 (@F_pow_spec q _)) in H; replace (x*1) with (x) in H by ring; trivial.
+      + apply IHp; auto. intro Hz; rewrite Hz in *. apply H, F_mul_0_r.
+  Qed.
+
+  Lemma Fq_pow_nonzero : forall (x : F q) p, x <> 0 -> x^p <> 0.
+  Proof.
+    induction p using N.peano_ind;
+    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
+    - intuition. auto using Fq_1_neq_0.
+    - intros H Hc. destruct (Fq_mul_zero_why _ _ Hc).
+      + intuition.
+      + apply IHp; auto.
+  Qed.
+
+  Lemma F_div_1_r : forall x : F q, (x/1)%F = x.
+  Proof.
+    intros; field. (* TODO: Warning: Collision between bound variables ... *)
+  Qed.
+  
+  Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
+  Proof.
+    intros.
+    (* TODO(jadep) *)
+  Admitted.
+End VariousModPrime.
\ No newline at end of file
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
new file mode 100644
index 000000000..ae2b63bad
--- /dev/null
+++ b/src/ModularArithmetic/Tutorial.v
@@ -0,0 +1,131 @@
+Require Import BinInt Zpower ZArith Znumtheory.
+Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems.
+
+Module Modulus31 <: PrimeModulus.
+  Definition modulus := 2^5 - 1.
+  Lemma prime_modulus : prime modulus.
+  Admitted.
+End Modulus31.
+
+Module Modulus127 <: PrimeModulus.
+  Definition modulus := 2^127 - 1.
+  Lemma prime_modulus : prime modulus.
+  Admitted.
+End Modulus127.
+
+Module Example31.
+  (* Then we can construct a field with that modulus *)
+  Module Import Field := FieldModulo Modulus31.
+  Import Modulus31.
+
+  (* And pull in the appropriate notations *)
+  Local Open Scope F_scope.
+
+  (* First, let's solve a ring example*)
+  Lemma ring_example: forall x: F modulus, x * (ZToField 2) = x + x.
+  Proof.
+    intros.
+    ring.
+  Qed.
+
+  (* Unfortunately, the [ring] and [field] tactics need syntactic
+    (not definitional) equality to recognize the ring in question.
+    Therefore, it is necessary to explicitly rewrite the modulus
+    (usually hidden by implicitn arguments) match the one passed to
+    [FieldModulo]. *)
+  Lemma ring_example': forall x: F (2^5-1), x * (ZToField 2) = x + x.
+  Proof.
+    intros.
+    change (2^5-1)%Z with modulus.
+    ring.
+  Qed.
+
+  (* Then a field example (we have to know we can't divide by zero!) *)
+  Lemma field_example: forall x y z: F modulus, z <> 0 ->
+    x * (y / z) / z = x * y / (z ^ 2).
+  Proof.
+    intros; simpl.
+    field; trivial.
+  Qed.
+
+  (* Then an example with exponentiation *)
+  Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField 2 * x + 1 = (x + 1) ^ 2.
+  Proof.
+    intros; simpl.
+    field; trivial.
+  Qed.
+
+  (* In general, the rule I've been using is:
+
+     - If our goal looks like x = y:
+
+        + If we need to use assumptions to prove the goal, then before
+          we apply field,
+
+          * Perform all relevant substitutions (especially subst)
+
+          * If we have something more complex, we're probably going
+            to have to performe some sequence of "replace X with Y"
+            and solve out the subgoals manually before we can use
+            field.
+
+        + Else, just use field directly
+
+     - If we just want to simplify terms and put them into a canonical
+       form, then field_simplify or ring_simplify should do the trick.
+       Note, however, that the canonical form has lots of annoying "/1"s
+
+     - Otherwise, do a "replace X with Y" to generate an equality
+       so that we can use field in the above case
+
+     *)
+
+End Example31.
+
+(* Notice that the field tactics work whether we know what the modulus is *)
+Module TimesZeroTransparentTestModule.
+  Module Import Theory := FieldModulo Modulus127.
+  Import Modulus127.
+  Local Open Scope F_scope.
+
+  Lemma timesZero : forall a : F modulus, a*0 = 0.
+    intros.
+    field.
+  Qed.
+End TimesZeroTransparentTestModule.
+
+(* Or if we don't (i.e. it's opaque) *)
+Module TimesZeroParametricTestModule (M: PrimeModulus).
+  Module Theory := FieldModulo M.
+  Import Theory M.
+  Local Open Scope F_scope.
+
+  Lemma timesZero : forall a : F modulus, a*0 = 0.
+    intros.
+    field.
+  Qed.
+
+  Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
+  Proof.
+    intros.
+    field; try exact Fq_1_neq_0.
+  Qed.
+
+  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, 
+   ZQ <> 0 ->
+   ZP <> 0 ->
+   ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
+   ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
+   ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
+
+   ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
+   (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) /
+   ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
+    (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) =
+   (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)).
+  Proof.
+    intros.
+    field; assumption.
+  Qed.
+End TimesZeroParametricTestModule.
+
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
new file mode 100644
index 000000000..23e201405
--- /dev/null
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -0,0 +1,53 @@
+Require BinInt Znumtheory.
+
+Require Crypto.CompleteEdwardsCurve.Pre.
+
+Require Import Crypto.Spec.ModularArithmetic.
+Local Open Scope F_scope.
+
+Class TwistedEdwardsParams := {
+  q : BinInt.Z;
+  a : F q;
+  d : F q;
+  prime_q : Znumtheory.prime q;
+  two_lt_q : BinInt.Z.lt 2 q;
+  nonzero_a : a <> 0;
+  square_a : exists sqrt_a, sqrt_a^2 = a;
+  nonsquare_d : forall x, x^2 <> d
+}.
+
+Section TwistedEdwardsCurves.
+  Context {prm:TwistedEdwardsParams}.
+
+  (* Twisted Edwards curves with complete addition laws. References:
+  * <https://eprint.iacr.org/2008/013.pdf>
+  * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
+  * <https://eprint.iacr.org/2015/677.pdf>
+  *)
+  Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
+  Definition point := { P | onCurve P}.
+  Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf.
+
+  Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
+  
+  Definition unifiedAdd' P1' P2' :=
+    let '(x1, y1) := P1' in
+    let '(x2, y2) := P2' in
+      (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
+
+  Definition unifiedAdd (P1 P2 : point) : point :=
+    let 'exist P1' pf1 := P1 in
+    let 'exist P2' pf2 := P2 in
+    mkPoint (unifiedAdd' P1' P2')
+      (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
+
+  Fixpoint scalarMult (n:nat) (P : point) : point :=
+    match n with
+    | O => zero
+    | S n' => unifiedAdd P (scalarMult n' P)
+    end.
+End TwistedEdwardsCurves.
+
+Delimit Scope E_scope with E.
+Infix "+" := unifiedAdd : E_scope.
+Infix "*" := scalarMult : E_scope.
\ No newline at end of file
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
new file mode 100644
index 000000000..e2243dfff
--- /dev/null
+++ b/src/Spec/ModularArithmetic.v
@@ -0,0 +1,63 @@
+Require Znumtheory BinNums.
+
+Require Crypto.ModularArithmetic.Pre.
+
+Delimit Scope N_scope with N.
+Infix "+" := BinNat.N.add : N_scope.
+Infix "*" := BinNat.N.mul : N_scope.
+Infix "-" := BinNat.N.sub : N_scope.
+Infix "/" := BinNat.N.div : N_scope.
+Infix "^" := BinNat.N.pow : N_scope.
+
+Delimit Scope Z_scope with Z.
+Infix "+" := BinInt.Z.add : Z_scope.
+Infix "*" := BinInt.Z.mul : Z_scope.
+Infix "-" := BinInt.Z.sub : Z_scope.
+Infix "/" := BinInt.Z.div : Z_scope.
+Infix "^" := BinInt.Z.pow : Z_scope.
+Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope.
+Local Open Scope Z_scope.
+
+Definition F (modulus : BinInt.Z) := { z : BinInt.Z | z = z mod modulus }.
+Coercion FieldToZ {m} (a:F m) : BinNums.Z := proj1_sig a.
+
+Section FieldOperations.
+  Context {m : BinInt.Z}.
+
+  Let Fm := F m. (* Note: if inlined, coercions say "anomaly please report" *)
+  Coercion unfoldFm (a:Fm) : F m := a.
+  Coercion ZToField (a:BinNums.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m).
+  
+  Definition add (a b:Fm) : Fm := ZToField (a + b).
+  Definition mul (a b:Fm) : Fm := ZToField (a * b).
+
+  Parameter opp : Fm -> Fm. 
+  Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0.
+  Definition sub (a b:Fm) : Fm := add a (opp b).
+
+  Parameter inv : Fm -> Fm. 
+  Axiom F_inv_spec : Znumtheory.prime m -> forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0.
+  Definition div (a b:Fm) : Fm := mul a (inv b).
+
+  Parameter pow : Fm -> BinNums.N ->  Fm. 
+  Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x, pow a (1 + x)%N = mul a (pow a x).
+End FieldOperations.
+
+Delimit Scope F_scope with F.
+Arguments F _%Z.
+Arguments ZToField {_} _%Z : simpl never.
+Arguments add {_} _%F _%F : simpl never.
+Arguments mul {_} _%F _%F : simpl never.
+Arguments sub {_} _%F _%F : simpl never.
+Arguments div {_} _%F _%F : simpl never.
+Arguments pow {_} _%F _%N : simpl never.
+Arguments inv {_} _%F : simpl never.
+Arguments opp {_} _%F : simpl never.
+Local Open Scope F_scope.
+Infix "+" := add : F_scope.
+Infix "*" := mul : F_scope.
+Infix "-" := sub : F_scope.
+Infix "/" := div : F_scope.
+Infix "^" := pow : F_scope.
+Notation "0" := (ZToField 0) : F_scope.
+Notation "1" := (ZToField 1) : F_scope.
\ No newline at end of file
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v
index 6ae501a28..d037339b4 100644
--- a/src/Specific/EdDSA25519.v
+++ b/src/Specific/EdDSA25519.v
@@ -594,7 +594,8 @@ Module EdDSA25519_Params <: EdDSAParams.
      I have so far not managed to unify them. *)
   Lemma point_eq_copy : forall x1 x2 y1 y2, x1 = x2 -> y1 = y2 ->
     forall p1 p2, mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2.
-  Admitted.
+    apply Facts.point_eq.
+  Qed.
 
   Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p.
   Proof.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 732779a1a..7ef2f0aaf 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -289,7 +289,6 @@ Proof.
   cbv [cap Base25Point5_10limbs.base].
   intros.
   rewrite map_length in *.
-  About map_nth_default.
   erewrite map_nth_default; [|assumption].
   instantiate (2 := 0%Z).
   (** For the division of maps of (2 ^ _) over lists, replace it with 2 ^ (_ - _) *)