nicer verify() derivation starter

3 files changed, 34 insertions, 13 deletions

diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 8dbfdf7b9..b7d2c0d8e 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -46,8 +46,11 @@ 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.
\ No newline at end of file
+Infix "*" := scalarMult : E_scope.
+Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 6f57d7bec..c9660bd98 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -14,6 +14,7 @@ Infix "mod" := NPeano.modulo.
 Infix "++" := Word.combine.
 
 Section EdDSAParams.
+
   Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *)
     E : TwistedEdwardsParams; (* underlying elliptic curve *)
 
@@ -70,8 +71,6 @@ Section EdDSA.
                               (r + H (enc R ++ public sk ++ M) * s)) in
         enc R ++ enc S.
 
-  Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}.
-  Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope.
   Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool :=
     let R_ := Word.split1 b b sig in
     let S_ := Word.split2 b b sig in
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 33c8398f7..efee4e7af 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -1,30 +1,49 @@
+Require Import Bedrock.Word.
 Require Import Crypto.Spec.Ed25519.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic.
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
+Require Import Crypto.Spec.CompleteEdwardsCurve.
+Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding.
+Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
+Require Import Crypto.Util.IterAssocOp.
 
 Local Infix "++" := Word.combine.
 Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40).
 Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40).
+Local Arguments H {_} _.
+Local Arguments scalarMultM1 {_} {_} _ _.
+Local Arguments unifiedAddM1 {_} {_} _ _.
 
 Lemma sharper_verify : { verify | forall pk l msg sig, verify pk l msg sig = ed25519_verify pk l msg sig}.
 Proof.
   eexists; intros.
-  cbv [ed25519_verify EdDSA.verify Encoding.dec EdDSA.PointEncoding PointEncoding
-                      PointEncoding.point_encoding EdDSA.FlEncoding FlEncoding
-                      Encoding.modular_word_encoding ed25519params].
-  break_match.
-  break_match.
-  break_match.
+  cbv [ed25519_verify EdDSA.verify
+                      ed25519params curve25519params
+                      EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H
+                      EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding].
+
+  (* zoom in to the interesting case *)
+  repeat match goal with |- context[match ?a with Some x => _ | _ => _ end] =>
+                    let n := fresh x in
+                    let H := fresh "Heq" x in
+                    destruct a as [x|]
+  end.
+
+  let p1 := constr:(scalarMultM1_rep eq_refl) in
+  let p2 := constr:(unifiedAddM1_rep eq_refl) in
   repeat match goal with
   | |- context [(?n * ?P)%E] =>
     rewrite <-(unExtendedPoint_mkExtendedPoint P);
-    erewrite <-scalarMultM1_rep
+    erewrite <-p1
   | |- context [(?P + unExtendedPoint _)%E] =>
     rewrite <-(unExtendedPoint_mkExtendedPoint P);
-    erewrite unifiedAddM1_rep
+    erewrite p2
   end.
   rewrite !Znat.Z_nat_N, <-!Word.wordToN_nat.
   
-  (* unfold scalarMultM1 at 1. *)
+  cbv [scalarMultM1 iter_op].
+  Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *)
+  cbv iota zeta delta [test_and_op].
+
+
 Admitted.
\ No newline at end of file