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

5 files changed, 329 insertions, 86 deletions

diff --git a/src/BoundedIterOp.v b/src/BoundedIterOp.v
new file mode 100644
index 000000000..14823ede8
--- /dev/null
+++ b/src/BoundedIterOp.v
@@ -0,0 +1,157 @@
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import BinNums NArith Nnat ZArith.
+
+Definition testbit_rev p i bound := Pos.testbit_nat p (bound - i).
+
+(* implements Pos.iter_op only using testbit, not destructing the positive *)
+Definition iter_op  {A} (op : A -> A -> A) (zero : A) (bound : nat) (p : positive) :=
+  fix iter (i : nat) (a : A) {struct i} : A :=
+    match i with
+    | O => zero
+    | S i' => let ret := iter i' (op a a) in
+             if testbit_rev p i bound
+               then op a ret
+               else      ret
+    end.
+
+Lemma testbit_rev_xI : forall p i b, (i < S b) ->
+  testbit_rev p~1 i (S b) = testbit_rev p i b.
+Proof.
+  unfold testbit_rev; intros.
+  replace (S b - i) with (S (b - i)) by omega.
+  case_eq (b - S i); intros; simpl; auto.
+Qed.
+
+Lemma testbit_rev_xO : forall p i b, (i < S b) ->
+  testbit_rev p~0 i (S b) = testbit_rev p i b.
+Proof.
+  unfold testbit_rev; intros.
+  replace (S b - i) with (S (b - i)) by omega.
+  case_eq (b - S i); intros; simpl; auto.
+Qed.
+
+Lemma testbit_rev_1 : forall i b, (i < S b) ->
+  testbit_rev 1%positive i (S b) = false.
+Proof.
+  unfold testbit_rev; intros.
+  replace (S b - i) with (S (b - i)) by omega.
+  case_eq (b - S i); intros; simpl; auto.
+Qed.
+
+Lemma iter_op_step_xI : forall {A} p i op z b (a : A), (i < S b) ->
+  iter_op op z (S b) p~1 i a = iter_op op z b p i a.
+Proof.
+  induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ].
+  simpl; rewrite testbit_rev_xI by omega.
+  case_eq i; intros; auto.
+  rewrite <- H0; simpl.
+  rewrite IHi by omega; auto.
+Qed.
+
+Lemma iter_op_step_xO : forall {A} p i op z b (a : A), (i < S b) ->
+  iter_op op z (S b) p~0 i a = iter_op op z b p i a.
+Proof.
+  induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ].
+  simpl; rewrite testbit_rev_xO by omega.
+  case_eq i; intros; auto.
+  rewrite <- H0; simpl.
+  rewrite IHi by omega; auto.
+Qed.
+
+Lemma iter_op_step_1 : forall {A} i op z b (a : A), (i < S b) ->
+  iter_op op z (S b) 1%positive i a = z.
+Proof.
+  induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ].
+  simpl; rewrite testbit_rev_1 by omega.
+  case_eq i; intros; auto.
+  rewrite <- H0; simpl.
+  rewrite IHi by omega; auto.
+Qed.
+
+Lemma pos_size_gt0 : forall p, 0 < Pos.size_nat p.
+Proof.
+  intros; case_eq p; intros; simpl; auto; try apply Lt.lt_0_Sn.
+Qed.
+Hint Resolve pos_size_gt0.
+
+Ltac iter_op_step := match goal with
+| [ |- context[iter_op ?op ?z ?b ?p~1 ?i ?a] ] => rewrite iter_op_step_xI
+| [ |- context[iter_op ?op ?z ?b ?p~0 ?i ?a] ] => rewrite iter_op_step_xO
+| [ |- context[iter_op ?op ?z ?b 1%positive ?i ?a] ] => rewrite iter_op_step_1
+end; auto.
+
+Lemma iter_op_spec : forall b p {A} op z (a : A) (zero_id : forall x : A, op x z = x), (Pos.size_nat p <= b) ->
+  iter_op op z b p b a = Pos.iter_op op p a.
+Proof.
+  induction b; intros; [pose proof (pos_size_gt0 p); omega |].
+  simpl; unfold testbit_rev; rewrite Minus.minus_diag.
+  case_eq p; intros; simpl; iter_op_step; simpl; 
+  rewrite IHb; rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto.
+Qed.
+
+Lemma xO_neq1 : forall p, (1 < p~0)%positive.
+Proof.
+  induction p; simpl; auto.
+  replace 2%positive with (Pos.succ 1) by auto.
+  apply Pos.lt_succ_diag_r.
+Qed.
+
+Lemma xI_neq1 : forall p, (1 < p~1)%positive.
+Proof.
+  induction p; simpl; auto.
+  replace 3%positive with (Pos.succ (Pos.succ 1)) by auto.
+  pose proof (Pos.lt_succ_diag_r (Pos.succ 1)).
+  pose proof (Pos.lt_succ_diag_r 1).
+  apply (Pos.lt_trans _ _ _ H0 H).
+Qed.
+
+Lemma xI_is_succ : forall n p
+  (H : Pos.of_succ_nat n = p~1%positive),
+  (Pos.to_nat (2 * p))%nat = n.
+Proof.
+  induction n; intros; simpl in *; auto. {
+    pose proof (xI_neq1 p).
+    rewrite H in H0.
+    pose proof (Pos.lt_irrefl p~1).
+    intuition.
+  } {
+    rewrite Pos.xI_succ_xO in H.
+    pose proof (Pos.succ_inj _ _ H); clear H.
+    rewrite Pos.of_nat_succ in H0.
+    rewrite <- Pnat.Pos2Nat.inj_iff in H0.
+    rewrite Pnat.Pos2Nat.inj_xO in H0.
+    rewrite Pnat.Nat2Pos.id in H0 by apply NPeano.Nat.neq_succ_0.
+    rewrite H0.
+    apply Pnat.Pos2Nat.inj_xO.
+  }
+Qed.
+
+Lemma xO_is_succ : forall n p
+  (H : Pos.of_succ_nat n = p~0%positive),
+  Pos.to_nat (Pos.pred_double p) = n.
+Proof.
+  induction n; intros; simpl; auto. {
+    pose proof (xO_neq1 p).
+    simpl in H; rewrite H in H0.
+    pose proof (Pos.lt_irrefl p~0).
+    intuition.
+  } {
+    rewrite Pos.pred_double_spec.
+    rewrite <- Pnat.Pos2Nat.inj_iff in H.
+    rewrite Pnat.Pos2Nat.inj_xO in H.
+    rewrite Pnat.SuccNat2Pos.id_succ in H.
+    rewrite Pnat.Pos2Nat.inj_pred by apply xO_neq1.
+    rewrite <- NPeano.Nat.succ_inj_wd.
+    rewrite Pnat.Pos2Nat.inj_xO.
+    rewrite <-  H.
+    auto.
+  }
+Qed.
+
+Lemma size_of_succ : forall n,
+  Pos.size_nat (Pos.of_nat n) <= Pos.size_nat (Pos.of_nat (S n)).
+Proof.
+  intros; induction n; [simpl; auto|].
+  apply Pos.size_nat_monotone.
+  apply Pos.lt_succ_diag_r.
+Qed.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v
new file mode 100644
index 000000000..7c1e173ee
--- /dev/null
+++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v
@@ -0,0 +1,71 @@
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.BoundedIterOp.
+Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import BinNums NArith Nnat ZArith.
+
+Section EdwardsDoubleAndAdd.
+  Context {prm:TwistedEdwardsParams}.
+  Definition doubleAndAdd (b n : nat) (P : point) : point :=
+    match N.of_nat n with
+    | 0%N => zero
+    | N.pos p => iter_op unifiedAdd zero b p b P
+    end.
+
+  Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P)%E.
+  Proof.
+    intros.
+    replace (n + n)%nat with (n * 2)%nat by omega.
+    induction n; simpl; auto.
+    rewrite twistedAddAssoc.
+    f_equal; auto.
+  Qed.
+
+  Lemma iter_op_double : forall p P,
+    Pos.iter_op unifiedAdd (p + p) P = Pos.iter_op unifiedAdd p (P + P)%E.
+  Proof.
+    intros.
+    rewrite Pos.add_diag.
+    unfold Pos.iter_op; simpl.
+    auto.
+  Qed.
+
+  Lemma doubleAndAdd_spec : forall n b P, (Pos.size_nat (Pos.of_nat n) <= b) ->
+    scalarMult n P = doubleAndAdd b n P.
+  Proof.
+    induction n; auto; intros.
+    unfold doubleAndAdd; simpl.
+    rewrite Pos.of_nat_succ.
+    rewrite iter_op_spec by (auto using zeroIsIdentity).
+    case_eq (Pos.of_nat (S n)); intros. {
+      simpl; f_equal.
+      rewrite (IHn b) by (pose proof (size_of_succ n); omega).
+      unfold doubleAndAdd.
+      rewrite H0 in H.
+      rewrite <- Pos.of_nat_succ in H0.
+      rewrite <- (xI_is_succ n p) by apply H0.
+      rewrite Znat.positive_nat_N; simpl.
+      rewrite iter_op_spec; auto using zeroIsIdentity.
+    } {
+      simpl; f_equal.
+      rewrite (IHn b) by (pose proof (size_of_succ n); omega).
+      unfold doubleAndAdd.
+      rewrite <- (xO_is_succ n p) by (rewrite Pos.of_nat_succ; auto).
+      rewrite Znat.positive_nat_N; simpl.
+      rewrite <- Pos.succ_pred_double in H0.
+      rewrite H0 in H.
+      rewrite iter_op_spec by (auto using zeroIsIdentity;
+        pose proof (Pos.lt_succ_diag_r (Pos.pred_double p));
+        apply Pos.size_nat_monotone in H1; omega; auto).
+      rewrite <- iter_op_double.
+      rewrite Pos.add_diag.
+      rewrite <- Pos.succ_pred_double.
+      rewrite Pos.iter_op_succ by apply twistedAddAssoc; auto.
+    } {
+      rewrite <- Pnat.Pos2Nat.inj_iff in H0.
+      rewrite Pnat.Nat2Pos.id in H0 by auto.
+      rewrite Pnat.Pos2Nat.inj_1 in H0.
+      assert (n = 0)%nat by omega; subst.
+      auto using zeroIsIdentity.
+    }
+  Qed.
+End EdwardsDoubleAndAdd.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index d2cd753fe..f2eba81eb 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -2,20 +2,93 @@ Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
+Local Open Scope F_scope.
 
-Section ExtendedCoordinates.
-  Local Open Scope F_scope.
-  Context {prm:TwistedEdwardsParams}.
-  Existing Instance prime_q.
+Section ExtendedCoordinatesFieldProofs.
+  (* If [field] worked on (F q) when Definition q := someProj someRecord, we
+     could inline this proof into unifiedAdd_repM1 *)
+  Context p (prime_p : Znumtheory.prime p) (two_lt_p : BinInt.Z.lt 2 p).
+  Existing Instance prime_p.
 
-  Add Field GFfield_Z : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
+  Add Field GFfield_Z : (@Ffield_theory p _)
+    (morphism (@Fring_morph p),
      preprocess [Fpreprocess],
      postprocess [Fpostprocess],
      constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     div (@Fmorph_div_theory p),
+     power_tac (@Fpower_theory p) [Fexp_tac]). 
+  
+  Lemma unifiedAdd_repM1_fieldproof:
+  forall (d XP YP ZP XQ YQ ZQ : F p)
+  (HZP : ZP <> 0)
+  (HZQ : ZQ <> 0)
+  (HoRp : forall x1 y1 x2 y2 : F p,
+    opp 1 * x1 ^ 2 + y1 ^ 2 = 1 + d * x1 ^ 2 * y1 ^ 2 ->
+    opp 1 * x2 ^ 2 + y2 ^ 2 = 1 + d * x2 ^ 2 * y2 ^ 2 ->
+    1 + d * x1 * x2 * y1 * y2 <> 0)
+  (HoRm : forall x1 y1 x2 y2 : F p,
+    opp 1 * x1 ^ 2 + y1 ^ 2 = 1 + d * x1 ^ 2 * y1 ^ 2 ->
+    opp 1 * x2 ^ 2 + y2 ^ 2 = 1 + d * x2 ^ 2 * y2 ^ 2 ->
+    1 - d * x1 * x2 * y1 * y2 <> 0)
+  (HoQ: opp 1 * (XQ / ZQ) ^ 2 + (YQ / ZQ) ^ 2 = 1 + d * (XQ / ZQ) ^ 2 * (YQ / ZQ) ^ 2)
+  (HoP : opp 1 * (XP / ZP) ^ 2 + (YP / ZP) ^ 2 = 1 + d * (XP / ZP) ^ 2 * (YP / ZP) ^ 2),
+      (((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))),
+      (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
+      ((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)))) =
+      ((XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) /
+                                                  (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)),
+      (YP / ZP * (YQ / ZQ) - opp 1 * (XP / ZP) * (XQ / ZQ)) /
+                                                              (1 - d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (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)) = 0 ->
+      False) /\
+      ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
+      ((YP + XP) * (YQ + XQ) + (YP - XP) * (YQ - XQ)) =
+      ((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)) *
+      ((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))).
+  Proof.
+    intros; repeat split; try apply (f_equal2 pair); try field; auto.
 
+    Ltac tnz := eauto 10 using Fq_mul_nonzero_nonzero, (@char_gt_2 p two_lt_p).
+    (* 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 (F p) _ _, H2: @eq (F p) _ _ |- _ ] =>
+      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
+      ); tnz
+    end. *)
+
+      - replace (ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz).
+      repeat apply Fq_mul_nonzero_nonzero.
+        + replace (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+        + replace (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+    Qed.
+End ExtendedCoordinatesFieldProofs.
+
+Section ExtendedCoordinates.
+  Context {prm:TwistedEdwardsParams}.
+  Existing Instance prime_q.
 
   (** [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>). *)
@@ -37,8 +110,8 @@ Section ExtendedCoordinates.
   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);
+  Ltac unfoldExtended := 
+    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
@@ -51,25 +124,29 @@ Section ExtendedCoordinates.
           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
+  end.
+  
+  Ltac solveExtended := unfoldExtended;
+    repeat match goal with
+      | [ |- _ /\ _ ] => split
       | [ |- @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
+      | _ => 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
+      | _ => solve [eapply @Fq_1_neq_0; eauto with typeclass_instances]
+      | _ => solve [eauto with typeclass_instances]
       | [ H: a = _ |- _ ] => rewrite H
-      | [ |- @eq (F q) _ _] => fail; field (*FIXME*)
   end.
 
   Lemma twistedToExtended_rep : forall P, twistedToExtended P ~= P.
   Proof.
-    extended_tac.
+    solveExtended.
   Qed.
 
   Lemma extendedToTwisted_rep : forall P rP, P ~= rP -> extendedToTwisted P = rP.
   Proof.
-    extended_tac.
+    solveExtended.
   Qed.
 
   Section TwistMinus1.
@@ -97,34 +174,10 @@ Section ExtendedCoordinates.
       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.
+      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d) as HoRp; simpl in HoRp.
+      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d) as HoRm; simpl in HoRm.
+      unfoldExtended; rewrite a_eq_minus1 in *.
+      apply unifiedAdd_repM1_fieldproof; auto using prime_q, two_lt_q.
     Qed.
+  End TwistMinus1.
 End ExtendedCoordinates.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v
deleted file mode 100644
index 8d24f2cd2..000000000
--- a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v
+++ /dev/null
@@ -1,38 +0,0 @@
-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/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 6594ae4ed..2f548935f 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -286,7 +286,7 @@ Section SquareRootsPrime5Mod8.
   (* This is only the square root of -1 if q mod 8 is 3 or 5 *)
   Definition sqrt_minus1 : F q :=  ZToField 2 ^ Z.to_N (q / 4).
 
-  Lemma two_lt_q : 2 < q.
+  Lemma two_lt_q_5mod8 : 2 < q.
   Proof.
     pose proof (prime_ge_2 q _) as two_le_q.
     apply Zle_lt_or_eq in two_le_q.
@@ -342,7 +342,7 @@ Section SquareRootsPrime5Mod8.
       replace (Z.to_N 2) with 2%N by auto.
       ring.
 
-      symmetry; apply euler_criterion_F; auto using two_lt_q.
+      symmetry; apply euler_criterion_F; auto using two_lt_q_5mod8.
     }
   Qed.