From 2e96e2cab74d00b40188b00a4e90eeeaa1c46706 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Sat, 25 Jun 2016 15:08:21 -0400
Subject: EdDSA: prove things about spec

---
 src/Spec/EdDSA.v | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

(limited to 'src/Spec')

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index c28ff0482..7e4d3ed25 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,4 +1,3 @@
-Require Import Crypto.Spec.Encoding.
 Require Bedrock.Word Crypto.Util.WordUtil.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
@@ -33,8 +32,8 @@ Section EdDSA.
 
         {B : E} (* base point *)
 
-        {PointEncoding : canonical encoding of E as Word.word b} (* wire format *)
-        {FlEncoding : canonical encoding of { n | n < l } as Word.word b}
+        {Eenc : E   -> Word.word b} (* normative encoding of elliptic cuve points *)
+        {Senc : nat -> Word.word b} (* normative encoding of scalars *)
     :=
       {
         EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
@@ -48,13 +47,13 @@ Section EdDSA.
 
         EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
         EdDSA_l_odd : l > 2;
-        EdDSA_l_order_B : EscalarMult l B = Ezero
+        EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero
       }.
   Global Existing Instance EdDSA_group.
 
   Context `{prm:EdDSA}.
 
-  Local Infix "=" := Eeq.
+  Local Infix "=" := Eeq : type_scope.
   Local Coercion Word.wordToNat : Word.word >-> nat.
   Local Notation secretkey := (Word.word b) (only parsing).
   Local Notation publickey := (Word.word b) (only parsing).
@@ -75,18 +74,18 @@ Section EdDSA.
   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).
+  Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B).
 
   Program Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
     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 : {n|n<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in
-        enc R ++ enc S.
+    let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l 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_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.
+    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).
+End EdDSA.
\ No newline at end of file
-- 
cgit v1.2.3