minor updates needed to make it compile with bbv

removing lemma wordToNat_wzero is ok because it's already in bbv

13 files changed, 17 insertions, 22 deletions

diff --git a/_CoqProject b/_CoqProject
index 5fd534bca..743a0a3a3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@ bbv/DepEqNat.v
 bbv/NatLib.v
 bbv/Nomega.v
 bbv/Word.v
+bbv/WordScope.v
 src/Demo.v
 src/Algebra/Field.v
 src/Algebra/Field_test.v
diff --git a/bbv b/bbv
-Subproject 8bd42f21304d7a22c1b1225fe81236ad106a530
+Subproject bf459e5378c13ca73cb5f2ca17ab2b55069ff82
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 375265c9c..5ecd088bd 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Export Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.
-Require Export Bedrock.Word.
+Require Export bbv.WordScope.
 Require Export Crypto.Util.Notations.
 
 Notation Const x := (Op (OpConst x) TT).
@@ -731,7 +731,7 @@ def header():
     return (r"""Require Import Coq.ZArith.ZArith.
 Require Export Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.
-Require Export Bedrock.Word.
+Require Export bbv.WordScope.
 Require Export Crypto.Util.Notations.
 
 Notation Const x := (Op (OpConst x) TT).
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 7d9061cad..435ec793e 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -245,7 +245,7 @@ End with_round_up_list.
     specified here. *)
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.FixedWordSizes.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 
 Module Export Exports. (* export unfolding strategy *)
   (* iota is probably (hopefully?) the cheapest reduction.
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 1c8468e68..9193ea17f 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -32,7 +32,7 @@ Require Import Crypto.Util.Tactics.UnfoldArg.
 Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.Option.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 
 (** The final tactic in this file, [do_reflective_pipeline], takes a
     goal of the form
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index fe08c9d1f..0e365d9f8 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Export Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.
-Require Export Bedrock.Word.
+Require Export bbv.WordScope.
 Require Export Crypto.Util.Notations.
 
 Notation Const x := (Op (OpConst x) TT).
@@ -731,7 +731,7 @@ def header():
     return (r"""Require Import Coq.ZArith.ZArith.
 Require Export Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.
-Require Export Bedrock.Word.
+Require Export bbv.WordScope.
 Require Export Crypto.Util.Notations.
 
 Notation Const x := (Op (OpConst x) TT).
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v
index de4626adb..dbc739dcb 100644
--- a/src/Compilers/Z/Syntax.v
+++ b/src/Compilers/Z/Syntax.v
@@ -1,6 +1,6 @@
 (** * PHOAS Syntax for expression trees on ℤ *)
 Require Import Coq.ZArith.ZArith.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.TypeUtil.
diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v
index 9239b9c81..d867a62df 100644
--- a/src/Primitives/EdDSARepChange.v
+++ b/src/Primitives/EdDSARepChange.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Util.FixCoqMistakes.
-Require Import Crypto.Spec.EdDSA Bedrock.Word.
+Require Import Crypto.Spec.EdDSA bbv.WordScope.
 Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
 Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.ScalarMult.
 Require Import Crypto.Util.Decidable Crypto.Util.Option.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index db350e4e0..8518821fc 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,4 +1,4 @@
-Require Bedrock.Word Crypto.Util.WordUtil.
+Require bbv.WordScope Crypto.Util.WordUtil.
 Require Crypto.Algebra.Hierarchy Algebra.ScalarMult.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v
index 2befc1ef6..10a7d78ff 100644
--- a/src/Util/FixedWordSizes.v
+++ b/src/Util/FixedWordSizes.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.BinNat.
 Require Import Coq.Arith.Arith.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 
 Definition word32 := word 32. (* 2^5 *)
 Definition word64 := word 64. (* 2^6 *)
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index f699adeed..bd71f5b80 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.BinNat.
 Require Import Coq.Arith.Arith.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.WordUtil.
 Require Import Crypto.Util.ZUtil.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index 9321f2b23..8c354690b 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -1,7 +1,8 @@
 Require Import Coq.NArith.NArith.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
-Require Bedrock.Word.
+Require bbv.WordScope.
+Require Import bbv.NatLib.
 Require Crypto.Util.WordUtil.
 
 Module N.
@@ -107,7 +108,7 @@ Module N.
   Section ZN.
     Import Coq.ZArith.ZArith.
     Lemma ZToN_NPow2_lt : forall z n, (0 <= z < 2 ^ Z.of_nat n)%Z ->
-                                      (Z.to_N z < Word.Npow2 n)%N.
+                                      (Z.to_N z < Npow2 n)%N.
     Proof.
       intros.
       apply WordUtil.bound_check_nat_N.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 64cfda434..c1eeb138b 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -15,8 +15,8 @@ Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Sigma.
 
-Require Import Bedrock.Word.
-Require Import Bedrock.Nomega.
+Require Import bbv.WordScope.
+Require Import bbv.Nomega.
 
 Require Import Crypto.Util.FixCoqMistakes.
 
@@ -370,8 +370,6 @@ Section WordToN.
       + clear IHk'.
         shatter x; simpl.
 
-        rewrite N.succ_double_spec; simpl.
-
         rewrite kill_match.
         replace (N.pos (Pos.of_succ_nat k'))
            with (N.succ (N.of_nat k'))
@@ -826,11 +824,6 @@ Definition setbit {b} n {H:n < b} (w:word b) : word b :=
 Definition clearbit {b} n {H:n < b} (w:word b) : word b :=
   wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w.
 
-Lemma wordToNat_wzero {n} : wordToNat (wzero n) = 0.
-Proof.
-  unfold wzero; induction n as [|n IHn]; simpl; try rewrite_hyp!*; omega.
-Qed.
-
 Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b),
   wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
 Proof.