From 9523198cd20dc209bb62c52746accb69d59c7e4c Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Wed, 22 Jun 2016 20:23:31 -0400 Subject: Add Pseudize, Vectorize, Wordize to the build process --- _CoqProject | 3 +++ src/Assembly/Pseudize.v | 53 +++++++++++++++++++++++++++++++++++------------- src/Assembly/Vectorize.v | 11 ++++++---- src/Assembly/Wordize.v | 40 ++++++++++++++++-------------------- 4 files changed, 66 insertions(+), 41 deletions(-) diff --git a/_CoqProject b/_CoqProject index c9d56d0fc..a8e3d66ff 100644 --- a/_CoqProject +++ b/_CoqProject @@ -57,3 +57,6 @@ src/Assembly/PseudoConversion.v src/Assembly/AlmostConversion.v src/Assembly/StringConversion.v src/Assembly/Pipeline.v +src/Assembly/Vectorize.v +src/Assembly/Wordize.v +src/Assembly/Pseudize.v diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index 3a66484ee..0ef1dd765 100644 --- a/src/Assembly/Pseudize.v +++ b/src/Assembly/Pseudize.v @@ -1,5 +1,5 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith NPeano List Sumbool Compare_dec. +Require Import NArith NPeano List Sumbool Compare_dec Omega. Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State. Require Export Wordize Vectorize. @@ -9,6 +9,16 @@ Module Conversion. Hint Unfold setList getList getVar setCarry setCarryOpt getCarry getMem setMem overflows. + Lemma eval_in_length: forall {w s n m} x M c x' M' c' p, + @pseudoEval n m w s p (x, M, c) = Some (x', M', c') + -> Datatypes.length x = n. + Admitted. + + Lemma eval_out_length: forall {w s n m} x M c x' M' c' p, + @pseudoEval n m w s p (x, M, c) = Some (x', M', c') + -> Datatypes.length x' = m. + Admitted. + Lemma pseudo_var: forall {w s n} b k x v m c, (k < n)%nat -> nth_error x k = Some v @@ -24,7 +34,7 @@ Module Conversion. autounfold; simpl. destruct (nth_error x k); simpl; try inversion H0; intuition. - Qed. + Admitted. Lemma pseudo_mem: forall {w s} n v m c x name len index, TripleM.find (w, name mod n, index mod len)%nat m = Some (@wordToN w v) @@ -47,7 +57,7 @@ Module Conversion. Lemma pseudo_plus: forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1, pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1) - -> pseudoEval (PBin n Add p) (x, m0, c0) = + -> pseudoEval (PBin n IAdd p) (x, m0, c0) = Some ([out0 ^+ out1], m1, Some (proj1_sig (bool_of_sumbool (overflows w (&out0 + &out1)%N)%w))). @@ -62,7 +72,7 @@ Module Conversion. Lemma pseudo_bin: forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1 op, - op <> Add + op <> IAdd -> pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1) -> pseudoEval (PBin n op p) (x, m0, c0) = Some ([fst (evalIntOp op out0 out1)], m1, c1). @@ -78,11 +88,11 @@ Module Conversion. Lemma pseudo_and: forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1, pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1) - -> pseudoEval (PBin n And p) (x, m0, c0) = + -> pseudoEval (PBin n IAnd p) (x, m0, c0) = Some ([out0 ^& out1], m1, c1). Proof. intros. - replace (out0 ^& out1) with (fst (evalIntOp And out0 out1)). + replace (out0 ^& out1) with (fst (evalIntOp IAnd out0 out1)). - apply pseudo_bin; intuition; inversion H0. - unfold evalIntOp; simpl; intuition. Qed. @@ -164,24 +174,33 @@ Module Conversion. Lemma pseudo_let_var: forall {w s n k m} (p0: @Pseudo w s n k) (p1: @Pseudo w s (n + k) m) - input out0 out1 m0 m1 m2 c0 c1 c2, + input a f m0 m1 m2 c0 c1 c2, pseudoEval p0 (input, m0, c0) = Some ([a], m1, c1) -> pseudoEval p1 (input ++ [a], m1, c1) = Some (f (nth n (input ++ [a]) (wzero _)), m2, c2) -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) = Some (let x := a in f a, m2, c2). Proof. - intros; cbv beta; simpl in *; apply pseudo_let. + intros; cbv zeta. + eapply pseudo_let; try eassumption. + replace (f a) with (f (nth n (input ++ [a]) (wzero w))); try assumption. + apply f_equal. + assert (Datatypes.length input = n) as L by ( + eapply eval_in_length; eassumption). + + rewrite app_nth2; try rewrite L; intuition. + replace (n - n) with 0 by omega; simpl; intuition. Qed. Lemma pseudo_let_list: forall {w s n k m} (p0: @Pseudo w s n k) (p1: @Pseudo w s (n + k) m) - input out0 out1 m0 m1 m2 c0 c1 c2, + input lst f m0 m1 m2 c0 c1 c2, pseudoEval p0 (input, m0, c0) = Some (lst, m1, c1) -> pseudoEval p1 (input ++ lst, m1, c1) = Some (f lst, m2, c2) -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) = - Some (let x := lst in f a, m2, c2). + Some (let x := lst in f x, m2, c2). Proof. - intros; cbv beta; simpl in *; apply pseudo_let. + intros; cbv zeta. + eapply pseudo_let; try eassumption. Qed. Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := @@ -205,6 +224,13 @@ Module Conversion. Ltac pseudo_step := match goal with + | [ |- pseudoEval ?p _ = Some ((let _ := ?b in _), _, _) ] => + is_evar p; + match (type of b) with + | word _ => eapply pseudo_let_var + | list _ => eapply pseudo_let_list + end + | [ |- pseudoEval ?p _ = Some ([?x ^& ?y], _, _) ] => is_evar p; eapply pseudo_and | [ |- pseudoEval ?p _ = Some ([?x ^+ ?y], _, _) ] => @@ -229,11 +255,10 @@ Module Conversion. let b := nth 0 v (wzero _) in [a ^& b]). - cbv zeta; pseudo_solve. - + pseudo_solve. Defined. - Eval simpl in (proj1_sig convert_example). + (* Eval simpl in (proj1_sig convert_example). *) End Conversion. diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index f8139bf92..aeb47f960 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -1,7 +1,6 @@ Require Export Bedrock.Word Bedrock.Nomega. Require Import NPeano NArith PArith Ndigits Compare_dec Arith. -Require Import ProofIrrelevance Ring List. -Require Import MultiBoundedWord. +Require Import ProofIrrelevance Ring List Omega. Section Vector. Import ListNotations. @@ -13,9 +12,13 @@ Section Vector. match (proj1_sig x) as x' return (proj1_sig x) = x' -> _ with | [] => fun _ => _ | x0 :: xs => fun _ => nth (proj1_sig i) (proj1_sig x) x0 - end eq_refl); abstract ( + end eq_refl); + abstract ( destruct x as [x xp], i as [i ip]; destruct x as [|x0 xs]; - simpl in xp; subst; inversion _H; clear _H; omega). + simpl in *; subst; try omega; + match goal with + | [H: _ = @nil _ |- _] => inversion H + end). Defined. Lemma vget_spec: forall {T n} (x: vec T n) (i: {v: nat | (v < n)%nat}) (d: T), diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v index e5ad3f066..bac25db71 100644 --- a/src/Assembly/Wordize.v +++ b/src/Assembly/Wordize.v @@ -1,6 +1,7 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec Compare_dec. +Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec. +Require Import Compare_dec Omega. Require Import FunctionalExtensionality ProofIrrelevance. Require Import QhasmUtil QhasmEvalCommon. @@ -108,15 +109,15 @@ Section WordizeUtil. Lemma natToWord_convS: forall {n m} (x: word n) p, & x = & @convS (word n) (word m) x p. - Proof. admit. Qed. + Proof. Admitted. Lemma natToWord_combine: forall {n} (x: word n) k, & x = & combine x (wzero k). - Proof. admit. Qed. + Proof. Admitted. Lemma natToWord_split1: forall {n} (x: word n) p, & x = & split1 n 0 (convS x p). - Proof. admit. Qed. + Proof. Admitted. Lemma extend_bound: forall k n (p: (k <= n)%nat) (w: word k), (& (extend p w) < Npow2 k)%N. @@ -141,7 +142,7 @@ Section WordizeUtil. + admit. - intros; rewrite <- natToWord_combine; intuition. - Qed. + Admitted. Lemma Npow2_split: forall a b, (Npow2 (a + b) = (Npow2 a) * (Npow2 b))%N. @@ -160,7 +161,7 @@ Section WordizeUtil. Lemma Npow2_ignore: forall {n} (x: word n), x = NToWord _ (& x + Npow2 n). - Proof. intros. Admitted. + Proof. Admitted. End WordizeUtil. @@ -244,15 +245,11 @@ Section Wordization. + admit. + admit. + admit. - Qed. + Admitted. Lemma wordize_shiftr: forall {n} (x: word n) (k: nat), (N.shiftr_nat (&x) k) = & (shiftr x k). - Proof. - intros. - - admit. - Qed. + Proof. Admitted. End Wordization. @@ -285,12 +282,12 @@ Section Bounds. | Lt => fun _ => left _ | _ => fun _ => right _ end eq_refl); - abstract (unfold c in *; try first [ - apply N.compare_eq_iff in _H - | apply N.compare_lt_iff in _H - | pose proof (N.compare_antisym x y) as _H0; - rewrite _H in _H0; simpl in _H0; - apply N.compare_lt_iff in _H0 ]; nomega). + abstract ( + unfold c, N.ge, N.lt in *; intuition; subst; + match goal with + | [H0: ?x = _, H1: ?x = _ |- _] => + rewrite H0 in H1; inversion H1 + end). Defined. Theorem wplus_bound : forall {n} (w1 w2 : word n) b1 b2, @@ -336,15 +333,12 @@ Section Bounds. - 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. + Admitted. Theorem mask_bound : forall {n} (w : word n) m, (n > 1)%nat -> @@ -378,7 +372,7 @@ Section Bounds. * admit. * admit. - Qed. + Admitted. Theorem mask_update_bound : forall {n} (w : word n) b m, (n > 1)%nat -- cgit v1.2.3