aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBenjamin Barenblat <bbaren@google.com>2019-04-26 16:35:42 -0400
committerBenjamin Barenblat <bbaren@google.com>2019-04-26 16:35:42 -0400
commitefdf63a5dd1dfbd4bafc121224c64822530185fe (patch)
tree633f4e1a254c0f15864b848fa4c1063a44b2c350
parentd20b2cbc862fb35b5e059cbfafaaa9360fb6afce (diff)
Remove WordUtil
Remove Util/NUtil.v and Util/WordUtil.v. This code is no longer in use.
-rw-r--r--_CoqProject2
-rw-r--r--src/Util/NUtil.v121
-rw-r--r--src/Util/WordUtil.v1362
3 files changed, 0 insertions, 1485 deletions
diff --git a/_CoqProject b/_CoqProject
index 40df1fb72..6e7e43e64 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -151,7 +151,6 @@ src/Util/LetInMonad.v
src/Util/ListUtil.v
src/Util/Logic.v
src/Util/Loops.v
-src/Util/NUtil.v
src/Util/NatUtil.v
src/Util/Notations.v
src/Util/NumTheoryUtil.v
@@ -177,7 +176,6 @@ src/Util/TagList.v
src/Util/Tower.v
src/Util/Tuple.v
src/Util/Unit.v
-src/Util/WordUtil.v
src/Util/ZBounded.v
src/Util/ZRange.v
src/Util/ZUtil.v
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
deleted file mode 100644
index 1d78e3276..000000000
--- a/src/Util/NUtil.v
+++ /dev/null
@@ -1,121 +0,0 @@
-Require Import Coq.NArith.NArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
-Require Export Crypto.Util.NUtil.WithoutReferenceToZ.
-Require bbv.WordScope.
-Require Import bbv.NatLib.
-Require Crypto.Util.WordUtil.
-Require Import Crypto.Util.ZUtil.Z2Nat.
-Require Import Crypto.Util.ZUtil.Shift.
-
-Module N.
- Lemma shiftr_size : forall n bound, N.size_nat n <= bound ->
- N.shiftr_nat n bound = 0%N.
- Proof.
- intros n bound H.
- rewrite <- (Nat2N.id bound).
- rewrite Nshiftr_nat_equiv.
- destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
- apply N.shiftr_eq_0.
- rewrite N.size_nat_equiv in *.
- rewrite N.size_log2 in * by auto.
- apply N.le_succ_l.
- rewrite <- N.compare_le_iff.
- rewrite N2Nat.inj_compare.
- rewrite <- Compare_dec.nat_compare_le.
- rewrite Nat2N.id.
- auto.
- Qed.
-
- Hint Rewrite
- N.succ_double_spec
- N.add_1_r
- Nat2N.inj_succ
- Nat2N.inj_mul
- N2Nat.id: N_nat_conv
- .
-
- Lemma succ_double_to_nat : forall n,
- N.succ_double n = N.of_nat (S (2 * N.to_nat n)).
- Proof.
- intros.
- replace 2 with (N.to_nat 2) by auto.
- autorewrite with N_nat_conv.
- reflexivity.
- Qed.
-
- Lemma double_to_nat : forall n,
- N.double n = N.of_nat (2 * N.to_nat n).
- Proof.
- intros.
- replace 2 with (N.to_nat 2) by auto.
- autorewrite with N_nat_conv.
- reflexivity.
- Qed.
-
- Lemma shiftr_succ : forall n i,
- N.to_nat (N.shiftr_nat n i) =
- if N.testbit_nat n i
- then S (2 * N.to_nat (N.shiftr_nat n (S i)))
- else (2 * N.to_nat (N.shiftr_nat n (S i))).
- Proof.
- intros n i.
- rewrite Nshiftr_nat_S.
- case_eq (N.testbit_nat n i); intro testbit_i;
- pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd;
- rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd;
- rewrite testbit_i in shiftr_n_odd.
- + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
- rewrite succ_double_to_nat in Nsucc_double_shift.
- apply Nat2N.inj.
- rewrite Nsucc_double_shift.
- apply N2Nat.id.
- + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
- rewrite double_to_nat in Nsucc_double_shift.
- apply Nat2N.inj.
- rewrite Nsucc_double_shift.
- 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 < Npow2 n)%N.
- Proof.
- intros.
- apply WordUtil.bound_check_nat_N.
- apply Znat.Nat2Z.inj_lt.
- rewrite Znat.Z2Nat.id by omega.
- rewrite 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 using Type.
- 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 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 <-Z.pow_Z2N_Zpow by omega.
- rewrite Nat.mul_comm.
- f_equal.
- Qed.
- End ZN.
-
-End N.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
deleted file mode 100644
index 932f48fee..000000000
--- a/src/Util/WordUtil.v
+++ /dev/null
@@ -1,1362 +0,0 @@
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.NArith.NArith.
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Program.Program.
-Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
-Require Import Coq.micromega.Psatz.
-Require Import Coq.Bool.Bool.
-
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.Util.Sigma.
-
-Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
-Require Import Crypto.Util.ZUtil.N2Z.
-Require Import Crypto.Util.ZUtil.Definitions.
-
-Require Import bbv.WordScope.
-Require Import bbv.Nomega.
-
-Require Import Crypto.Util.FixCoqMistakes.
-
-Local Open Scope nat_scope.
-
-Create HintDb pull_wordToN discriminated.
-Create HintDb push_wordToN discriminated.
-Create HintDb pull_ZToWord discriminated.
-Create HintDb push_ZToWord discriminated.
-
-Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN.
-Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN.
-Hint Extern 1 => autorewrite with pull_ZToWord in * : pull_ZToWord.
-Hint Extern 1 => autorewrite with push_ZToWord in * : push_ZToWord.
-
-Module Word.
- Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool :=
- match x, y with
- | WO, WO => true
- | WO, _ => false
- | WS b _ x', WS b' _ y'
- => eqb b b' && @weqb_hetero _ _ x' y'
- | WS _ _ _, _
- => false
- end%bool.
- Global Arguments weqb_hetero {_ _} _ _.
- Theorem weqb_hetero_true_iff : forall sz1 x sz2 y,
- @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y.
- Proof.
- induction x; intros sz2 y; (split; [ destruct y | ]);
- repeat first [ progress simpl
- | intro
- | congruence
- | exists eq_refl
- | progress destruct_head ex
- | progress destruct_head bool
- | progress subst
- | progress split_andb
- | match goal with
- | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ]
- => apply IHx in H
- | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
- => apply IHx
- end ].
- Defined.
- (* oh, the hoops I jump through to make this transparent... *)
- Theorem weqb_hetero_homo_true_iff : forall sz x y,
- @weqb_hetero sz sz x y = true <-> x = y.
- Proof.
- intros sz x y; etransitivity; [ apply weqb_hetero_true_iff | ].
- split; [ intros [pf H] | intro ]; try (subst y; exists eq_refl; reflexivity).
- revert y H; induction x as [|b n x IHx]; intros y H.
- { subst y;
- refine match pf in (_ = z)
- return match z return 0 = z -> Prop with
- | 0 => fun pf => WO = eq_rect 0 word WO 0 pf
- | _ => fun pf => True
- end pf
- with
- | eq_refl => eq_refl
- end. }
- { revert x y H IHx.
- refine (match pf in _ = Sn
- return match Sn return S n = Sn -> Prop with
- | 0 => fun _ => True
- | S n' => fun pf =>
- forall (pfn : n = n')
- (x : word n)
- (y : word (S n'))
- (H : eq_rect (S n) word (WS b x) (S n') pf = y)
- (IHx : forall (pf : n = n') (y : word n'), eq_rect n word x n' pf = y -> eq_rect n word x n' pfn = y),
- WS b (eq_rect n word x n' pfn) = y
- end pf
- with
- | eq_refl
- => fun pfn x y H IHx
- => eq_trans
- (f_equal2 (fun b => @WS b _)
- (f_equal (@whd _) H)
- (IHx eq_refl (wtl y) (f_equal (@wtl _) H)))
- _
- end eq_refl).
- refine match y in word Sn return match Sn return word Sn -> Prop with
- | 0 => fun _ => True
- | S n => fun y => WS (whd y) (wtl y) = y
- end y
- with
- | WS _ _ _ => eq_refl
- | _ => I
- end. }
- Defined.
-End Word.
-
-(* Utility Tactics *)
-
-Ltac word_util_arith := omega.
-
-Ltac destruct_min :=
- match goal with
- | [|- context[Z.min ?a ?b]] =>
- let g := fresh in
- destruct (Z.min_dec a b) as [g|g]; rewrite g; clear g
- end.
-
-Ltac destruct_max :=
- match goal with
- | [|- context[Z.max ?a ?b]] =>
- let g := fresh in
- destruct (Z.max_dec a b) as [g|g]; rewrite g; clear g
- end.
-
-Ltac shatter a :=
- let H := fresh in
- pose proof (shatter_word a) as H; simpl in H;
- try rewrite H in *; clear H.
-
-Section Natural.
- Definition Nge_dec (x y: N): {N.ge x y} + {N.lt x y}.
- refine (
- let c := (x ?= y)%N in
- match c as c' return c = c' -> _ with
- | Lt => fun _ => right _
- | _ => fun _ => left _
- end eq_refl); abstract (
- unfold c in *; unfold N.lt, N.ge;
- repeat match goal with
- | [ H: (_ ?= _)%N = _ |- _] =>
- rewrite H; intuition; try inversion H
- | [ H: Eq = _ |- _] => inversion H
- | [ H: Gt = _ |- _] => inversion H
- | [ H: Lt = _ |- _] => inversion H
- end).
- Defined.
-
- Lemma N_ge_0: forall x: N, (0 <= x)%N.
- Proof.
- intro x0; unfold N.le.
- pose proof (N.compare_0_r x0) as H.
- rewrite N.compare_antisym in H.
- induction x0; simpl in *;
- intro V; inversion V.
- Qed.
-
- Lemma of_nat_lt: forall x b, (x < b)%nat <-> (N.of_nat x < N.of_nat b)%N.
- Proof.
- intros x b; split; intro H.
-
- - unfold N.lt; rewrite N2Nat.inj_compare.
- repeat rewrite Nat2N.id.
- apply nat_compare_lt in H.
- intuition.
-
- - unfold N.lt in H; rewrite N2Nat.inj_compare in H.
- repeat rewrite Nat2N.id in H.
- apply nat_compare_lt in H.
- intuition.
- Qed.
-End Natural.
-
-Section Pow2.
- Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)).
- Proof.
- induction n as [|n IHn]; 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 Npow2_gt0 : forall x, (0 < Npow2 x)%N.
- Proof.
- intros x; induction x as [|x IHx].
-
- - simpl; apply N.lt_1_r; intuition.
-
- - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition.
- apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0.
-
- + intuition; inversion H.
-
- + apply N.neq_0_lt_0 in IHx; intuition.
- Qed.
-
- Lemma Npow2_ge1 : forall x, (1 <= Npow2 x)%N.
- Proof.
- intro x.
- pose proof (Npow2_gt0 x) as Z.
- apply N.lt_pred_le; simpl.
- assumption.
- Qed.
-
- Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N.
- Proof.
- induction n as [|n IHn].
-
- - simpl; intuition.
-
- - rewrite Nat2N.inj_succ.
- rewrite N.pow_succ_r; [|apply N_ge_0].
- rewrite <- IHn.
- simpl; intuition.
- Qed.
-
- Lemma Npow2_Zlog2 : forall x n,
- (Z.log2 (Z.of_N x) < Z.of_nat n)%Z
- -> (x < Npow2 n)%N.
- Proof.
- intros x n H.
- apply N2Z.inj_lt.
- rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
- destruct (N.eq_dec x 0%N) as [e|e].
-
- - rewrite e.
- apply Z.pow_pos_nonneg; [cbv; reflexivity|apply Nat2Z.is_nonneg].
-
- - apply Z.log2_lt_pow2; [|assumption].
- apply N.neq_0_lt_0, N2Z.inj_lt in e.
- assumption.
- Qed.
-
- Lemma Npow2_ordered: forall n m, (n <= m)%nat -> (Npow2 n <= Npow2 m)%N.
- Proof.
- induction n as [|n IHn]; intros m H; try rewrite Npow2_succ.
-
- - simpl; apply Npow2_ge1.
-
- - induction m; try rewrite Npow2_succ.
-
- + inversion H.
-
- + assert (n <= m)%nat as H0 by omega.
- apply IHn in H0.
- apply N.mul_le_mono_l.
- assumption.
- Qed.
-End Pow2.
-
-Section WordToN.
- Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
- wordToN (NToWord sz n) = n.
- Proof.
- intros.
- rewrite wordToN_nat, NToWord_nat.
- rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
- Qed.
-
- Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
- Proof.
- intros.
- rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
- apply natToWord_wordToNat.
- Qed.
-
- Lemma wordToN_zero: forall w, wordToN (wzero w) = 0%N.
- Proof.
- intros.
- unfold wzero; rewrite wordToN_nat.
- rewrite wordToNat_natToWord_idempotent; simpl; intuition.
- apply Npow2_gt0.
- Qed.
-
- Fixpoint wbit {n} (x: word n) (k: nat): bool :=
- match n as n' return word n' -> bool with
- | O => fun _ => false
- | S m => fun x' =>
- match k with
- | O => (whd x')
- | S k' => wbit (wtl x') k'
- end
- end x.
-
- Lemma wbit_large {n} (x: word n) (k: nat)
- : n <= k -> wbit x k = false.
- Proof.
- revert k; induction x as [|b n x IHx], k; intro H; simpl; try reflexivity; try omega.
- apply IHx; omega.
- Qed.
-
- Lemma wbit_inj_iff {n} (x y : word n)
- : (forall k, wbit x k = wbit y k) <-> x = y.
- Proof.
- split; intro H; subst; try reflexivity.
- induction x.
- { revert dependent y.
- let G := match goal with |- forall y, @?G y => G end in
- intro y;
- refine (match y in word n return match n with
- | 0 => G
- | _ => fun _ => True
- end y
- with
- | WO => fun _ => eq_refl
- | _ => I
- end). }
- { move y at top; revert dependent n.
- let G := match goal with |- forall n y, @?G n y => G end in
- intros n y;
- refine (match y in word n return match n with
- | 0 => fun _ => True
- | S n' => G n'
- end y
- with
- | WO => I
- | _ => _
- end).
- intros x H IH.
- pose proof (H 0) as H0; simpl in H0; subst; f_equal.
- apply IH; intro k; specialize (H (S k)); apply H. }
- Qed.
-
- Lemma wbit_inj_iff_lt {n} (x y : word n)
- : (forall k, k < n -> wbit x k = wbit y k) <-> x = y.
- Proof.
- rewrite <- wbit_inj_iff.
- split; intros H k; specialize (H k);
- destruct (le_lt_dec n k);
- rewrite ?wbit_large by assumption;
- auto.
- Qed.
-
- Lemma wordToN_testbit: forall {n} (x: word n) k,
- N.testbit (wordToN x) k = wbit x (N.to_nat k).
- Proof.
- assert (forall x: N, match x with
- | 0%N => 0%N
- | N.pos q => N.pos (q~0)%positive
- end = N.double x) as kill_match by (
- induction x; simpl; intuition).
-
- induction n as [|n IHn]; intros x k.
-
- - shatter x; simpl; intuition.
-
- - revert IHn; rewrite <- (N2Nat.id k).
- generalize (N.to_nat k) as k'; intros k' IHn; clear k.
- rewrite Nat2N.id in *.
-
- induction k' as [|k' IHk'].
-
- + clear IHn; induction x as [|b ? x IHx]; simpl; intuition.
- destruct (wordToN x), b; simpl; intuition.
-
- + clear IHk'.
- shatter x; simpl.
-
- rewrite kill_match.
- replace (N.pos (Pos.of_succ_nat k'))
- with (N.succ (N.of_nat k'))
- by (rewrite <- Nat2N.inj_succ;
- simpl; intuition).
-
- rewrite N.double_spec.
- replace (N.succ (2 * wordToN (wtl x)))
- with (2 * wordToN (wtl x) + 1)%N
- by nomega.
-
- destruct (whd x);
- try rewrite N.testbit_odd_succ;
- try rewrite N.testbit_even_succ;
- let k' := k' in
- try abstract (
- unfold N.le; simpl;
- induction (N.of_nat k'); intuition;
- match goal with H : _ |- _ => solve [ inversion H ] end);
- rewrite IHn;
- rewrite Nat2N.id;
- reflexivity.
- Qed.
-
- Lemma wbit_NToWord {sz} k v
- : wbit (NToWord sz v) k = if Nat.ltb k sz
- then N.testbit v (N.of_nat k)
- else false.
- Proof.
- revert k v; induction sz as [|sz IHsz], k; intros v **; try reflexivity.
- { destruct v as [|p]; simpl; try reflexivity.
- destruct p; simpl; reflexivity. }
- { pose proof (fun v k => IHsz k (Npos v)) as IHszp.
- pose proof (fun k => IHsz k 0%N) as IHsz0.
- destruct v as [|p]; simpl in *.
- { rewrite IHsz0; break_match; reflexivity. }
- { destruct p; simpl in *; try (rewrite IHsz0; break_match; reflexivity);
- rewrite IHszp, N.pos_pred_spec;
- change (N.pos (Pos.of_succ_nat k)) with (N.of_nat (S k));
- rewrite <- Nat2N.inj_pred; simpl;
- reflexivity. } }
- Qed.
-
- Lemma NToWord_wordToN_NToWord_small : forall sz1 sz2 w,
- (wordToN (NToWord sz2 w) < 2^N.of_nat sz1)%N
- -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w.
- Proof.
- intros sz1 sz2 w H.
- apply wbit_inj_iff_lt; intros k Hlt.
- rewrite !wbit_NToWord, wordToN_testbit, wbit_NToWord, Nat2N.id.
- destruct (N.eq_dec (wordToN (NToWord sz2 w)) 0) as [H'|H'];
- [ apply N.bits_inj_iff in H'; specialize (H' (N.of_nat k));
- rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'; simpl in *
- | assert (H'' : sz1 <= k -> N.testbit (wordToN (NToWord sz2 w)) (N.of_nat k) = false);
- [ intro;
- apply N.log2_lt_pow2 in H; [ | lia.. ]
- | rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'' ] ];
- break_match; try reflexivity;
- repeat match goal with
- | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
- | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
- | _ => omega
- | _ => congruence
- | _ => rewrite N.bits_above_log2 by lia
- | _ => solve [ symmetry; auto ]
- end.
- Qed.
-
- Lemma NToWord_wordToN_NToWord : forall sz1 sz2 w,
- sz2 <= sz1 -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w.
- Proof.
- intros.
- apply wbit_inj_iff_lt; intros k Hlt.
- rewrite !wbit_NToWord, wordToN_testbit, wbit_NToWord, Nat2N.id.
- break_match; try reflexivity;
- repeat match goal with
- | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
- | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
- | _ => omega
- end.
- Qed.
-
- Lemma wordToN_NToWord_wordToN : forall sz1 sz2 w, (sz1 <= sz2)%nat -> wordToN (NToWord sz2 (@wordToN sz1 w)) = wordToN w.
- Proof.
- intros sz1 sz2 w H.
- apply N.bits_inj; intro k.
- rewrite !wordToN_testbit, !wbit_NToWord, wordToN_testbit, N2Nat.id.
- destruct (N.to_nat k <? sz2) eqn:H'; try reflexivity.
- apply Nat.ltb_ge in H'.
- rewrite wbit_large by omega.
- reflexivity.
- Qed.
-
- Lemma wordToN_NToWord_mod : forall sz w, wordToN (NToWord sz w) = N.modulo w (2^N.of_nat sz).
- Proof.
- intros.
- apply N.bits_inj; intro k.
- repeat match goal with
- | _ => reflexivity
- | _ => progress rewrite ?wordToN_testbit, ?wbit_NToWord, ?N2Nat.id
- | _ => rewrite N.mod_pow2_bits_low by lia
- | _ => rewrite N.mod_pow2_bits_high by lia
- | _ => progress break_match
- | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
- | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
- | _ => omega
- end.
- Qed.
-
- Lemma wordToN_split1: forall {n m} x,
- wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)).
- Proof.
- intros n m x.
-
- pose proof (Word.combine_split _ _ x) as C; revert C.
- generalize (split1 n m x) as a, (split2 n m x) as b.
- intros a b C; rewrite <- C; clear C x.
-
- apply N.bits_inj_iff; unfold N.eqf; intro x.
- rewrite N.land_spec.
- repeat rewrite wordToN_testbit.
- revert x a b.
-
- induction n as [|n IHn], m; intros;
- shatter a; shatter b;
- induction (N.to_nat x) as [|n0];
- try rewrite <- (Nat2N.id n0);
- try rewrite andb_false_r;
- try rewrite andb_true_r;
- simpl; intuition.
- Qed.
-
- Lemma wordToN_split2: forall {n m} x,
- wordToN (@split2 n m x) = N.shiftr (wordToN x) (N.of_nat n).
- Proof.
- intros n m x.
-
- pose proof (Word.combine_split _ _ x) as C; revert C.
- generalize (split1 n m x) as a, (split2 n m x) as b.
- intros a b C.
- rewrite <- C; clear C x.
-
- apply N.bits_inj_iff; unfold N.eqf; intro x;
- rewrite N.shiftr_spec;
- repeat rewrite wordToN_testbit;
- try apply N_ge_0.
-
- revert x a b.
- induction n as [|n IHn], m; intros;
- shatter a;
- try apply N_ge_0.
-
- - simpl; intuition.
-
- - replace (x + N.of_nat 0)%N with x by nomega.
- simpl; intuition.
-
- - rewrite (IHn x (wtl a) b).
- rewrite <- (N2Nat.id x).
- repeat rewrite <- Nat2N.inj_add.
- repeat rewrite Nat2N.id; simpl.
- replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega.
- reflexivity.
-
- - rewrite (IHn x (wtl a) b).
- rewrite <- (N2Nat.id x).
- repeat rewrite <- Nat2N.inj_add.
- repeat rewrite Nat2N.id; simpl.
- replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega.
- reflexivity.
- Qed.
-
- Lemma wordToN_wones: forall x, wordToN (wones x) = N.ones (N.of_nat x).
- Proof.
- induction x as [|x IHx].
-
- - simpl; intuition.
-
- - rewrite Nat2N.inj_succ.
- replace (wordToN (wones (S x))) with (2 * wordToN (wones x) + N.b2n true)%N
- by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
- replace (N.ones (N.succ _))
- with (2 * N.ones (N.of_nat x) + N.b2n true)%N.
-
- + rewrite IHx; nomega.
-
- + replace (N.succ (N.of_nat x)) with (1 + (N.of_nat x))%N by (
- rewrite N.add_comm; nomega).
- rewrite N.ones_add.
- replace (N.ones 1) with 1%N by (
- unfold N.ones; simpl; intuition).
- simpl.
- reflexivity.
- Qed.
-
- Tactic Notation "replaceAt1" constr(x) "with" constr(y) "by" tactic(tac) :=
- let tmp := fresh in
- set (tmp := x) at 1;
- replace tmp with y by (unfold tmp; tac);
- clear tmp.
-
- Lemma wordToN_combine: forall {n m} a b,
- wordToN (@Word.combine n a m b)
- = N.lxor (N.shiftl (wordToN b) (N.of_nat n)) (wordToN a).
- Proof.
- intros n m a b; symmetry.
-
- replaceAt1 a with (Word.split1 _ _ (Word.combine a b))
- by (apply Word.split1_combine).
-
- replaceAt1 b with (Word.split2 _ _ (Word.combine a b))
- by (apply Word.split2_combine).
-
- generalize (Word.combine a b); intro x; clear a b.
-
- rewrite wordToN_split1, wordToN_split2, wordToN_wones.
- generalize (wordToN x); clear x; intro x.
- apply N.bits_inj_iff; unfold N.eqf; intro k.
- rewrite N.lxor_spec.
-
- destruct (Nge_dec k (N.of_nat n)).
-
- - rewrite N.shiftl_spec_high; try apply N_ge_0;
- [|apply N.ge_le; assumption].
- rewrite N.shiftr_spec; try apply N_ge_0.
- replace (k - N.of_nat n + N.of_nat n)%N with k by nomega.
- rewrite N.land_spec, N.ones_spec_high; [|apply N.ge_le; assumption].
- induction (N.testbit x k); cbv; reflexivity.
-
- - rewrite N.shiftl_spec_low; try assumption; try apply N_ge_0.
- rewrite N.land_spec, N.ones_spec_low; [|nomega].
- induction (N.testbit x k); cbv; reflexivity.
- Qed.
-
- Lemma NToWord_equal: forall n (x y: word n),
- wordToN x = wordToN y -> x = y.
- Proof.
- intros n x y H.
- rewrite <- (NToWord_wordToN _ x).
- rewrite <- (NToWord_wordToN _ y).
- rewrite H; reflexivity.
- Qed.
-
- Lemma Npow2_ignore: forall {n} (x: word n),
- x = NToWord _ (wordToN x + Npow2 n).
- Proof.
- intros n x.
- rewrite <- (NToWord_wordToN n x) at 1.
- repeat rewrite NToWord_nat.
- rewrite N2Nat.inj_add.
- rewrite Npow2_nat.
- replace (N.to_nat (wordToN x))
- with ((N.to_nat (wordToN x) + pow2 n) - 1 * pow2 n)
- by omega.
- rewrite drop_sub; f_equal; nomega.
- Qed.
-End WordToN.
-
-Section WordBounds.
- Lemma word_size_bound : forall {n} (w: word n), (wordToN w < Npow2 n)%N.
- Proof.
- intros n w; pose proof (wordToNat_bound w) as B;
- rewrite of_nat_lt in B;
- rewrite <- Npow2_nat in B;
- rewrite N2Nat.id in B;
- rewrite <- wordToN_nat in B;
- assumption.
- Qed.
-
- Lemma wordize_plus: forall {n} (x y: word n),
- (wordToN x + wordToN y < Npow2 n)%N
- -> (wordToN x + wordToN y)%N = wordToN (x ^+ y).
- Proof.
- intros n x y H.
- pose proof (word_size_bound x) as Hbx.
- pose proof (word_size_bound y) as Hby.
-
- unfold wplus, wordBin.
- rewrite wordToN_NToWord_idempotent; intuition.
- Qed.
-
- Lemma wordize_minus: forall {n} (x y: word n),
- (wordToN x >= wordToN y)%N
- -> (wordToN x - wordToN y)%N = wordToN (x ^- y).
- Proof.
- intros n x y H.
-
- destruct (Nge_dec 0%N (wordToN y)). {
- unfold wminus, wneg.
- replace (wordToN y) with 0%N in * by nomega.
- replace (Npow2 n - 0)%N with (wordToN (wzero n) + Npow2 n)%N
- by (rewrite wordToN_zero; nomega).
- rewrite <- Npow2_ignore.
- rewrite wplus_comm.
- rewrite wplus_unit.
- nomega.
- }
-
- assert (wordToN x - wordToN y < Npow2 n)%N. {
- transitivity (wordToN x);
- try apply word_size_bound;
- apply N.sub_lt;
- [apply N.ge_le|]; assumption.
- }
-
- assert (wordToN x - wordToN y + wordToN y < Npow2 n)%N. {
- replace (wordToN x - wordToN y + wordToN y)%N
- with (wordToN x) by nomega;
- apply word_size_bound.
- }
-
- assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. {
- apply NToWord_equal.
- rewrite <- wordize_plus; rewrite wordToN_NToWord_idempotent; try assumption.
- nomega.
- }
-
- symmetry.
- rewrite Hv at 1.
- unfold wminus.
- repeat rewrite <- wplus_assoc.
- rewrite wminus_inv.
- rewrite wplus_comm.
- rewrite wplus_unit.
- rewrite wordToN_NToWord_idempotent; try assumption.
- reflexivity.
- Qed.
-
- Lemma wordize_mult: forall {n} (x y: word n),
- (wordToN x * wordToN y < Npow2 n)%N
- -> (wordToN x * wordToN y)%N = wordToN (x ^* y).
- Proof.
- intros n x y H.
- pose proof (word_size_bound x) as Hbx.
- pose proof (word_size_bound y) as Hby.
-
- unfold wmult, wordBin.
- rewrite wordToN_NToWord_idempotent; intuition.
- Qed.
-
- Lemma wordize_and: forall {n} (x y: word n),
- wordToN (wand x y) = N.land (wordToN x) (wordToN y).
- Proof.
- intros n x y.
- apply N.bits_inj_iff; unfold N.eqf; intro k.
- rewrite N.land_spec.
- repeat rewrite wordToN_testbit.
- revert x y.
- generalize (N.to_nat k) as k'.
- induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|].
- induction k'; [reflexivity|].
- fold wand.
- rewrite IHn.
- reflexivity.
- Qed.
-
- Lemma wordize_or: forall {n} (x y: word n),
- wordToN (wor x y) = N.lor (wordToN x) (wordToN y).
- Proof.
- intros n x y.
- apply N.bits_inj_iff; unfold N.eqf; intro k.
- rewrite N.lor_spec.
- repeat rewrite wordToN_testbit.
- revert x y.
- generalize (N.to_nat k) as k'; clear k.
- induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|].
- induction k'; [reflexivity|].
- rewrite IHn.
- reflexivity.
- Qed.
-End WordBounds.
-
-Hint Rewrite NToWord_wordToN : pull_wordToN.
-
-Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
-Proof.
- intros x n bound_nat.
- rewrite <- Nnat.N2Nat.id, Npow2_nat.
- replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
- apply (Nat2N_inj_lt _ (pow2 n)).
- assumption.
-Qed.
-
-Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y.
-Proof.
- intros sz x y; split; intros.
- + intro eq_xy; apply weqb_true_iff in eq_xy; congruence.
- + case_eq (weqb x y); intros weqb_xy; auto.
- apply weqb_true_iff in weqb_xy.
- congruence.
-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.
-
-Lemma combine_eq_iff {a b} (A:word a) (B:word b) C :
- combine A B = C <-> A = split1 a b C /\ B = split2 a b C.
-Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed.
-
-Class wordsize_eq (x y : nat) := wordsize_eq_to_eq : x = y.
-Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
-Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
-Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
-
-Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
- := match x, y with
- | O, O => fun _ => eq_refl
- | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf))
- | _, _ => fun x => x
- end.
-
-Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
-Proof.
- induction n as [|n IHn]; [ reflexivity | simpl ].
- rewrite IHn; reflexivity.
-Qed.
-
-Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m :=
- match correct_wordsize_eq n m pf in _ = y return word n -> word y with
- | eq_refl => fun w => w
- end.
-
-Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed.
-
-Lemma wordToNat_cast_word {n} (w:word n) m pf :
- wordToNat (@cast_word n m pf w) = wordToNat w.
-Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
-
-Lemma wordToN_cast_word {n} (w:word n) m pf :
- wordToN (@cast_word n m pf w) = wordToN w.
-Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
-Hint Rewrite @wordToN_cast_word : push_wordToN.
-
-Import NPeano Nat.
-Local Infix "++" := combine.
-
-Definition zext_ge n {m} {pf:m <= n} (w:word m) : word n :=
- cast_word (w ++ wzero (n - m)).
-
-Definition keeplow {b} n (w:word b) : word b :=
- wand (cast_word( wones (min b n) ++ wzero (b-n) )) w.
-
-Definition clearlow {b} n (w:word b) : word b :=
- wand (cast_word( wzero (min b n) ++ wones (b-n) )) w.
-
-Definition setbit {b} n {H:n < b} (w:word b) : word b :=
- wor (cast_word( wzero n ++ wones 1 ++ wzero (b-n-1) )) w.
-
-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_combine : forall {a} (wa:word a) {b} (wb:word b),
- wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
-Proof.
- induction wa as [|??? IHwa]; intros; simpl; rewrite ?IHwa; break_match; nia.
-Qed.
-
-Lemma wordToNat_zext_ge {n m pf} (w:word m) : wordToNat (@zext_ge n m pf w) = wordToNat w.
-Proof.
- unfold zext_ge.
- rewrite wordToNat_cast_word, wordToNat_combine, wordToNat_wzero; nia.
-Qed.
-
-Lemma bitwp_combine {a b} f (x x' : word a) (y y' : word b)
- : bitwp f x x' ++ bitwp f y y' = bitwp f (x ++ y) (x' ++ y').
-Proof.
- revert x' y y'.
- induction x as [|b' n x IHx]; simpl.
- { intro x'; intros.
- refine match x' with
- | WO => _
- | _ => I
- end.
- reflexivity. }
- { intros x' y y'; rewrite IHx; clear IHx; revert x.
- refine match x' in word Sn return match Sn return word Sn -> _ with
- | 0 => fun _ => True
- | S _ => fun x' => forall x, WS (f b' (whd x')) (bitwp f (x ++ y) (wtl x' ++ y')) = WS (f b' (whd (x' ++ y'))) (bitwp f (x ++ y) (wtl (x' ++ y')))
- end x'
- with
- | WO => I
- | WS _ _ _ => fun _ => Logic.eq_refl
- end. }
-Qed.
-
-Lemma wand_combine {a b} (x : word a) (y : word b) (z : word (a + b))
- : (x ++ y) ^& z = ((x ^& split1 _ _ z) ++ (y ^& split2 _ _ z)).
-Proof.
- rewrite <- (combine_split _ _ z) at 1.
- unfold wand.
- rewrite bitwp_combine.
- reflexivity.
-Qed.
-
-Lemma wordToNat_clearlow {b} (c : nat) (x : Word.word b) :
- wordToNat (clearlow c x) = wordToNat x - (wordToNat x) mod (2^c).
-Proof.
- assert (2^c <> 0) by auto with arith.
- unfold clearlow.
- match goal with
- | [ |- context[@cast_word _ _ ?pf ?w] ]
- => generalize pf
- end.
- intro H'; revert x; destruct H'; intro x; rewrite cast_word_refl.
- rewrite <- (combine_split _ _ x) at 2 3.
- rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero.
- repeat match goal with H := _ |- _ => subst H end. (* only needed in 8.4 *)
- let min := match type of x with word (?min _ _ + _) => min end in
- repeat match goal with
- | [ |- context[?min' b c] ]
- => progress change min' with min
- end.
- generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl.
- apply Min.min_case_strong; intros Hbc x0 x1;
- pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1).
- { assert (b - c = 0) by omega.
- assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
- generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega; [].
- simpl; rewrite mul_0_r, add_0_r.
- rewrite mod_small by omega.
- omega. }
- { rewrite !(mul_comm (2^c)), mod_add, mod_small by omega.
- lia. }
-Qed.
-
-Lemma wordToNat_keeplow {b} (c : nat) (x : Word.word b) :
- wordToNat (keeplow c x) = (wordToNat x) mod (2^c).
-Proof.
- assert (2^c <> 0) by auto with arith.
- unfold keeplow.
- match goal with
- | [ |- context[@cast_word _ _ ?pf ?w] ]
- => generalize pf
- end.
- intro H'; revert x; destruct H'; intro x; rewrite cast_word_refl.
- repeat match goal with H := _ |- _ => subst H end. (* only needed in 8.4 *)
- let min := match type of x with word (?min _ _ + _) => min end in
- repeat match goal with
- | [ |- context[?min' b c] ]
- => progress change min' with min
- end.
- rewrite <- (combine_split _ _ x) at 2 3.
- rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero.
- generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl.
- apply Min.min_case_strong; intros Hbc x0 x1;
- pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1).
- { assert (b - c = 0) by omega.
- assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
- generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega.
- simpl; rewrite mul_0_r, add_0_r.
- rewrite mod_small by omega.
- omega. }
- { rewrite !(mul_comm (2^c)), mod_add, mod_small by omega.
- lia. }
-Qed.
-
-Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
-Proof.
- intro a; induction a as [|a IHa].
- { reflexivity. }
- { simpl; intros b w; rewrite IHa; clear IHa.
- rewrite (shatter_word w); simpl.
- change (2^a + (2^a + 0)) with (2 * 2^a).
- rewrite (mul_comm 2 (2^a)).
- assert (2^a <> 0) by auto with arith.
- destruct (whd w); try rewrite S_mod; try rewrite mul_mod_distr_r; omega. }
-Qed.
-
-Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
-Proof.
- unfold wfirstn.
- intros; rewrite wordToNat_split1.
- match goal with |- context[match ?x with _ => _ end] => generalize x end.
- intro H'; destruct H'.
- reflexivity.
-Qed.
-
-Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y.
-Proof.
- match goal with |- ?LHS = ?RHS => destruct LHS eqn:HL, RHS eqn:HR end;
- repeat match goal with
- | _ => reflexivity
- | _ => progress unfold not in *
- | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H
- | [ |- Z.eqb _ _ = true ] => apply Z.eqb_eq
- | [ H : context[Z.of_N _ = Z.of_N _] |- _ ] => rewrite N2Z.inj_iff in H
- | [ H : wordToN _ = wordToN _ |- _ ] => apply wordToN_inj in H
- | [ H : x = y :> word _ |- _ ] => apply weqb_true_iff in H
- | [ H : ?x = false |- _ ] => progress rewrite <- H; clear H
- | _ => congruence
- | [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst
- end.
-Qed.
-
-Section Bounds.
- Local Notation bounds_2statement wop Zop := (forall {sz} (x y : word sz),
- (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))
- -> (Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz)
- -> (Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))))%Z).
-
- Lemma wordToN_wplus : bounds_2statement (@wplus _) Z.add.
- Proof.
- intros sz x y H H0.
- rewrite <- wordize_plus; [rewrite N2Z.inj_add; reflexivity|].
- destruct (N.eq_dec (wordToN x + wordToN y) 0%N) as [e|e];
- [rewrite e; apply Npow2_gt0|].
- apply N.neq_0_lt_0 in e.
- apply N2Z.inj_lt in e.
- apply N2Z.inj_lt.
- rewrite N2Z.inj_add in *.
- rewrite Npow2_N.
- rewrite N2Z.inj_pow.
- replace (Z.of_N 2%N) with 2%Z by auto.
- apply Z.log2_lt_pow2; [auto|].
- rewrite nat_N_Z.
- assumption.
- Qed.
-
- Lemma wordToN_wminus : bounds_2statement (@wminus _) Z.sub.
- Proof.
- intros sz x y H ?.
- assert (wordToN y <= wordToN x)%N. {
- apply N2Z.inj_le.
- rewrite <- (Z.add_0_l (Z.of_N (wordToN y))).
- apply Z.le_add_le_sub_r; assumption.
- }
-
- rewrite <- N2Z.inj_sub; [|assumption].
- rewrite <- wordize_minus; [reflexivity|apply N.le_ge; assumption].
- Qed.
-
- Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul.
- Proof.
- intros sz x y H H0.
- rewrite <- wordize_mult; [rewrite N2Z.inj_mul; reflexivity|].
- destruct (N.eq_dec (wordToN x * wordToN y) 0%N) as [e|e];
- [rewrite e; apply Npow2_gt0|].
- apply N.neq_0_lt_0 in e.
- apply N2Z.inj_lt in e.
- apply N2Z.inj_lt.
- rewrite N2Z.inj_mul in *.
- rewrite Npow2_N.
- rewrite N2Z.inj_pow.
- replace (Z.of_N 2%N) with 2%Z by auto.
- apply Z.log2_lt_pow2; [auto|].
- rewrite nat_N_Z.
- assumption.
- Qed.
-
- Lemma wordToN_wand : bounds_2statement (@wand _) Z.land.
- Proof.
- intros.
- rewrite wordize_and.
- apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
- rewrite Z.land_spec.
- rewrite Z2N.inj_testbit; [|apply Z.ge_le; assumption].
- rewrite N.land_spec.
- repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]).
- reflexivity.
- Qed.
-
- Lemma wordToN_wor : bounds_2statement (@wor _) Z.lor.
- Proof.
- intros.
- rewrite wordize_or.
- apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
- rewrite Z.lor_spec.
- rewrite Z2N.inj_testbit; [|apply Z.ge_le; assumption].
- rewrite N.lor_spec.
- repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]).
- reflexivity.
- Qed.
-End Bounds.
-
-Hint Rewrite @wordToN_wplus using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wplus using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wminus using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wminus using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wand using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wand using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN.
-
-Section Updates.
- Local Notation bound n lower value upper := (
- (0 <= lower)%Z
- /\ (lower <= Z.of_N (@wordToN n value))%Z
- /\ (Z.of_N (@wordToN n value) <= upper)%Z
- /\ (Z.log2 upper < Z.of_nat n)%Z).
-
- Definition valid_update n lowerF valueF upperF : Prop :=
- forall lower0 value0 upper0
- lower1 value1 upper1,
-
- bound n lower0 value0 upper0
- -> bound n lower1 value1 upper1
- -> (0 <= lowerF lower0 upper0 lower1 upper1)%Z
- -> (Z.log2 (upperF lower0 upper0 lower1 upper1) < Z.of_nat n)%Z
- -> bound n (lowerF lower0 upper0 lower1 upper1)
- (valueF value0 value1)
- (upperF lower0 upper0 lower1 upper1).
-
- Local Ltac add_mono :=
- etransitivity; [| apply Z.add_le_mono_r; eassumption]; omega.
-
- Lemma add_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => l0 + l1)%Z
- (@wplus n)
- (fun l0 u0 l1 u1 => u0 + u1)%Z.
- Proof.
- unfold valid_update; intros until upper1; intros B0 B1 H0 H1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1.
- repeat split; [add_mono| | |assumption]; (
- rewrite wordToN_wplus; [add_mono|add_mono|];
- eapply Z.le_lt_trans; [| eassumption];
- apply Z.log2_le_mono; add_mono).
- Qed.
-
- Local Ltac sub_mono :=
- etransitivity;
- [| apply Z.sub_le_mono_r]; eauto;
- first [ reflexivity
- | apply Z.sub_le_mono_l; assumption
- | apply Z.le_add_le_sub_l; etransitivity; [|eassumption];
- repeat rewrite Z.add_0_r; assumption].
-
- Lemma sub_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => l0 - u1)%Z
- (@wminus n)
- (fun l0 u0 l1 u1 => u0 - l1)%Z.
- Proof.
- unfold valid_update; intros until upper1; intros B0 B1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1.
- repeat split; [sub_mono| | |assumption]; (
- rewrite wordToN_wminus; [sub_mono|omega|];
- eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]; sub_mono).
- Qed.
-
- Local Ltac mul_mono :=
- etransitivity; [|apply Z.mul_le_mono_nonneg_r];
- repeat (instantiate; first
- [ eassumption
- | reflexivity
- | apply Z.mul_le_mono_nonneg_l
- | rewrite Z.mul_0_l
- | omega]).
-
- Lemma mul_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => l0 * l1)%Z
- (@wmult n)
- (fun l0 u0 l1 u1 => u0 * u1)%Z.
- Proof.
- unfold valid_update; intros until upper1; intros B0 B1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1.
- repeat split; [mul_mono| | |assumption]; (
- rewrite wordToN_wmult; [mul_mono|mul_mono|];
- eapply Z.le_lt_trans; [| eassumption];
- apply Z.log2_le_mono; mul_mono).
- Qed.
-
- Local Ltac solve_land_ge0 :=
- apply Z.land_nonneg; left; etransitivity; [|eassumption]; assumption.
-
- Local Ltac land_mono :=
- first [assumption | etransitivity; [|eassumption]; assumption].
-
- Lemma land_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => 0)%Z
- (@wand n)
- (fun l0 u0 l1 u1 => Z.min u0 u1)%Z.
- Proof.
- unfold valid_update; intros until upper1; intros B0 B1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
- repeat split; [reflexivity|apply N2Z.is_nonneg| |assumption].
- rewrite wordToN_wand; [|solve_land_ge0|].
-
- - destruct_min;
- (etransitivity; [|eassumption]); [|rewrite Z.land_comm];
- (apply Z.land_le; land_mono).
-
- - eapply Z.le_lt_trans; [apply Z.log2_land; land_mono|destruct_min]; (
- eapply Z.le_lt_trans; [apply Z.log2_le_mono; eassumption|];
- assumption).
- Qed.
-
- Local Ltac lor_mono :=
- first [assumption | etransitivity; [|eassumption]; assumption].
-
- Local Ltac lor_trans :=
- destruct_max; (
- eapply Z.le_lt_trans; [apply Z.log2_le_mono; eassumption|];
- assumption).
-
- Lemma lor_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => Z.max l0 l1)%Z
- (@wor n)
- (fun l0 u0 l1 u1 => 2^(Z.max (Z.log2_up (u0+1)) (Z.log2_up (u1+1))) - 1)%Z.
- Proof.
- unfold valid_update; intros until upper1; intros B0 B1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
- repeat split; [destruct_max; assumption| | |assumption].
-
- - rewrite wordToN_wor;
- [ destruct_max; [|rewrite Z.lor_comm];
- (etransitivity; [|apply Z.lor_lower]; lor_mono)
- | apply Z.lor_nonneg; split; lor_mono|].
-
- rewrite Z.log2_lor; [lor_trans|lor_mono|lor_mono].
-
- - rewrite wordToN_wor; [
- | apply Z.lor_nonneg; split; lor_mono
- | rewrite Z.log2_lor; [lor_trans|lor_mono|lor_mono]].
-
- destruct (Z_ge_dec upper0 upper1) as [g|g].
-
- + apply Z.ge_le in g; pose proof g as g'.
- apply -> (Z.add_le_mono_r upper1 upper0 1) in g'.
- apply Z.log2_up_le_mono, Z.max_l in g'.
- rewrite g'; clear g'.
-
- destruct (Z.le_ge_cases (Z.of_N (wordToN value0)) (Z.of_N (wordToN value1)));
- [|rewrite Z.lor_comm];
- apply Z.lor_le; lor_mono.
-
- + assert (upper1 >= upper0)%Z as g'' by omega; clear g.
- pose proof g'' as g; pose proof g'' as g'; clear g''.
- apply Z.ge_le in g; apply Z.ge_le in g'.
- apply -> (Z.add_le_mono_r upper0 upper1 1) in g'.
- apply Z.log2_up_le_mono, Z.max_r in g'.
- rewrite g'; clear g'.
-
- destruct (Z.le_ge_cases (Z.of_N (wordToN value0)) (Z.of_N (wordToN value1)));
- [|rewrite Z.lor_comm];
- apply Z.lor_le; lor_mono.
- Qed.
-
- Local Ltac shift_mono := repeat progress first
- [ eassumption
- | etransitivity; [|eassumption]].
-
- Lemma shr_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => Z.shiftr l0 u1)%Z
- (@wordBin N.shiftr n)
- (fun l0 u0 l1 u1 => Z.shiftr u0 l1)%Z.
- Proof.
- unfold valid_update, wordBin; intros until upper1; intros B0 B1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
-
- repeat split; [assumption| | |assumption];
- (rewrite wordToN_NToWord_idempotent; [|apply Npow2_Zlog2]; rewrite N2Z.inj_shiftr);
- [ | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]
- | | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]];
- apply Z.shiftr_le_mono; shift_mono.
- Qed.
-
- Lemma shl_valid_update: forall n,
- valid_update n
- (fun l0 u0 l1 u1 => Z.shiftl l0 l1)%Z
- (@wordBin N.shiftl n)
- (fun l0 u0 l1 u1 => Z.shiftl u0 u1)%Z.
- Proof.
- unfold valid_update, wordBin; intros until upper1; intros B0 B1.
- do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
-
- repeat split; [assumption| | |assumption];
- (rewrite wordToN_NToWord_idempotent; [|apply Npow2_Zlog2]; rewrite N2Z.inj_shiftl);
- [ | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]
- | | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]];
- apply Z.shiftl_le_mono; shift_mono.
- Qed.
-End Updates.
-
-Definition winit {sz} (x: word (sz + 1)): word sz :=
- split1 sz 1 x.
-
-Definition wlast {sz} (x: word (sz + 1)): bool :=
- whd (split2 sz 1 x).
-
-Arguments winit {_} _.
-Arguments wlast {_} _.
-
-Lemma combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
- @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
-Proof.
- intros sz a b c; split; unfold winit, wlast; intro H.
-
- - rewrite <- H.
- rewrite split1_combine, split2_combine.
- split; [reflexivity|].
- shatter b; simpl; f_equal.
- generalize (wtl b) as b'; intro;
- shatter b'; reflexivity.
-
- - destruct H as [H0 H1]; rewrite H0.
- replace b with (split2 sz 1 c); [apply combine_split|].
- rewrite H1.
- generalize (split2 sz 1 c) as b'; intro b'.
- shatter b'.
- generalize (wtl b') as b''; intro;
- shatter b''; reflexivity.
-Qed.
-
-Lemma winit_combine : forall sz a b, @winit sz (combine a b) = a.
-Proof.
- intros; unfold winit; rewrite split1_combine; reflexivity.
-Qed.
-
-Lemma wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
-Proof.
- intros; unfold wlast; rewrite split2_combine; cbv; reflexivity.
-Qed.
-
-(* TODO : automate *)
-Lemma WordNZ_split1 : forall {n m} w,
- Z.of_N (Word.wordToN (Word.split1 n m w)) = Z.pow2_mod (Z.of_N (Word.wordToN w)) (Z.of_nat n).
-Proof.
- intros n m w; unfold Z.pow2_mod.
- rewrite wordToN_split1.
- apply Z.bits_inj_iff'; intros k Hpos.
- rewrite Z.land_spec.
- repeat (rewrite Z2N.inj_testbit; [|assumption]).
- rewrite N.land_spec; f_equal.
- rewrite wordToN_wones.
-
- destruct (Nge_dec (Z.to_N k) (N.of_nat n)).
-
- - rewrite Z.ones_spec_high, N.ones_spec_high;
- [reflexivity|apply N.ge_le; assumption|split; [omega|]].
- apply Z2N.inj_le; [apply Nat2Z.is_nonneg|assumption|].
- etransitivity; [|apply N.ge_le; eassumption].
- apply N.eq_le_incl.
- induction n as [|n IHn]; simpl; reflexivity.
-
- - rewrite Z.ones_spec_low, N.ones_spec_low;
- [reflexivity|assumption|split; [omega|]].
- apply Z2N.inj_lt; [assumption|apply Nat2Z.is_nonneg|].
- eapply N.lt_le_trans; [eassumption|].
- apply N.eq_le_incl.
- induction n as [|n IHn]; simpl; reflexivity.
-Qed.
-
-(* TODO : automate *)
-Lemma WordNZ_split2 : forall {n m} w,
- Z.of_N (Word.wordToN (Word.split2 n m w)) = Z.shiftr (Z.of_N (Word.wordToN w)) (Z.of_nat n).
-Proof.
- intros n m w; unfold Z.pow2_mod.
- rewrite wordToN_split2.
- apply Z.bits_inj_iff'; intros k Hpos.
- rewrite Z2N.inj_testbit; [|assumption].
- rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption.
- rewrite Z2N.inj_testbit; [f_equal|omega].
- rewrite Z2N.inj_add; [f_equal|assumption|apply Nat2Z.is_nonneg].
- induction n as [|n IHn]; simpl; reflexivity.
-Qed.
-
-Lemma WordNZ_range : forall {n} B w,
- (2 ^ Z.of_nat n <= B)%Z ->
- (0 <= Z.of_N (@Word.wordToN n w) < B)%Z.
-Proof.
- intros n B w H.
- split; [apply N2Z.is_nonneg|].
- eapply Z.lt_le_trans; [apply N2Z.inj_lt; apply word_size_bound|].
- rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
- assumption.
-Qed.
-
-Lemma WordNZ_range_mono : forall {n} m w,
- (Z.of_nat n <= m)%Z ->
- (0 <= Z.of_N (@Word.wordToN n w) < 2 ^ m)%Z.
-Proof.
- intros n m w H.
- split; [apply N2Z.is_nonneg|].
- eapply Z.lt_le_trans; [apply N2Z.inj_lt; apply word_size_bound|].
- rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
- apply Z.pow_le_mono; [|assumption].
- split; simpl; omega.
-Qed.