From eb5ba0931359308f1df43d34d8a95e4df23b11a7 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Wed, 3 Apr 2024 16:27:10 -0400
Subject: [PATCH] instantiate Edwards-Montgomery isomorphism for Curve25519
 (#1847)

---
 src/Algebra/Group.v                 | 10 ++++++
 src/Curves/EdwardsMontgomery25519.v | 51 +++++++++++++++++++++++++++++
 src/Spec/Curve25519.v               | 10 ++++++
 3 files changed, 71 insertions(+)
 create mode 100644 src/Curves/EdwardsMontgomery25519.v

diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index ca4d76f59c..363099bf90 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -87,6 +87,16 @@ Section Homomorphism.
     apply inv_unique.
     rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity.
   Qed.
+
+  Lemma compose_homomorphism
+    {H2 eq2 op2 id2 inv2} {groupH2:@group H2 eq2 op2 id2 inv2}
+    {phi2:H->H2}`{homom2:@Monoid.is_homomorphism H eq op H2 eq2 op2 phi2}
+    : @Monoid.is_homomorphism G EQ OP H2 eq2 op2 (fun x => phi2 (phi x)).
+  Proof.
+    split; repeat intro.
+    { do 2 rewrite homomorphism. f_equiv. }
+    { f_equiv. f_equiv. trivial. }
+  Qed.
 End Homomorphism.
 
 Section GroupByIsomorphism.
diff --git a/src/Curves/EdwardsMontgomery25519.v b/src/Curves/EdwardsMontgomery25519.v
new file mode 100644
index 0000000000..d418218077
--- /dev/null
+++ b/src/Curves/EdwardsMontgomery25519.v
@@ -0,0 +1,51 @@
+Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+Require Import Crypto.Spec.ModularArithmetic. Local Open Scope F_scope.
+Require Import Crypto.Curves.EdwardsMontgomery. Import M.
+Require Import Crypto.Curves.Edwards.TwistIsomorphism.
+Require Import Crypto.Spec.Curve25519.
+
+Local Definition sqrtm1 : F p := F.pow (F.of_Z _ 2) ((N.pos p-1)/4).
+Local Definition sqrt := PrimeFieldTheorems.F.sqrt_5mod8 sqrtm1.
+
+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 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.
+
+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 :=
+ @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).
+
+Local Notation Eopp := ((@AffineProofs.E.opp _ _ _ _ _ _ _ _ _ _ field _ E.a E.d E.nonzero_a)).
+
+Local Arguments Hierarchy.commutative_group _ {_} _ {_ _}.
+Local Arguments CompleteEdwardsCurve.E.add {_ _ _ _ _ _ _ _ _ _ _ _ _} _ _ {_ _ _}.
+Local Arguments Monoid.is_homomorphism {_ _ _ _ _ _}.
+Local Arguments to_Edwards {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _} _ _ { _ _ _ }.
+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.
+Proof.
+  cbv [Montgomery_of_Edwards Edwards_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].
+  pose proof Group.compose_homomorphism(homom:=ab)(homom2:=bc) as ac.
+  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).
+Qed.
diff --git a/src/Spec/Curve25519.v b/src/Spec/Curve25519.v
index f8a7d55650..2908a63c7a 100644
--- a/src/Spec/Curve25519.v
+++ b/src/Spec/Curve25519.v
@@ -82,7 +82,17 @@ Require Import Spec.CompleteEdwardsCurve.
 Module E.
   Definition a : F := F.opp 1.
   Definition d : F := F.div (F.opp (F.of_Z _ 121665)) (F.of_Z _ 121666).
+
+  Lemma nonzero_a : a <> F.zero. Proof. Decidable.vm_decide. Qed.
+  Lemma square_a : exists sqrt_a, F.mul sqrt_a sqrt_a = a.
+  Proof. epose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide. Qed.
+  Lemma nonsquare_d : forall x, F.mul x x <> d.
+  Proof. epose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide. Qed.
+
   Definition point := @E.point F eq F.one F.add F.mul a d.
+  Definition add := E.add(field:=field)(char_ge_3:=char_ge_3)(a:=a)(d:=d)
+    (nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d).
+  Definition zero := E.zero(field:=field)(a:=a)(d:=d)(nonzero_a:=nonzero_a).
   Definition B : E.point.
     refine (
     exist _ (F.of_Z _ 15112221349535400772501151409588531511454012693041857206046113283949847762202, F.div (F.of_Z _ 4) (F.of_Z _ 5)) _).