diff options
Diffstat (limited to 'src/Assembly/WordizeUtil.v')
| -rw-r--r-- | src/Assembly/WordizeUtil.v | 996 |
1 files changed, 0 insertions, 996 deletions
diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v deleted file mode 100644 index b5f246fb1..000000000 --- a/src/Assembly/WordizeUtil.v +++ /dev/null @@ -1,996 +0,0 @@ -Require Import Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec. -Require Import List Omega NArith Nnat BoolEq Compare_dec. -Require Import SetoidTactics. -Require Import ProofIrrelevance FunctionalExtensionality. -Require Import QhasmUtil QhasmEvalCommon. - -(* Custom replace-at wrapper for 8.4pl3 compatibility *) -Definition ltac_nat_from_int (x:BinInt.Z) : nat := - match x with - | BinInt.Z0 => 0%nat - | BinInt.Zpos p => BinPos.nat_of_P p - | BinInt.Zneg p => 0%nat - end. - -Ltac nat_from_number N := - match type of N with - | nat => constr:(N) - | BinInt.Z => let N' := constr:(ltac_nat_from_int N) in eval compute in N' - end. - -Tactic Notation "replace'" constr(x) "with" constr(y) "at" constr(n) "by" tactic(tac) := - let tmp := fresh in ( - match nat_from_number n with - | 1 => set (tmp := x) at 1 - | 2 => set (tmp := x) at 2 - | 3 => set (tmp := x) at 3 - | 4 => set (tmp := x) at 4 - | 5 => set (tmp := x) at 5 - end; - replace tmp with y by (unfold tmp; tac); - clear tmp). - -(* Word-shattering tactic *) -Ltac shatter a := - let H := fresh in - pose proof (shatter_word a) as H; simpl in H; - try rewrite H in *; clear H. - -Section Misc. - Local Open Scope nword_scope. - - Lemma word_replace: forall n m, n = m -> word n = word m. - Proof. intros; subst; intuition. 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. - - Lemma to_nat_lt: forall x b, (x < b)%N <-> (N.to_nat x < N.to_nat b)%nat. - Proof. - intros x b; split; intro H. - - - unfold N.lt in H; rewrite N2Nat.inj_compare in H. - apply nat_compare_lt in H. - intuition. - - - unfold N.lt; rewrite N2Nat.inj_compare. - apply nat_compare_lt. - intuition. - Qed. - - Lemma to_nat_le: forall x b, (x <= b)%N <-> (N.to_nat x <= N.to_nat b)%nat. - Proof. - intros x b; split; intro H. - - - unfold N.le in H; rewrite N2Nat.inj_compare in H. - apply nat_compare_le in H. - intuition. - - - unfold N.le; rewrite N2Nat.inj_compare. - apply nat_compare_le. - intuition. - Qed. - - Lemma word_size_bound : forall {n} (w: word n), (&w < Npow2 n)%N. - Proof. - intros; 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 ge_to_le: forall (x y: N), (x >= y)%N <-> (y <= x)%N. - Proof. - intros x y; split; intro H; - unfold N.ge, N.le in *; - intro H0; contradict H; - rewrite N.compare_antisym; - rewrite H0; simpl; intuition. - Qed. - - 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 Pos_ge_1: forall p, (1 <= N.pos p)%N. - Proof. - intro. - replace (N.pos p) with (N.succ (N.pos p - 1)%N) by ( - induction p; simpl; - try rewrite Pos.succ_pred_double; - try reflexivity). - unfold N.succ. - apply N.le_pred_le_succ. - replace (N.pred 1%N) with 0%N by (simpl; intuition). - apply N_ge_0. - Qed. - - Lemma testbit_wones_false: forall n k, - (k >= N.of_nat n)%N - -> false = N.testbit (& wones n) k. - Proof. - induction n; try abstract (simpl; intuition). - induction k; try abstract ( - intro H; destruct H; simpl; intuition). - - intro H. - assert (N.pos p - 1 >= N.of_nat n)%N as Z. - apply ge_to_le; - apply ge_to_le in H; - apply (N.add_le_mono_r _ _ 1%N); - replace (N.of_nat n + 1)%N with (N.of_nat (S n)); - replace (N.pos p - 1 + 1)%N with (N.pos p); - try rewrite N.sub_add; - try assumption; - try nomega; - apply Pos_ge_1. - - rewrite (IHn (N.pos p - 1)%N Z) at 1. - - assert (N.pos p = N.succ (N.pos p - 1)) as Hp by ( - rewrite <- N.pred_sub; - rewrite N.succ_pred; - try abstract intuition; - intro H0; inversion H0). - - symmetry. - rewrite Hp at 1. - rewrite Hp in H. - - revert H; clear IHn Hp Z; - generalize (N.pos p - 1)%N as x; - intros x H. - - replace (& wones (S n)) with (2 * & (wones n) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - - rewrite N.testbit_succ_r; reflexivity. - Qed. - - Lemma testbit_wones_true: forall n k, - (k < N.of_nat n)%N - -> true = N.testbit (& wones n) k. - Proof. - induction n; intros k H; try nomega. - destruct (N.eq_dec k (N.of_nat n)). - - - clear IHn H; subst. - induction n. - - + simpl; intuition. - - + replace (& (wones (S (S n)))) - with (2 * (& (wones (S n))) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - rewrite Nat2N.inj_succ. - rewrite N.testbit_succ_r. - assumption. - - - induction k. - - + replace (& (wones (S n))) with (2 * (& (wones n)) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - rewrite N.testbit_0_r. - reflexivity. - - + assert (N.pos p < N.of_nat n)%N as IH by ( - rewrite Nat2N.inj_succ in H; - nomega). - apply N.lt_lt_pred in IH. - apply IHn in IH. - replace (N.pos p) with (N.succ (N.pred (N.pos p))) by ( - induction p; simpl; - try rewrite Pos.succ_pred_double; - intuition). - replace (& (wones (S n))) with (2 * (& (wones n)) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - rewrite N.testbit_succ_r. - assumption. - Qed. - - - Lemma plus_le: forall {n} (x y: word n), - (& (x ^+ y) <= &x + &y)%N. - Proof. - intros. - unfold wplus, wordBin. - rewrite wordToN_nat. - rewrite NToWord_nat. - pose proof (wordToNat_natToWord n (N.to_nat (& x + & y))) as H. - destruct H as [k H]. - destruct H as [Heq Hk]. - rewrite Heq. - rewrite Nat2N.inj_sub. - rewrite N2Nat.id. - generalize (&x + &y)%N; intro a. - generalize (N.of_nat (k * pow2 n))%N; intro b. - clear Heq Hk; clear x y k; clear n. - replace a with (a - 0)%N by nomega. - replace' (a - 0)%N with a at 1 by nomega. - apply N.sub_le_mono_l. - apply N_ge_0. - Qed. - - Lemma mult_le: forall {n} (x y: word n), - (& (x ^* y) <= &x * &y)%N. - Proof. - intros. - unfold wmult, wordBin. - rewrite wordToN_nat. - rewrite NToWord_nat. - pose proof (wordToNat_natToWord n (N.to_nat (& x * & y))) as H. - destruct H as [k H]. - destruct H as [Heq Hk]. - rewrite Heq. - rewrite Nat2N.inj_sub. - rewrite N2Nat.id. - generalize (&x * &y)%N; intro a. - generalize (N.of_nat (k * pow2 n))%N; intro b. - clear Heq Hk; clear x y k; clear n. - replace a with (a - 0)%N by nomega. - replace' (a - 0)%N with a at 1 by nomega. - apply N.sub_le_mono_l. - apply N_ge_0. - Qed. - - Lemma log2_conv: forall z, Z.log2 z = Z.of_N (N.log2 (Z.to_N z)). - Proof. - intro z; induction z as [| |p]; auto. - induction p; auto. - Qed. -End Misc. - -Section Exp. - Local Open Scope nword_scope. - - Lemma pow2_inv : forall n m, pow2 n = pow2 m -> n = m. - Proof. - induction n; intros; simpl in *; - induction m; simpl in *; try omega. - f_equal; apply IHn. - omega. - Qed. - - Lemma pow2_gt0 : forall n, (pow2 n > O)%nat. - Proof. induction n; simpl; omega. Qed. - - Lemma pow2_N_bound: forall n j, - (j < pow2 n)%nat -> (N.of_nat j < Npow2 n)%N. - Proof. - intros. - rewrite <- Npow2_nat in H. - unfold N.lt. - rewrite N2Nat.inj_compare. - rewrite Nat2N.id. - apply nat_compare_lt in H. - assumption. - Qed. - - Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N. - Proof. - intros; induction x. - - - 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_split: forall a b, - (Npow2 (a + b) = (Npow2 a) * (Npow2 b))%N. - Proof. - intros; revert a. - induction b. - - - intros; simpl; replace (a + 0) with a; try nomega. - rewrite N.mul_1_r; intuition. - - - intros. - replace (a + S b) with (S a + b) by omega. - rewrite (IHb (S a)); simpl; clear IHb. - induction (Npow2 a), (Npow2 b); simpl; intuition. - rewrite Pos.mul_xO_r; intuition. - Qed. - - Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N. - Proof. - induction n. - - - simpl; intuition. - - - rewrite Nat2N.inj_succ. - rewrite N.pow_succ_r; try apply N_ge_0. - rewrite <- IHn. - simpl; intuition. - Qed. - - Lemma Npow2_succ: forall n, (Npow2 (S n) = 2 * (Npow2 n))%N. - Proof. intros; simpl; induction (Npow2 n); intuition. Qed. - - Lemma Npow2_ordered: forall n m, (n <= m)%nat -> (Npow2 n <= Npow2 m)%N. - Proof. - induction n; 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 Exp. - -Section Conversions. - Local Open Scope nword_scope. - - Lemma NToWord_wordToN: forall sz x, NToWord sz (wordToN x) = x. - Proof. - intros. - rewrite NToWord_nat. - rewrite wordToN_nat. - rewrite Nat2N.id. - rewrite natToWord_wordToNat. - intuition. - Qed. - - Lemma NToWord_equal: forall n (x y: word n), - wordToN x = wordToN y -> x = y. - Proof. - intros. - rewrite <- (NToWord_wordToN _ x). - rewrite <- (NToWord_wordToN _ y). - rewrite H; reflexivity. - Qed. - - Lemma wordToN_NToWord: forall sz x, (x < Npow2 sz)%N -> wordToN (NToWord sz x) = x. - Proof. - intros. - rewrite NToWord_nat. - rewrite wordToN_nat. - rewrite <- (N2Nat.id x). - apply Nat2N.inj_iff. - rewrite Nat2N.id. - apply natToWord_inj with (sz:=sz); - try rewrite natToWord_wordToNat; - intuition. - - - apply wordToNat_bound. - - rewrite <- Npow2_nat; apply to_nat_lt; assumption. - Qed. - - Lemma Npow2_ignore: forall {n} (x: word n), - x = NToWord _ (& x + Npow2 n). - Proof. - intros. - rewrite <- (NToWord_wordToN n x) at 1. - repeat rewrite NToWord_nat. - rewrite N2Nat.inj_add. - rewrite Npow2_nat. - replace' (N.to_nat (&x)) - with ((N.to_nat (&x) + pow2 n) - 1 * pow2 n) - at 1 by omega. - rewrite drop_sub; [intuition|omega]. - Qed. -End Conversions. - -Section SpecialFunctions. - Local Open Scope nword_scope. - - Lemma convS_id: forall n x p, (@convS n n x p) = x. - Proof. - intros; unfold convS; vm_compute. - replace (convS_subproof n n x p) - with (eq_refl (word n)) by (apply proof_irrelevance). - reflexivity. - Qed. - - Lemma wordToN_convS: forall {n m} x p, - wordToN (@convS n m x p) = wordToN x. - Proof. - intros. - revert x. - rewrite p. - intro x. - rewrite convS_id. - reflexivity. - Qed. - - Lemma wordToN_zext: forall {n m} (x: word n), - wordToN (@zext n x m) = wordToN x. - Proof. - intros; induction x; simpl; intuition. - - - unfold zext, Word.combine. - rewrite wordToN_nat. - unfold wzero. - rewrite (@wordToNat_natToWord_idempotent m 0); simpl; intuition. - apply Npow2_gt0. - - - unfold zext in IHx; rewrite IHx; clear IHx; - destruct b; intuition. - Qed. - - Lemma wordToN_div2: forall {n} (x: word (S n)), - N.div2 (&x) = & (wtl x). - Proof. - intros. - pose proof (shatter_word x) as Hx; simpl in Hx; rewrite Hx; simpl. - destruct (whd x). - replace (match & wtl x with - | 0%N => 0%N - | N.pos q => N.pos (xO q) - end) - with (N.double (& (wtl x))) - by (induction (& (wtl x)); simpl; intuition). - - - rewrite N.div2_succ_double. - reflexivity. - - - induction (& (wtl x)); simpl; intuition. - 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_wtl: forall {n} (x: word (S n)) k, - wbit x (S k) = wbit (wtl x) k. - Proof. - intros. - pose proof (shatter_word x) as Hx; - simpl in Hx; rewrite Hx; simpl. - reflexivity. - Qed. - - Lemma wordToN_testbit: forall {n} (x: word n) k, - N.testbit (& 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; intros. - - - shatter x; simpl; intuition. - - - revert IHn; rewrite <- (N2Nat.id k). - generalize (N.to_nat k) as k'; intros; clear k. - rewrite Nat2N.id in *. - - induction k'. - - + clear IHn; induction x; simpl; intuition. - destruct (& x), b; simpl; intuition. - - + 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')) - by (rewrite <- Nat2N.inj_succ; - simpl; intuition). - - rewrite N.double_spec. - replace (N.succ (2 * & wtl x)) - with (2 * & wtl x + 1)%N - by nomega. - - destruct (whd x); - try rewrite N.testbit_odd_succ; - try rewrite N.testbit_even_succ; - try abstract ( - unfold N.le; simpl; - induction (N.of_nat k'); intuition; - try inversion H); - rewrite IHn; - rewrite Nat2N.id; - reflexivity. - Qed. - - Lemma wordToN_split1: forall {n m} x, - & (@split1 n m x) = N.land (& x) (& (wones n)). - Proof. - intros. - - 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, 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, - & (@split2 n m x) = N.shiftr (& x) (N.of_nat n). - Proof. - intros. - - 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, 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_combine: forall {n m} a b, - & (@Word.combine n a m b) = N.lxor (N.shiftl (& b) (N.of_nat n)) (& a). - Proof. - intros; symmetry. - - replace' a with (Word.split1 _ _ (Word.combine a b)) at 1 - by (apply Word.split1_combine). - - replace' b with (Word.split2 _ _ (Word.combine a b)) at 1 - by (apply Word.split2_combine). - - generalize (Word.combine a b); intro x; clear a b. - - rewrite wordToN_split1, wordToN_split2. - generalize (&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; - try (apply ge_to_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. - induction (N.testbit x k); - replace (N.testbit (& wones n) k) with false; - simpl; intuition; - try apply testbit_wones_false; - try assumption. - - - rewrite N.shiftl_spec_low; try assumption; try apply N_ge_0. - rewrite N.land_spec. - induction (N.testbit x k); - replace (N.testbit (& wones n) k) with true; - simpl; intuition; - try apply testbit_wones_true; - try assumption. - Qed. - - Lemma wordToN_wones: forall x, & (wones x) = N.ones (N.of_nat x). - Proof. - induction x. - - - simpl; intuition. - - - rewrite Nat2N.inj_succ. - replace (& wones (S x)) with (2 * & (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. - - 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. - - Lemma NToWord_zero: forall w, NToWord w 0%N = wzero w. - Proof. - intros. - unfold wzero; rewrite NToWord_nat. - f_equal. - Qed. - - Ltac propagate_wordToN := - unfold extend, low, high, break; - repeat match goal with - | [|- context[@wordToN _ (@convS _ _ _ _)] ] => - rewrite wordToN_convS - | [|- context[@wordToN _ (@split1 _ _ _)] ] => - rewrite wordToN_split1 - | [|- context[@wordToN _ (@split2 _ _ _)] ] => - rewrite wordToN_split2 - | [|- context[@wordToN _ (@combine _ _ _ _)] ] => - rewrite wordToN_combine - | [|- context[@wordToN _ (@zext _ _ _)] ] => - rewrite wordToN_zext - | [|- context[@wordToN _ (@wones _)] ] => - rewrite wordToN_wones - end. - - Lemma break_spec: forall (m n: nat) (x: word n) low high, - (low, high) = break m x - -> &x = (&high * Npow2 m + &low)%N. - Proof. - intros m n x low high H. - unfold break in H. - destruct (le_dec m n). - - - inversion H; subst; clear H. - propagate_wordToN. - rewrite N.land_ones. - rewrite N.shiftr_div_pow2. - replace (n - (n - m)) with m by omega. - rewrite N.mul_comm. - rewrite Npow2_N. - rewrite <- (N.div_mod' (& x) (2 ^ (N.of_nat m))%N). - reflexivity. - - - inversion H; subst; clear H. - propagate_wordToN; simpl; nomega. - Qed. - - Lemma extend_bound: forall k n (p: (k <= n)%nat) (w: word k), - (& (extend p w) < Npow2 k)%N. - Proof. - intros. - propagate_wordToN. - apply word_size_bound. - Qed. - - Lemma mask_spec : forall (n: nat) (x: word n) m, - & (mask (N.to_nat m) x) = (N.land (& x) (N.ones m)). - Proof. - intros; unfold mask. - destruct (le_dec (N.to_nat m) n). - - - propagate_wordToN. - rewrite N2Nat.id. - reflexivity. - - - rewrite N.land_ones. - rewrite N.mod_small; try reflexivity. - rewrite <- (N2Nat.id m). - rewrite <- Npow2_N. - apply (N.lt_le_trans _ (Npow2 n) _); try apply word_size_bound. - apply Npow2_ordered. - omega. - Qed. - - Lemma mask_bound : forall (n: nat) (x: word n) m, - (& (mask m x) < Npow2 m)%N. - Proof. - intros; unfold mask. - destruct (le_dec m n). - - - apply extend_bound. - - - apply (N.lt_le_trans _ (Npow2 n) _); try apply word_size_bound. - apply Npow2_ordered. - omega. - Qed. - -End SpecialFunctions. - -Section TopLevel. - Local Open Scope nword_scope. - - Coercion ind : bool >-> N. - - Lemma wordize_plus: forall {n} (x y: word n), - (&x + &y < Npow2 n)%N - -> (&x + &y)%N = & (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; intuition. - Qed. - - Lemma wordize_awc: forall {n} (x y: word n) (c: bool), - (&x + &y + c < Npow2 n)%N - -> (&x + &y + c)%N = &(addWithCarry x y c). - Proof. - intros n x y c H. - unfold wplus, wordBin, addWithCarry. - destruct c; simpl in *. - - - replace 1%N with (wordToN (natToWord n 1)) in * by ( - rewrite wordToN_nat; - rewrite wordToNat_natToWord_idempotent; - nomega). - - rewrite <- N.add_assoc. - rewrite wordize_plus; try nomega. - rewrite wordize_plus; try nomega. - - + rewrite wplus_assoc. - reflexivity. - - + apply (N.le_lt_trans _ (& x + & y + & natToWord n 1)%N _); - try assumption. - rewrite <- N.add_assoc. - apply N.add_le_mono. - - * apply N.eq_le_incl; reflexivity. - - * apply plus_le. - - - rewrite wplus_comm. - rewrite wplus_unit. - rewrite N.add_0_r in *. - apply wordize_plus; assumption. - Qed. - - Lemma wordize_minus: forall {n} (x y: word n), - (&x >= &y)%N -> (&x - &y)%N = &(x ^- y). - Proof. - intros n x y H. - - destruct (Nge_dec 0%N (&y)). { - unfold wminus, wneg. - replace (& y) with 0%N in * by nomega. - replace (Npow2 n - 0)%N with (& (wzero n) + Npow2 n)%N - by (rewrite wordToN_zero; nomega). - rewrite <- Npow2_ignore. - rewrite wplus_comm. - rewrite wplus_unit. - nomega. - } - - assert (& x - & y < Npow2 n)%N. { - transitivity (wordToN x); - try apply word_size_bound; - apply N.sub_lt; - [apply N.ge_le|]; assumption. - } - - assert (& x - & y + & y < Npow2 n)%N. { - replace (& x - & y + & 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; 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; try assumption. - reflexivity. - Qed. - - Lemma wordize_mult: forall {n} (x y: word n), - (&x * &y < Npow2 n)%N - -> (&x * &y)%N = &(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; intuition. - Qed. - - Lemma wordize_shiftr: forall {n} (x: word n) (k: nat), - (N.shiftr_nat (&x) k) = & (shiftr x k). - Proof. - intros n x k. - unfold shiftr, extend, high. - destruct (le_dec k n). - - - repeat first [ - rewrite wordToN_convS - | rewrite wordToN_zext - | rewrite wordToN_split2 ]. - rewrite <- Nshiftr_equiv_nat. - reflexivity. - - - rewrite (wordToN_nat (wzero n)); unfold wzero. - destruct (Nat.eq_dec n O); subst. - - + rewrite (shatter_word_0 x); simpl; intuition. - rewrite <- Nshiftr_equiv_nat. - rewrite N.shiftr_0_l. - reflexivity. - - + rewrite wordToNat_natToWord_idempotent; - try nomega. - - * pose proof (word_size_bound x). - rewrite <- Nshiftr_equiv_nat. - rewrite N.shiftr_eq_0_iff. - destruct (N.eq_dec (&x) 0%N) as [E|E]; - try rewrite E in *; - try abstract (left; reflexivity). - - right; split; try nomega. - apply (N.le_lt_trans _ (N.log2 (Npow2 n)) _). { - apply N.log2_le_mono. - apply N.lt_le_incl. - assumption. - } - - rewrite Npow2_N. - rewrite N.log2_pow2; try nomega. - apply N_ge_0. - - * simpl; apply Npow2_gt0. - Qed. - - Lemma wordize_and: forall {n} (x y: word n), - & (wand x y) = N.land (&x) (&y). - Proof. - intros. - 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'; clear k. - induction n; 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), - & (wor x y) = N.lor (&x) (&y). - Proof. - intros. - 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; intros; shatter x; shatter y; simpl; [reflexivity|]. - induction k'; [reflexivity|]. - rewrite IHn. - reflexivity. - Qed. - - Lemma conv_mask: forall {n} (x: word n) (k: nat), - (k <= n)%nat -> - mask k x = x ^& (NToWord _ (N.ones (N.of_nat k))). - Proof. - intros n x k H. - apply NToWord_equal. - - rewrite <- (Nat2N.id k). - rewrite mask_spec. - apply N.bits_inj_iff; unfold N.eqf; intro m. - rewrite N.land_spec. - repeat rewrite wordToN_testbit. - rewrite <- (N2Nat.id m). - rewrite <- wordToN_wones. - repeat rewrite wordToN_testbit. - repeat rewrite N2Nat.id. - rewrite <- wordToN_wones. - - assert (forall n (a b: word n) k, - wbit (a ^& b) k = andb (wbit a k) (wbit b k)) as Hwand. { - intros n0 a b. - induction n0 as [|n1]; - shatter a; shatter b; - simpl; try reflexivity. - - intro k0; induction k0 as [|k0]; - simpl; try reflexivity. - - fold wand. - rewrite IHn1. - reflexivity. - } - - rewrite Hwand; clear Hwand. - induction (wbit x (N.to_nat m)); - repeat rewrite andb_false_l; - repeat rewrite andb_true_l; - try reflexivity. - - repeat rewrite <- wordToN_testbit. - rewrite wordToN_NToWord; try reflexivity. - apply (N.lt_le_trans _ (Npow2 k) _). - - + apply word_size_bound. - - + apply Npow2_ordered. - omega. - Qed. - - Close Scope nword_scope. -End TopLevel. |