From 3fd5f652ba38a0b308b6e2e86783d82b861fb5bf Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Fri, 2 Feb 2018 16:09:01 -0500 Subject: minor updates needed to make it compile with bbv removing lemma wordToNat_wzero is ok because it's already in bbv --- _CoqProject | 1 + bbv | 2 +- src/Compilers/Z/BinaryNotationConstants.v | 4 ++-- src/Compilers/Z/Bounds/Pipeline/Definition.v | 2 +- src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 2 +- src/Compilers/Z/HexNotationConstants.v | 4 ++-- src/Compilers/Z/Syntax.v | 2 +- src/Primitives/EdDSARepChange.v | 2 +- src/Spec/EdDSA.v | 2 +- src/Util/FixedWordSizes.v | 2 +- src/Util/FixedWordSizesEquality.v | 2 +- src/Util/NUtil.v | 5 +++-- src/Util/WordUtil.v | 11 ++--------- 13 files changed, 18 insertions(+), 23 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 index 8bd42f213..bf459e537 160000 --- a/bbv +++ b/bbv @@ -1 +1 @@ -Subproject commit 8bd42f21304d7a22c1b1225fe81236ad106a5309 +Subproject commit bf459e5378c13ca73cb5f2ca17ab2b55069ff82a 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. -- cgit v1.2.3