diff options
author | jadep <jade.philipoom@gmail.com> | 2017-02-13 14:25:52 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-02-22 21:45:56 -0500 |
commit | febcf9b98a4cd668e4f5d390d9ce1ae1fa30055b (patch) | |
tree | 3797581fa28f8e1d82d6abce6c2c38d76b893997 /src/Util/NUtil.v | |
parent | 305253c724b263476e0aaf0359e5f9ec83211be6 (diff) |
moved more stuff to NUtil
Diffstat (limited to 'src/Util/NUtil.v')
-rw-r--r-- | src/Util/NUtil.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v index 309272a90..6f50642c3 100644 --- a/src/Util/NUtil.v +++ b/src/Util/NUtil.v @@ -1,6 +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 Crypto.Util.WordUtil. Module N. Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N. @@ -102,5 +104,45 @@ Module N. apply N2Nat.id. Qed. + 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. + Proof. + intros. + apply WordUtil.bound_check_nat_N. + apply Znat.Nat2Z.inj_lt. + rewrite Znat.Z2Nat.id by omega. + rewrite ZUtil.Z.pow_Zpow. + replace (Z.of_nat 2) with 2%Z by reflexivity. + omega. + Qed. + + Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x). + Lemma combine_ZNWord : forall sz1 sz2 z1 z2, + (0 <= Z.of_nat sz1)%Z -> + (0 <= Z.of_nat sz2)%Z -> + (0 <= z1 < 2 ^ (Z.of_nat sz1))%Z -> + (0 <= z2 < 2 ^ (Z.of_nat sz2))%Z -> + Word.combine (ZNWord sz1 z1) (ZNWord sz2 z2) = + ZNWord (sz1 + sz2) (Z.lor z1 (Z.shiftl z2 (Z.of_nat sz1))). + Proof. + cbv [ZNWord]; intros. + rewrite !Word.NToWord_nat. + match goal with |- ?a = _ => rewrite <- (Word.natToWord_wordToNat a) end. + rewrite WordUtil.wordToNat_combine. + rewrite !Word.wordToNat_natToWord_idempotent by (rewrite Nnat.N2Nat.id; auto using ZToN_NPow2_lt). + f_equal. + rewrite ZUtil.Z.lor_shiftl by auto. + rewrite !Z_N_nat. + rewrite Znat.Z2Nat.inj_add by (try apply Z.shiftl_nonneg; omega). + f_equal. + rewrite Z.shiftl_mul_pow2 by auto. + rewrite Znat.Z2Nat.inj_mul by omega. + rewrite <-ZUtil.Z.pow_Z2N_Zpow by omega. + rewrite Nat.mul_comm. + f_equal. + Qed. + End ZN. End N. |