diff options
author | 2016-05-07 23:55:45 -0400 | |
---|---|---|
committer | 2016-05-07 23:55:45 -0400 | |
commit | cf508b3dc2fd5a732aec16ea1aaa8e9d89673aa9 (patch) | |
tree | d289a46ebddaa7f98e403cf8c0cf8d9fc17fde56 /src | |
parent | 1cd34679ee6a10425c7b8e794997421235e6d0be (diff) |
Pushed through 2-ary multiplication except conversions
Diffstat (limited to 'src')
-rw-r--r-- | src/Assembly/Pseudo.v | 167 | ||||
-rw-r--r-- | src/Assembly/QhasmCommon.v | 4 | ||||
-rw-r--r-- | src/Assembly/QhasmEvalCommon.v | 22 |
3 files changed, 121 insertions, 72 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index 10f9f4ab2..f5baa96c6 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -43,8 +43,10 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition State := list const. Inductive WBinOp: Set := - | Wplus: WBinOp - | Wminus: WBinOp | Wand: WBinOp. + | Wplus: WBinOp | Wminus: WBinOp | Wand: WBinOp. + + Inductive WDualOp: Set := + | Wmult: WDualOp. Inductive WNatOp: Set := | Wones: WNatOp | Wzeros: WNatOp. @@ -58,6 +60,7 @@ Module Pseudo (M: PseudoMachine) <: Language. | PBin: forall n, WBinOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 1 | PNat: forall n, WNatOp -> Index width -> Pseudo n 1 + | PDual: forall n, WDualOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 2 | PShift: forall n, WShiftOp -> Pseudo n 1 -> Index width -> Pseudo n 1 | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m @@ -71,27 +74,35 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition Program := Pseudo vars vars. - Definition applyBin (op: WBinOp) (a b: word width): option (list const) := + Definition applyBin (op: WBinOp) (a b: word width): const := + match op with + | Wplus => wplus a b + | Wminus => wminus a b + | Wand => wand a b + end. + + Definition applyDual (op: WDualOp) (a b: word width): list const := match op with - | Wplus => Some [(wplus a b)] - | Wminus => Some [(wminus a b)] - | Wand => Some [(wand a b)] + | Wmult => + let wres := natToWord (width + width) + (N.to_nat ((wordToN a) * (wordToN b))) in + [split1 _ _ wres; split2 _ _ wres] end. - Definition applyNat (op: WNatOp) (v: Index width): option (list const). + Definition applyNat (op: WNatOp) (v: Index width): const. refine match op with - | Wones => Some [convert (zext (wones v) (width - v)) _] - | Wzeros => Some [wzero width] + | Wones => convert (zext (wones v) (width - v)) _ + | Wzeros => wzero width end; abstract ( destruct v; simpl; replace (x + (width - x)) with width; intuition ). Defined. - Definition applyShift (op: WShiftOp) (v: const) (n: Index width): option (list const). + Definition applyShift (op: WShiftOp) (v: const) (n: Index width): const. refine match op with - | Wshl => Some [convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _] - | Wshr => Some [convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _] + | Wshl => convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _ + | Wshr => convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _ end; abstract ( unfold const; destruct n; simpl; @@ -100,66 +111,78 @@ Module Pseudo (M: PseudoMachine) <: Language. intuition ). Defined. - Inductive PseudoEval: forall n m, Pseudo n m -> State -> State -> Prop := - | PEVar: forall s n (i: Index n) w, - nth_error s i = Some w - -> PseudoEval n 1 (PVar n i) s [w] - - | PEConst: forall n s w, - PseudoEval n 1 (PConst n w) s [w] - - | PEBin: forall n a b s sa sb s' op, - applyBin op sa sb = Some s' - -> PseudoEval n 1 a s [sa] - -> PseudoEval n 1 b s [sb] - -> PseudoEval n 1 (PBin n op a b) s s' - - | PENat: forall n op v s s', - applyNat op v = Some s' - -> PseudoEval n 1 (PNat n op v) s s' - - | PEShift: forall n m a s s' w op, - applyShift op w m = Some s' - -> PseudoEval n 1 a s [w] - -> PseudoEval n 1 (PShift n op a m) s s' - - | PELet: forall n m k s x s' a b, - PseudoEval n k a s x - -> PseudoEval (n + k) m b (s ++ x) s' - -> PseudoEval n m (PLet n k m a b) s s' - - | PEComp: forall n k m s s' s'' a b, - PseudoEval n k a s s' - -> PseudoEval k m b s' s'' - -> PseudoEval n m (PComp n k m a b) s s'' - - | PEComb: forall n a b x y s sx sy, - PseudoEval n a x s sx - -> PseudoEval n b y s sy - -> PseudoEval n (a + b) (PComb n a b x y) s (sx ++ sy) - - | PEIfTrue: forall n m t x y s sx wx wy (i0 i1: Index n), - nth_error s i0 = Some wx - -> evalTest t wx wy = true - -> PseudoEval n m x s sx - -> PseudoEval n m (PIf n m t i0 i1 x y) s sx - - | PEIfFalse: forall n m t x y s sy wx wy (i0 i1: Index n), - nth_error s i1 = Some wy - -> evalTest t wx wy = false - -> PseudoEval n m y s sy - -> PseudoEval n m (PIf n m t i0 i1 x y) s sy - - | PEFunExpO: forall n f s, - PseudoEval n n (PFunExp n f O) s s - - | PEFunExpS: forall n f s s' s'' e e', - e = S e' - -> PseudoEval n n f s s' - -> PseudoEval n n (PFunExp n f e') s' s'' - -> PseudoEval n n (PFunExp n f e) s s''. - - Definition evaluatesTo := PseudoEval vars vars. + Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State := + let option_map' := fun {A B: Type} (x: option A) (f: A -> option B) => + match x with + | Some x' => + match (f x') with + | Some res => Some res + | None => None + end + | _ => None + end in + + match prog with + | PVar n i => option_map' (nth_error st i) (fun x => Some [x]) + | PConst n c => Some ([c]) + | PNat n o i => Some [applyNat o i] + + | PBin n o a b => + option_map' (pseudoEval a st) (fun sa => + option_map' (pseudoEval b st) (fun sb => + match (sa, sb) with + | ([wa], [wb]) => Some [applyBin o wa wb] + | _ => None + end )) + + | PDual n o a b => + option_map' (pseudoEval a st) (fun sa => + option_map' (pseudoEval b st) (fun sb => + match (sa, sb) with + | ([wa], [wb]) => Some (applyDual o wa wb) + | _ => None + end )) + + | PShift n o x y => + option_map' (pseudoEval x st) (fun sx => + match sx with + | [wx] => Some [applyShift o wx y] + | _ => None + end ) + + | PLet n k m f g => + option_map' (pseudoEval f st) (fun sf => + option_map' (pseudoEval g (st ++ sf)) + (fun sg => Some sg)) + + | PComp n k m f g => + option_map' (pseudoEval f st) (fun sf => + option_map' (pseudoEval g sf) + (fun sg => Some sg)) + + | PComb n a b f g => + option_map' (pseudoEval f st) (fun sf => + option_map' (pseudoEval g st) (fun sg => + Some (sf ++ sg))) + + | PIf n m t i0 i1 l r => + option_map' (nth_error st i0) (fun v0 => + option_map' (nth_error st i1) (fun v1 => + if (evalTest t v0 v1) + then pseudoEval l st + else pseudoEval r st )) + + | PFunExp n p e => + (fix funexpseudo (e': nat) (st': State) := + match e' with + | O => Some st' + | S e'' => + option_map' (pseudoEval p st') (fun st'' => + funexpseudo e'' st'') + end) e st + end. + + Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st'). (* world peace *) End Pseudo. diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 410389638..f213dc9a4 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -55,12 +55,16 @@ Inductive IntOp := | IPlus: IntOp | IMinus: IntOp | IXor: IntOp | IAnd: IntOp | IOr: IntOp. +Inductive DualOp := + | IMult: DualOp. + Inductive RotOp := | Shl: RotOp | Shr: RotOp. Inductive Operation := | IOpConst: forall n, IntOp -> IReg n -> IConst n -> Operation | IOpReg: forall n, IntOp -> IReg n -> IReg n -> Operation + | DOpReg: forall n, DualOp -> IReg n -> IReg n -> option (IReg n) -> Operation | OpRot: forall n, RotOp -> IReg n -> Index n -> Operation. Hint Constructors Operation. diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v index 5d61561cc..cc0b7c63b 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -51,6 +51,13 @@ Definition evalOperation (o: Operation) (state: State): option State := | Shr => NToWord b (N.shiftr_nat (wordToN x) n) end in + let evalDualOp := fun {b} (duo: DualOp) (x y: word b) => + match duo with + | IMult => + let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in + (split1 b b wres, split2 b b wres) + end in + let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) => match (xo, yo) with | (Some x, Some y) => f x y @@ -67,6 +74,21 @@ Definition evalOperation (o: Operation) (state: State): option State := liftOpt (fun x y => setIntReg a (evalIOp o x y) state) (getIntReg a state) (getIntReg b state) + | DOpReg n o a b h => + liftOpt (fun x y => + match (evalDualOp o x y) with + | (lw, hw) => + match (setIntReg a lw state) with + | Some st' => + match h with + | Some hr => setIntReg hr hw st' + | _ => Some st' + end + | None => None + end + end) + (getIntReg a state) (getIntReg b state) + | OpRot n o r i => match (getIntReg r state) with | Some va => setIntReg r (evalRotOp o va i) state |