From 81884333100fe69baa060f341e2a9f0c8caf9296 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Tue, 14 Jun 2016 23:25:40 -0400 Subject: first pseudo conversion lemma --- src/Assembly/Pseudize.v | 44 +++++++++++++ src/Assembly/Pseudo.v | 3 + src/Assembly/Wordize.v | 160 ++++++++++++++++++++++++++++++------------------ 3 files changed, 148 insertions(+), 59 deletions(-) create mode 100644 src/Assembly/Pseudize.v (limited to 'src/Assembly') diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v new file mode 100644 index 000000000..b5d1a2b95 --- /dev/null +++ b/src/Assembly/Pseudize.v @@ -0,0 +1,44 @@ +Require Export Bedrock.Word Bedrock.Nomega. +Require Import NArith List. +Require Import Pseudo State Wordize. + +Module Conversion. + Import Pseudo ListNotations StateCommon. + + Definition run {n m w s} (prog: @Pseudo w s n m) (inList: list (word w)) : list (word w) := + match (pseudoEval prog (inList, TripleM.empty N, None)) with + | Some (outList, _, _) => outList + | _ => [] + end. + + Lemma pseudo_plus: forall {w s n} (p0 p1: @Pseudo w s n 1) x out0 out1 b, + (b <= Npow2 w)%N + -> ((&out0)%w < b)%N + -> ((&out1)%w < (Npow2 w - b))%N + -> run p0 x = [out0] + -> run p1 x = [out1] + -> run (p0 :+: p1)%p x = [out0 ^+ out1]. + Proof. + intros; unfold run in *; simpl. + destruct (pseudoEval p0 _) as [r0|], (pseudoEval p1 _) as [r1|]. + destruct r0 as [r0 rc0], r1 as [r1 rc1]. + destruct r0 as [r0 rm0], r1 as [r1 rm1]. + + - subst; simpl. + destruct ((& out0)%w + (& out1)%w ?= Npow2 w)%N; simpl; + rewrite (wordize_plus out0 out1 b); try assumption; + rewrite NToWord_wordToN; intuition. + + - inversion H3. + + - inversion H2. + + - inversion H2. + Qed. + + Program Definition ex0: Program Unary32 := ($0 :-: $0)%p. + + Eval vm_compute in (run ex0 [natToWord _ 7]). + +End Conversion. + diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index ede9607cf..fb9402523 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -111,6 +111,7 @@ Module Pseudo <: Language. pseudoEval prog st = Some st'. Delimit Scope pseudo_notations with p. + Local Open Scope pseudo_notations. Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n. intros; exists (x mod n); @@ -172,5 +173,7 @@ Module Pseudo <: Language. Notation "n ::: A :():" := (PCall _ _ n A) (at level 65, left associativity) : pseudo_notations. + + Close Scope pseudo_notations. End Pseudo. diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v index df04a467c..8d0b86e8a 100644 --- a/src/Assembly/Wordize.v +++ b/src/Assembly/Wordize.v @@ -1,27 +1,31 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Compare_dec. +Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec Compare_dec. Require Import FunctionalExtensionality ProofIrrelevance. Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N. -Delimit Scope wordize_scope with wordize. -Open Scope wordize_scope. +Delimit Scope wordize_scope with w. +Local Open Scope wordize_scope. Notation "& x" := (wordToN x) (at level 30) : wordize_scope. Notation "** x" := (NToWord _ x) (at level 30) : wordize_scope. -Notation "$ x" := (natToWord x) (at level 30) : wordize_scope. Section Definitions. Definition convS {A B: Set} (x: A) (H: A = B): B := eq_rect A (fun B0 : Set => B0) x B H. - Definition take {k n: nat} (p: (k <= n)%nat) (w: word n): word k. + Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k. refine (split1 k (n - k) (convS w _)). abstract (replace n with (k + (n - k)) by omega; intuition). Defined. + Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k. + refine (split2 (n - k) k (convS w _)). + abstract (replace n with (k + (n - k)) by omega; intuition). + Defined. + Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n. refine (convS (zext w (n - k)) _). abstract (replace (k + (n - k)) with n by omega; intuition). @@ -29,19 +33,25 @@ Section Definitions. Definition shiftr {n} (w: word n) (k: nat): word n := match (le_dec k n) with - | left p => extend p (take p w) + | left p => extend p (high p w) | right _ => wzero n end. Definition mask {n} (k: nat) (w: word n): word n := match (le_dec k n) with - | left p => w ^& (extend p (wones k)) + | left p => extend p (low p w) | right _ => w end. End Definitions. Section WordizeUtil. + Lemma mask_wand : forall (n: nat) (x: word n) m b, + (& (mask (N.to_nat m) x) < b)%N + -> (& (x ^& (@NToWord n (N.ones m))) < b)%N. + Proof. + Admitted. + Lemma convS_id: forall A x p, x = (@convS A A x p). Proof. intros; unfold convS; vm_compute. @@ -161,6 +171,21 @@ Section WordizeUtil. - intros; rewrite <- natToWord_combine; intuition. 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; nomega. + + - intros. + replace (a + S b) with (S a + b) by intuition. + rewrite (IHb (S a)); simpl; clear IHb. + induction (Npow2 a), (Npow2 b); simpl; intuition. + rewrite Pos.mul_xO_r; intuition. + Qed. + End WordizeUtil. (** Wordization Lemmas **) @@ -244,6 +269,16 @@ Section Bounds. (& k < & k + 1)%N. Proof. intros; nomega. Qed. + Theorem constant_bound_nat : forall (n k: nat), + (N.of_nat k < Npow2 n)%N + -> (& (@natToWord n k) < (N.of_nat k) + 1)%N. + Proof. + intros. + rewrite wordToN_nat. + rewrite wordToNat_natToWord_idempotent; + try assumption; nomega. + Qed. + Lemma let_bound : forall {n} (x: word n) (f: word n -> word n) xb fb, (& x < xb)%N -> (forall x', & x' < xb -> & (f x') < fb)%N @@ -297,18 +332,25 @@ Section Bounds. Admitted. Theorem shiftr_bound : forall {n} (w : word n) b bits, - (&w <= b)%N - -> (&(shiftr w bits) <= N.shiftr_nat b bits)%N. + (&w < b)%N + -> (&(shiftr w bits) < N.succ (N.shiftr_nat b bits))%N. Proof. intros. - rewrite <- wordize_shiftr. - induction bits; unfold N.shiftr_nat in *; simpl; intuition. - revert IHbits; - generalize (nat_iter bits N.div2 (& w)), - (nat_iter bits N.div2 b); - clear; intros x y H. - - admit. (* Monotonicity of N.div2 *) + assert (& shiftr w bits <= N.shiftr_nat b bits)%N. { + rewrite <- wordize_shiftr. + induction bits; unfold N.shiftr_nat in *; simpl; intuition. + + - unfold N.le, N.lt in *; rewrite H; intuition; inversion H0. + + - revert IHbits; + generalize (nat_iter bits N.div2 (& w)), + (nat_iter bits N.div2 b); + clear; intros x y H. + + admit. (* Monotonicity of N.div2 *) + } + + apply N.le_lteq in H0; destruct H0; nomega. Qed. Theorem mask_bound : forall {n} (w : word n) m, @@ -316,19 +358,33 @@ Section Bounds. (&(mask m w) < Npow2 m)%N. Proof. intros. - unfold mask in *; destruct (le_dec m n); simpl. + unfold mask in *; destruct (le_dec m n); simpl; + try apply extend_bound. - - admit. + pose proof (word_size_bound w). + apply (N.le_lt_trans _ (Npow2 n) _). - - transitivity (Npow2 n); try assumption; try apply word_size_bound. - replace m with (n + (m - n)) by intuition. - replace (Npow2 n) with ((Npow2 n) * 1)%N by nomega. - replace (Npow2 (n + (m - n))) - with (Npow2 n * Npow2 (m - n))%N. + - unfold N.le, N.lt in *; rewrite H0; intuition; inversion H1. - + admit. + - clear H H0. + replace m with ((m - n) + n) by nomega. + replace (Npow2 n) with (1 * (Npow2 n))%N + by (rewrite N.mul_comm; nomega). + rewrite Npow2_split. + apply N.mul_lt_mono_pos_r. - + admit. + + apply Npow2_gt0. + + + assert (0 < m - n)%nat by omega. + induction (m - n); try inversion H; try abstract ( + simpl; replace 2 with (S 1) by omega; + apply N.lt_1_2). + + assert (0 < n1)%nat as Z by omega; apply IHn1 in Z. + apply (N.le_lt_trans _ (Npow2 n1) _). + + * admit. + * admit. Qed. Theorem mask_update_bound : forall {n} (w : word n) b m, @@ -336,28 +392,12 @@ Section Bounds. -> (&w < b)%N -> (&(mask m w) < (N.min b (Npow2 m)))%N. Proof. - intros. - pose proof (mask_bound w m H). - assert (&(mask m w) < b)%N. + intros; unfold mask, N.min; + destruct (le_dec m n), + (N.compare b (Npow2 m)); + simpl; try assumption. - - induction m. - - + replace (&(mask 0 w)) with 0%N by admit. - admit. - - + induction (&w); intuition. - - induction n; rewrite (shatter_word w) in *; - try inversion H; subst. - - + rewrite (shatter_word (wtl w)) in *. - replace (wtl (wtl w)) with WO in * by admit. - induction (whd w), (whd (wtl w)); simpl in *. - + - - - unfold N.min; destruct (b ?= Npow2 m)%N; - simpl; try assumption. - Qed. + Admitted. End Bounds. @@ -378,27 +418,28 @@ Ltac wordize_ast := Ltac lt_crush := try abstract (clear; vm_compute; intuition). (** Bounding Tactics **) + Ltac multi_apply0 A L := pose proof (L A). Ltac multi_apply1 A L := match goal with - | [ H: A <= ?b |- _] => pose proof (L A b H) + | [ H: A < ?b |- _] => pose proof (L A b H) end. Ltac multi_apply2 A B L := match goal with - | [ H1: A <= ?b1, H2: B <= ?b2 |- _] => pose proof (L A B b1 b2 H1 H2) + | [ H1: A < ?b1, H2: B < ?b2 |- _] => pose proof (L A B b1 b2 H1 H2) end. Ltac multi_recurse n T := match goal with - | [ H: T <= _ |- _] => idtac + | [ H: (T < _)%N |- _] => idtac | _ => is_var T; let T' := (eval cbv delta [T] in T) in multi_recurse n T'; match goal with - | [ H : T' <= ?x |- _ ] => - pose proof (H : T <= x) + | [ H : T' < ?x |- _ ] => + pose proof (H : T < x) end | _ => @@ -422,35 +463,34 @@ Ltac multi_recurse n T := | ?x ^& (@NToWord _ (N.ones ?m)) => multi_recurse n (mask (N.to_nat m) x); match goal with - | [ H: (mask (N.to_nat m) x) <= ?b |- _] => + | [ H: (& (mask (N.to_nat m) x) < ?b)%N |- _] => pose proof (@mask_wand n x m b H) end | shiftr ?w ?bits => multi_recurse n w; match goal with - | [ H: w <= ?b |- _] => + | [ H: (w < ?b)%N |- _] => pose proof (@shiftr_bound n w b bits H) end | NToWord _ ?k => pose proof (@constant_bound_N n k) | natToWord _ ?k => pose proof (@constant_bound_nat n k) - | ($ ?k) => pose proof (@constant_bound_nat n k) | _ => pose proof (@word_size_bound n T) end end. Lemma unwrap_let: forall {n} (y: word n) (f: word n -> word n) (b: N), - (let x := y in f x) <= b <-> let x := y in (f x <= b). + (&(let x := y in f x) < b)%N <-> let x := y in (&(f x) < b)%N. Proof. intuition. Qed. Ltac multi_bound n := match goal with | [|- let A := ?B in _] => multi_recurse n B; intro; multi_bound n - | [|- (let A := _ in _) <= _] => + | [|- ((let A := _ in _) < _)%N] => apply unwrap_let; multi_bound n - | [|- ?W <= _ ] => + | [|- (?W < _)%N ] => multi_recurse n W end. @@ -469,4 +509,6 @@ Module WordizationExamples. transitivity 10%N; try assumption; lt_crush. Qed. -End WordizationExamples. \ No newline at end of file +End WordizationExamples. + +Close Scope wordize_scope. -- cgit v1.2.3