Spec/EdDSA: comments, remove prehashing

1 files changed, 4 insertions, 7 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index c7314486e..35fc1d543 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -28,7 +28,7 @@ Section EdDSAParams.
   Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *)
     E : TwistedEdwardsParams; (* underlying elliptic curve *)
                         
-    b : nat;
+    b : nat; (* public keys are k bits, signatures are 2*k bits *)
     b_valid : 2^(b - 1) > BinInt.Z.to_nat q;
     FqEncoding : encoding of F q as Word.word (b-1);
     PointEncoding : encoding of point as Word.word b;
@@ -38,7 +38,7 @@ Section EdDSAParams.
     c : nat; (* cofactor E = 2^c *)
     c_valid : c = 2 \/ c = 3;
   
-    n : nat;
+    n : nat; (* secret keys are (n+1) bits *)
     n_ge_c : n >= c;
     n_le_b : n <= b;
   
@@ -48,11 +48,8 @@ Section EdDSAParams.
     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 : scalarMult l B = zero;
-    FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b;
-
-    H'_out_len : nat -> nat;
-    H' : forall {n}, Word.word n -> Word.word (H'_out_len n) (* prehash function *)
+    l_order_B : (l*B)%E = zero;
+    FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b
   }.
 End EdDSAParams.