Factor out some bedrock dependencies into WordUtil

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

6 files changed, 39 insertions, 35 deletions

diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index adc40dae6..e16cc73f6 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -4,7 +4,7 @@ Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding.
 Require Import Crypto.Spec.EdDSA.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
+Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
 Require Import VerdiTactics.
 Require Import Decidable.
@@ -150,7 +150,7 @@ Instance x : EdDSAParams := {
   FqEncoding := FqEncoding;
   FlEncoding := FlEncoding;
   PointEncoding := PointEncoding;
- 
+
   b_valid := b_valid;
   c_valid := c_valid;
   n_ge_c := n_ge_c;
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 :=
diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v
index 95ac85c97..7bef9295b 100644
--- a/src/Spec/Encoding.v
+++ b/src/Spec/Encoding.v
@@ -4,6 +4,7 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithme
 Require Import Bedrock.Word.
 Require Import VerdiTactics.
 Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.WordUtil.
 
 Class Encoding (T B:Type) := {
   enc : T -> B ;
@@ -33,7 +34,7 @@ Section ModularWordEncoding.
     rewrite <- Nnat.N2Nat.id.
     rewrite Npow2_nat.
     apply (Nat2N_inj_lt (Z.to_nat x) (pow2 sz)).
-    rewrite ZUtil.Zpow_pow2.
+    rewrite Zpow_pow2.
     destruct x_range as [x_low x_high].
     apply Z2Nat.inj_lt in x_high; try omega.
     rewrite <- ZUtil.pow_Z2N_Zpow by omega.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 256654df7..4ba6d0808 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,5 +1,4 @@
 Require Import NPeano Omega.
-Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
 
@@ -57,8 +56,3 @@ Proof.
     rewrite <- nat_compare_lt; auto.
   }
 Qed.
-
-Lemma pow2_id : forall n, pow2 n = 2 ^ n.
-Proof.
-  induction n; intros; simpl; auto.
-Qed.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
new file mode 100644
index 000000000..49de971ef
--- /dev/null
+++ b/src/Util/WordUtil.v
@@ -0,0 +1,27 @@
+Require Import NPeano.
+Require Import ZArith.ZArith.
+Require Import Bedrock.Word.
+
+Local Open Scope nat_scope.
+
+Lemma pow2_id : forall n, pow2 n = 2 ^ n.
+Proof.
+  induction n; intros; simpl; auto.
+Qed.
+
+Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)).
+Proof.
+  induction n; intros; auto.
+  simpl pow2.
+  rewrite Nat2Z.inj_succ.
+  rewrite Z.pow_succ_r by apply Zle_0_nat.
+  rewrite untimes2.
+  rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
+  rewrite <- IHn.
+  auto.
+Qed.
+
+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.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index ac1c47152..2cfab2e90 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,7 +1,6 @@
 Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
 Require Import Crypto.Util.NatUtil.
-Require Import Bedrock.Word.
 Local Open Scope Z.
 
 Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
@@ -38,7 +37,7 @@ Proof.
   rewrite Zmod_mod; auto.
 Qed.
 
-Lemma pos_pow_nat_pos : forall x n, 
+Lemma pos_pow_nat_pos : forall x n,
   Z.pos x ^ Z.of_nat n > 0.
   do 2 (intros; induction n; subst; simpl in *; auto with zarith).
   rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
@@ -53,18 +52,6 @@ Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
   intuition.
 Qed.
 
-Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)).
-Proof.
-  induction n; intros; auto.
-  simpl pow2.
-  rewrite Nat2Z.inj_succ.
-  rewrite Z.pow_succ_r by apply Zle_0_nat.
-  rewrite untimes2.
-  rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
-  rewrite <- IHn.
-  auto.
-Qed.
-
 Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
   ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
 Proof.