fix merge conflicts + PointFormats proofs

4 files changed, 424 insertions, 108 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index ad04c1ec6..248e0af6e 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -10,6 +10,7 @@ End Modulus25519.
 
 Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
   Module Import GFDefs := GaloisField Modulus25519.
+
   Local Open Scope GF_scope.
 
   Definition a : GF := -1.
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index c5e071169..cd27a2033 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -179,6 +179,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     apply mul_zero_why in H1.
     destruct H1; subst; intuition.
   Qed.
+  Hint Resolve mul_nonzero_nonzero.
 
   Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0.
     intros.
@@ -241,7 +242,10 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
         assert (rhs <> 0) by (rewrite H; auto)
     | [H: (?a^?p)%GF <> 0 |- _ ] =>
         match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
-        assert (a <> 0) by (eapply root_nonzero; eauto)
+        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 root_nonzero; eauto);
+          clear Z)
     | [H: (?a*?b)%GF <> 0 |- _ ] =>
         match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
         assert (a <> 0) by (eapply mul_nonzero_l; eauto)
@@ -258,11 +262,14 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     (* TODO: this proof was made inconsistent by an actually
              correct version of root_nonzero. This adds the necessary
              hypothesis*)
-    assert (2 <> 0)%N as Z by (intuition; inversion H).
     unfold onCurve; intuition; 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 Ha_nonzero.
+
     (* Furthermore... *)
-    pose proof  (eq_refl (d*x1^2*y1^2*(a*x2^2 + y2^2))) as Heqt.
+    pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
     rewrite H0 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.
@@ -270,59 +277,36 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
     rewrite <-H in Heqt.
 
-    (* main equation *)
-    case_eq_GF (sqrt_a*x2 + y2) 0%GF.
-    case_eq_GF (sqrt_a*x2 - y2) 0%GF.
-
-    - destruct H4.
-      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 (inject 2 * sqrt_a * x2) in Hc by field.
-
-      (* contradiction: product of nonzero things is zero *)
-      destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try (subst; field).
-      destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc].
-      + destruct char_gt_2; rewrite <- Hccc; field.
-      + destruct a_nonzero; rewrite <-a_square, Hccc; field.
-
-    - rewrite <- a_square in *.
-      assert ((sqrt_a*x1 - d * x1 * x2 * y1 * y2*y1)^2 = (sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2 - d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1) as Heqw by field.
-      rewrite H1 in Heqw.
-      replace (1 * y1^2) with (y1^2) in Heqw by field.
-      rewrite <- Heqt in Heqw.
-      replace (d * x1^2    *  y1^2    * (sqrt_a * sqrt_a * x2 ^ 2 + y2 ^ 2) +
-               d * x1 * x2 *  y1  * y2 * sqrt_a * inject 2 * x1 * y1)
-         with (d * (x1 * y1 * (sqrt_a * x2 + y2))^2)
-           in Heqw by field.
-      assert (d = (sqrt_a * x1 - d * x1 * x2 * y1 * y2 * y1)^2 / (x1 * y1 *
-      (sqrt_a * x2 - y2)) ^ 2) by (rewriteAny; field; auto).
-
-      (* FIXME: field fails if I remove this remember *)
-      remember (sqrt_a * x1 - d * x1 * x2 * y1 * y2 * y1) as p.
-      assert (d = (p/(x1 * y1 * (sqrt_a * x2 - y2)))^2) by (rewriteAny; field; auto).
-      subst p.
-
-      edestruct d_nonsquare; eauto.
-
-    - rewrite <- a_square in *.
-      assert ((sqrt_a*x1 + d * x1 * x2 * y1 * y2*y1)^2 = (sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2 + d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1) as Heqw by field.
-      rewrite H1 in Heqw.
-      replace (1 * y1^2) with (y1^2) in Heqw by field.
-      rewrite <- Heqt in Heqw.
-      replace (d * x1^2    *  y1^2    * (sqrt_a * sqrt_a * x2 ^ 2 + y2 ^ 2) +
-               d * x1 * x2 *  y1  * y2 * sqrt_a * inject 2 * x1 * y1)
-         with (d * (x1 * y1 * (sqrt_a * x2 + y2))^2)
-           in Heqw by field.
-      assert (d = (sqrt_a * x1 + d * x1 * x2 * y1 * y2 * y1)^2 / (x1 * y1 * (sqrt_a * x2 + y2)) ^ 2)
-        by (rewriteAny; field; auto).
-
-      (* FIXME: field fails if I remove this remember *)
-      remember (sqrt_a * x1 + d * x1 * x2 * y1 * y2 * y1) as p.
-      assert (d = (p/(x1 * y1 * (sqrt_a * x2 + y2)))^2) by (rewriteAny; field; auto).
-      subst p.
-
-      edestruct d_nonsquare; eauto.
+    (* main equation for both potentially nonzero denominators *)
+    case_eq_GF (sqrt_a*x2 + y2) 0; case_eq_GF (sqrt_a*x2 - y2) 0;
+      try match 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*(inject 2)*x1*y1)) as Heqw1 by field;
+        rewrite H1 in *;
+        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).
+
+    rewrite a_square in *.
+    replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field.
+
+    (* contradiction: product of nonzero things is zero *)
+    destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition].
+    destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero.
+
+    + replace (inject 2%Z) with (1+1) in Hccc by field; intuition.
+
+    + rewrite <- a_square; simpl; rewrite Hccc; field.
   Qed.
-  
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
     onCurve (x1,y1) ->
     onCurve (x2, y2) ->
@@ -369,6 +353,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Proof.
     (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
       * c=1 and an extra a in front of x^2 *) 
+
     unfold unifiedAdd', onCurve in *; injection H; clear H; intros.
 
     Ltac t x1 y1 x2 y2 :=
@@ -376,8 +361,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
              = (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.
+    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.
@@ -385,7 +369,6 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     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 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
 
     match goal with [ |- ?x = 1 ] => replace x with
@@ -393,18 +376,13 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
      ((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; try field; auto.
-
-    rewrite <-HT1, <-HT2; field; rewrite HT1.
-
-    - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
+    - 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; simpl.
-      repeat apply mul_nonzero_nonzero; auto.
-
+           by field; simpl; auto.
     - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
          with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
-           by field.
-      repeat apply mul_nonzero_nonzero; auto.
+           by field; auto.
   Qed.
 
   Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 ->
@@ -672,13 +650,7 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
   Definition point := extended.
   Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T).
   Definition extendedValid (P : point) : Prop :=
-    let pP := extendedToProjective P in
-    let X := projectiveX pP in
-    let Y := projectiveY pP in
-    let Z := projectiveZ pP in
-    let T := extendedT P in
-    T = X*Y/Z.
-
+    let '(X, Y, Z, T) := P in T = X*Y/Z.
 
   Definition twistedToExtended (P : (GF*GF)) : point :=
     let '(x, y) := P in (x, y, 1, x*y).
@@ -725,21 +697,12 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
   Local Notation "2" := (1+1).
   (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
   Definition unifiedAdd (P1 P2 : point) : point :=
-    let k := 2 * d in
-    let pP1 := extendedToProjective P1 in
-    let X1 := projectiveX pP1 in
-    let Y1 := projectiveY pP1 in
-    let Z1 := projectiveZ pP1 in
-    let T1 := extendedT P1 in
-    let pP2 := extendedToProjective P2 in
-    let X2 := projectiveX pP2 in
-    let Y2 := projectiveY pP2 in
-    let Z2 := projectiveZ pP2 in
-    let T2 := extendedT P2 in
+    let '(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*k*T2 in
-    let  D := Z1*2*Z2 in
+    let  C := T1*2*d*T2 in
+    let  D := Z1*2  *Z2 in
     let  E := B-A in
     let  F := D-C in
     let  G := D+C in
@@ -762,9 +725,7 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
     destruct P1 as [[X1 Y1 Z1] T1].
     destruct P2 as [[X2 Y2 Z2] T2].
     destruct P3 as [[X3 Y3 Z3] T3].
-    unfold extendedValid, extendedToProjective, projectiveToTwisted in *.
     invcs HeqP3.
-    subst.
     field.
     (* TODO: prove that denominators are nonzero *)
   Admitted.
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v
index 32ae4dde7..194f94385 100644
--- a/src/Specific/EdDSA25519.v
+++ b/src/Specific/EdDSA25519.v
@@ -95,7 +95,7 @@ Module EdDSA25519_Params <: EdDSAParams.
   Qed.
 
   Lemma square_mod_GF : forall (a x : Z),
-    (0 <= x < q /\ x * x mod q = a)%Z ->
+    (x * x mod q = a)%Z ->
     (inject x * inject x = inject a)%GF.
   Proof.
     intros.
@@ -103,7 +103,7 @@ Module EdDSA25519_Params <: EdDSAParams.
     rewrite <- inject_distr_mul.
     rewrite inject_mod_eq.
     replace modulus with q by auto.
-    rewrite H1; reflexivity.
+    reflexivity.
   Qed.
 
   Lemma a_square_old : exists x, (x * x = a)%GF.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 4a54e5437..55caf1e20 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -1,13 +1,374 @@
 Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil.
+Require Import VerdiTactics.
 Local Open Scope Z.
 
-Lemma euler_criterion : forall (a x p : Z) (prime_p : prime p),
-  (x * 2 + 1 = p)%Z -> (a ^ x mod p = 1)%Z ->
-    exists b : Z, (0 <= b < p /\ b * b mod p = a)%Z.
+(* TODO : integrate Andres's Fermat's little theorem proof *)
+Lemma fermat_little: forall (a p : Z) (prime_p : prime p),
+  a mod p <> 0 -> a ^ (p - 1) mod p = 1.
 Admitted.
 
+Ltac prime_bound := match goal with
+| H : prime ?p |- _ => pose proof (prime_ge_2 p H); try omega
+end.
+
+Lemma prime_minus1_div2_nonneg : forall (x p : Z) (prime_p : prime p),
+  x * 2 + 1 = p -> 0 < x.
+Proof.
+  intros; prime_bound.
+Qed.
+
+Lemma squared_fermat_little: forall (a x p : Z) (prime_p : prime p),
+  x * 2 + 1 = p -> a mod p <> 0 -> (a * a) ^ x mod p = 1.
+Proof.
+  intros.
+  rewrite <- Z.pow_2_r.
+  rewrite <- Z.pow_mul_r by
+    (pose proof (prime_minus1_div2_nonneg x p prime_p H); omega).
+  rewrite Z.mul_comm.
+  replace (x * 2) with (x * 2 + 1 - 1) by omega.
+  rewrite H.
+  apply fermat_little; auto.
+Qed.
+
+Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
+  a ^ x mod m = 0.
+Proof.
+  intros.
+  replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
+  induction (Z.to_nat x). {
+    simpl in *; omega.
+  } {
+    rewrite Nat2Z.inj_succ in *.
+    rewrite Z.pow_succ_r by omega.
+    rewrite Z.mul_mod by omega.
+    case_eq n; intros. {
+      subst. simpl.
+      rewrite Zmod_1_l by omega.
+      rewrite H1.
+      apply Zmod_0_l.
+    } {
+      subst.
+      rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega).
+      rewrite H1.
+      auto.
+    }
+  }
+Qed.
+
+Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
+    a ^ b mod m = (a mod m) ^ b mod m.
+Proof.
+  intros; rewrite <- (Z2Nat.id b) by auto.
+  induction (Z.to_nat b); auto.
+  rewrite Nat2Z.inj_succ.
+  do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
+  rewrite Z.mul_mod by auto.
+  rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto.
+  rewrite <- IHn by auto.
+  rewrite Z.mod_mod by auto.
+  reflexivity.
+Qed.
+
+Lemma euler_criterion_reverse : forall (a x p : Z) (prime_p : prime p),
+  (x * 2 + 1 = p) -> (a mod p <> 0) ->
+  (exists b, b * b mod p = a mod p) -> (a ^ x mod p = 1).
+Proof.
+  intros.
+  destruct H1.
+  assert (x0 mod p <> 0). {
+    intuition.
+    assert (2 > 0) by omega.
+    assert (p > 1) by prime_bound.
+    pose proof (mod_exp_0 x0 2 p H3 H4 H2); clear H3; clear H4.
+    rewrite Z.pow_2_r in H5.
+    rewrite H5 in H1.
+    intuition.
+  }
+  pose proof (squared_fermat_little x0 x p prime_p H H2).
+  assert (0 <= x) by (pose proof (prime_minus1_div2_nonneg x p prime_p H); omega).
+  assert (p <> 0) by prime_bound.
+  rewrite mod_pow by auto.
+  pose proof (mod_pow (x0 * x0) p x H4 H5).
+  rewrite H3 in H6.
+  rewrite H1 in H6.
+  auto.
+Qed.
+
+Fixpoint order_mod' y p i r :=
+  match i with
+  | O => r
+  | S i' => if (Zeq_bool (y ^ (Z.of_nat i) mod p) 1)
+            then order_mod' y p i' (Z.of_nat i)
+            else order_mod' y p i' r
+  end.
+
+Definition order_mod y p := order_mod' y p (Z.to_nat (p - 2)) (p - 1).
+
+Lemma order_mod'_le_r : forall y p i r, Z.of_nat i <= r ->
+  order_mod' y p i r <= r.
+Proof.
+  induction i; intros; try (simpl; omega).
+  unfold order_mod'; fold order_mod'.
+  assert (Z.of_nat i <= Z.of_nat (S i)) by (rewrite <- Nat2Z.inj_le; omega).
+  break_if. {
+    specialize (IHi (Z.of_nat (S i)) H0).
+    omega.
+  } {
+    apply IHi.
+    omega.
+  }
+Qed.
+
+Lemma order_mod'_pos : forall y p i r, 1 <= r -> 1 <= order_mod' y p i r.
+Proof.
+  induction i; intros; auto.
+  unfold order_mod'; fold order_mod'.
+  break_if; apply IHi; auto.
+  replace 1 with (Z.of_nat 1) by auto.
+  rewrite <- Nat2Z.inj_le.
+  pose proof (lt_0_Sn i); omega.
+Qed.
+
+Lemma order_mod_bounds : forall y p (prime_p : prime p),
+  1 <= order_mod y p <= p - 1.
+Proof.
+  unfold order_mod; split; intros. {
+    apply order_mod'_pos; prime_bound.
+  } {
+    apply order_mod'_le_r.
+    rewrite Z2Nat.id; prime_bound; omega.
+  }
+Qed.
+
+Lemma order_mod'_id : forall y p i r,
+  y ^ r mod p = 1 ->
+  y ^ (order_mod' y p i r) mod p = 1.
+Proof.
+  induction i; intros; [simpl; auto |].
+  unfold order_mod'; fold order_mod'.
+  break_if; auto.
+  apply IHi.
+  apply Zeq_bool_eq; auto.
+Qed.
+
+Lemma order_mod_id : forall y p (prime_p : prime p), (y mod p <> 0) -> y ^ (order_mod y p) mod p = 1.
+Proof.
+  intros.
+  unfold order_mod; apply order_mod'_id.
+  apply fermat_little; auto.
+Qed.
+
+Lemma order_mod'_upper_bound : forall x y p i r, 1 <= x <= Z.of_nat i ->
+  (Z.of_nat i <= r) -> (y ^ x mod p = 1) -> order_mod' y p i r <= x.
+Proof.
+  induction i; intros; try (simpl in H; omega).
+  unfold order_mod'; fold order_mod'.
+  assert (Z.of_nat i <= Z.of_nat (S i)) by (rewrite <- Nat2Z.inj_le; omega).
+  break_if. {
+    specialize (IHi (Z.of_nat (S i))).
+    destruct (Z.eq_dec x (Z.of_nat (S i))). {
+      rewrite e.
+      apply order_mod'_le_r; auto.
+    } {
+      destruct H.
+      rewrite Nat2Z.inj_succ in H3.
+      apply (Z.le_succ_r x (Z.of_nat i)) in H3.
+      destruct H3; intuition.
+      rewrite Nat2Z.inj_succ.
+      rewrite H3.
+      apply order_mod'_le_r.
+      omega.
+    }
+  } {
+    destruct H.
+    apply Z.le_lteq in H3; destruct H3. {
+      rewrite Nat2Z.inj_succ in H3.
+      apply IHi; omega.
+    } {
+      exfalso.
+      destruct H3.
+      apply Zeq_is_eq_bool in H1.
+      rewrite Heqb in H1.
+      intuition.
+    }
+  }
+Qed.
+
+Lemma order_mod_upper_bound : forall x y p (prime_p : prime p),
+  (1 <= x <= p - 2) ->
+  (y ^ x mod p = 1) -> order_mod y p <= x.
+Proof.
+  unfold order_mod; intros.
+  apply order_mod'_upper_bound; (rewrite Z2Nat.id; omega) || prime_bound.
+Qed.
+
+Lemma order_mod_lowest : forall x y p (prime_p : prime p),
+  1 <= x < order_mod y p -> y ^ x mod p <> 1.
+Proof.
+  intros.
+  intuition.
+  pose proof (order_mod_upper_bound x y p prime_p).
+  assert (1 <= x <= p - 2) as x_bounds. {
+    pose proof (order_mod_bounds y p prime_p).
+    omega.
+  }
+  specialize (H x_bounds H0).
+  omega.
+Qed.
+
+Lemma pow_mod_order : forall x y p (prime_p : prime p), 1 <= x ->
+  y ^ x mod p = 1 -> y ^ (x mod (order_mod y p)) mod p = 1.
+Proof.
+  intros.
+  remember (order_mod y p) as ord.
+  pose proof (order_mod_bounds y p prime_p).
+  assert (0 <= x / ord) by (apply Z.div_pos; omega).
+  assert (y mod p <> 0) by (intuition; apply (mod_exp_0 _ x) in H3; prime_bound).
+  rewrite (Z_div_mod_eq x ord) in H0 by omega.
+  rewrite Z.pow_add_r in H0 by (try apply Z.mul_nonneg_nonneg;
+    try apply Z.mod_pos_bound; omega).
+  rewrite Zmult_mod in H0.
+  rewrite Z.pow_mul_r in H0 by (try apply Z.mod_pos_bound; omega).
+  rewrite mod_pow in H0 by (prime_bound || auto).
+  rewrite Heqord in H0 at 1.
+  rewrite order_mod_id in H0; auto.
+  rewrite Z.pow_1_l in H0 by auto.
+  rewrite Z.mod_1_l in H0 by prime_bound.
+  rewrite Z.mul_1_l in H0.
+  rewrite Z.mod_mod in H0 by prime_bound.
+  auto.
+Qed.
+
+Lemma order_mod_divide : forall x y p (prime_p : prime p), 1 <= x ->
+  y ^ x mod p = 1 -> (order_mod y p | x).
+Proof.
+  intros.
+  pose proof (order_mod_bounds y p prime_p).
+  apply pow_mod_order in H0; auto.
+  assert (0 < order_mod y p) by omega.
+  apply (Z.mod_pos_bound x _) in H2.
+  pose proof (Z.nonpos_pos_cases (x mod order_mod y p)).
+  destruct H3. {
+    assert (x mod order_mod y p = 0) by omega.
+    apply Z.mod_divide; omega.
+  } {
+    assert (1 <= x mod order_mod y p <= p - 2) by omega.
+    pose proof (order_mod_upper_bound _ y p prime_p H4 H0).
+    omega.
+  }
+Qed.
+
+Lemma primitive_root_prime : forall p (prime_p : prime p),
+  exists y, 1 <= y <= p - 1 /\ order_mod y p = p - 1.
+Proof.
+Admitted.
+
+Lemma exists_primitive_root_power : forall x y p (prime_p : prime p),
+  order_mod y p = p - 1 -> exists j, 1 <= j <= p - 1 /\ y ^ j mod p = x mod p.
+Admitted.
+
+Lemma pred_odd : forall x, ~ (2 | x) -> (2 | x - 1).
+Proof.
+  intros.
+  rewrite <- Z.mod_divide in H by omega.
+  rewrite <- Z.mod_divide by omega.
+  pose proof (Zmod_odd x).
+  break_if; intuition.
+  replace x with (Z.succ (x - 1)) in Heqb by omega.
+  rewrite Z.odd_succ in Heqb.
+  pose proof (Zmod_even (x - 1)).
+  rewrite Heqb in H1; simpl in H1; auto.
+Qed.
+
+Ltac Zdivide_exists_mul := match goal with
+| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H
+| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
+end; (omega || auto).
+
+Lemma prime_pred_divide2 : forall p (prime_p : prime p) (p_odd : p <> 2),
+  (2 | p - 1).
+Proof.
+  intros.
+  apply pred_odd.
+  intuition.
+  Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound p 2); omega].
+  rewrite Z.mul_comm in H.
+  apply Zdivide_intro in H.
+  apply prime_divisors in H; auto.
+  intuition.
+  prime_bound.
+Qed.
+
+Lemma prime_odd : forall p (prime_p : prime p) (p_odd : p <> 2),
+  Zodd p.
+Proof.
+  intros.
+  pose proof (prime_pred_divide2 p prime_p p_odd).
+  assert (Zeven (p - 1)) by (Zdivide_exists_mul; [rewrite H; apply Zeven_2p
+  | pose proof (Zmod_pos_bound (p - 1) 2); omega]).
+  replace p with (Z.succ (p - 1)) by ring.
+  apply Zodd_Sn; auto.
+Qed.
+
+Lemma prime_minus1_div2_exact : forall x p (prime_p : prime p) (p_odd : p <> 2),
+  (x * 2 + 1 = p) -> x = (p - 1) / 2.
+Proof.
+  intros.
+  apply Zeq_plus_swap in H.
+  replace (p - 1) with (2 * ((p - 1) / 2)) in H by
+    (symmetry; apply Z_div_exact_2; try apply Z.mod_divide;
+    try apply prime_pred_divide2; (auto || omega)).
+  ring_simplify in H.
+  apply Z.mul_cancel_l in H; omega.
+Qed.
+
+Lemma divide_mul_div: forall a b c, a <> 0 -> c <> 0 ->
+  (a | b * (a / c)) -> (c | a) -> (c | b).
+Proof.
+  intros.
+  Zdivide_exists_mul.
+  Zdivide_exists_mul.
+  rewrite H2 in H1.
+  rewrite Z_div_mul' in H1 by auto.
+  replace (b * x) with (x * b) in H1 by ring.
+  replace (c * x * x0) with (x * (x0 * c)) in H1 by ring.
+  rewrite Z.mul_cancel_l in H1 by (intuition; rewrite H3 in H2; ring_simplify in H2; intuition).
+  eapply Zdivide_intro; eauto.
+Qed.
+
+Lemma euler_criterion : forall (a x p : Z) (prime_p : prime p)
+  (p_odd : p <> 2), x * 2 + 1 = p -> a ^ x mod p = 1 ->
+  exists b : Z, b * b mod p = a mod p.
+Proof.
+  intros.
+  destruct (primitive_root_prime p prime_p).
+  intuition.
+  pose proof (exists_primitive_root_power a x0 p prime_p H3).
+  destruct H2.
+  rewrite mod_pow in H0 by prime_bound.
+  intuition.
+  rewrite <- H6 in H0.
+  rewrite <- mod_pow in H0 by prime_bound.
+  rewrite <- Z.pow_mul_r in H0 by omega.
+  assert (p - 1 | x1 * x). {
+    rewrite <- H3.
+    apply order_mod_divide; auto.
+    assert (0 < x1 * x) by (apply Z.mul_pos_pos; omega).
+    omega.
+  }
+  exists (x0 ^ (x1 / 2)).
+  rewrite <- Z.pow_add_r by (apply Z.div_pos; omega).
+  rewrite <- Z_div_plus by omega.
+  rewrite Z.mul_comm.
+  rewrite (prime_minus1_div2_exact x p) in H5; auto.
+  apply (divide_mul_div _ x1 2) in H5; try (apply prime_pred_divide2 || prime_bound); auto.
+  rewrite <- Zdivide_Zdiv_eq by (auto || omega).
+  rewrite Zplus_diag_eq_mult_2.
+  rewrite Z_div_mult by omega; auto.
+Qed.
+
 Lemma divide2_1mod4 : forall x, x mod 4 = 1 -> 0 <= x -> (2 | x / 2).
 Proof.
   intros.
@@ -57,25 +418,18 @@ Proof.
 Qed.
 
 Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p),
-  (p mod 4 = 1)%Z -> exists b : Z, (0 <= b < p /\ b * b mod p = p - 1)%Z.
+  (p mod 4 = 1)%Z -> exists b : Z, (b * b mod p = p - 1)%Z.
 Proof.
   intros.
   assert (4 <> 0)%Z by omega.
   pose proof (Z.div_mod p 4 H0).
   pose proof (prime_ge_2 p (prime_p)).
   assert (2 | p / 2)%Z by (apply divide2_1mod4; (auto || omega)).
+  replace (p - 1) with ((p - 1) mod p) by (apply Zmod_small; omega).
+  assert (p <> 2) as neq_p_2 by intuition.
   apply (euler_criterion (p - 1) (p / 2) p prime_p);
-    [ | apply minus1_even_pow; (omega || auto); apply Z_div_pos; omega].
-  rewrite <- H.
-  rewrite H1 at 3.
-  f_equal.
-  replace 4%Z with (2 * 2)%Z by auto.
-  rewrite <- Z.div_div by omega.
-  rewrite <- Zdivide_Zdiv_eq_2 by (auto || omega).
-  replace (2 * 2 * (p / 2) / 2)%Z with (2 * (2 * (p / 2)) / 2)%Z
-    by (f_equal; apply Z.mul_assoc).
-  rewrite ZUtil.Z_div_mul' by omega.
-  rewrite Z.mul_comm.
-  auto.
+    [ auto |  | apply minus1_even_pow; (omega || auto); apply Z_div_pos; omega].
+  pose proof (prime_odd p prime_p neq_p_2).
+  rewrite <- Zdiv2_div.
+  rewrite Zodd_div2; (ring || auto).
 Qed.
-