From 841cc2fa3ed0cb3a8b795097574399ae5083c9a6 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Thu, 4 Apr 2024 02:13:28 -0400
Subject: [PATCH] decide point equality (#1848)

---
 src/Curves/Edwards/AffineProofs.v   |  2 ++
 src/Curves/EdwardsMontgomery25519.v | 34 ++++++++++++++++++-----------
 src/Curves/Montgomery/Affine.v      |  2 ++
 src/Spec/Curve25519.v               |  2 +-
 src/Util/Decidable.v                | 10 +++++++++
 5 files changed, 36 insertions(+), 14 deletions(-)

diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v
index e0647c266d..255d5e0a62 100644
--- a/src/Curves/Edwards/AffineProofs.v
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -46,6 +46,8 @@ Module E.
     Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)).
     Next Obligation. match goal with P : point |- _ => destruct P as [ [??]?] end; cbv; fsatz. Qed.
 
+    Global Instance Decidable_eq : Decidable.DecidableRel (@E.eq _ Feq Fone Fadd Fmul a d) := _.
+
     Ltac t_step :=
       match goal with
       | _ => solve [trivial | exact _ ]
diff --git a/src/Curves/EdwardsMontgomery25519.v b/src/Curves/EdwardsMontgomery25519.v
index d418218077..b5b1d7b5a6 100644
--- a/src/Curves/EdwardsMontgomery25519.v
+++ b/src/Curves/EdwardsMontgomery25519.v
@@ -1,4 +1,5 @@
 Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Spec.ModularArithmetic. Local Open Scope F_scope.
 Require Import Crypto.Curves.EdwardsMontgomery. Import M.
 Require Import Crypto.Curves.Edwards.TwistIsomorphism.
@@ -11,19 +12,26 @@ Import MontgomeryCurve CompleteEdwardsCurve.
 
 Local Definition a' := (M.a + (1 + 1)) / M.b.
 Local Definition d' := (M.a - (1 + 1)) / M.b.
-Definition r := sqrt (F.inv ((a' / M.b) / E.a)).
+Local Definition r := sqrt (F.inv ((a' / M.b) / E.a)).
 
-Local Lemma is_twist : E.a * d' = a' * E.d. Proof. Decidable.vm_decide. Qed.
-Local Lemma nonzero_a' : a' <> 0. Proof. Decidable.vm_decide. Qed.
-Local Lemma r_correct : E.a = r * r * a'. Proof. Decidable.vm_decide. Qed.
+Local Lemma is_twist : E.a * d' = a' * E.d. Proof. vm_decide. Qed.
+Local Lemma nonzero_a' : a' <> 0. Proof. vm_decide. Qed.
+Local Lemma r_correct : E.a = r * r * a'. Proof. vm_decide. Qed.
 
-Definition Montgomery_of_Edwards (P : Curve25519.E.point) : Curve25519.M.point :=
-  @of_Edwards _ _ _ _ _  _ _ _ _ _ field _ char_ge_3 M.a M.b M.b_nonzero a' d' eq_refl eq_refl nonzero_a'
-    (@E.point2_of_point1 _ _ _ _ _ _ _ _ _ _ field _ E.a E.d a' d' is_twist E.nonzero_a nonzero_a' r r_correct P).
-
-Definition Edwards_of_Montgomery (P : Curve25519.M.point) : Curve25519.E.point :=
+Module E.
+Definition of_Montgomery (P : Curve25519.M.point) : Curve25519.E.point :=
  @E.point1_of_point2 _ _ _ _ _ _ _ _ _ _ field _ E.a E.d a' d' is_twist E.nonzero_a nonzero_a' r r_correct
    (@to_Edwards _ _ _ _ _ _ _ _ _ _ field _ M.a M.b M.b_nonzero a' d' eq_refl eq_refl nonzero_a' P).
+Lemma of_Montgomery_B : E.eq E.B (of_Montgomery M.B). Proof. vm_decide. Qed.
+End E.
+
+Module M.
+Definition of_Edwards (P : Curve25519.E.point) : Curve25519.M.point :=
+  @of_Edwards _ _ _ _ _  _ _ _ _ _ field _ char_ge_3 M.a M.b M.b_nonzero a' d' eq_refl eq_refl nonzero_a'
+    (@E.point2_of_point1 _ _ _ _ _ _ _ _ _ _ field _ E.a E.d a' d' is_twist E.nonzero_a nonzero_a' r r_correct P).
+Lemma of_Edwards_B : M.eq M.B (of_Edwards E.B). Proof.
+Proof. simple notypeclasses refine (@dec_bool _ _ _). apply Affine.M.Decidable_eq. vm_decide. Qed.
+End M.
 
 Local Notation Eopp := ((@AffineProofs.E.opp _ _ _ _ _ _ _ _ _ _ field _ E.a E.d E.nonzero_a)).
 
@@ -36,9 +44,9 @@ Local Arguments of_Edwards {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _} _ _ { _ _ _ }.
 Lemma EdwardsMontgomery25519 : @Group.isomorphic_commutative_groups
        Curve25519.E.point E.eq Curve25519.E.add Curve25519.E.zero Eopp Curve25519.M.point
        M.eq Curve25519.M.add M.zero Curve25519.M.opp
-       Montgomery_of_Edwards Edwards_of_Montgomery.
+       M.of_Edwards E.of_Montgomery.
 Proof.
-  cbv [Montgomery_of_Edwards Edwards_of_Montgomery].
+  cbv [M.of_Edwards E.of_Montgomery].
   epose proof E.twist_isomorphism(a1:=E.a)(a2:=a')(d1:=E.d)(d2:=d')(r:=r) as AB.
   epose proof EdwardsMontgomeryIsomorphism(a:=Curve25519.M.a)(b:=Curve25519.M.b)as BC.
   destruct AB as [A B ab ba], BC as [_ C bc cb].
@@ -46,6 +54,6 @@ Proof.
   pose proof Group.compose_homomorphism(homom:=cb)(homom2:=ba)(groupH2:=ltac:(eapply A)) as ca.
   split; try exact ac; try exact ca; try exact A; try exact C.
   Unshelve.
-  all : try (pose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide).
-  all : try (eapply Hierarchy.char_ge_weaken; try apply ModularArithmeticTheorems.F.char_gt; Decidable.vm_decide).
+  all : try (pose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); vm_decide).
+  all : try (eapply Hierarchy.char_ge_weaken; try apply ModularArithmeticTheorems.F.char_gt; vm_decide).
 Qed.
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index 0bcf46b6c3..c7c77a125f 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -31,6 +31,8 @@ Module M.
     Local Notation add := (M.add(b_nonzero:=b_nonzero)).
     Local Notation point := (@M.point F Feq Fadd Fmul a b).
 
+    Global Instance Decidable_eq : Decidable.DecidableRel (@M.eq _ Feq Fadd Fmul a b) := _.
+
     Section MontgomeryWeierstrass.
       Local Notation "2" := (1+1).
       Local Notation "3" := (1+2).
diff --git a/src/Spec/Curve25519.v b/src/Spec/Curve25519.v
index 2908a63c7a..9ee465b880 100644
--- a/src/Spec/Curve25519.v
+++ b/src/Spec/Curve25519.v
@@ -97,7 +97,7 @@ Module E.
     refine (
     exist _ (F.of_Z _ 15112221349535400772501151409588531511454012693041857206046113283949847762202, F.div (F.of_Z _ 4) (F.of_Z _ 5)) _).
     Decidable.vm_decide.
-  Qed.
+  Defined.
 End E.
 
 Require Import Spec.MontgomeryCurve.
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index 2353210d68..b2dc209706 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -136,12 +136,22 @@ Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B}
   : Decidable (let '(a, b) := x in P a b) | 1.
 Proof. edestruct (_ : _ * _); assumption. Defined.
 
+Global Instance dec_match_sum {A B} {P : A -> Prop} {Q : B -> Prop}
+       {HP : forall x, Decidable (P x)} {HQ : forall x, Decidable (Q x)}
+       {x : A + B}
+  : Decidable (match x with inl a => P a | inr b => Q b end) | 1.
+Proof. edestruct (_ : _ + _); eauto. Defined.
+
 Global Instance dec_if_bool {b : bool} {A B} {HA : Decidable A} {HB : Decidable B}
   : Decidable (if b then A else B) | 10
   := if b return Decidable (if b then A else B)
      then HA
      else HB.
 
+Global Instance dec_match_unit {P} {HP : Decidable P} {x : unit}
+  : Decidable (match x with tt => P end) | 1.
+Proof. edestruct x. assumption. Defined.
+
 Lemma not_not P {d:Decidable P} : not (not P) <-> P.
 Proof. destruct (dec P); intuition. Qed.