port some edwards curve theorems

2 files changed, 238 insertions, 0 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
new file mode 100644
index 000000000..90f5907fd
--- /dev/null
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -0,0 +1,52 @@
+Require Export Crypto.Spec.CompleteEdwardsCurve.
+
+Require Import Crypto.CompleteEdwardsCurve.Pre.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Eqdep_dec.
+Require Import Crypto.Tactics.VerdiTactics.
+
+Section CompleteEdwardsCurveTheorems.
+  Context {prm:TwistedEdwardsParams}.
+  Existing Instance prime_q.
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [idtac],
+     postprocess [try exact Fq_1_neq_0; try assumption],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+
+  Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2,
+    mkPoint p1 pf1 = mkPoint p2 pf2.
+  Proof.
+    destruct p1, p2; intros; find_injection; intros; subst; apply f_equal.
+    apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) 
+  Qed.
+  Hint Resolve point_eq.
+
+  Ltac Edefn := unfold unifiedAdd, zero; intros;
+                  repeat match goal with
+                         | [ p : point |- _ ] =>
+                           let x := fresh "x" p in
+                           let y := fresh "y" p in
+                           let pf := fresh "pf" p in
+                           destruct p as [[x y] pf]; unfold onCurve in pf
+                  | _ => eapply point_eq, f_equal2
+                  | _ => eapply point_eq
+  end.
+  Lemma twistedAddComm : forall A B, (A+B = B+A)%E.
+  Proof.
+    Edefn; f_equal; field.
+  Qed.
+
+  Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C.
+  Proof.
+    (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
+  Admitted.
+
+  Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
+  Proof.
+    Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
+           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl.
+  Qed.
+End CompleteEdwardsCurveTheorems.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
new file mode 100644
index 000000000..e4dc140e1
--- /dev/null
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -0,0 +1,186 @@
+Require Import BinInt Znumtheory VerdiTactics.
+
+Require Import Crypto.Spec.ModularArithmetic.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Local Open Scope F_scope.
+  
+Section Pre.
+  Context {q : BinInt.Z}.
+  Context {a : F q}.
+  Context {d : F q}.
+  Context {prime_q : Znumtheory.prime q}.
+  Context {two_lt_q : 2 < q}.
+  Context {a_nonzero : a <> 0}.
+  Context {a_square : exists sqrt_a, sqrt_a^2 = a}.
+  Context {d_nonsquare : forall x, x^2 <> d}.
+
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+  
+  (* the canonical definitions are in Spec *)
+  Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
+  Local Notation unifiedAdd' P1' P2' := (
+    let '(x1, y1) := P1' in
+    let '(x2, y2) := P2' in
+    (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
+  ).
+  
+  Lemma char_gt_2 : ZToField 2 <> (0: F q).
+    intro; find_injection.
+    pose proof two_lt_q.
+    rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega.
+  Qed.
+
+  Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
+  Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
+  
+  Ltac whatsNotZero :=
+    repeat match goal with
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
+    | [H: (?a^?p)%F <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        let Y:=fresh in let Z:=fresh in try (
+          assert (p <> 0%N) as Z by (intro Y; inversion Y);
+          assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0);
+          clear Z)
+    | [H: (?a*?b)%F <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0)
+    | [H: (?a*?b)%F <> 0 |- _ ] =>
+        match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0)
+    end.
+
+  Lemma edwardsAddComplete' x1 y1 x2 y2 :
+    onCurve (x1, y1) ->
+    onCurve (x2, y2) ->
+    (d*x1*x2*y1*y2)^2 <> 1.
+  Proof.
+    intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
+  
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+    destruct a_square as [sqrt_a a_square'].
+    rewrite <-a_square' in *.
+  
+    (* Furthermore... *)
+    pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
+    rewrite Hc2 in Heqt at 2.
+    replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2))
+       with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field.
+    rewrite Hcontra in Heqt.
+    replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
+    rewrite <-Hc1 in Heqt.
+  
+    (* main equation for both potentially nonzero denominators *)
+    destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
+      try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
+        assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 =
+                 f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2)
+                   (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field;
+        rewrite Hcontra in Heqw1;
+        replace (1 * y1^2) with (y1^2) in * by field;
+        rewrite <- Heqt in *;
+        assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 /
+                                 (x1 * y1 * (f (sqrt_a * x2)  y2))^2)
+                                 by (rewriteAny; field; auto);
+        match goal with [H: d = (?n^2)/(?l^2) |- _ ] =>
+            destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
+        end
+      end.
+  
+    assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
+  
+    replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
+  
+    (* contradiction: product of nonzero things is zero *)
+    destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
+    destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
+    apply Ha_nonzero; field.
+  Qed.
+
+  Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
+    onCurve (x1, y1) ->
+    onCurve (x2, y2) ->
+    (1 + d*x1*x2*y1*y2) <> 0.
+  Proof.
+    intros Hc1 Hc2; simpl in Hc1, Hc2.
+    intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H].
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
+      intro Hz; rewrite Hz in H; intuition.
+  Qed.
+  
+  Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
+    onCurve (x1, y1) ->
+    onCurve (x2, y2) ->
+    (1 - d*x1*x2*y1*y2) <> 0.
+  Proof.
+    intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H].
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
+      intro Hz; rewrite Hz in H; apply H; field.
+  Qed.
+  
+  Definition zeroOnCurve : onCurve (0, 1).
+    simpl. field.
+  Qed.
+  
+  Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
+    (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
+    onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
+  Proof.
+    (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
+      * c=1 and an extra a in front of x^2 *) 
+  
+    injection H; clear H; intros.
+  
+    Ltac t x1 y1 x2 y2 :=
+      assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
+             = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
+      assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
+             = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
+    t x1 y1 x2 y2; t x2 y2 x1 y1.
+  
+    remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
+      (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
+    assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
+    assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +(
+    (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
+     y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
+    replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
+  
+    match goal with [ |- ?x = 1 ] => replace x with
+    ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
+     ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
+      d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
+    ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end.
+    - rewrite <-HT1, <-HT2; field; rewrite HT1.
+      replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
+      with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field.
+      auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
+        edwardsAddCompleteMinus, edwardsAddCompletePlus.
+    - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
+         with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
+           by field;
+      auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
+        edwardsAddCompleteMinus, edwardsAddCompletePlus.
+  Qed.
+  
+  Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
+    onCurve (unifiedAdd' P1 P2).
+  Proof.
+    intros; destruct P1, P2.
+    remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
+    eapply unifiedAdd'_onCurve'; eauto.
+  Qed.
+End Pre.
\ No newline at end of file