Most of Medial, less the conversions

2 files changed, 440 insertions, 0 deletions

diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v
new file mode 100644
index 000000000..aea77932d
--- /dev/null
+++ b/src/Assembly/Medial.v
@@ -0,0 +1,109 @@
+Require Import QhasmEvalCommon Pseudo.
+Require Import Language.
+Require Import List.
+
+Module Medial (M: PseudoMachine) <: Language.
+  Import ListNotations.
+  Import State.
+  Import M.
+
+  Definition W := word width.
+
+  (* Program Types *)
+  Definition State := DefMap.
+
+  Inductive MAssignment : Type :=
+    | MAVar: nat -> nat -> MAssignment 
+    | MAConst: nat -> W -> MAssignment.
+
+  Inductive MOperation :=
+    | MIOpConst: IntOp -> nat -> W -> MOperation
+    | MIOpReg: IntOp -> nat -> nat -> MOperation
+    | MDOpReg: DualOp -> nat -> nat -> option nat -> MOperation
+    | MOpRot: RotOp -> nat -> Index width -> MOperation.
+
+  Inductive MConditional :=
+    | MC: TestOp -> nat -> nat -> MConditional.
+
+  Inductive Medial: Set :=
+    | MSkip: Medial
+    | MSeq: Medial -> Medial -> Medial
+    | MAssign: MAssignment -> Medial
+    | MOp: MOperation -> Medial
+    | MCond: MConditional -> Medial -> Medial -> Medial
+    | MFunexp: nat -> Medial -> Medial.
+
+  Definition Program := Medial.
+
+  Fixpoint meval (m: Medial) (st: State): option State :=
+    let omap := fun {A B} (x: option A) (f: A -> option B) =>
+      match x with | Some y => f y | _ => None end in
+    match m with
+    | MSkip => Some st
+    | MSeq a b => omap (meval a st) (fun s => meval b s)
+    | MAssign a =>
+      match a with
+      | MAVar x y =>
+        match (NatM.find y st) with
+        | (Some v) => Some (NatM.add x v st)
+        | _ => None
+        end
+      | MAConst x c => Some (NatM.add x (wordToN c) st)
+      end
+    | MOp o =>
+      match o with
+      | MIOpConst io a c =>
+        omap (NatM.find a st) (fun v =>
+          let res := evalIOp io (NToWord _ v) c in
+          Some (NatM.add a (wordToN res) st))
+
+      | MIOpReg io a b =>
+        omap (NatM.find a st) (fun va =>
+          omap (NatM.find b st) (fun vb =>
+            let res := evalIOp io (NToWord width va) (NToWord width vb) in
+            Some (NatM.add a (wordToN res) st)))
+
+      | MDOpReg duo a b (Some x) =>
+        omap (NatM.find a st) (fun va =>
+          omap (NatM.find b st) (fun vb =>
+            let res := evalDualOp duo (NToWord width va) (NToWord width vb) in
+            Some (NatM.add a (wordToN (fst res))
+                   (NatM.add x (wordToN (snd res)) st))))
+
+      | MDOpReg duo a b None =>
+        omap (NatM.find a st) (fun va =>
+          omap (NatM.find b st) (fun vb =>
+            let res := evalDualOp duo (NToWord width va) (NToWord width vb) in
+            Some (NatM.add a (wordToN (fst res)) st)))
+
+      | MOpRot ro a x =>
+        omap (NatM.find a st) (fun v =>
+          let res := evalRotOp ro (NToWord width v) (proj1_sig x) in
+          Some (NatM.add a (wordToN res) st))
+      end
+    | MCond c a b =>
+      match c with
+      | MC t x y =>
+        omap (NatM.find x st) (fun vx =>
+          omap (NatM.find y st) (fun vy =>
+            if (evalTest t (NToWord width vx) (NToWord width vy))
+            then meval a st
+            else meval b st))
+      end
+    | MFunexp n a =>
+      (fix fexp (m: nat) (f: State -> option State) (s: State) :=
+        match m with
+        | O => Some s
+        | S m' =>
+          match f s with
+          | None => None
+          | Some s' => fexp m' f s'
+          end
+        end
+      ) n (meval a) st
+    end.
+
+  Definition evaluatesTo := fun m st0 st1 => meval m st0 = Some st1.
+
+  (* world peace *)
+End Medial.
diff --git a/src/Assembly/MedialConversion.v b/src/Assembly/MedialConversion.v
new file mode 100644
index 000000000..79a0cc934
--- /dev/null
+++ b/src/Assembly/MedialConversion.v
@@ -0,0 +1,331 @@
+
+Require Export Language Conversion QhasmCommon QhasmUtil.
+Require Export AlmostQhasm Pseudo State.
+Require Export Bedrock.Word NArith NPeano.
+Require Export List Sumbool.
+Require Vector.
+
+Module PseudoConversion (M: PseudoMachine).
+  Import QhasmCommon AlmostQhasm State Util.
+  Import ListNotations.
+
+  Module P := Pseudo M.
+
+  Fixpoint take {A} (n: nat) (lst: list A) :=
+    match n with
+    | O => []
+    | S m =>
+      match lst with
+      | [] => []
+      | l :: ls => l :: (take m ls)
+      end
+    end.
+
+  Module Conv <: Conversion P AlmostQhasm.
+    Import P M.
+
+    Definition activeRegisters := 4.
+    Definition r0 := ireg 4. (* Invariant: these are never used in a Mapping *)
+    Definition r1 := ireg 5.
+    Definition r2 := ireg 6.
+
+    Definition convertState (st: AlmostQhasm.State): option P.State :=
+      match st with
+      | fullState _ stackState _ =>
+        Some (take vars (map (fun x => NToWord width (snd x))
+                       (NatM.elements stackState)))
+      end.
+
+    Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}.
+      assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true})
+        by abstract (destruct (a <? b)%nat; intuition);
+        destruct H.
+
+      - left; abstract (apply Nat.ltb_lt in e; intuition).
+
+      - right; abstract (rewrite Nat.ltb_lt in n; intuition).
+    Defined.
+
+    Inductive Mapping :=
+      | regM: forall (r: IReg width) (v: nat), v = getIRegIndex r -> Mapping
+      | stackM: forall (r: Stack width) (v: nat), v = getStackIndex r -> Mapping
+      | constM: forall (r: IConst width) (v: nat), v = getIConstValue r -> Mapping.
+
+    Definition wordToM (w: word width) :=
+      constM (iconst w) (getIConstValue (iconst w)) eq_refl.
+
+    Definition regToM (r: IReg width) :=
+      regM r (getIRegIndex r) eq_refl.
+
+    Definition stackToM (s: Stack width) :=
+      stackM s (getStackIndex s) eq_refl.
+
+    Definition constToM (c: IConst width) :=
+      constM c (getIConstValue c) eq_refl.
+
+    Definition mapping_dec (a b: Mapping): {a = b} + {a <> b}.
+      refine (match (a, b) as p' return (a, b) = p' -> _ with
+      | (regM x v _, regM y v' _) => fun _ => 
+        if (Nat.eq_dec v v') then left _ else right _
+
+      | (stackM x v _, stackM y v' _) => fun _ => 
+        if (Nat.eq_dec v v') then left _ else right _
+
+      | (constM x v _, constM y v' _) => fun _ => 
+        if (Nat.eq_dec v v') then left _ else right _
+
+      | _ => fun _ => right _
+      end (eq_refl (a, b))); admit. (* TODO (rsloan): prove *)
+    Defined.
+
+    Fixpoint usedStackEntries (lst: list Mapping): list nat :=
+      match lst with
+      | nil => []
+      | cons c cs =>
+        match c with
+        | stackM _ v _ => cons v (usedStackEntries cs)
+        | _ => usedStackEntries cs
+        end
+      end.
+
+    Definition getFreshStack (cur: list Mapping) (len: nat): list (Stack width) :=
+      let used := usedStackEntries cur in
+
+      let open := fun x =>
+        negb (proj1_sig (bool_of_sumbool (in_dec Nat.eq_dec x used))) in
+
+      let maxStack := len + (length cur) in 
+
+     (fix gen (rem bound: nat) :=
+        match bound with
+        | O => []
+        | S bound' =>
+          match rem with
+          | O => []
+          | S rem' =>
+            let loc := (maxStack - bound) in
+
+            if (open loc)
+            then cons (stack loc) (gen rem' bound')
+            else gen rem bound'
+          end
+        end) len maxStack.
+
+    Definition freshMapping (cur: list Mapping) (len: nat): list Mapping :=
+      map (fun s => stackToM s) (getFreshStack cur len).
+
+    Definition getS (lst: list (Stack width)) (n: nat) := nth n lst (stack 0).
+
+    Fixpoint moveMapping (a b: list Mapping): AlmostQhasm.Program :=
+      match (a, b) with
+      | (cons ahd atl, cons bhd btl) =>
+        let curOp := 
+          match (ahd, bhd) with
+          | (regM ra va _, regM rb vb _) =>
+            AAssign (ARegRegInt width rb ra)
+
+          | (stackM ra va _, regM rb vb _) =>
+            AAssign (ARegStackInt width rb ra)
+
+          | (regM ra va _, stackM rb vb _) =>
+            AAssign (AStackRegInt width rb ra)
+
+          | (stackM ra va _, stackM rb vb _) =>
+            ASeq
+              (AAssign (ARegStackInt width r0 ra))
+              (AAssign (AStackRegInt width rb r0))
+
+          | (constM ra va _, stackM rb vb _) =>
+            ASeq
+              (AAssign (AConstInt width r0 ra))
+              (AAssign (AStackRegInt width rb r0))
+
+          | (constM ra va _, regM rb vb _) =>
+            AAssign (AConstInt width rb ra)
+
+          | _ => ASkip
+          end in
+        ASeq curOp (moveMapping atl btl)
+      | _ => ASkip
+      end.
+
+    Definition wrapM (m: Mapping) (freeR: IReg width) (freeS: Stack width)
+               (inside: IReg width -> (AlmostQhasm.Program * Mapping)):
+        (AlmostQhasm.Program * Mapping) :=
+
+      match m with
+      | regM r v _ => inside r
+      | stackM s v _ =>
+        let p := (inside freeR) in
+
+        if (mapping_dec (snd p) (regToM freeR))
+        then (ASeq (AAssign (ARegStackInt width freeR s))
+               (ASeq (fst p)
+               (AAssign (AStackRegInt width s freeR))), m)
+        else (ASeq (AAssign (ARegStackInt width freeR s)) (fst p), (snd p))
+
+      | constM r v _ =>
+        let p := (inside freeR) in
+
+        if (mapping_dec (snd p) (regToM freeR))
+        then (ASeq (AAssign (ARegStackInt width freeR freeS))
+               (ASeq (fst p)
+                     (AAssign (AStackRegInt width freeS freeR))),
+              stackToM freeS)
+        else (ASeq (AAssign (ARegStackInt width freeR freeS)) (fst p), (snd p))
+
+      end.
+
+    Definition binProg (op: WBinOp) (a b: Mapping) (avoid: list Mapping):
+        AlmostQhasm.Program * Mapping :=
+      let iop := match op with | Wplus => IPlus | Wminus => IMinus | _ => IAnd end in
+      let sl := getFreshStack avoid 2 in
+      
+      wrapM a r0 (getS sl 0) (fun ra =>
+        wrapM b r1 (getS sl 1) (fun rb =>
+          (AOp (IOpReg width iop ra rb), regToM ra))).
+
+    Definition dualProg (op: WDualOp) (a b x: Mapping) (avoid: list Mapping):
+        AlmostQhasm.Program * Mapping :=
+      let dop := match op with | Wmult => IMult end in
+      let sl := getFreshStack avoid 3 in
+
+      wrapM a r0 (getS sl 0) (fun ra =>
+        wrapM b r1 (getS sl 1) (fun rb =>
+          wrapM x r2 (getS sl 2) (fun rx =>
+            (AOp (DOpReg width dop ra rb (Some rx)), regToM ra)))).
+
+    Definition shiftProg (op: WShiftOp) (m: Mapping) (n: Index width) (avoid: list Mapping):
+        AlmostQhasm.Program * Mapping :=
+      let qop := match op with | Wshl => Shl | Wshr => Shr end in
+      let sl := getFreshStack avoid 1 in
+
+      wrapM m r0 (getS sl 0) (fun ra =>
+        (AOp (OpRot width qop ra n), regToM ra)).
+
+    Fixpoint convertProgram' {n m}
+             (prog: Pseudo n m)
+             (mapping: list Mapping)
+             (avoid: list Mapping):
+        option (AlmostQhasm.Program * list Mapping) :=
+
+      let option_map' := fun x f => option_map f x in
+      let otup_map := fun x f =>
+        match x with
+        | Some res =>
+          match (f (fst res) (snd res)) with
+          | Some res' => Some res'
+          | _ => None
+          end
+        | _ => None
+        end in
+ 
+      match prog with
+      | PVar n i =>
+        option_map' (nth_error mapping i) (fun v => (ASkip, [v]))
+
+      | PConst n c =>
+        Some (ASkip, [wordToM c])
+
+      | PBin n o p =>
+        otup_map (convertProgram' a mapping avoid) (fun aprog amap =>
+          let tmp := freshMapping (avoid ++ mapping ++ amap) n in
+          let mov := moveMapping mapping tmp in
+
+          otup_map (convertProgram' b tmp (avoid ++ amap)) (fun bprog bmap =>
+            match (amap, bmap) with
+            | ([av], [bv]) =>
+              let oper := binProg o av bv (avoid ++ mapping ++ amap ++ bmap) in
+
+              Some (ASeq mov (ASeq bprog (ASeq aprog (fst oper))), [snd oper])
+
+            | _ => None
+            end))
+
+      | PDual n o a b =>
+        otup_map (convertProgram' a mapping avoid) (fun aprog amap =>
+          let tmpb := freshMapping (avoid ++ mapping ++ amap) n in
+          let movb := moveMapping mapping tmpb in
+
+          otup_map (convertProgram' b tmpb (avoid ++ amap)) (fun bprog bmap =>
+            let xs := getFreshStack (avoid ++ mapping ++ amap ++ bmap) 1 in
+
+            match (amap, bmap) with
+            | ([av], [bv]) =>
+              let x := stackToM (getS xs 0) in
+              let oper := dualProg o av bv x (avoid ++ mapping ++ amap ++ bmap) in
+
+              Some (ASeq movb (ASeq bprog
+                (ASeq aprog (fst oper))), [snd oper; x])
+
+            | _ => None
+            end))
+
+      | PNat n o v =>
+        Some (ASkip, [constToM (iconst (applyNat o v))])
+
+      | PShift n o a x =>
+        otup_map (convertProgram' a mapping avoid) (fun aprog amap =>
+          match amap with
+          | [av] => let oper := shiftProg o av x (mapping ++ avoid ++ amap) in
+
+            Some (ASeq aprog (fst oper), [snd oper])
+
+          | _ => None
+          end)
+
+      | PLet n k m f g =>
+        otup_map (convertProgram' f mapping avoid) (fun fprog fmap =>
+          otup_map (convertProgram' g (mapping ++ fmap) avoid) (fun gprog gmap =>
+            Some (ASeq fprog gprog, gmap)))
+
+      | PComp n k m f g =>
+        otup_map (convertProgram' f mapping avoid) (fun fprog fmap =>
+          otup_map (convertProgram' g fmap avoid) (fun gprog gmap =>
+            Some (ASeq fprog gprog, gmap)))
+
+      | PComb n a b f g =>
+        otup_map (convertProgram' f mapping avoid) (fun fprog fmap =>
+          otup_map (convertProgram' g (mapping ++ fmap) avoid) (fun gprog gmap =>
+            Some (ASeq fprog gprog, fmap ++ gmap)))
+
+      | PIf n m o i0 i1 l r =>
+        otup_map (convertProgram' l mapping avoid) (fun lprog lmap =>
+          otup_map (convertProgram' r mapping avoid) (fun rprog rmap =>
+            match (nth_error mapping i0, nth_error mapping i1) with
+            | (Some (regM a _ _), Some (regM b _ _)) =>
+              Some (ACond (TestInt width o a b) lprog (ASeq rprog (moveMapping rmap lmap)), lmap)
+            | _ => None
+            end))
+
+      | PFunExp n f e =>
+        otup_map (convertProgram' f mapping avoid) (fun fprog fmap =>
+          let mov := moveMapping mapping fmap in
+
+          match (freshMapping (avoid ++ fmap) 1) with
+          | [regM rc _ _] => 
+            Some (ASeq mov
+              (ASeq (AAssign (AConstInt width rc (iconst (natToWord width e))))
+                (AWhile (TestInt width TGt rc r0)
+                  (ASeq fprog
+                    (ASeq (AAssign (AConstInt width r0 (iconst (wzero width))))
+                      (AOp (IOpConst width IMinus rc (iconst (natToWord width 1)))))))), fmap)
+          | [stackM sc _ _] => None
+          | _ => None
+          end)
+      end.
+
+    Definition convertProgram (prog: Pseudo vars vars): option AlmostQhasm.Program :=
+      match (convertProgram' prog (freshMapping [] vars) []) with
+      | Some (prog', _) => Some prog'
+      | _ => None
+      end.
+
+    Lemma convert_spec:  forall a a' b b' prog prog',
+      convertProgram prog = Some prog' ->
+      convertState a = Some a' -> convertState b = Some b' ->
+      AlmostQhasm.evaluatesTo prog' a b <-> P.evaluatesTo prog a' b'.
+    Admitted.
+
+  End Conv.
+End PseudoConversion.