Factor out some bedrock dependencies into WordUtil

Also move a definition about words, with a TODO about location, into WordUtil.

1 files changed, 7 insertions, 12 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index a7b8fe987..45950f6a1 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -2,16 +2,11 @@ Require Import Crypto.Spec.Encoding.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.Spec.CompleteEdwardsCurve.
 
+Require Import Crypto.Util.WordUtil.
 Require Bedrock.Word.
 Require Znumtheory BinInt.
 Require NPeano.
 
-(* TODO : where should this be? *)
-Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
-  refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
-                            | eq_refl => w
-                            end)); abstract omega. Defined.
-
 Coercion Word.wordToNat : Word.word >-> nat.
 
 Infix "^" := NPeano.pow.
@@ -21,21 +16,21 @@ Infix "++" := Word.combine.
 Section EdDSAParams.
   Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *)
     E : TwistedEdwardsParams; (* underlying elliptic curve *)
-                        
+
     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;
-  
+
     H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *)
-  
+
     c : nat; (* cofactor E = 2^c *)
     c_valid : c = 2 \/ c = 3;
-  
+
     n : nat; (* secret keys are (n+1) bits *)
     n_ge_c : n >= c;
     n_le_b : n <= b;
-  
+
     B : point;
     B_not_identity : B <> zero;
 
@@ -74,7 +69,7 @@ Section EdDSA.
     let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat
                               (r + H (enc R ++ public sk ++ M) * s)) in
         enc R ++ enc S.
-  
+
   Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}.
   Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope.
   Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool :=