consolidate and rename Edwards curve lemmas

1 files changed, 8 insertions, 9 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 8a48f4dea..80aed4a20 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -22,7 +22,7 @@ Section EdDSAParams.
     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;
+    PointEncoding : encoding of E.point as Word.word b;
 
     H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *)
 
@@ -33,13 +33,13 @@ Section EdDSAParams.
     n_ge_c : n >= c;
     n_le_b : n <= b;
 
-    B : point;
-    B_not_identity : B <> zero;
+    B : E.point;
+    B_not_identity : B <> E.zero;
 
     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 = zero;
+    l_order_B : (l*B)%E = E.zero;
     FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b
   }.
 End EdDSAParams.
@@ -55,8 +55,7 @@ Section EdDSA.
   Notation secretkey := (Word.word b) (only parsing).
   Notation publickey := (Word.word b) (only parsing).
   Notation signature := (Word.word (b + b)) (only parsing).
-  Let point_eq_dec : forall P Q, {P = Q} + {P <> Q} := CompleteEdwardsCurveTheorems.point_eq_dec.
-  Local Infix "==" := point_eq_dec (at level 70) : E_scope .
+  Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope .
 
   (* TODO: proofread curveKey and definition of n *)
   Definition curveKey (sk:secretkey) : nat :=
@@ -68,7 +67,7 @@ Section EdDSA.
 
   Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
     let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
-    let R : point := (r * B)%E in (* commitment to nonce *)
+    let R : E.point := (r * B)%E 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
@@ -78,8 +77,8 @@ Section EdDSA.
     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 point with None => false | Some A =>
-    match dec R_ : option point with None => false | Some R =>
+    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