From 90d292593bb7bce72a30f43a4c202b6b4cbc7094 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Mon, 6 Jun 2016 13:47:27 -0400 Subject: Proper word-based vectorization Basic wordization lemmas Really complex derivation of wand correctness --- src/Assembly/Wordize.v | 343 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 306 insertions(+), 37 deletions(-) (limited to 'src/Assembly/Wordize.v') diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v index f08f1a940..b3beaacd3 100644 --- a/src/Assembly/Wordize.v +++ b/src/Assembly/Wordize.v @@ -1,58 +1,327 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Compare_dec Arith. -Require Import ProofIrrelevance Ring List. -Require Export MultiBoundedWord QhasmCommon. +Require Import NPeano NArith PArith Ndigits Nnat Pnat. +Require Import Arith Ring List Compare_dec Bool. +Require Import FunctionalExtensionality. -Import ListNotations. +Delimit Scope wordize_scope with wordize. +Local Open Scope wordize_scope. -(* Tuple Manipulations *) +Notation "& x" := (wordToNat x) (at level 30) : wordize_scope. -Fixpoint Tuple (T: Type) (n: nat): Type := - match n with - | O => T - | S m => (T * (Tuple T m))%type - end. +Lemma word_size_bound : forall {n} (w: word n), + (& w <= pow2 n - 1)%nat. +Proof. intros; assert (B := wordToNat_bound w); omega. Qed. -Definition just {T} (x: T): Tuple T O := x. +Lemma pow2_gt0 : forall x, (pow2 x > 0)%nat. +Proof. intros; induction x; simpl; intuition. Qed. -Definition cross {T n} (x: T) (tup: Tuple T n): Tuple T (S n) := (x, tup). +Lemma wordize_plus: forall {n} (x y: word n) (b: nat), + (&x <= b)%nat + -> (&y <= (pow2 n - b - 1))%nat + -> (&x + &y) = wordToNat (x ^+ y). +Proof. + intros; unfold wplus, wordBin; + repeat rewrite wordToN_nat in *; + repeat rewrite NToWord_nat in *; + rewrite <- Nat2N.inj_add; rewrite Nat2N.id. + + destruct (wordToNat_natToWord n (&x + &y)) as [k HW]; + destruct HW as [HW HK]; rewrite HW; clear HW. + + assert ((&x) + (&y) <= (pow2 n - 1))%nat by ( + pose proof (word_size_bound x); + pose proof (word_size_bound y); + omega). + + assert (k * pow2 n <= pow2 n - 1)%nat by omega. + + destruct k; subst; simpl in *; intuition; + clear H H0 H1 HK; + contradict H2. + + pose proof (pow2_gt0 n). + induction k; simpl; intuition. +Qed. + +Lemma wordize_mult: forall {n} (x y: word n) (b: nat), + (1 <= n)%nat + -> (&x <= b)%nat + -> (&y <= (pow2 n - 1) / b)%nat + -> (&x * &y)%nat = wordToNat (x ^* y). +Proof. + intros; unfold wmult, wordBin; + repeat rewrite wordToN_nat in *; + repeat rewrite NToWord_nat in *; + rewrite <- Nat2N.inj_mul; rewrite Nat2N.id. + + destruct (wordToNat_natToWord n (&x * &y)) as [k HW]; + destruct HW as [HW HK]; rewrite HW; clear HW. + + assert ((&x) * (&y) <= (pow2 n - 1))%nat. { + destruct (Nat.eq_dec b 0); subst; + try abstract (replace (&x) with 0 by intuition; omega). + + transitivity ((&x * (pow2 n - 1)) / b). { + transitivity (&x * ((pow2 n - 1) / b)). + + + apply Nat.mul_le_mono_nonneg_l; intuition. + + apply Nat.div_mul_le; assumption. + } + + transitivity ((b * (pow2 n - 1)) / (b * 1)). { + rewrite Nat.div_mul_cancel_l; intuition. + rewrite Nat.div_1_r. + apply Nat.div_le_upper_bound; intuition. + apply Nat.mul_le_mono_pos_r; intuition. + induction n; try inversion H; simpl; intuition. + pose proof (pow2_gt0 n). + omega. + } + + rewrite Nat.div_mul_cancel_l; intuition. + rewrite Nat.div_1_r; intuition. + } -Definition getLen {T n} (tup: Tuple T n) := (S n). + assert (k * (pow2 n) <= pow2 n - 1)%nat by omega. + + induction k; try omega. + + assert (pow2 n - 1 < S k * (pow2 n))%nat. { + destruct n; try inversion H; simpl; try omega. + pose proof (pow2_gt0 n). + induction k; try omega. + + transitivity (pow2 n + pow2 n + pow2 n); try omega. + replace (pow2 n + (pow2 n + 0) + S k * _) + with (pow2 n + pow2 n + pow2 n + + (pow2 n + k * (pow2 n + (pow2 n + 0)))). + apply Nat.lt_add_pos_r. + apply Nat.add_pos_nonneg; try omega; intuition. + + simpl; omega. + } + + contradict H3; omega. +Qed. + +Lemma testbit_pos0: forall p k, + testbit (Pos.to_nat p~0) k = + match k with | O => false | S k' => testbit (Pos.to_nat p) k' end. + intros; destruct k. + + - unfold testbit; simpl; intuition. + unfold odd; replace (even _) with true; intuition. + symmetry; apply even_spec. + exists (Pos.to_nat p). + replace (p~0)%positive with (2*p)%positive by intuition. + apply Pos2Nat.inj_mul. + + - rewrite (Pos2Nat.inj_xO); intuition. + rewrite Nat.testbit_even_succ; intuition. +Qed. + +Lemma testbit_pos1: forall p k, + testbit (Pos.to_nat p~1) k = + match k with | O => true | S k' => testbit (Pos.to_nat p) k' end. + intros; destruct k. + + - unfold testbit; simpl; intuition. + apply odd_spec; exists (Pos.to_nat p). + replace (p~1)%positive with (2*p + 1)%positive by intuition. + rewrite Pos2Nat.inj_add; rewrite Pos2Nat.inj_mul; intuition. + + - rewrite (Pos2Nat.inj_xI); intuition. + replace (S (2 * Pos.to_nat p)) with ((2 * Pos.to_nat p) + 1) by intuition. + rewrite Nat.testbit_odd_succ; intuition. +Qed. + +Lemma testbit_zero: testbit 0 = (fun (_: nat) => false). + apply functional_extensionality; intros; + rewrite testbit_0_l; intuition. +Qed. -Fixpoint tget' {T n} (tup: Tuple T n) (x: nat): T. - induction x, n; try exact tup. +Definition even_dec (x: nat): {exists x', x = 2*x'} + {exists x', x = 2*x' + 1}. + refine (if (bool_dec (odd x) true) then right _ else left _). - exact (fst tup). - exact (tget' _ _ (snd tup) x). + - apply odd_spec in _H; destruct _H; exists x0. abstract intuition. + - unfold odd in _H. + assert (even x = true) by abstract (destruct (even x); intuition). + apply even_spec in H; destruct H; exists x0; abstract intuition. Defined. -Definition tget {T n} (tup: Tuple T n) (x: nat): T := - tget' tup (n - x). +Lemma testbit_spec: forall (n x y: nat), (x < pow2 n)%nat -> (y < pow2 n)%nat -> + (forall k, (k < n)%nat -> testbit x k = testbit y k) -> x = y. +Proof. + intro n; induction n; intros. simpl in *; omega. + destruct (even_dec x) as [px|px], (even_dec y) as [py|py]; + destruct px as [x' px], py as [y' py]; + rewrite px in *; rewrite py in *; + clear x y px py; + replace (pow2 (S n)) with (2 * (pow2 n)) in * by intuition; + assert (x' < pow2 n)%nat by intuition; + assert (y' < pow2 n)%nat by intuition. + + - apply Nat.mul_cancel_l; intuition. + apply IHn; intuition. + assert (S k < S n)%nat as Z by intuition. + pose proof (H1 (S k) Z); intuition. + repeat rewrite testbit_even_succ in H5; intuition. + + - assert (0 < S n)%nat as Z by intuition. + apply (H1 0) in Z. + rewrite testbit_even_0 in Z; + rewrite testbit_odd_0 in Z; + inversion Z. + + - assert (0 < S n)%nat as Z by intuition. + apply (H1 0) in Z. + rewrite testbit_even_0 in Z; + rewrite testbit_odd_0 in Z; + inversion Z. -Lemma tget_inc: forall {T k} (x: nat) (v: T) (tup: Tuple T k), - (x <= k)%nat -> tget tup x = tget (cross v tup) x. + - apply Nat.add_cancel_r; apply Nat.mul_cancel_l; intuition. + apply IHn; intuition. + assert (S k < S n)%nat as Z by intuition. + pose proof (H1 (S k) Z); intuition. + repeat rewrite testbit_odd_succ in H5; intuition. +Qed. + +Lemma odd_def0: forall x, odd (S (x*2)) = true. +Proof. intros; intuition. apply odd_spec. exists x. omega. Qed. + +Lemma odd_def1: forall x, odd (x * 2) = false. Proof. - intros; unfold cross, tget. - replace (S k - x) with (S (k - x)) by intuition. - unfold tget'; simpl; intuition. + intros; intuition; unfold odd. + replace (even _) with true; intuition; symmetry. + rewrite even_spec. + exists x. omega. Qed. -Ltac tupleize n := - repeat match goal with - | [T: Tuple _ ?k, w: word n |- _] => let H := fresh in - replace w with (tget (cross w T) (S k)) by (simpl; intuition); +Inductive BinF := | binF: forall (a b c d: bool), BinF. + +Definition applyBinF (f: BinF) (x y: bool) := + match f as f' return f = f' -> _ with + | binF a b c d => fun _ => + if x + then if y + then a + else b + else if y + then c + else d + end eq_refl. + +Definition boolToBinF (f: bool -> bool -> bool): {g: BinF | f = applyBinF g}. + intros; exists (binF (f true true) (f true false) (f false true) (f false false)); + abstract ( + apply functional_extensionality; intro x; + apply functional_extensionality; intro y; + destruct x, y; unfold applyBinF; simpl; intuition). +Qed. + +Lemma testbit_odd_succ': forall x k, testbit (S (x * 2)) (S k) = testbit x k. + intros. + replace (S (x * 2)) with ((2 * x) + 1) by omega. + apply testbit_odd_succ. +Qed. + +Lemma testbit_even_succ': forall x k, testbit (x * 2) (S k) = testbit x k. + intros; replace (x * 2) with (2 * x) by omega; apply testbit_even_succ. +Qed. + +Lemma testbit_odd_zero': forall x, testbit (S (x * 2)) 0 = true. + intros. + replace (S (x * 2)) with ((2 * x) + 1) by omega. + apply testbit_odd_0. +Qed. + +Lemma testbit_even_zero': forall x, testbit (x * 2) 0 = false. + intros; replace (x * 2) with (2 * x) by omega; apply testbit_even_0. +Qed. + +Lemma testbit_bitwp: forall {n} (x y: word n) f k, (k < n)%nat -> + testbit (wordToNat (bitwp f x y)) k = f (testbit (&x) k) (testbit (&y) k). +Proof. + intros. - assert (forall m, (m <= k)%nat -> tget T m = tget (cross w T) m) as H - by (intros; apply tget_inc; intuition); - repeat rewrite H by intuition; + pose proof (shatter_word x); + pose proof (shatter_word y); + simpl in *. - generalize (cross w T); clear w T H; intro T + induction n. inversion H. clear IHn; rewrite H0, H1; clear H0 H1; simpl. - | [w: word n |- _] => - replace w with (tget (just w) O) by (simpl; intuition); - generalize (just w); clear w; let T := fresh in intro T - end. + replace f with (applyBinF (proj1_sig (boolToBinF f))) in * + by (destruct (boolToBinF f); simpl; intuition); + generalize (boolToBinF f) as g; intro g; + destruct g as [g pg]; simpl; clear pg f. -(* Conversion from nvec functions to wvec functions *) + revert x y H; generalize k n; clear k n; induction k, n; + intros; try omega. + - destruct g as [a b c d], (whd x), (whd y); + destruct a, b, c, d; unfold applyBinF in *; clear H; + repeat rewrite testbit_odd_zero'; + repeat rewrite testbit_even_zero'; + reflexivity. + + - destruct g as [a b c d], (whd x), (whd y); + destruct a, b, c, d; unfold applyBinF in *; clear H; + repeat rewrite testbit_odd_zero'; + repeat rewrite testbit_even_zero'; + reflexivity. + + - assert (k < S n)%nat as HB by omega; + pose proof (IHk n (wtl x) (wtl y) HB) as Z; clear HB IHk. + + assert (forall {m} (w: word (S m)), + &w = if whd w + then S (& wtl w * 2) + else & wtl w * 2) as r0. { + clear H Z x y; intros. + pose proof (shatter_word w); simpl in H; rewrite H; clear H; simpl. + destruct (whd w); intuition. + } repeat rewrite <- r0 in Z; clear r0. + + assert (forall {m} (a b: word (S m)), + & bitwp (applyBinF g) a b + = if applyBinF g (whd a) (whd b) + then S (& bitwp (applyBinF g) (wtl a) (wtl b) * 2) + else & bitwp (applyBinF g) (wtl a) (wtl b) * 2) as r1. { + clear H Z x y; intros. + pose proof (shatter_word a); pose proof (shatter_word b); + simpl in *; rewrite H; rewrite H0; clear H H0; simpl. + destruct (applyBinF g (whd a) (whd b)); intuition. + } repeat rewrite <- r1 in Z; clear r1. + + destruct g as [a b c d], (whd x), (whd y); + destruct a, b, c, d; unfold applyBinF in *; clear H; + repeat rewrite testbit_odd_succ'; + repeat rewrite testbit_even_succ'; + assumption. +Qed. + +(* (forall k, testbit x k = testbit y k) <-> x = y. *) +Lemma wordize_and: forall {n} (x y: word n), + (Nat.land (&x) (&y))%nat = & (x ^& y). +Proof. + intros n x y. + pose proof (pow2_gt0 n). + assert (&x < pow2 n)%nat by (pose proof (word_size_bound x); intuition). + assert (&y < pow2 n)%nat by (pose proof (word_size_bound y); intuition). + apply (testbit_spec n). + + - induction n. + + + simpl in *; intuition. + replace (&x) with 0 by intuition. + replace (&y) with 0 by intuition. + simpl; intuition. + + + admit. + + - pose (word_size_bound (x ^& y)); intuition. + + - intros; rewrite land_spec. + unfold wand; rewrite testbit_bitwp; intuition. +Qed. -- cgit v1.2.3