EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and the sign bit of x, then solves the curve equation for x ^ 2. Required adding several lemmas to GaloisField (and moving others there from PointFormats).

2 files changed, 177 insertions, 16 deletions

diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v
index d87e35dc4..f3c769e67 100644
--- a/src/Galois/GaloisField.v
+++ b/src/Galois/GaloisField.v
@@ -116,4 +116,128 @@ Module GaloisField (M: Modulus).
      div GFmorph_div_theory,
      power_tac GFpower_theory [GFexp_tac]). 
 
+  Local Open Scope GF_scope.
+
+  Lemma GF_mul_eq : forall x y z, z <> 0 -> x * z = y * z -> x = y.
+  Proof.
+    intros ? ? ? z_nonzero mul_z_eq.
+    replace x with (x * 1) by field.
+    rewrite <- (GF_multiplicative_inverse z_nonzero).
+    replace (x * (GFinv z * z)) with ((x * z) * GFinv z) by ring.
+    rewrite mul_z_eq.
+    replace (y * z * GFinv z) with (y * (GFinv z * z)) by ring.
+    rewrite GF_multiplicative_inverse; auto; field.
+  Qed.
+
+  Lemma GF_mul_0_l : forall x, 0 * x = 0.
+  Proof.
+    intros; field.
+  Qed.
+
+  Lemma GF_mul_0_r : forall x, x * 0 = 0.
+  Proof.
+    intros; field.
+  Qed.
+
+  Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
+    intros.
+    assert (H := Z.eq_dec (inject x) (inject y)).
+
+    destruct H.
+    
+    - left; galois; intuition.
+
+    - right; intuition.
+      rewrite H in n.
+      assert (y = y); intuition.
+  Qed.
+
+    Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
+    intros; intuition; subst.
+    assert (0 * b = 0) by field; intuition.
+  Qed.
+
+  Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
+    intros; intuition; subst.
+    assert (a * 0 = 0) by field; intuition.
+  Qed.
+
+  Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
+    intros.
+    assert (Z := GF_eq_dec a 0); destruct Z.
+
+    - left; intuition.
+
+    - assert (a * b / a = 0) by
+        ( rewrite H; field; intuition ).
+
+      field_simplify in H0.
+      replace (b/1) with b in H0 by (field; intuition).
+      right; intuition.
+      apply n in H0; intuition.
+  Qed.
+
+  Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
+    intros; intuition; subst.
+    apply mul_zero_why in H1.
+    destruct H1; subst; intuition.
+  Qed.
+  Hint Resolve mul_nonzero_nonzero.
+
+  Lemma GFexp_distr_mul : forall x y z, (0 <= z)%N ->
+    (x ^ z) * (y ^ z) = (x * y) ^ z.
+  Proof.
+    intros.
+    replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
+    apply natlike_ind with (x := Z.of_N z); simpl; [ field | | 
+      replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
+    intros z' z'_nonneg IHz'.
+    rewrite Z2N.inj_succ by auto.
+    rewrite (GFexp_pred x) by apply N.neq_succ_0.
+    rewrite (GFexp_pred y) by apply N.neq_succ_0.
+    rewrite (GFexp_pred (x * y)) by apply N.neq_succ_0.
+    rewrite N.pred_succ.
+    rewrite <- IHz'.
+    field.
+  Qed.
+
+  Lemma GF_square_mul : forall x y z, (y <> 0) ->
+    x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
+  Proof.
+    intros ? ? ? y_nonzero A.
+    exists (x / y).
+    assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div. {
+      unfold GFdiv, GFexp, GFexp'.
+      replace (GFinv (y * y)) with (GFinv y * GFinv y); try ring.
+      unfold GFinv.
+      destruct (N.eq_dec (N.pred (totientToN totient)) 0) as [ eq_zero | neq_zero ];
+        [ rewrite eq_zero | rewrite GFexp_distr_mul ]; try field.
+      simpl.
+      do 2 rewrite <- Z2N.inj_pred.
+      replace 0%N with (Z.to_N 0%Z) by auto.
+      apply Z2N.inj_le; modulus_bound.
+    }
+    assert (y ^ 2 <> 0) as y2_nonzero by (apply mul_nonzero_nonzero; auto).
+    rewrite (GF_mul_eq _ z (y ^ 2)); auto.
+    unfold GFdiv.
+    rewrite <- A.
+    field; auto.
+  Qed.
+
+  Lemma sqrt_solutions : forall x y, y ^ 2 = x ^ 2 -> y = x \/ y = GFopp x.
+  Proof.
+    intros.
+    (* TODO(jadep) *)
+  Admitted.
+
+  Lemma GFopp_swap : forall x y, GFopp x = y <-> x = GFopp y.
+  Proof.
+    split; intro; subst; field.
+  Qed.
+
+  Lemma GFopp_involutive : forall x, GFopp (GFopp x) = x.
+  Proof.
+    intros; field.
+  Qed.
+
 End GaloisField.
diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v
index 6bf0621eb..feb37007a 100644
--- a/src/Galois/GaloisTheory.v
+++ b/src/Galois/GaloisTheory.v
@@ -246,22 +246,20 @@ Module GaloisTheory (M: Modulus).
   Qed.
 
   Lemma GFexp'_pred : forall x p,
-    p <> 0
-    -> x <> 1%positive
+    x <> 1%positive
     -> GFexp' p x = GFexp' p (Pos.pred x) * p.
   Proof.
     intros; rewrite <- (Pos.succ_pred x) at 1; auto using GFexp'_pred'.
   Qed.
 
-  Lemma GFexp_pred : forall p x,
-    p <> 0
-    -> x <> 0%N
+  Lemma GFexp_pred : forall x p,
+    x <> 0%N
     -> p^x = p^N.pred x * p.
   Proof.
     destruct x; simpl; intuition.
-    destruct (Pos.eq_dec p0 1); subst; simpl; try ring.
+    destruct (Pos.eq_dec p 1); subst; simpl; try ring.
     rewrite GFexp'_pred by auto.
-    destruct p0; intuition.
+    destruct p; intuition.
   Qed.
 
   (* Show that GFinv actually defines multiplicative inverses *)
@@ -301,11 +299,16 @@ Module GaloisTheory (M: Modulus).
   Ltac modulus_bound :=
     pose proof (prime_ge_2 (primeToZ modulus) (proj2_sig modulus)); omega.
 
-  Lemma GFexp_Zpow : forall (a : GF) (a_nonzero : a <> 0)
+  Lemma GFToZ_inject : forall x, GFToZ (inject x) = (x mod primeToZ modulus)%Z.
+  Proof.
+    intros; unfold GFToZ, proj1_sig, inject; reflexivity.
+  Qed.
+
+  Lemma GFexp_Zpow : forall (a : GF)
     (k : Z) (k_nonneg : (0 <= k)%Z),
     a ^ (Z.to_N k) = ((GFToZ a) ^ k)%Z.
   Proof.
-    intros a a_nonzero.
+    intro a.
     apply natlike_ind; [ galois; symmetry; apply Z.mod_small; modulus_bound | ].
     intros k k_nonneg IHk.
     rewrite Z2N.inj_succ by auto.
@@ -316,11 +319,6 @@ Module GaloisTheory (M: Modulus).
     galois.
   Qed.
 
-  Lemma GFToZ_inject : forall x, GFToZ (inject x) = (x mod primeToZ modulus)%Z.
-  Proof.
-    intros; unfold GFToZ, proj1_sig, inject; reflexivity.
-  Qed.
-
   Lemma GF_Zmod : forall x, ((GFToZ x) mod primeToZ modulus = GFToZ x)%Z.
   Proof.
     intros.
@@ -350,9 +348,32 @@ Module GaloisTheory (M: Modulus).
     }
   Qed.
 
-  Lemma GFexp_0 : forall e : N, e <> 0%N -> 0 ^ e = 0.
+  Lemma inject_Zmod : forall x y, inject x = inject y <-> (x mod primeToZ modulus = y mod primeToZ modulus)%Z.
   Proof.
-  Admitted.
+    split; intros A.
+    + apply gf_eq in A.
+      do 2 rewrite GFToZ_inject in A; auto.
+    + rewrite (inject_mod_eq x).
+      rewrite (inject_mod_eq y).
+      rewrite A; auto.
+  Qed.
+
+  Lemma GFexp_0 : forall e : N, (0 < e)%N -> 0 ^ e = 0.
+  Proof.
+    intros.
+    replace e with (Z.to_N (Z.of_N e)) by apply N2Z.id.
+    replace e with (N.succ (N.pred e)) by (apply N.succ_pred_pos; auto).
+    rewrite N2Z.inj_succ.
+    apply natlike_ind with (x := Z.of_N (N.pred e)); try reflexivity.
+    + intros x x_pos IHx.
+      rewrite Z2N.inj_succ by omega.
+      rewrite GFexp_pred by apply N.neq_succ_0. 
+      rewrite N.pred_succ.
+      rewrite IHx; ring.
+    + replace 0%Z with (Z.of_N 0%N) by auto.
+      rewrite <- N2Z.inj_le.
+      apply N.lt_le_pred; auto.
+  Qed.
 
   Lemma nonzero_Zmod_GF : forall a,
     (inject a <> 0) <-> (a mod primeToZ modulus <> 0)%Z.
@@ -384,4 +405,20 @@ Module GaloisTheory (M: Modulus).
    omega.
   Qed.
 
+  Lemma GF_mod_bound : forall (x : GF), (0 <= x < modulus)%Z.
+  Proof.
+    intros.
+    assert (0 < modulus)%Z as gt_0_modulus by modulus_bound.
+    pose proof (Z.mod_pos_bound x modulus gt_0_modulus).
+    rewrite <- (inject_eq x).
+    unfold GFToZ, inject in *.
+    auto.
+  Qed.
+
+  Lemma GF_minus_plus : forall x y z, x + y = z <-> x = z - y.
+  Proof.
+    split; intros A; [ symmetry in A | ]; rewrite A; ring.
+  Qed.
+
+
 End GaloisTheory.
\ No newline at end of file