extended coordinates setoid boilerplate

1 files changed, 97 insertions, 3 deletions

diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 226600428..e918ac128 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -3,6 +3,9 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.FField.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Util.IterAssocOp BinNat NArith. 
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
+Local Open Scope equiv_scope.
 Local Open Scope F_scope.
 
 Section ExtendedCoordinates.
@@ -80,10 +83,43 @@ Section ExtendedCoordinates.
     solveExtended.
   Qed.
 
+  Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ onCurve (extendedToTwisted P) }.
+
+  Program Definition mkExtendedPoint : point -> extendedPoint := twistedToExtended.
+  Next Obligation.
+    destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
+  Qed.
+
+  Program Definition unExtendedPoint : extendedPoint -> point := extendedToTwisted.
+  Next Obligation.
+    destruct x; simpl; intuition.
+  Qed.
+
+  Definition extendedPoint_eq P Q := unExtendedPoint P = unExtendedPoint Q.
+  Global Instance Equivalence_extendedPoint_eq : Equivalence extendedPoint_eq.
+  Proof.
+    repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence.
+  Qed.
+
+  Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P.
+  Proof.
+    destruct P; eapply point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
+  Qed.
+
+  Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint.
+  Proof.
+    repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence.
+  Qed.
+
+  Global Instance Proper_unExtendedPoint : Proper (equiv==>eq) unExtendedPoint.
+  Proof.
+    repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence.
+  Qed.
+
   Section TwistMinus1.
     Context (a_eq_minus1 : a = opp 1).
     (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
-    Definition unifiedAddM1 (P1 P2 : extended) : extended :=
+    Definition unifiedAddM1' (P1 P2 : extended) : extended :=
       let '(X1, Y1, Z1, T1) := P1 in
       let '(X2, Y2, Z2, T2) := P2 in
       let  A := (Y1-X1)*(Y2-X2) in
@@ -101,8 +137,8 @@ Section ExtendedCoordinates.
       (X3, Y3, Z3, T3).
     Local Hint Unfold unifiedAdd.
 
-    Lemma unifiedAdd_repM1: forall P Q rP rQ, onCurve rP -> onCurve rQ ->
-      P ~= rP -> Q ~= rQ -> (unifiedAddM1 P Q) ~= (unifiedAdd' rP rQ).
+    Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ ->
+      P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ).
     Proof.
       intros P Q rP rQ HoP HoQ HrP HrQ.
       pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d).
@@ -136,5 +172,63 @@ Section ExtendedCoordinates.
       - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
       - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
     Qed.
+
+    Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q).
+    Proof.
+      intros; pose proof (proj2_sig (unifiedAdd (mkPoint _ H) (mkPoint _ H0))); eauto.
+    Qed.
+
+    Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'.
+    Next Obligation.
+      destruct x, x0; simpl; intuition.
+      - erewrite extendedToTwisted_rep; eauto using unifiedAddM1'_rep.
+      - erewrite extendedToTwisted_rep.
+        (* It would be nice if I could use eauto here, but it gets evars wrong :( *)
+        2: eapply unifiedAddM1'_rep. 5:apply H1. 4:apply H. 3:auto. 2:auto.
+        eauto using unifiedAdd'_onCurve.
+    Qed.
+
+    Lemma unifiedAddM1_rep : forall P Q, unifiedAdd (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q).
+    Proof.
+      destruct P, Q; unfold unExtendedPoint, unifiedAdd, unifiedAddM1; eapply point_eq; simpl in *; intuition.
+      pose proof (unifiedAddM1'_rep x x0 (extendedToTwisted x) (extendedToTwisted x0));
+        destruct (unifiedAddM1' x x0);
+        unfold rep in *; intuition.
+    Qed.
+
+    Global Instance Proper_unifiedAddM1 : Proper (equiv==>equiv==>equiv) unifiedAddM1.
+    Proof.
+      repeat (econstructor || intro).
+      repeat match goal with [H: _ === _ |- _ ] => inversion H; clear H end; unfold equiv, extendedPoint_eq.
+      rewrite <-!unifiedAddM1_rep.
+      destruct x, y, x0, y0; simpl in *; eapply point_eq; congruence.
+    Qed.
+
+    Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint zero) === P.
+      unfold equiv, extendedPoint_eq; intros.
+      rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto.
+    Qed.
+
+    Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint zero) P === P.
+      unfold equiv, extendedPoint_eq; intros.
+      rewrite <-!unifiedAddM1_rep, twistedAddComm, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto.
+    Qed.
+
+    Lemma unifiedAddM1_assoc : forall a b c, unifiedAddM1 a (unifiedAddM1 b c) === unifiedAddM1 (unifiedAddM1 a b) c.
+    Proof.
+      unfold equiv, extendedPoint_eq; intros.
+      rewrite <-!unifiedAddM1_rep, twistedAddAssoc; auto.
+    Qed.
+    
+    Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero).
+    Definition scalarMultM1_spec := iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint zero) unifiedAddM1_0_l.
+    Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P) = scalarMult n (unExtendedPoint P).
+      intros; rewrite scalarMultM1_spec, Nat2N.id.
+      induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|].
+      unfold scalarMult; fold scalarMult.
+      rewrite <-IHn, unifiedAddM1_rep; auto.
+    Qed.
+
   End TwistMinus1.
+
 End ExtendedCoordinates.
\ No newline at end of file