From 543400d59cba6139368847de7760ccfedbf5f713 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Sat, 2 Jan 2016 04:25:53 -0500
Subject: UNTESTED simplification of specific GF25519 derivation

---
 src/Specific/GF25519.v | 149 ++++++++++++-------------------------------------
 1 file changed, 37 insertions(+), 112 deletions(-)

(limited to 'src')

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index d30d1f7fe..a96997612 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -102,13 +102,6 @@ End GF25519Base25Point5Params.
 
 Module GF25519Base25Point5 := GFPseudoMersenneBase Base25Point5_10limbs Modulus25519 GF25519Base25Point5Params.
 
-Ltac expand_list f :=
-  assert ((length f < 100)%nat) as _ by (simpl length in *; omega);
-    repeat progress (
-    let n := fresh f in
-    destruct f as [ | n ];
-    try solve [simpl length in *; try discriminate]).
-
 (* TODO: move to ListUtil *)
 Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y.
 Proof.
@@ -119,6 +112,18 @@ Proof.
   intros; solve_by_inversion.
 Qed.
 
+Ltac measure_length ls :=
+  pose proof (eq_refl (length ls)) as Hlen;
+  match goal with [H: ls = ?lsdef |- _ ] => rewrite H in Hlen at 2 end;
+  simpl in Hlen.
+
+Ltac expand_list f :=
+  assert ((length f < 100)%nat) as _ by (simpl length in *; omega);
+    repeat progress (
+    let n := fresh f in
+    destruct f as [ | n ];
+    try solve [simpl length in *; try discriminate]).
+
 Ltac expand_list_equalities := repeat match goal with
   | [H: (?x::?xs = ?y::?ys) |- _ ] =>
       let eq_head := fresh "Heq" x in
@@ -146,89 +151,44 @@ Section GF25519Base25Point5Formula.
 
     pose proof (mul_rep _ _  _ _ Hf Hg) as HmulRef.
     remember (GF25519Base25Point5.mul [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9]) as h.
-    unfold
-      GF25519Base25Point5.mul,
-      GF25519Base25Point5.B.add,
-      GF25519Base25Point5.E.mul,
-      GF25519Base25Point5.E.mul',
-      GF25519Base25Point5.E.mul_bi,
-      GF25519Base25Point5.E.mul_bi',
-      GF25519Base25Point5.E.mul_each,
-      GF25519Base25Point5.E.add,
-      GF25519Base25Point5.B.digits,
-      GF25519Base25Point5.E.digits,
-      Base25Point5_10limbs.base,
-      GF25519Base25Point5.E.crosscoef,
-      nth_default
-    in Heqh; simpl in Heqh.
-
-    unfold
-      two_power_pos,
-      shift_pos
-    in Heqh; simpl in Heqh.
-
-    (* evaluate row-column crossing coefficients for variable base multiplication *)
-    (* unfoldZ.div in Heqh; simpl in Heqh. *) (* THIS TAKES TOO LONG *)
-    repeat rewrite Z_div_same_full in Heqh by (abstract (apply Zeq_bool_neq; reflexivity)).
-    repeat match goal with [ Heqh : context[ (?a / ?b)%Z ]  |- _ ] =>
-      replace (a / b)%Z with 2%Z in Heqh by
-        (abstract (symmetry; erewrite <- Z.div_unique_exact; try apply Zeq_bool_neq; reflexivity))
-    end.
+    cbv [plus
+         seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
+         Base25Point5_10limbs.base GF25519Base25Point5Params.k GF25519Base25Point5Params.c
+         mul reduce
+         B.add
+         E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.crosscoef E.zeros
+         EC.base] in *.
+    simpl two_p in *.
 
+    Ltac acfo := abstract (clear; firstorder).
     Hint Rewrite
+      two_power_pos_equiv
       Z.mul_0_l
       Z.mul_0_r
       Z.mul_1_l
       Z.mul_1_r
       Z.add_0_l
       Z.add_0_r
+      Zdiv_1_r
       : Z_identities.
-    autorewrite with Z_identities in Heqh.
-
-    (* inline explicit formulas for modular reduction *)
-    cbv beta iota zeta delta [GF25519Base25Point5.reduce Base25Point5_10limbs.base] in Heqh.
-    remember GF25519Base25Point5Params.c as c in Heqh; unfold GF25519Base25Point5Params.c in Heqc.
-    simpl in Heqh.
-
-    (* prettify resulting modular multiplication expression *)
-    repeat rewrite (Z.mul_add_distr_l c) in Heqh.
-    repeat rewrite (Z.mul_assoc _ _ 2) in Heqh.
-    repeat rewrite (Z.mul_comm _ 2) in Heqh.
-    repeat rewrite (Z.mul_assoc 2 c) in Heqh.
-    remember (2 * c)%Z as TwoC in Heqh; subst c; simpl in HeqTwoC; subst TwoC. (* perform operations on constants *)
-    repeat rewrite Z.add_assoc in Heqh.
-    repeat rewrite Z.mul_assoc in Heqh.
-    assert (Hhl: length h = 10%nat) by (subst h; reflexivity); expand_list h; clear Hhl.
-    expand_list_equalities.
+    Hint Rewrite <- Zpower_exp using acfo : Z_identities.
+    Hint Rewrite <- Z.pow_sub_r using acfo : Z_identities. (* division is too slow to even compute once, simplify it away*)
+    autorewrite with Z_identities in *.
+
+    simpl Z.pow in *. cbv [Z.pow_pos Pos.iter] in *. (* compute the exponents that no longer need division *)
+    autorewrite with Z_identities in *.
+
+    (* remove redundant parentheses *)
+    repeat rewrite Z.add_assoc in *.
+    repeat rewrite Z.mul_assoc in *.
+    (* one equation per limb *)
+    measure_length h; expand_list h; expand_list_equalities.
     (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *)
-    (* output:
-      h0 = (f0*g0 + 38*f9*g1 + 19*f8*g2 + 38*f7*g3 + 19*f6*g4 + 38*f5*g5 + 19*f4*g6 + 38*f3*g7 + 19*f2*g8 + 38*f1*g9)
-      h1 = (f1*g0 + f0*g1    + 19*f9*g2 + 19*f8*g3 + 19*f7*g4 + 19*f6*g5 + 19*f5*g6 + 19*f4*g7 + 19*f3*g8 + 19*f2*g9)
-      h2 = (f2*g0 + 2*f1*g1  + f0*g2    + 38*f9*g3 + 19*f8*g4 + 38*f7*g5 + 19*f6*g6 + 38*f5*g7 + 19*f4*g8 + 38*f3*g9)
-      h3 = (f3*g0 + f2*g1    + f1*g2    + f0*g3    + 19*f9*g4 + 19*f8*g5 + 19*f7*g6 + 19*f6*g7 + 19*f5*g8 + 19*f4*g9)
-      h4 = (f4*g0 + 2*f3*g1  + f2*g2    + 2*f1*g3  + f0*g4    + 38*f9*g5 + 19*f8*g6 + 38*f7*g7 + 19*f6*g8 + 38*f5*g9)
-      h5 = (f5*g0 + f4*g1    + f3*g2    + f2*g3    + f1*g4    + f0*g5    + 19*f9*g6 + 19*f8*g7 + 19*f7*g8 + 19*f6*g9)
-      h6 = (f6*g0 + 2*f5*g1  + f4*g2    + 2*f3*g3  + f2*g4    + 2*f1*g5  + f0*g6    + 38*f9*g7 + 19*f8*g8 + 38*f7*g9)
-      h7 = (f7*g0 + f6*g1    + f5*g2    + f4*g3    + f3*g4    + f2*g5    + f1*g6    + f0*g7    + 19*f9*g8 + 19*f8*g9)
-      h8 = (f8*g0 + 2*f7*g1  + f6*g2    + 2*f5*g3  + f4*g4    + 2*f3*g5  + f2*g6    + 2*f1*g7  + f0*g8    + 38*f9*g9)
-      h9 = (f9*g0 + f8*g1    + f7*g2    + f6*g3    + f5*g4    + f4*g5    + f3*g6    + f2*g7    + f1*g8    + f0*g9)
-    *)
-    
-    (* prove equivalence of multiplication to the stated *)
-    assert (rep [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9] (f * g)%GF) as Hh. {
-      subst h0. subst h1. subst h2. subst h3. subst h4. subst h5. subst h6. subst h7. subst h8. subst h9.
-      repeat match goal with [H: _ = _ |- _ ] =>
-          rewrite <- H; clear H
-      end.
-      assumption.
-    }
 
     (* --- carry phase --- *)
     remember (rev [0;1;2;3;4;5;6;7;8;9;0])%nat as is; simpl in Heqis.
-    destruct (fun pf pf2 => carry_sequence_rep is _ _ pf pf2 Hh). {
-      subst is. clear. intros. simpl in *. firstorder.
-    } {
-      reflexivity.
+    destruct (fun pf pf2 => carry_sequence_rep is _ _ pf pf2 HmulRef); auto. {
+      subst is; clear. intros. simpl in *. repeat break_or_hyp; firstorder.
     }
     remember (carry_sequence is [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9]) as r; subst is.
 
@@ -264,10 +224,6 @@ Section GF25519Base25Point5Formula.
     rewrite Zdiv_1_r in *.
 
     (* replace division and Z.modulo with bit operations *)
-    remember (2 ^ 25)%Z as t25 in *.
-    remember (2 ^ 26)%Z as t26 in *.
-    repeat match goal with [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a end.
-    subst t25. subst t26.
     rewrite <- Z.land_ones in * by (abstract (clear; firstorder)).
     rewrite <- Z.shiftr_div_pow2 in * by (abstract (clear; firstorder)).
 
@@ -304,37 +260,6 @@ Section GF25519Base25Point5Formula.
     clear HmulRef Hh Hf Hg.
     existsFromEquations r.
     split; auto; congruence.
-
-    (* Here's the tactic code I added at this point at the end of the old version.
-     * Erase after reading, since it isn't needed anymore.
-
-    replace ([r0; r1; r2; r3; r4; r5; r6; r7; r8; r9]) with r; unfold rep; auto.
-
-    subst r.
-
-    Ltac rsubstBoth := repeat (match goal with [ |- ?a = ?b] => subst a; subst b; repeat progress f_equal || reflexivity end).
-    Ltac t := f_equal; abstract rsubstBoth || (try t).
-
-    Time t.
-    
-
-    (* But there's a nicer way! *)
-    Undo 2.
-
-    (* This tactic finds an [x := e] hypothesis and adds a matching [x = e] hypothesis. *)
-    Ltac letToEquality :=
-      match goal with
-      | [ x := ?e |- _ ] =>
-        match goal with
-        | [ _ : x = e |- _ ] => fail 1 (* To avoid infinite loop, make sure we didn't already do this one! *)
-        | _ => assert (x = e) by reflexivity
-        end
-      end.
-
-    (* Repeated introduction of those equalities enables [congruence] to solve the goal. *)
-    Ltac smarter_congruence := repeat letToEquality; congruence.
-
-    Time smarter_congruence.*)
   Defined.
 End GF25519Base25Point5Formula.
 
-- 
cgit v1.2.3


From bd39778e0679d1f67b5595e655aba1f62ac14e97 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Mon, 4 Jan 2016 08:43:33 -0500
Subject: prettier GF25519 derivation that runs out of memory

---
 src/Specific/GF25519.v | 207 +++++++++++++++++++++++--------------------------
 1 file changed, 97 insertions(+), 110 deletions(-)

(limited to 'src')

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index a96997612..f6fd63c0d 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -86,7 +86,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
   Lemma base_tail_matches_modulus:
     2^k mod nth_default 0 base (pred (length base)) = 0.
   Proof.
-    nth_tac.
+    reflexivity.
   Qed.
 
   Lemma b0_1 : forall x, nth_default x base 0 = 1.
@@ -112,17 +112,14 @@ Proof.
   intros; solve_by_inversion.
 Qed.
 
-Ltac measure_length ls :=
-  pose proof (eq_refl (length ls)) as Hlen;
-  match goal with [H: ls = ?lsdef |- _ ] => rewrite H in Hlen at 2 end;
-  simpl in Hlen.
-
-Ltac expand_list f :=
-  assert ((length f < 100)%nat) as _ by (simpl length in *; omega);
-    repeat progress (
-    let n := fresh f in
-    destruct f as [ | n ];
-    try solve [simpl length in *; try discriminate]).
+Ltac expand_list ls :=
+  let Hlen := fresh "Hlen" in
+  match goal with [H: ls = ?lsdef |- _ ] =>
+      assert (Hlen:length ls=length lsdef) by (f_equal; exact H)
+  end;
+  simpl in Hlen;
+  repeat progress (let n:=fresh ls in destruct ls as [|n ]; try solve [revert Hlen; clear; discriminate]);
+  clear Hlen.
 
 Ltac expand_list_equalities := repeat match goal with
   | [H: (?x::?xs = ?y::?ys) |- _ ] =>
@@ -133,8 +130,33 @@ Ltac expand_list_equalities := repeat match goal with
   | [H:?x = ?x|-_] => clear H
 end.
 
+
+(* This tactic takes in [r], a variable that we want to use to instantiate an existential.
+ * We find one other variable mentioned in [r], with its own equality in the hypotheses.
+ * That equality is then switched into a [let] in [r]'s defining equation. *)
+Ltac letify r :=
+  match goal with
+  | [ H : ?x = ?e |- _ ] =>
+    is_var x;
+    match goal with
+    | [ H' : r = _ |- _ ] =>
+      pattern x in H';
+        match type of H' with
+        | (fun z => r = @?e' z) x =>
+          let H'' := fresh "H" in assert (H'' : r = let x := e in e' x) by congruence;
+            clear H'; subst x; rename H'' into H'; cbv beta in H'
+        end
+    end
+  end.
+
+(* To instantiate an existential, give a variable with a defining equation to this tactic.
+ * We instantiate with a [let]-ified version of that equation. *)
+Ltac existsFromEquations r := repeat letify r;
+                             match goal with
+                             | [ _ : r = ?e |- context[?u] ] => unify u e
+                             end.
+
 Section GF25519Base25Point5Formula.
-  Local Open Scope Z_scope.
   Import GF25519Base25Point5.
   Import GF.
 
@@ -145,122 +167,84 @@ Section GF25519Base25Point5Formula.
                         -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
                         -> rep ls (f*g)%GF}.
   Proof.
-    intros.
-    eexists.
-    intros f g Hf Hg.
-
-    pose proof (mul_rep _ _  _ _ Hf Hg) as HmulRef.
-    remember (GF25519Base25Point5.mul [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9]) as h.
-    cbv [plus
-         seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
-         Base25Point5_10limbs.base GF25519Base25Point5Params.k GF25519Base25Point5Params.c
-         mul reduce
-         B.add
-         E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.crosscoef E.zeros
-         EC.base] in *.
-    simpl two_p in *.
 
-    Ltac acfo := abstract (clear; firstorder).
     Hint Rewrite
-      two_power_pos_equiv
       Z.mul_0_l
       Z.mul_0_r
       Z.mul_1_l
       Z.mul_1_r
       Z.add_0_l
       Z.add_0_r
-      Zdiv_1_r
+      Z.add_assoc
+      Z.mul_assoc
       : Z_identities.
-    Hint Rewrite <- Zpower_exp using acfo : Z_identities.
-    Hint Rewrite <- Z.pow_sub_r using acfo : Z_identities. (* division is too slow to even compute once, simplify it away*)
-    autorewrite with Z_identities in *.
-
-    simpl Z.pow in *. cbv [Z.pow_pos Pos.iter] in *. (* compute the exponents that no longer need division *)
-    autorewrite with Z_identities in *.
-
-    (* remove redundant parentheses *)
-    repeat rewrite Z.add_assoc in *.
-    repeat rewrite Z.mul_assoc in *.
-    (* one equation per limb *)
-    measure_length h; expand_list h; expand_list_equalities.
-    (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *)
 
-    (* --- carry phase --- *)
-    remember (rev [0;1;2;3;4;5;6;7;8;9;0])%nat as is; simpl in Heqis.
-    destruct (fun pf pf2 => carry_sequence_rep is _ _ pf pf2 HmulRef); auto. {
-      subst is; clear. intros. simpl in *. repeat break_or_hyp; firstorder.
-    }
-    remember (carry_sequence is [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9]) as r; subst is.
-
-    (* unroll the carry loop, create a separate variable for each of the 10 list elements *)
-    cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqr.
+    Ltac deriveModularMultiplicationWithCarries carryscript :=
+    let h := fresh "h" in
+    let fg := fresh "fg" in
+    let Hfg := fresh "Hfg" in
     repeat match goal with
+    | [ |- { _ | forall f g, rep ?fs f -> rep ?gs g -> rep _ ?ret } ] =>
+        remember (carry_sequence carryscript (mul fs gs)) as fg;
+        assert (forall f g, rep fs f -> rep gs g -> rep fg ret) as Hfg
+    | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition)
+    | [ Heqfg: fg = carry_sequence _ (mul _ _) |- { _ | forall f g, rep ?fs f -> rep ?gs g -> rep _ ?ret } ] =>
+        (* expand bignum multiplication *)
+        cbv [plus
+          seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
+          mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c
+          E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg;
+        repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *)
+            let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end;
+        autorewrite with Z_identities in Heqfg;
+        (* speparate out carries *)
+        match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end;
+        (* one equation per limb *)
+        expand_list h; expand_list_equalities;
+        (* expand carry *)
+        cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg
     | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a
-    | [H: context[GF25519Base25Point5.carry ?i (?x::?xs)] |- _ ] =>
+    | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *)
         let cr := fresh "cr" in
-        remember (GF25519Base25Point5.carry i (x::xs)) as cr;
+        idtac i x xs;
+        remember (carry i (x::xs)) as cr in Hfg;
         match goal with [ Heq : cr = ?crdef |- _ ] =>
-            cbv [GF25519Base25Point5.carry GF25519Base25Point5.carry_simple GF25519Base25Point5.carry_and_reduce] in Heq;
+            cbv [carry carry_simple carry_and_reduce] in Heq;
             simpl eq_nat_dec in Heq; cbv iota beta in Heq;
-            cbv [set_nth nth_default nth_error value GF25519Base25Point5.add_to_nth] in Heq;
-            let Heql := fresh "Heql" in
-              assert (length cr = length crdef) as Heql by (subst cr; reflexivity);
-              simpl length in Heql; expand_list cr; clear Heql;
-            expand_list_equalities
+            cbv [set_nth nth_default nth_error value add_to_nth] in Heq;
+            expand_list cr; expand_list_equalities
         end
+    | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H;
+        match goal with [Heqc: c = cap i |- _ ] =>
+            unfold cap, Base25Point5_10limbs.base in Heqc;
+            simpl eq_nat_dec in Heqc;
+            cbv [nth_default nth_error value error] in Heqc;
+            simpl map in Heqc;
+            cbv [GF25519Base25Point5Params.k] in Heqc
+        end;
+        subst c;
+        repeat rewrite Zdiv_1_r in H;
+        repeat rewrite two_power_pos_equiv in H;
+        repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder));
+        repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity));
+        repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity));
+        simpl Z.sub in H;
+        unfold  GF25519Base25Point5Params.c in H
+    | [H: context[Z.ones ?l] |- _ ] =>
+            (* postponing this to the main loop makes the autorewrite slow *)
+          let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c
+    | [ |- _ ] => subst fg; apply carry_sequence_rep, mul_rep
+    | [ |- _ ] => abstract (solve [auto])
+    | [ |- _ ] => progress intros
     end.
+    Time deriveModularMultiplicationWithCarries (rev [0;1;2;3;4;5;6;7;8;9;0]).
 
-    (* compute the human-meaningful froms of constants used during carrying *)
-    cbv [GF25519Base25Point5.cap Base25Point5_10limbs.base GF25519Base25Point5Params.k] in *.
-    simpl eq_nat_dec in *; cbv iota in *.
-    repeat match goal with
-    | [H: _ |- _ ] =>
-      rewrite (map_nth_default _ _ _ _ 0%nat 0%Z) in H by (abstract (clear; rewrite seq_length; firstorder))
-    end.
-    simpl two_p in *.
-    repeat rewrite two_power_pos_equiv in *.
-    repeat rewrite <- Z.pow_sub_r in * by (abstract (clear; firstorder)).
-    simpl Z.sub in *;
-    rewrite Zdiv_1_r in *.
-
-    (* replace division and Z.modulo with bit operations *)
-    rewrite <- Z.land_ones in * by (abstract (clear; firstorder)).
-    rewrite <- Z.shiftr_div_pow2 in * by (abstract (clear; firstorder)).
-
-    (* evaluate the constant arguments to bit operations *)
-    remember (Z.ones 25) as m25 in *. compute in Heqm25. subst m25.
-    remember (Z.ones 26) as m26 in *. compute in Heqm26. subst m26.
-    unfold GF25519Base25Point5Params.c in *.
-
-    (* This tactic takes in [r], a variable that we want to use to instantiate an existential.
-     * We find one other variable mentioned in [r], with its own equality in the hypotheses.
-     * That equality is then switched into a [let] in [r]'s defining equation. *)
-    Ltac letify r :=
-      match goal with
-      | [ H : ?x = ?e |- _ ] =>
-        is_var x;
-        match goal with
-        | [ H' : r = _ |- _ ] =>
-          pattern x in H';
-            match type of H' with
-            | (fun z => r = @?e' z) x =>
-              let H'' := fresh "H" in assert (H'' : r = let x := e in e' x) by congruence;
-                clear H'; subst x; rename H'' into H'; cbv beta in H'
-            end
-        end
-      end.
-
-    (* To instantiate an existential, give a variable with a defining equation to this tactic.
-     * We instantiate with a [let]-ified version of that equation. *)
-    Ltac existsFromEquations r := repeat letify r;
-                                 match goal with
-                                 | [ _ : r = ?e |- context[?u] ] => unify u e
-                                 end.
+    (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *)
 
-    clear HmulRef Hh Hf Hg.
-    existsFromEquations r.
-    split; auto; congruence.
-  Defined.
+    eexists.
+    existsFromEquations fg.
+    subst; auto.
+  Time Defined.
 End GF25519Base25Point5Formula.
 
 Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
@@ -268,3 +252,6 @@ Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
  * More Ltac acrobatics will be needed to get out that formula for further use in Coq.
  * The easiest fix will be to make the proof script above fully automated,
  * using [abstract] to contain the proof part. *)
+
+
+
-- 
cgit v1.2.3


From aebc0124ee411786cd711042da7abb67cdf5b40a Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Wed, 6 Jan 2016 00:46:50 -0500
Subject: fix letify to only insert a term once

---
 src/Specific/GF25519.v | 240 +++++++++++++++++++++++--------------------------
 src/Util/ListUtil.v    |   9 ++
 2 files changed, 120 insertions(+), 129 deletions(-)

(limited to 'src')

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index f6fd63c0d..51f1b14c8 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -6,17 +6,24 @@ Require Import QArith.QArith QArith.Qround.
 Require Import VerdiTactics.
 Close Scope Q.
 
+Ltac twoIndices i j base := 
+    intros;
+    assert (In i (seq 0 (length base))) by nth_tac;
+    assert (In j (seq 0 (length base))) by nth_tac;
+    repeat match goal with [ x := _ |- _ ] => subst x end;
+    simpl in *; repeat break_or_hyp; try omega; vm_compute; reflexivity.
+
 Module Base25Point5_10limbs <: BaseCoefs.
   Local Open Scope Z_scope.
   Definition base := map (fun i => two_p (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10).
   Lemma base_positive : forall b, In b base -> b > 0.
   Proof.
-    compute; intros; repeat break_or_hyp; intuition.
+    compute; intuition; subst; intuition.
   Qed.
 
   Lemma b0_1 : forall x, nth_default x base 0 = 1.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma base_good :
@@ -25,11 +32,7 @@ Module Base25Point5_10limbs <: BaseCoefs.
     let r := (b i * b j) / b (i+j)%nat in
     b i * b j = r * b (i+j)%nat.
   Proof.
-    intros.
-    assert (In i (seq 0 (length base))) by nth_tac.
-    assert (In j (seq 0 (length base))) by nth_tac.
-    subst b; subst r; simpl in *.
-    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+    twoIndices i j base.
   Qed.
 End Base25Point5_10limbs.
 
@@ -53,7 +56,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
   Lemma modulus_pseudomersenne :
     primeToZ modulus = 2^k - c.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma base_matches_modulus :
@@ -65,53 +68,35 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
     let r := (b i * b j)  /   (2^k * b (i+j-length base)%nat) in
               b i * b j = r * (2^k * b (i+j-length base)%nat).
   Proof.
-    intros.
-    assert (In i (seq 0 (length base))) by nth_tac.
-    assert (In j (seq 0 (length base))) by nth_tac.
-    subst b; subst r; simpl in *.
-    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+    twoIndices i j base.
   Qed.
 
   Lemma base_succ : forall i, ((S i) < length base)%nat -> 
     let b := nth_default 0 base in
     b (S i) mod b i = 0.
   Proof.
-    intros.
-    assert (In i (seq 0 (length base))) by nth_tac.
-    assert (In (S i) (seq 0 (length base))) by nth_tac.
-    subst b; simpl in *.
-    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+    intros; twoIndices i (S i) base.
   Qed.
 
   Lemma base_tail_matches_modulus:
     2^k mod nth_default 0 base (pred (length base)) = 0.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma b0_1 : forall x, nth_default x base 0 = 1.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma k_nonneg : 0 <= k.
   Proof.
-    rewrite Zle_is_le_bool; reflexivity.
+    rewrite Zle_is_le_bool; auto.
   Qed.
 End GF25519Base25Point5Params.
 
 Module GF25519Base25Point5 := GFPseudoMersenneBase Base25Point5_10limbs Modulus25519 GF25519Base25Point5Params.
 
-(* TODO: move to ListUtil *)
-Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y.
-Proof.
-  intros; solve_by_inversion.
-Qed.
-Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys.
-Proof.
-  intros; solve_by_inversion.
-Qed.
-
 Ltac expand_list ls :=
   let Hlen := fresh "Hlen" in
   match goal with [H: ls = ?lsdef |- _ ] =>
@@ -121,6 +106,28 @@ Ltac expand_list ls :=
   repeat progress (let n:=fresh ls in destruct ls as [|n ]; try solve [revert Hlen; clear; discriminate]);
   clear Hlen.
 
+Ltac letify r :=
+  match goal with
+  | [ H' : r = _ |- _ ] =>
+    match goal with
+    | [ H : ?x = ?e |- _ ] =>
+      is_var x;
+      match goal with (* only letify equations that appear nowhere other than r *)
+      | _ => clear H H' x; fail 1
+      | _ => fail 2
+      end || idtac;
+      pattern x in H';
+      match type of H' with
+      | (fun z => r = @?e' z) x =>
+        let H'' := fresh "H" in
+        assert (H'' : r = let x := e in e' x) by
+          (* congruence is slower for every subsequent letify *)
+          (rewrite H'; subst x; reflexivity);
+        clear H'; subst x; rename H'' into H'; cbv beta in H'
+      end
+    end
+  end.
+
 Ltac expand_list_equalities := repeat match goal with
   | [H: (?x::?xs = ?y::?ys) |- _ ] =>
       let eq_head := fresh "Heq" x in
@@ -130,36 +137,81 @@ Ltac expand_list_equalities := repeat match goal with
   | [H:?x = ?x|-_] => clear H
 end.
 
-
-(* This tactic takes in [r], a variable that we want to use to instantiate an existential.
- * We find one other variable mentioned in [r], with its own equality in the hypotheses.
- * That equality is then switched into a [let] in [r]'s defining equation. *)
-Ltac letify r :=
-  match goal with
-  | [ H : ?x = ?e |- _ ] =>
-    is_var x;
-    match goal with
-    | [ H' : r = _ |- _ ] =>
-      pattern x in H';
-        match type of H' with
-        | (fun z => r = @?e' z) x =>
-          let H'' := fresh "H" in assert (H'' : r = let x := e in e' x) by congruence;
-            clear H'; subst x; rename H'' into H'; cbv beta in H'
-        end
-    end
-  end.
-
-(* To instantiate an existential, give a variable with a defining equation to this tactic.
- * We instantiate with a [let]-ified version of that equation. *)
-Ltac existsFromEquations r := repeat letify r;
-                             match goal with
-                             | [ _ : r = ?e |- context[?u] ] => unify u e
-                             end.
-
 Section GF25519Base25Point5Formula.
   Import GF25519Base25Point5.
   Import GF.
 
+  Hint Rewrite
+    Z.mul_0_l
+    Z.mul_0_r
+    Z.mul_1_l
+    Z.mul_1_r
+    Z.add_0_l
+    Z.add_0_r
+    Z.add_assoc
+    Z.mul_assoc
+    : Z_identities.
+
+  Ltac deriveModularMultiplicationWithCarries carryscript :=
+  let h := fresh "h" in
+  let fg := fresh "fg" in
+  let Hfg := fresh "Hfg" in
+  intros;
+  repeat match goal with
+  | [ Hf: rep ?fs ?f, Hg: rep ?gs ?g |- rep _ ?ret ] =>
+      remember (carry_sequence carryscript (mul fs gs)) as fg;
+      assert (rep fg ret) as Hfg; [subst fg; apply carry_sequence_rep, mul_rep; eauto|]
+  | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition)
+  | [ Heqfg: fg = carry_sequence _ (mul _ _) |- rep _ ?ret ] =>
+      (* expand bignum multiplication *)
+      cbv [plus
+        seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
+        mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c
+        E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg;
+      repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *)
+          let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end;
+      autorewrite with Z_identities in Heqfg;
+      (* speparate out carries *)
+      match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end;
+      (* one equation per limb *)
+      expand_list h; expand_list_equalities;
+      (* expand carry *)
+      cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg
+  | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a
+  | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *)
+      let cr := fresh "cr" in
+      remember (carry i (x::xs)) as cr in Hfg;
+      match goal with [ Heq : cr = ?crdef |- _ ] =>
+          (* is there any simpler way to do this? *)
+          cbv [carry carry_simple carry_and_reduce] in Heq;
+          simpl eq_nat_dec in Heq; cbv iota beta in Heq;
+          cbv [set_nth nth_default nth_error value add_to_nth] in Heq;
+          expand_list cr; expand_list_equalities
+      end
+  | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H;
+      match goal with [Heqc: c = cap i |- _ ] =>
+          (* is there any simpler way to do this? *)
+          unfold cap, Base25Point5_10limbs.base in Heqc;
+          simpl eq_nat_dec in Heqc;
+          cbv [nth_default nth_error value error] in Heqc;
+          simpl map in Heqc;
+          cbv [GF25519Base25Point5Params.k] in Heqc
+      end;
+      subst c;
+      repeat rewrite Zdiv_1_r in H;
+      repeat rewrite two_power_pos_equiv in H;
+      repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder));
+      repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity));
+      repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity));
+      simpl Z.sub in H;
+      unfold  GF25519Base25Point5Params.c in H
+  | [H: context[Z.ones ?l] |- _ ] =>
+          (* postponing this to the main loop makes the autorewrite slow *)
+        let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c
+  | [ |- _ ] => abstract (solve [auto])
+  | [ |- _ ] => progress intros
+  end.
+
   Lemma GF25519Base25Point5_mul_reduce_formula :
     forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 
       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
@@ -168,82 +220,12 @@ Section GF25519Base25Point5Formula.
                         -> rep ls (f*g)%GF}.
   Proof.
 
-    Hint Rewrite
-      Z.mul_0_l
-      Z.mul_0_r
-      Z.mul_1_l
-      Z.mul_1_r
-      Z.add_0_l
-      Z.add_0_r
-      Z.add_assoc
-      Z.mul_assoc
-      : Z_identities.
+    eexists.
 
-    Ltac deriveModularMultiplicationWithCarries carryscript :=
-    let h := fresh "h" in
-    let fg := fresh "fg" in
-    let Hfg := fresh "Hfg" in
-    repeat match goal with
-    | [ |- { _ | forall f g, rep ?fs f -> rep ?gs g -> rep _ ?ret } ] =>
-        remember (carry_sequence carryscript (mul fs gs)) as fg;
-        assert (forall f g, rep fs f -> rep gs g -> rep fg ret) as Hfg
-    | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition)
-    | [ Heqfg: fg = carry_sequence _ (mul _ _) |- { _ | forall f g, rep ?fs f -> rep ?gs g -> rep _ ?ret } ] =>
-        (* expand bignum multiplication *)
-        cbv [plus
-          seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
-          mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c
-          E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg;
-        repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *)
-            let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end;
-        autorewrite with Z_identities in Heqfg;
-        (* speparate out carries *)
-        match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end;
-        (* one equation per limb *)
-        expand_list h; expand_list_equalities;
-        (* expand carry *)
-        cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg
-    | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a
-    | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *)
-        let cr := fresh "cr" in
-        idtac i x xs;
-        remember (carry i (x::xs)) as cr in Hfg;
-        match goal with [ Heq : cr = ?crdef |- _ ] =>
-            cbv [carry carry_simple carry_and_reduce] in Heq;
-            simpl eq_nat_dec in Heq; cbv iota beta in Heq;
-            cbv [set_nth nth_default nth_error value add_to_nth] in Heq;
-            expand_list cr; expand_list_equalities
-        end
-    | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H;
-        match goal with [Heqc: c = cap i |- _ ] =>
-            unfold cap, Base25Point5_10limbs.base in Heqc;
-            simpl eq_nat_dec in Heqc;
-            cbv [nth_default nth_error value error] in Heqc;
-            simpl map in Heqc;
-            cbv [GF25519Base25Point5Params.k] in Heqc
-        end;
-        subst c;
-        repeat rewrite Zdiv_1_r in H;
-        repeat rewrite two_power_pos_equiv in H;
-        repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder));
-        repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity));
-        repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity));
-        simpl Z.sub in H;
-        unfold  GF25519Base25Point5Params.c in H
-    | [H: context[Z.ones ?l] |- _ ] =>
-            (* postponing this to the main loop makes the autorewrite slow *)
-          let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c
-    | [ |- _ ] => subst fg; apply carry_sequence_rep, mul_rep
-    | [ |- _ ] => abstract (solve [auto])
-    | [ |- _ ] => progress intros
-    end.
     Time deriveModularMultiplicationWithCarries (rev [0;1;2;3;4;5;6;7;8;9;0]).
-
     (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *)
 
-    eexists.
-    existsFromEquations fg.
-    subst; auto.
+    Time repeat letify fg; subst fg; eauto.
   Time Defined.
 End GF25519Base25Point5Formula.
 
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 350f55dd8..783e3f527 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -524,3 +524,12 @@ Ltac set_nth_inbounds :=
   end.
 
 Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds.
+
+Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y.
+Proof.
+  intros; solve_by_inversion.
+Qed.
+Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys.
+Proof.
+  intros; solve_by_inversion.
+Qed.
-- 
cgit v1.2.3


From a1ab6f7b47173ff927958a19b952f26078ddf373 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Thu, 7 Jan 2016 11:20:39 -0500
Subject: Start writing PointFormats field proofs

---
 src/Curves/PointFormats.v | 34 +++++++++++++++++++++++++++++-----
 1 file changed, 29 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 1e8df9337..cae6f939d 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
+Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField.
 Require Import Tactics.VerdiTactics.
 Require Import Logic.Eqdep_dec.
 Require Import BinNums NArith.
@@ -8,7 +8,7 @@ Module GaloisDefs (M : Modulus).
 End GaloisDefs.
 
 Module Type TwistedEdwardsParams (M : Modulus).
-  Module Export GFDefs := GaloisDefs M.
+  Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
   Parameter a : GF.
   Axiom a_nonzero : a <> 0.
@@ -125,7 +125,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Hint Unfold onCurve mkPoint.
 
   Definition zero : point. exists (0, 1).
-    abstract (unfold onCurve; ring).
+    abstract (unfold onCurve; field).
   Defined.
 
   Definition unifiedAdd' (P1' P2' : (GF*GF)) :=
@@ -138,8 +138,28 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     let 'exist P2' pf2 := P2 in
     mkPoint (unifiedAdd' P1' P2') _).
   Proof.
-    destruct P1' as [x1 y1], P2' as [x2 y2]; unfold unifiedAdd', onCurve.
-    admit. (* field will likely work here, but I have not done this by hand *)
+    (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1, c=1 and an extra a in front of x^2 *) 
+    destruct P1' as [x1 y1], P2' as [x2 y2].
+    remember (unifiedAdd' (x1, y1) (x2, y2)) as P3.
+    destruct P3 as [x3 y3]. injection HeqP3; clear HeqP3; intros.
+    unfold unifiedAdd', onCurve in *.
+
+    Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
+    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 (T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
+    assert (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.
+    (* change all fractions to a common denominator and merge. That fraction will be T/T based on the hypotheses. Which is 1. *)
+    admit.
   Defined.
   Local Infix "+" := unifiedAdd.
 
@@ -221,6 +241,10 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
     (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
   Admitted.
 
+  Lemma zeroIsIdentity' : forall P, unifiedAdd' P  zero = P.
+  Admitted.
+  Hint Resolve zeroIsIdentity.
+
   Lemma zeroIsIdentity : forall P, P + zero = P.
   Admitted.
   Hint Resolve zeroIsIdentity.
-- 
cgit v1.2.3


From ba1053c19ee10cfb2f28318d2fab8577d56eb749 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Thu, 7 Jan 2016 15:03:32 -0500
Subject: fix unverified typo in fermat proof

---
 src/Scratch/fermat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/Scratch/fermat.v b/src/Scratch/fermat.v
index 7871db92f..947ffce15 100644
--- a/src/Scratch/fermat.v
+++ b/src/Scratch/fermat.v
@@ -42,7 +42,7 @@ Section Fq.
 
   Axiom inv : Fq -> Fq.
   Axiom inv_spec : forall a, inv a * a = one.
-  Definition div a b := add a (inv b).
+  Definition div a b := mul a (inv b).
   Infix "/" := div.
 
   Fixpoint replicate {T} n (x:T) : list T := match n with O => nil | S n' => x::replicate n' x end.
-- 
cgit v1.2.3


From 07cfa74f85145dca389fb07f5472365a9bca94be Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Thu, 7 Jan 2016 15:03:54 -0500
Subject: fix field for division by constant (by dmz@mit.edu)

---
 src/Galois/GaloisExamples.v |  6 ++++++
 src/Galois/ZGaloisField.v   | 13 ++++++++++---
 2 files changed, 16 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v
index f649701b7..12bcfa2c8 100644
--- a/src/Galois/GaloisExamples.v
+++ b/src/Galois/GaloisExamples.v
@@ -42,6 +42,12 @@ Module Example31.
     field; trivial.
   Qed.
 
+  Lemma example4: forall x: GF, x/(inject 1) = x.
+  Proof.
+    intros; field.
+    discriminate.
+  Qed.
+
 End Example31.
 
 Module TimesZeroTransparentTestModule.
diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v
index bf9efa964..a554e826a 100644
--- a/src/Galois/ZGaloisField.v
+++ b/src/Galois/ZGaloisField.v
@@ -1,7 +1,7 @@
-
 Require Import BinInt BinNat ZArith Znumtheory.
 Require Import BoolEq Field_theory.
 Require Import Galois GaloisTheory.
+Require Import Tactics.VerdiTactics.
 
 Module ZGaloisField (M: Modulus).
   Module G := Galois M.
@@ -52,11 +52,20 @@ Module ZGaloisField (M: Modulus).
       apply prime_ge_2 in p; intuition.
   Qed.
 
+  Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
+  Proof.
+    intuition; solve_by_inversion.
+  Qed.
+
   Ltac GFpreprocess :=
     repeat rewrite injectZeroIsGFZero;
     repeat rewrite injectOneIsGFOne.
 
   Ltac GFpostprocess :=
+    repeat split;
+		repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
+			replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
+		end;
     repeat rewrite <- injectZeroIsGFZero;
     repeat rewrite <- injectOneIsGFOne.
 
@@ -79,6 +88,4 @@ Module ZGaloisField (M: Modulus).
      constants [GFconstant],
      div GFmorph_div_theory,
      power_tac GFpower_theory [GFexp_tac]). 
-
 End ZGaloisField.
-
-- 
cgit v1.2.3


From cd6479fa848f48892c370970f87595773108b099 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Thu, 7 Jan 2016 16:01:17 -0500
Subject: PointFormats: addition produces points on curve

---
 src/Curves/PointFormats.v | 56 +++++++++++++++++++++++++++++++++--------------
 1 file changed, 39 insertions(+), 17 deletions(-)

(limited to 'src')

diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index cae6f939d..11b048cf4 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -133,34 +133,56 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     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. refine (
-    let 'exist P1' pf1 := P1 in
-    let 'exist P2' pf2 := P2 in
-    mkPoint (unifiedAdd' P1' P2') _).
+  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 *) 
-    destruct P1' as [x1 y1], P2' as [x2 y2].
-    remember (unifiedAdd' (x1, y1) (x2, y2)) as P3.
-    destruct P3 as [x3 y3]. injection HeqP3; clear HeqP3; intros.
-    unfold unifiedAdd', onCurve in *.
+    (* 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 rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
+
     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).
+      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 (T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
-    assert (T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +(
+    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 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
-    (* change all fractions to a common denominator and merge. That fraction will be T/T based on the hypotheses. Which is 1. *)
-    admit.
-  Defined.
+
+    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; try field.
+
+    rewrite <-HT1, <-HT2; field; rewrite HT1.
+
+    (* denominators are not zero, I promise *)
+  Admitted.
+
+  Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 ->
+    onCurve (unifiedAdd' P1 P2).
+  Proof.
+    intros; destruct P1, P2.
+    remember (unifiedAdd' (g, g0) (g1, g2)) as p; destruct p.
+    eapply unifiedAdd'_onCurve; eauto.
+  Qed.
+
+  Definition unifiedAdd (P1 P2 : point) : point :=
+    let 'exist P1' pf1 := P1 in
+    let 'exist P2' pf2 := P2 in
+    mkPoint (unifiedAdd' P1' P2') (unifiedAdd'_onCurve' _ _ pf1 pf2).
   Local Infix "+" := unifiedAdd.
 
   Fixpoint scalarMult (n:nat) (P : point) : point :=
-- 
cgit v1.2.3


From 533f5480932761073b9e55874d45d1c51825cfbb Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Fri, 8 Jan 2016 02:47:06 -0500
Subject: PointFormats: no zero denominators in Edwards addition

---
 src/Curves/PointFormats.v | 171 ++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 142 insertions(+), 29 deletions(-)

(limited to 'src')

diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 11b048cf4..4eb5a9ea5 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -3,16 +3,14 @@ Require Import Tactics.VerdiTactics.
 Require Import Logic.Eqdep_dec.
 Require Import BinNums NArith.
 
-Module GaloisDefs (M : Modulus).
-  Module Export GT := GaloisTheory M.
-End GaloisDefs.
-
 Module Type TwistedEdwardsParams (M : Modulus).
   Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
+  Axiom char_gt_2 : (1+1) <> 0.
   Parameter a : GF.
   Axiom a_nonzero : a <> 0.
-  Axiom a_square : exists x, x * x = a.
+  Parameter sqrt_a : GF.
+  Axiom a_square : sqrt_a^2 = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End TwistedEdwardsParams.
@@ -116,6 +114,119 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Definition point := { P | onCurve P}.
   Definition mkPoint := exist onCurve.
 
+  Lemma GFdecidable_neq : forall x y : GF, Zbool.Zeq_bool x y = false -> x <> y.
+  Proof.
+    intros. intro. rewrite GFcomplete in H; intuition.
+  Qed.
+
+  Ltac case_eq_GF a b :=
+    case_eq (Zbool.Zeq_bool a b); intro Hx;
+    match type of Hx with
+    | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = true =>
+        pose proof (GFdecidable a b Hx)
+    | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = false =>
+        pose proof (GFdecidable_neq a b Hx)
+    end; clear Hx.
+
+  Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
+  Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
+
+  (* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *)
+  (* c=1 and an extra a in front of x^2 *) 
+
+  Lemma onCurveDenominatorOk' x1 y1 x2 y2 :
+    onCurve (x1,y1) ->
+    onCurve (x2, y2) ->
+    (d*x1*x2*y1*y2)^2 <> 1.
+  Proof.
+    unfold onCurve; intros. intro.
+    (* TODO: lemma+tactic to inspect a*b*c*d*e<>0 *)
+    case_eq_GF x1 0%GF; [admit|].
+    case_eq_GF y1 0%GF; [admit|].
+    case_eq_GF x2 0%GF; [admit|].
+    case_eq_GF y2 0%GF; [admit|].
+
+    (* Furthermore... *)
+    pose proof  (eq_refl (d*x1^2*y1^2*(a*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.
+    rewrite H1 in Heqt.
+    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.
+      (* TODO: lemma+tactic to inspect a*b*c*d*e=0 *)
+      admit.
+
+    - 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.
+  Qed.
+  
+  Lemma onCurveDenominatorOkPlus x1 y1 x2 y2 :
+    onCurve (x1,y1) ->
+    onCurve (x2, y2) ->
+    (1 + d*x1*x2*y1*y2) <> 0.
+  Proof.
+    unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF.
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (onCurveDenominatorOk' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H1 by field.
+      intro; rewrite H2 in H1; intuition.
+  Qed.
+  
+  Lemma onCurveDenominatorOkMinus x1 y1 x2 y2 :
+    onCurve (x1,y1) ->
+    onCurve (x2, y2) ->
+    (1 - d*x1*x2*y1*y2) <> 0.
+  Proof.
+    unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF.
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (onCurveDenominatorOk' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H1 by field.
+      intro; rewrite H2 in H1; apply H1; field.
+  Qed.
+  Hint Resolve onCurveDenominatorOkPlus onCurveDenominatorOkMinus.
+
   Definition projX (P:point) := fst (proj1_sig P).
   Definition projY (P:point) := snd (proj1_sig P).
 
@@ -141,8 +252,6 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
       * c=1 and an extra a in front of x^2 *) 
     unfold unifiedAdd', onCurve in *; injection H; clear H; intros.
 
-    Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
-
     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);
@@ -164,12 +273,20 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     ((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; try field.
+    ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto.
 
     rewrite <-HT1, <-HT2; field; rewrite HT1.
 
-    (* denominators are not zero, I promise *)
-  Admitted.
+    - 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.
+      admit.
+
+    - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
+         with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
+           by field.
+      admit.
+  Qed.
 
   Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 ->
     onCurve (unifiedAdd' P1 P2).
@@ -263,11 +380,13 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
     (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
   Admitted.
 
-  Lemma zeroIsIdentity' : forall P, unifiedAdd' P  zero = P.
-  Admitted.
-  Hint Resolve zeroIsIdentity.
+  Lemma zeroIsIdentity' : forall P, unifiedAdd' P (proj1_sig zero) = P.
+    unfold unifiedAdd', zero; simpl; intros; break_let; f_equal; field;
+    assert (1 <> 0) by admit; auto.
+  Qed.
 
   Lemma zeroIsIdentity : forall P, P + zero = P.
+    (* Should follow from zeroIsIdentity', but dependent types... *)
   Admitted.
   Hint Resolve zeroIsIdentity.
 
@@ -399,11 +518,13 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
 End CompleteTwistedEdwardsFacts.
 
 Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
-  Module Export GFDefs := GaloisDefs M.
+  Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
+  Axiom char_gt_2 : (1+1) <> 0.
   Definition a := inject (- 1).
   Axiom a_nonzero : a <> 0.
-  Axiom a_square : exists x, x * x = a.
+  Parameter sqrt_a : GF.
+  Axiom a_square : sqrt_a^2 = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End Minus1Params.
@@ -428,7 +549,10 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
   Hint Unfold projectiveToTwisted twistedToProjective.
 
   Lemma GFdiv_1 : forall x, x/1 = x.
-  Admitted.
+  Proof.
+    intros; field.
+    assert (1 <> 0) by admit; auto.
+  Qed.
   Hint Resolve GFdiv_1.
 
   Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P.
@@ -536,19 +660,8 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
     unfold extendedValid, extendedToProjective, projectiveToTwisted in *.
     invcs HeqP3.
     subst.
-    (* field. -- fails. but it works in sage:
-sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2");
-print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
-((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) ==
-((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
-(2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) /
-((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-(2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))'
-      Outputs:
-        True
-    *)
+    field.
+    (* TODO: prove that denominators are nonzero *)
   Admitted.
 
   Ltac extended0 := repeat progress (autounfold; simpl); intros;
-- 
cgit v1.2.3


From bb4c8e7d281279eb9aeb44c5d0de5be1d022028c Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Fri, 8 Jan 2016 13:52:27 -0500
Subject: PointFormats: factor out admits

---
 src/Curves/PointFormats.v | 87 +++++++++++++++++++++++++++++------------------
 src/Galois/Galois.v       |  7 ++++
 2 files changed, 60 insertions(+), 34 deletions(-)

(limited to 'src')

diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 4eb5a9ea5..7e1fd0f81 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -134,17 +134,46 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   (* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *)
   (* c=1 and an extra a in front of x^2 *) 
 
-  Lemma onCurveDenominatorOk' x1 y1 x2 y2 :
+  Lemma root_zero : forall x p, x^p = 0 -> x = 0.
+  Admitted.
+  Lemma root_nonzero : forall x p, x^p <> 0 -> x <> 0.
+  Admitted.
+  Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
+  Admitted.
+  Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
+  Admitted.
+  Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
+  Admitted.
+  Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
+  Admitted.
+  Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
+  Admitted.
+
+  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)
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        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)
+    | [H: (?a*?b)%GF <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (a <> 0) by (eapply mul_nonzero_l; eauto)
+    | [H: (?a*?b)%GF <> 0 |- _ ] =>
+        match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (b <> 0) by (eapply mul_nonzero_r; eauto)
+    end.
+
+  Lemma edwardsAddComplete' x1 y1 x2 y2 :
     onCurve (x1,y1) ->
     onCurve (x2, y2) ->
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
-    unfold onCurve; intros. intro.
-    (* TODO: lemma+tactic to inspect a*b*c*d*e<>0 *)
-    case_eq_GF x1 0%GF; [admit|].
-    case_eq_GF y1 0%GF; [admit|].
-    case_eq_GF x2 0%GF; [admit|].
-    case_eq_GF y2 0%GF; [admit|].
+    unfold onCurve; intuition; whatsNotZero.
 
     (* Furthermore... *)
     pose proof  (eq_refl (d*x1^2*y1^2*(a*x2^2 + y2^2))) as Heqt.
@@ -162,8 +191,12 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     - 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.
-      (* TODO: lemma+tactic to inspect a*b*c*d*e=0 *)
-      admit.
+
+      (* 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.
@@ -204,28 +237,28 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
       edestruct d_nonsquare; eauto.
   Qed.
   
-  Lemma onCurveDenominatorOkPlus x1 y1 x2 y2 :
+  Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
     onCurve (x1,y1) ->
     onCurve (x2, y2) ->
     (1 + d*x1*x2*y1*y2) <> 0.
   Proof.
     unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF.
-    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (onCurveDenominatorOk' x1 y1 x2 y2); auto.
+    - 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 H1 by field.
       intro; rewrite H2 in H1; intuition.
   Qed.
   
-  Lemma onCurveDenominatorOkMinus x1 y1 x2 y2 :
+  Lemma edwardsAddCompletePlusMinus x1 y1 x2 y2 :
     onCurve (x1,y1) ->
     onCurve (x2, y2) ->
     (1 - d*x1*x2*y1*y2) <> 0.
   Proof.
     unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF.
-    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (onCurveDenominatorOk' x1 y1 x2 y2); auto.
+    - 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 H1 by field.
       intro; rewrite H2 in H1; apply H1; field.
   Qed.
-  Hint Resolve onCurveDenominatorOkPlus onCurveDenominatorOkMinus.
+  Hint Resolve edwardsAddCompletePlus edwardsAddCompletePlusMinus.
 
   Definition projX (P:point) := fst (proj1_sig P).
   Definition projY (P:point) := snd (proj1_sig P).
@@ -280,12 +313,12 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     - 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.
-      admit.
+      repeat apply mul_nonzero_nonzero; auto.
 
     - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
          with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
            by field.
-      admit.
+      repeat apply mul_nonzero_nonzero; auto.
   Qed.
 
   Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 ->
@@ -338,18 +371,6 @@ End CompleteTwistedEdwardsPointFormat.
 Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M).
   Local Open Scope GF_scope.
   Module Import Curve := CompleteTwistedEdwardsCurve M P.
-  Lemma twistedAddCompletePlus : forall (P1 P2:point),
-    let '(x1, y1) := proj1_sig P1 in
-    let '(x2, y2) := proj1_sig P2 in
-    (1 + d*x1*x2*y1*y2) <> 0.
-    (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
-  Admitted.
-  Lemma twistedAddCompleteMinus : forall (P1 P2:point),
-    let '(x1, y1) := proj1_sig P1 in
-    let '(x2, y2) := proj1_sig P2 in
-    (1 - d*x1*x2*y1*y2) <> 0.
-    (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
-  Admitted.
 
   Lemma point_eq : forall x1 x2 y1 y2,
     x1 = x2 -> y1 = y2 ->
@@ -358,7 +379,7 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
   Proof.
     intros; subst; f_equal.
     apply (UIP_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. *)
-    admit. (* GF_eq_dec *)
+    apply GF_eq_dec.
   Qed.
   Hint Resolve point_eq.
 
@@ -381,8 +402,7 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
   Admitted.
 
   Lemma zeroIsIdentity' : forall P, unifiedAdd' P (proj1_sig zero) = P.
-    unfold unifiedAdd', zero; simpl; intros; break_let; f_equal; field;
-    assert (1 <> 0) by admit; auto.
+    unfold unifiedAdd', zero; simpl; intros; break_let; f_equal; field; auto.
   Qed.
 
   Lemma zeroIsIdentity : forall P, P + zero = P.
@@ -550,14 +570,13 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
 
   Lemma GFdiv_1 : forall x, x/1 = x.
   Proof.
-    intros; field.
-    assert (1 <> 0) by admit; auto.
+    intros; field; auto.
   Qed.
   Hint Resolve GFdiv_1.
 
   Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P.
   Proof.
-    twisted; eapply GFdiv_1.
+    twisted; eauto.
   Qed.
 
   (** [extended] represents a point on an elliptic curve using extended projective
diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v
index 3ee86e4e4..4fd151d36 100644
--- a/src/Galois/Galois.v
+++ b/src/Galois/Galois.v
@@ -53,6 +53,13 @@ Module Galois (M: Modulus).
               apply prime_ge_2 in p; intuition).
   Defined.
 
+  Lemma GFone_nonzero : GFone <> GFzero.
+  Proof.
+    unfold GFone, GFzero.
+    intuition; solve_by_inversion.
+  Qed.
+  Hint Resolve GFone_nonzero.
+
   Definition GFplus(x y: GF): GF.
     exists ((x + y) mod modulus);
     abstract (rewrite Zmod_mod; trivial).
-- 
cgit v1.2.3


From f4425e8a1de9cff978f794e4783eff1bcfede412 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Fri, 8 Jan 2016 20:09:52 -0500
Subject: cleanup

---
 src/Curves/Curve25519.v   |   7 ++-
 src/Curves/PointFormats.v | 135 +++++++++++++++-------------------------------
 src/Galois/EdDSA.v        |   6 ++-
 3 files changed, 53 insertions(+), 95 deletions(-)

(limited to 'src')

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index 8bb2148db..4162d4c1c 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -1,5 +1,6 @@
 Require Import Zpower ZArith Znumtheory.
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
+Require Import Crypto.Galois.ZGaloisField.
 Require Import Crypto.Curves.PointFormats.
 
 Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *)
@@ -9,7 +10,11 @@ Module Modulus25519 <: Modulus.
 End Modulus25519.
 
 Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
-  Module Import GFDefs := GaloisDefs Modulus25519.
+  Module Import GFDefs := ZGaloisField Modulus25519.
+
+  Lemma char_gt_2 : inject 2 <> 0%GF.
+  Admitted.
+
   Local Open Scope GF_scope.
   Coercion inject : Z >-> GF.
 
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 7e1fd0f81..32e6acdd0 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -6,11 +6,10 @@ Require Import BinNums NArith.
 Module Type TwistedEdwardsParams (M : Modulus).
   Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
-  Axiom char_gt_2 : (1+1) <> 0.
+  Axiom char_gt_2 : inject 2 <> 0.
   Parameter a : GF.
   Axiom a_nonzero : a <> 0.
-  Parameter sqrt_a : GF.
-  Axiom a_square : sqrt_a^2 = a.
+  Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End TwistedEdwardsParams.
@@ -148,6 +147,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Admitted.
   Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
   Admitted.
+  Hint Resolve mul_nonzero_nonzero.
 
   Ltac whatsNotZero :=
     repeat match goal with
@@ -175,8 +175,12 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Proof.
     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 *.
+
     (* 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.
@@ -184,57 +188,29 @@ 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).
+    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; field.
   Qed.
   
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
@@ -290,8 +266,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.
@@ -299,7 +274,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
@@ -307,18 +281,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 ->
@@ -540,11 +509,10 @@ End CompleteTwistedEdwardsFacts.
 Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
   Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
-  Axiom char_gt_2 : (1+1) <> 0.
+  Axiom char_gt_2 : inject 2 <> 0.
   Definition a := inject (- 1).
   Axiom a_nonzero : a <> 0.
-  Parameter sqrt_a : GF.
-  Axiom a_square : sqrt_a^2 = a.
+  Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End Minus1Params.
@@ -586,13 +554,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).
@@ -639,21 +601,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
@@ -676,9 +629,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/Galois/EdDSA.v b/src/Galois/EdDSA.v
index af4f892ca..de26c678c 100644
--- a/src/Galois/EdDSA.v
+++ b/src/Galois/EdDSA.v
@@ -1,7 +1,7 @@
 Require Import ZArith NPeano.
 Require Import Bedrock.Word.
 Require Import Crypto.Curves.PointFormats.
-Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
+Require Import Crypto.Galois.BaseSystem Crypto.Galois.ZGaloisField Crypto.Galois.GaloisTheory.
 Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import VerdiTactics.
 
@@ -54,7 +54,7 @@ Module Type EdDSAParams.
   Axiom n_ge_c : n >= c.
   Axiom n_le_b : n <= b.
 
-  Module Import GFDefs := GaloisDefs Modulus_q.
+  Module Import GFDefs := ZGaloisField Modulus_q.
   Local Open Scope GF_scope.
 
   (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit
@@ -83,6 +83,8 @@ Module Type EdDSAParams.
    *   twisted Edwards addition law. *)
   Module CurveParameters <: TwistedEdwardsParams Modulus_q.
     Module GFDefs := GFDefs.
+    Definition char_gt_2 : inject 2 <> 0.
+    Admitted. (* follows from q_odd *)
     Definition a : GF := a.
     Definition a_nonzero := a_nonzero.
     Definition a_square := a_square.
-- 
cgit v1.2.3