From b9fcdc12c330b078574ba3feb2ab9e383fbc4e83 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Thu, 23 Jun 2016 15:55:41 -0400 Subject: Pseudize Lemmas for Dual Operations --- src/Assembly/Pipeline.v | 16 ++++---- src/Assembly/Pseudize.v | 84 ++++++++++++++++++++++++++++++++--------- src/Assembly/PseudoConversion.v | 64 ++++++++++++++++++++----------- src/Assembly/StringConversion.v | 10 ++++- src/Assembly/Vectorize.v | 44 +++++++++++++++++++++ 5 files changed, 168 insertions(+), 50 deletions(-) (limited to 'src') diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 9299d9d52..9d6c4c9da 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -22,21 +22,19 @@ Module Pipeline. End Pipeline. Module PipelineExample. - Import Pipeline ListNotations. + Import Pipeline ListNotations StateCommon EvalUtil ListState. Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). Local Notation "$$ v" := (natToWord _ v) (at level 40). Definition example: @pseudeq 32 W32 1 1 (fun v => - Let_In ($$ 1) (fun a => - Let_In (v[[0]]) (fun b => [ - a ^& b - ]))). - + plet a := $$ 1 in + plet b := v[[0]] in + plet c := multHigh a b in + plet d := a ^* b in + [b ^& d]). pseudo_solve. Defined. - Definition exStr := Pipeline.toString (proj1_sig example). - - (* Eval vm_compute in exStr. *) + Eval vm_compute in (Pipeline.toString (proj1_sig example)). End PipelineExample. diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index fb3a8b81b..c167dd6a1 100644 --- a/src/Assembly/Pseudize.v +++ b/src/Assembly/Pseudize.v @@ -7,8 +7,6 @@ Import Pseudo ListNotations StateCommon EvalUtil ListState. Section Conversion. - Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. - Hint Unfold setList getList getVar setCarry setCarryOpt getCarry getMem setMem overflows. @@ -130,15 +128,6 @@ Section Conversion. rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition. Qed. - Lemma pseudo_mult: - 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 (PDual n Mult p) (x, m0, c0) = - Some ([out0 ^* out1; multHigh out0 out1], m1, c1). - Proof. - intros; simpl; rewrite H; autounfold; simpl; intuition. - Qed. - Lemma pseudo_comb: forall {w s n a b} (p0: @Pseudo w s n a) (p1: @Pseudo w s n b) input out0 out1 m0 m1 m2 c0 c1 c2, @@ -210,6 +199,54 @@ Section Conversion. eapply pseudo_let; try eassumption. Qed. + Lemma pseudo_mult_single: + forall {w s n m} (p0: @Pseudo w s n 2) + (p1: @Pseudo w s (n + 2) m) + out0 out1 f x m0 m1 m2 c0 c1 c2, + pseudoEval p0 (x, m0, c0) = Some ([out0; out1], m1, c1) + -> pseudoEval p1 (x ++ [out0 ^* out1; multHigh out0 out1], m1, c1) = + Some (f (nth n (x ++ [out0 ^* out1; multHigh out0 out1]) (wzero _)), m2, c2) + -> pseudoEval (@PLet w s n 2 m (PDual n Mult p0) p1) (x, m0, c0) = + Some (Let_In (out0 ^* out1) f, m2, c2). + Proof. + intros; simpl; rewrite H; autounfold; simpl; rewrite H0; simpl; intuition. + replace (nth n (x ++ _) _) with (out0 ^* out1); simpl; intuition. + assert (Datatypes.length x = 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_mult_dual: + forall {w s n m} (p0: @Pseudo w s n 2) + (p1: @Pseudo w s (n + 2) m) + out0 out1 f x m0 m1 m2 c0 c1 c2, + pseudoEval p0 (x, m0, c0) = Some ([out0; out1], m1, c1) + -> pseudoEval p1 (x ++ [out0 ^* out1; multHigh out0 out1], m1, c1) = + Some (f (nth n (x ++ [out0 ^* out1; multHigh out0 out1]) (wzero _)) + (nth (S n) (x ++ [out0 ^* out1; multHigh out0 out1]) (wzero _)), + m2, c2) + -> pseudoEval (@PLet w s n 2 m (PDual n Mult p0) p1) (x, m0, c0) = + Some (Let_In (multHigh out0 out1) (fun x => + Let_In (out0 ^* out1) (fun y => + f y x)), m2, c2). + Proof. + intros; simpl; rewrite H; autounfold; simpl; rewrite H0; simpl; intuition. + assert (Datatypes.length x = n) as L by (eapply eval_in_length; eassumption). + + replace (nth n (x ++ _) _) with (out0 ^* out1); simpl; intuition. + replace (nth (S n) (x ++ _) _) with (multHigh out0 out1); simpl; intuition. + + - rewrite app_nth2; try rewrite L; intuition. + replace (S n - n) with 1 by omega. + simpl; intuition. + + - rewrite app_nth2; try rewrite L; intuition. + replace (n - n) with 0 by omega. + simpl; intuition. + Qed. + Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := {p: @Pseudo w s n m | forall x: (list (word w)), List.length x = n -> exists m' c', @@ -232,21 +269,34 @@ Ltac autodestruct := Ltac pseudo_step := match goal with - | [ |- pseudoEval ?p _ = Some ((Let_In ?a ?f), _, _) ] => - is_evar p; - match (type of a) with - | word _ => eapply pseudo_let_var - | list _ => eapply pseudo_let_list - end + | [ |- pseudoEval ?p _ = Some (( + Let_In (multHigh ?a ?b) (fun x => + Let_In (?a ^* ?b) (fun y => _))), _, _) ] => + is_evar p; eapply pseudo_mult_dual + + | [ |- pseudoEval ?p _ = Some (Let_In (?a ^* ?b) _, _, _) ] => + is_evar p; eapply pseudo_mult_single | [ |- pseudoEval ?p _ = Some ([?x ^& ?y], _, _) ] => is_evar p; eapply pseudo_and + | [ |- pseudoEval ?p _ = Some ([?x ^+ ?y], _, _) ] => is_evar p; eapply pseudo_plus + | [ |- pseudoEval ?p _ = Some (cons ?x (cons _ _), _, _) ] => is_evar p; eapply pseudo_cons; try reflexivity + | [ |- pseudoEval ?p _ = Some ([natToWord _ ?x], _, _)%p ] => is_evar p; eapply pseudo_const + + | [ |- pseudoEval ?p _ = Some ((Let_In ?a ?f), _, _) ] => + is_evar p; + match (type of a) with + | list _ => eapply pseudo_let_list + | word _ => eapply pseudo_let_var + | (_ * _)%type => rewrite detuple_let + end + | [ |- @pseudoEval ?n _ _ _ ?P _ = Some ([nth ?i ?lst _], _, _)%p ] => eapply (pseudo_var None i); simpl; intuition diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v index 9c3fda2a0..9959e5319 100644 --- a/src/Assembly/PseudoConversion.v +++ b/src/Assembly/PseudoConversion.v @@ -16,6 +16,8 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. Definition FMap := NatM.t (AlmostProgram * (list (Mapping w))). Definition fempty := NatM.empty (AlmostProgram * (list (Mapping w))). + Transparent MMap FMap. + Definition getStart {n m} (prog: @Pseudo w s n m) := let ns := (fix getStart' {n' m'} (prog': @Pseudo w s n' m') := match prog' with @@ -54,48 +56,60 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. let stack' := stack s in let const' := constant s in - let G := fun (k: nat) => - match (NatM.find k M) with + let get := fun (k: nat) (default: nat -> Mapping w) (M': MMap) => + match (NatM.find k M') with | Some v => v - | _ => rM k (* TODO: more intelligent defaults *) + | _ => default k end in - let madd := fun (k: nat) (f: nat -> Mapping w) => - NatM.add k (f k) in + let madd := fun (a: nat) (default: nat -> Mapping w) (M': MMap) => + NatM.add a (get a default M') M' in let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping w)) => NatM.add k (f, r) in + let updateM := ( + fix updateM' (k: nat) (mtmp: list (Mapping w)) (Miter: MMap) : MMap := + match mtmp with + | [] => Miter + | a :: mtmp' => NatM.add k a (updateM' (S k) mtmp' Miter) + end) in + match prog with - | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM M, F) - | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM M, F) - | PVar n None i => Some (ASkip, [G i], M, F) + | PVar n (Some true) i => + Some (ASkip, [get i rM M], madd i rM M, F) + + | PVar n (Some false) i => + Some (ASkip, [get i sM M], madd i sM M, F) + + | PVar n None i => (* assign to register by default *) + Some (ASkip, [get i rM M], madd i rM M, F) | PConst n c => Some (AAssign (AConstInt (reg' start) (const' c)), - [rM start], madd start rM M, F) + [get start rM M], madd start rM M, F) | PMem n m v i => Some (AAssign (ARegMem (reg' start) (mem s v) i), - [rM start], madd start rM M, F) + [get start rM M], madd start rM M, F) | PBin n o p => match (convertProgram' p start M F) with | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') => Some (ASeq p' (AOp (IOpReg o (reg' a) (reg' b))), - [rM a], madd a rM (madd b rM M'), F') + [get a rM M'], madd a rM (madd b rM M'), F') | Some (p', [regM (reg _ _ a); constM c], M', F') => Some (ASeq p' (AOp (IOpConst o (reg' a) c)), - [rM a], madd a rM M', F') + [get a rM M'], madd a rM M', F') | Some (p', [regM (reg _ _ a); memM _ b i], M', F') => Some (ASeq p' (AOp (IOpMem o (reg' a) b i)), - [rM a], madd a rM M', F') + [get a rM M'], madd a rM M', F') | Some (p', [regM (reg _ _ a); stackM (stack _ _ b)], M', F') => Some (ASeq p' (AOp (IOpStack o (reg' a) (stack' b))), - [rM a], madd a rM (madd b sM M'), F') + [get a rM M'], madd a rM (madd b sM M'), F') | _ => None end @@ -104,7 +118,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. match (convertProgram' p start M F) with | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') => Some (ASeq p' (AOp (COp o (reg' a) (reg' b))), - [rM a], madd a rM (madd b rM M'), F') + [get a rM M'], madd a rM (madd b rM M'), F') | _ => None end @@ -113,7 +127,8 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. match (convertProgram' p (S start) M F) with | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') => Some (ASeq p' (AOp (DOp o (reg' a) (reg' b) (Some (reg' start)))), - [rM a; rM start], madd a rM (madd b rM (madd start rM M')), F') + [get a rM M'; get start rM M'], + madd a rM (madd b rM (madd start rM M')), F') | _ => None end @@ -122,7 +137,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. match (convertProgram' p start M F) with | Some (p', [regM (reg _ _ a)], M', F') => Some (ASeq p' (AOp (ROp o (reg' a) x)), - [rM a], madd a rM M', F') + [get a rM M'], madd a rM M', F') | _ => None end @@ -131,10 +146,15 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. match (convertProgram' f start M F) with | None => None | Some (fp, fm, M', F') => - match (convertProgram' g (start + (length fm)) M' F') with - | None => None - | Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'') - end + + (* Make sure all of the new variables are bound to their results *) + let M'' := updateM start fm M' in + + (* Then convert the second program *) + match (convertProgram' g (start + (length fm)) M'' F') with + | None => None + | Some (gp, gm, M''', F'') => Some (ASeq fp gp, gm, M''', F'') + end end | PComb n a b f g => @@ -158,7 +178,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. if (list_eq_dec mapping_dec lr rr) then - match (G (proj1_sig i0), G (proj1_sig i1)) with + match (get (proj1_sig i0) rM M, get (proj1_sig i1) rM M) with | (regM r0, regM r1) => Some (ACond (CReg _ o r0 r1) lp rp, lr, M', F') | (regM r, constM c) => Some (ACond (CConst _ o r c) lp rp, lr, M', F') | _ => None diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v index 66a83cfa3..9f3908a26 100644 --- a/src/Assembly/StringConversion.v +++ b/src/Assembly/StringConversion.v @@ -127,7 +127,13 @@ Module StringConversion <: Conversion Qhasm QhasmString. end. Definition operationToString (op: Operation): option string := - let f := fun x => if (Nat.eq_dec x 32) then "32" else "64" in + let f := fun x => ( + if (Nat.eq_dec x 32) + then "32" + else if (Nat.eq_dec x 64) + then "64" + else "128") in + match op with | IOpConst n o r c => r ++ " " ++ o ++ "= " ++ c @@ -140,7 +146,7 @@ Module StringConversion <: Conversion Qhasm QhasmString. | DOp n o a b x => match x with | Some r => - "inline " ++ r ++ " " ++ a ++ " " ++ o ++ "= " ++ b + "(int" ++ (f (2 * n)) ++ ") " ++ r ++ " " ++ a ++ " " ++ o ++ "= " ++ b | None => a ++ " " ++ o ++ "= " ++ b end | COp n o a b => diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index aeb47f960..d2fca3ce6 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -2,6 +2,11 @@ Require Export Bedrock.Word Bedrock.Nomega. Require Import NPeano NArith PArith Ndigits Compare_dec Arith. Require Import ProofIrrelevance Ring List Omega. +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := + let y := x in f y. + +Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)) (at level 60). + Section Vector. Import ListNotations. @@ -62,6 +67,45 @@ Section Vector. Defined. End Vector. +Section Vectorization. + Import ListNotations. + + Lemma detuple_let: forall {A B C} (y0: A) (y1: B) (z: (A * B) -> C), + Let_In (y0, y1) z = + Let_In y0 (fun x0 => + Let_In y1 (fun x1 => + z (x0, x1))). + Proof. intros; unfold Let_In; cbv zeta; intuition. Qed. + + Lemma listize_let: forall {A B} (y d: A) (z: A -> B), + Let_In y z = Let_In [y] (fun x => z (nth 0 x d)). + Proof. intros; unfold Let_In; cbv zeta; intuition. Qed. + + Lemma combine_let_lists: forall {A B} (a: list A) (b: list A) (d: A) (z: list A -> list A -> B), + Let_In a (fun x => Let_In b (z x)) = + Let_In (a ++ b) (fun x => z (firstn (length a) x) (skipn (length a) x)). + Proof. + + intros; unfold Let_In; cbv zeta. + + assert (forall b0, firstn (length a) (a ++ b0) = a) as HA. { + induction a; intros; simpl; try reflexivity. + apply f_equal; apply IHa. + } + + assert (forall b0, skipn (length a) (a ++ b0) = b0) as HB. { + induction a; intros; simpl; try reflexivity. + apply IHa; intro; simpl in HA. + pose proof (HA b1) as HA'; inversion HA' as [HA'']. + rewrite HA''. + assumption. + } + + rewrite HA, HB; reflexivity. + Qed. + +End Vectorization. + Ltac vectorize := repeat match goal with | [ |- context[?a - 1] ] => -- cgit v1.2.3