From ff072622443657c02b37c0bb8d7405ed4830c2c0 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Wed, 22 Jun 2016 00:22:17 -0400 Subject: Full automation for relevant parts of pseudo conversion except lets --- src/Assembly/Pseudize.v | 97 ++++++++++++++++++++++++++++-------------- src/Assembly/Pseudo.v | 23 +++++----- src/Assembly/QhasmCommon.v | 2 +- src/Assembly/QhasmEvalCommon.v | 13 +++--- 4 files changed, 87 insertions(+), 48 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index 164fc8866..af311963d 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. +Require Import NArith NPeano List Sumbool Compare_dec. Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State. Require Export Wordize Vectorize. @@ -9,22 +9,35 @@ Module Conversion. Hint Unfold setList getList getVar setCarry setCarryOpt getCarry getMem setMem overflows. - Lemma pseudo_var: forall {w s n} x k v b p m c, - nth_error x k = Some v - -> pseudoEval (@PVar w s n b (exist _ k p)) (x, m, c) = Some ([v], m, c). + Lemma pseudo_var: forall {w s n} b k x v m c, + (k < n)%nat + -> nth_error x k = Some v + -> pseudoEval (@PVar w s n b (indexize k)) (x, m, c) = Some ([v], m, c). Proof. - intros; simpl; autounfold; simpl. - destruct (nth_error x k); simpl; try inversion H; intuition. + intros; autounfold; simpl; unfold indexize. + destruct (le_dec n 0); simpl. { + replace k with 0 in * by omega; autounfold; simpl in *. + rewrite H0; simpl; intuition. + } + + replace (k mod n) with k by admit. (* TODO (rsloan): find lemma name *) + + autounfold; simpl. + destruct (nth_error x k); simpl; try inversion H0; intuition. Qed. - Lemma pseudo_mem: forall {w s} n v m c x name len index p0 p1, + 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) - -> pseudoEval (@PMem w s n len (indexize _ p0 name) (indexize _ p1 index)) (x, m, c) = Some ([v], m, c). + -> pseudoEval (@PMem w s n len (indexize name) (indexize index)) (x, m, c) = Some ([v], m, c). Proof. intros; autounfold; simpl. - unfold getMem; simpl. - rewrite H; autounfold; simpl. - rewrite NToWord_wordToN; intuition. + unfold indexize; + destruct (le_dec n 0), (le_dec len 0); + try replace n with 0 in * by intuition; + try replace len with 0 in * by intuition; + autounfold; simpl in *; rewrite H; + autounfold; simpl; rewrite NToWord_wordToN; + intuition. Qed. Lemma pseudo_const: forall {w s n} x v m c, @@ -100,14 +113,13 @@ Module Conversion. rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition. Qed. - Lemma pseudo_dual: - forall {w s n} (p: @Pseudo w s n 1) x out0 out1 m0 m1 c0 c1 k, + 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 ([x ^* y; (highBits (n/2) x) ^* (highBits (n/2) y)], m1, c1). + Some ([out0 ^* out1; multHigh out0 out1], m1, c1). Proof. - intros; simpl; rewrite H; autounfold; simpl. - rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition. + intros; simpl; rewrite H; autounfold; simpl; intuition. Qed. Lemma pseudo_comb: @@ -137,14 +149,24 @@ Module Conversion. apply (pseudo_comb p0 p1 input _ _ m0 m1 m2 c0 c1 c2); intuition. Qed. + Lemma pseudo_let: + 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, + pseudoEval p0 (input, m0, c0) = Some (out0, m1, c1) + -> pseudoEval p1 (input ++ out0, m1, c1) = Some (out1, m2, c2) + -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) = + Some (out1, m2, c2). + Proof. + intros; autounfold; simpl. + rewrite H; autounfold; simpl. + rewrite H0; autounfold; 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', pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}. - Definition example (v: list (word 32)) : list (word 32) := - [(natToWord _ 1) ^& (nth 0 v (wzero _))]. - Ltac autodestruct := repeat match goal with | [H: context[Datatypes.length (cons _ _)] |- _] => simpl in H @@ -159,23 +181,34 @@ Module Conversion. end end. - Definition convert_example: @pseudeq 32 W32 1 1 example. - repeat eexists; unfold example; autounfold; autodestruct. - - eapply pseudo_and. - eapply pseudo_cons. - eapply pseudo_const. - eapply pseudo_var. + Ltac pseudo_step := + match goal with + | [ |- 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 ?n _ _ _ ?P (?lst, _, _) = + Some ([nth ?i ?lst _], _, _)%p ] => + eapply (pseudo_var None); simpl; intuition + end. - (* leftovers *) + Ltac pseudo_solve := + repeat eexists; + autounfold; + autodestruct; + repeat pseudo_step. - instantiate (1 := 0); simpl; intuition. - reflexivity. + Definition convert_example: @pseudeq 32 W32 1 1 (fun v => + let a := natToWord _ 1 in + let b := nth 0 v (wzero _) in + [a ^& b]). - Grab Existential Variables. + cbv zeta; pseudo_solve. - abstract (simpl; intuition). - exact None. Defined. Eval simpl in (proj1_sig convert_example). diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index 6102b9642..48e642151 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,6 +1,6 @@ Require Import QhasmUtil QhasmCommon QhasmEvalCommon QhasmUtil State. Require Import Language. -Require Import List. +Require Import List Compare_dec. Module Pseudo <: Language. Import EvalUtil ListState. @@ -113,18 +113,21 @@ Module Pseudo <: Language. 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); - abstract (pose proof (mod_bound_pos x n); omega). + Definition indexize {n: nat} (x: nat): Index n. + intros; destruct (le_dec n 0). + + - exists 0; abstract intuition. + - exists (x mod n); abstract ( + pose proof (mod_bound_pos x n); omega). Defined. - Notation "% A" := (PVar _ (Some false) (indexize _ _ A)) + Notation "% A" := (PVar _ (Some false) (indexize A)) (at level 20, right associativity) : pseudo_notations. - Notation "$ A" := (PVar _ (Some true) (indexize _ _ A)) + Notation "$ A" := (PVar _ (Some true) (indexize A)) (at level 20, right associativity) : pseudo_notations. - Notation "A :[ B ]:" := (PMem _ _ (indexize _ _ A) (indexize _ _ B)) + Notation "A :[ B ]:" := (PMem _ _ (indexize A) (indexize B)) (at level 20, right associativity) : pseudo_notations. Notation "# A" := (PConst _ (natToWord _ A)) @@ -145,17 +148,17 @@ Module Pseudo <: Language. Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B)) (at level 45, right associativity) : pseudo_notations. - Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A) + Notation "A :>>: B" := (PShift _ Shr (indexize B) A) (at level 60, right associativity) : pseudo_notations. - Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A) + Notation "A :<<: B" := (PShift _ Shl (indexize B) A) (at level 60, right associativity) : pseudo_notations. Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B)) (at level 55, right associativity) : pseudo_notations. Notation "O :( A , B ): :?: L ::: R" := - (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R) + (PIf _ _ O (indexize A) (indexize B) L R) (at level 70, right associativity) : pseudo_notations. Notation "F :**: e" := diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 654f109f3..ccec401d2 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -4,7 +4,7 @@ Require Export Bedrock.Word. (* Utilities *) Definition Label := nat. -Definition Index (limit: nat) := {x: nat | (x < limit)%nat}. +Definition Index (limit: nat) := {x: nat | (x <= (pred limit))%nat}. Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. Inductive Either A B := diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v index e7e9b0c7d..dbd46b1b4 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -50,13 +50,16 @@ Module EvalUtil. Definition highBits {n} (m: nat) (x: word n) := snd (break m x). - Definition evalDualOp {n} (duo: DualOp) (x y: word n): word n * word n. - refine match duo with - | Mult => (x ^* y, - @extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y))) - end; abstract omega. + Definition multHigh {n} (x y: word n): word n. + refine (@extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y))); + abstract omega. Defined. + Definition evalDualOp {n} (duo: DualOp) (x y: word n) := + match duo with + | Mult => (x ^* y, multHigh x y) + end. + Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) := match ro with | Shl => NToWord b (N.shiftl_nat (wordToN x) n) -- cgit v1.2.3