Derive EdDSA.verify from equational specification

Experiments/SpecEd25519 will come back soon

1 files changed, 16 insertions, 15 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 38dc64cef..2971bfef8 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -3,6 +3,10 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
+Require Import Omega. (* TODO: remove this import when we drop 8.4 *)
+
+Require Import Crypto.Spec.ModularArithmetic.
+
 (** In Coq 8.4, we have [NPeano.pow] and [NPeano.modulo].  In Coq 8.5,
     they are [Nat.pow] and [Nat.modulo].  To allow this file to work
     with both versions, we create a module where we (locally) import
@@ -28,12 +32,12 @@ Section EdDSA.
         {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *)
         {c : nat} (* cofactor E = 2^c *)
         {n : nat} (* secret keys are (n+1) bits *)
-        {l : nat} (* order of the subgroup of E generated by B *)
+        {l : BinInt.Z} (* order of the subgroup of E generated by B *)
 
         {B : E} (* base point *)
 
         {Eenc : E   -> Word.word b} (* normative encoding of elliptic cuve points *)
-        {Senc : nat -> Word.word b} (* normative encoding of scalars *)
+        {Senc : F l -> Word.word b} (* normative encoding of scalars *)
     :=
       {
         EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
@@ -44,19 +48,19 @@ Section EdDSA.
         EdDSA_n_ge_c : n >= c;
         EdDSA_n_le_b : n <= b;
 
-        EdDSA_B_not_identity : B <> Ezero;
+        EdDSA_B_not_identity : not (Eeq B Ezero);
 
-        EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
-        EdDSA_l_odd : l > 2;
-        EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero
+        EdDSA_l_prime : Znumtheory.prime l;
+        EdDSA_l_odd : BinInt.Z.lt 2 l;
+        EdDSA_l_order_B : Eeq (EscalarMult (BinInt.Z.to_nat l) B) Ezero
       }.
   Global Existing Instance EdDSA_group.
   Global Existing Instance EdDSA_scalarmult.
 
   Context `{prm:EdDSA}.
 
-  Local Infix "=" := Eeq : type_scope.
   Local Coercion Word.wordToNat : Word.word >-> nat.
+  Local Coercion BinInt.Z.to_nat : BinInt.Z >-> nat.
   Local Notation secretkey := (Word.word b) (only parsing).
   Local Notation publickey := (Word.word b) (only parsing).
   Local Notation signature := (Word.word (b + b)) (only parsing).
@@ -64,8 +68,7 @@ Section EdDSA.
   Local Arguments H {n} _.
   Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing).
 
-  Require Import Coq.omega.Omega.
-  Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega.
+  Local Obligation Tactic := destruct prm; simpl; intros; omega.
 
   Program Definition curveKey (sk:secretkey) : nat :=
     let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *)
@@ -82,12 +85,10 @@ Section EdDSA.
     let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
     let R : E := r * B in (* commitment to nonce *)
     let s : nat := curveKey sk in (* secret scalar *)
-    let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l in
+    let S : F l := F.nat_mod l (r + H (Eenc R ++ A_ ++ M) * s) in
         Eenc R ++ Senc S.
 
-  (* For a [n]-bit [message] from public key [A_], validity of a signature [R_ ++ S_] *)
-  Inductive valid {n:nat} : Word.word n -> publickey -> signature -> Prop :=
-    ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat),
-      S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A
-      -> valid message (Eenc A) (Eenc R ++ Senc S).
+  Definition valid {n} (message : Word.word n) pubkey signature :=
+    exists A S R, Eenc A = pubkey /\ Eenc R ++ Senc S = signature /\
+                  Eeq (F.to_nat S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A).
 End EdDSA.