port EdDSA spec

1 files changed, 51 insertions, 56 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index a0e5e9da7..bd8a095dd 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,6 +1,4 @@
 Require Import Crypto.Spec.Encoding.
-Require Import Crypto.Spec.ModularArithmetic.
-Require Import Crypto.Spec.CompleteEdwardsCurve.
 
 Require Import Crypto.Util.WordUtil.
 Require Bedrock.Word.
@@ -8,80 +6,77 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
-Coercion Word.wordToNat : Word.word >-> nat.
+Local Infix "^" := NPeano.pow.
+Local Infix "mod" := NPeano.modulo (at level 40, no associativity).
+Local Infix "++" := Word.combine.
 
-Infix "^" := NPeano.pow.
-Infix "mod" := NPeano.modulo.
-Infix "++" := Word.combine.
+Generalizable All Variables.
+Section EdDSA.
+  Class EdDSA (* <https://eprint.iacr.org/2015/677.pdf> *)
+        {E Eeq Eadd Ezero Eopp} {EscalarMult} (* the underllying elliptic curve operations *)
 
-Section EdDSAParams.
+        {b : nat} (* public keys are k bits, signatures are 2*k bits *)
+        {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 *)
 
-  Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *)
-    E : TwistedEdwardsParams; (* underlying elliptic curve *)
+        {B : E} (* base point *)
 
-    b : nat; (* public keys are k bits, signatures are 2*k bits *)
-    b_valid : 2^(b - 1) > BinInt.Z.to_nat q;
-    FqEncoding : canonical encoding of F q as Word.word (b-1);
-    PointEncoding : canonical encoding of E.point as Word.word b;
+        {PointEncoding : canonical encoding of E as Word.word b} (* wire format *)
+        {FlEncoding : canonical encoding of { n | n < l } as Word.word b}
+    :=
+      { 
+        EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
 
-    H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *)
+        EdDSA_c_valid : c = 2 \/ c = 3;
 
-    c : nat; (* cofactor E = 2^c *)
-    c_valid : c = 2 \/ c = 3;
+        EdDSA_n_ge_c : n >= c;
+        EdDSA_n_le_b : n <= b;
 
-    n : nat; (* secret keys are (n+1) bits *)
-    n_ge_c : n >= c;
-    n_le_b : n <= b;
+        EdDSA_B_not_identity : B <> Ezero;
 
-    B : E.point;
-    B_not_identity : B <> E.zero;
+        EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
+        EdDSA_l_odd : l > 2;
+        EdDSA_l_order_B : EscalarMult l B = Ezero
+      }.
+  Global Existing Instance EdDSA_group.
 
-    l : nat; (* order of the subgroup of E generated by B *)
-    l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
-    l_odd : l > 2;
-    l_order_B : (l*B)%E = E.zero;
-    FlEncoding : canonical encoding of F (BinInt.Z.of_nat l) as Word.word b
-  }.
-End EdDSAParams.
+  Context `{prm:EdDSA}.
+
+  Local Infix "=" := Eeq.
+  Local Coercion Word.wordToNat : Word.word >-> 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).
 
-Section EdDSA.
-  Context {prm:EdDSAParams}.
-  Global Existing Instance E.
-  Global Existing Instance PointEncoding.
-  Global Existing Instance FlEncoding.
-  Existing Class le.
-  Existing Instance n_le_b.
-
-  Notation secretkey := (Word.word b) (only parsing).
-  Notation publickey := (Word.word b) (only parsing).
-  Notation signature := (Word.word (b + b)) (only parsing).
-  Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope .
+
+  Existing Class le. Local Existing Instance EdDSA_n_le_b.
+  Local Arguments H {n} _.
 
   (* TODO: proofread curveKey and definition of n *)
   Definition curveKey (sk:secretkey) : nat :=
     let x := wfirstn n sk in (* first half of the secret key is a scalar *)
     let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *)
              x + 2^n. (* and the high bit is always set *)
+
+  Local Infix "+" := Eadd.
+  Local Infix "*" := EscalarMult.
+
   Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk).
-  Definition public (sk:secretkey) : publickey := enc (curveKey sk * B)%E.
+  Definition public (sk:secretkey) : publickey := enc (curveKey sk*B).
 
-  Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
+  Program Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
     let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
-    let R : E.point := (r * B)%E in (* commitment to nonce *)
+    let R : E := r * B in (* commitment to nonce *)
     let s : nat := curveKey sk in (* secret scalar *)
-    let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat
-                              (r + H (enc R ++ public sk ++ M) * s)) in
+    let S : {n|n<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in
         enc R ++ enc S.
+  Admit Obligations.
 
-  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
-    match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' =>
-    match dec A_ : option E.point with None => false | Some A =>
-    match dec R_ : option E.point with None => false | Some R =>
-    if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A
-    then true else false
-    end
-    end
-    end%E.
+  (* 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_lt_l,
+      S * B = R + (H (enc R ++ enc A ++ message) mod l) * A
+      -> valid message (enc A) (enc R ++ enc (exist _ S S_lt_l)).
 End EdDSA.
\ No newline at end of file