point_eq_dec

4 files changed, 73 insertions, 12 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index d39f864da..2fdaff4a5 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -30,13 +30,76 @@ Section CompleteEdwardsCurveTheorems.
     generalize dependent q; intro q; intros;
     clear prm.
 
+  Lemma point_eq' : forall xy1 xy2 pf1 pf2,
+    xy1 = xy2 -> exist onCurve xy1 pf1 = exist onCurve xy2 pf2.
+  Proof.
+    destruct xy1, xy2; 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.
+
   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. *)
+    eauto using point_eq'.
+  Qed.
+  Hint Resolve point_eq' point_eq.
+
+  Definition point_eqb (p1 p2:point) : bool := andb
+      (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2)))
+      (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))).
+
+  Local Ltac t :=
+    unfold point_eqb;
+      repeat match goal with
+      | _ => progress intros
+      | _ => progress simpl in *
+      | _ => progress subst
+      | [P:point |- _ ] => destruct P
+      | [x: (F q * F q)%type |- _ ] => destruct x
+      | [H: _ /\ _ |- _ ] => destruct H
+      | [H: _ |- _ ] => rewrite Bool.andb_true_iff in H
+      | [H: _ |- _ ] => apply F_eqb_eq in H
+      | _ => rewrite F_eqb_refl
+      end; eauto.
+
+  Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2.
+  Proof.
+    t.
+  Qed.
+
+  Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true.
+  Proof.
+    t.
+  Qed.
+
+  Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2.
+  Proof.
+    intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
+    apply point_eqb_complete in H0; congruence.
+  Qed.
+
+  Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false.
+  Proof.
+    intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
+    apply point_eqb_sound in Hneq. congruence.
+  Qed.
+
+  Lemma point_eqb_refl : forall p, point_eqb p p = true.
+  Proof.
+    t.
+  Qed.
+
+  Definition point_eq_dec (p1 p2:point) : {p1 = p2} + {p1 <> p2}.
+    destruct (point_eqb p1 p2) eqn:H; match goal with
+                                      | [ H: _ |- _ ] => apply point_eqb_sound in H
+                                      | [ H: _ |- _ ] => apply point_eqb_neq in H
+                                      end; eauto.
+  Qed.
+
+  Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false.
+  Proof.
+    intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete.
   Qed.
-  Hint Resolve point_eq.
 
   Ltac Edefn := unfold unifiedAdd, unifiedAdd', zero; intros;
                   repeat match goal with
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index b7d2c0d8e..8dbfdf7b9 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -46,11 +46,8 @@ Section TwistedEdwardsCurves.
     | O => zero
     | S n' => unifiedAdd P (scalarMult n' P)
     end.
-
-  Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}.
 End TwistedEdwardsCurves.
 
 Delimit Scope E_scope with E.
 Infix "+" := unifiedAdd : E_scope.
-Infix "*" := scalarMult : E_scope.
-Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope.
+Infix "*" := scalarMult : E_scope.
\ No newline at end of file
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 3decae6a7..8a48f4dea 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -6,6 +6,7 @@ Require Import Crypto.Util.WordUtil.
 Require Bedrock.Word.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
+Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
 Coercion Word.wordToNat : Word.word >-> nat.
 
@@ -54,6 +55,8 @@ Section EdDSA.
   Notation secretkey := (Word.word b) (only parsing).
   Notation publickey := (Word.word b) (only parsing).
   Notation signature := (Word.word (b + b)) (only parsing).
+  Let point_eq_dec : forall P Q, {P = Q} + {P <> Q} := CompleteEdwardsCurveTheorems.point_eq_dec.
+  Local Infix "==" := point_eq_dec (at level 70) : E_scope .
 
   (* TODO: proofread curveKey and definition of n *)
   Definition curveKey (sk:secretkey) : nat :=
@@ -82,4 +85,4 @@ Section EdDSA.
     end
     end
     end%E.
-End EdDSA.
+End EdDSA.
\ No newline at end of file
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 50379b8d1..2bafd4c8a 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -7,6 +7,7 @@ Require Import ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Spec.CompleteEdwardsCurve.
 Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
+Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.Util.IterAssocOp.
 
 Local Infix "++" := Word.combine.
@@ -57,9 +58,6 @@ Proof.
            end. }
 Qed.
 
-Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool.
-Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false.
-
 Axiom xB : F q.
 Axiom yB : F q.
 Axiom B_proj : proj1_sig B = (xB, yB).
@@ -517,4 +515,4 @@ Proof.
        point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q].
     *)
   reflexivity.
-Admitted.
\ No newline at end of file
+Admitted.