MedialConversions done

5 files changed, 378 insertions, 520 deletions

diff --git a/src/Assembly/MedialConversion.v b/src/Assembly/MedialConversion.v
deleted file mode 100644
index a72e2dad7..000000000
--- a/src/Assembly/MedialConversion.v
+++ /dev/null
@@ -1,372 +0,0 @@
-
-Require Export Language Conversion QhasmCommon QhasmUtil.
-Require Export Pseudo Medial AlmostQhasm State.
-Require Export Bedrock.Word NArith NPeano.
-Require Export List Sumbool.
-Require Vector.
-
-Module MedialConversion (Arch: PseudoMachine).
-  Import QhasmCommon AlmostQhasm State Util.
-  Import ListNotations.
-
-  Module M := Medial Arch.
-
-  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 M AlmostQhasm.
-    Import M Arch.
-
-    Definition width_dec: {width = 32} + {width = 64}.
-      destruct width_spec.
-      - left; abstract intuition.
-      - right; abstract intuition.
-    Defined.
-
-    Definition ireg (x: nat): IReg width :=
-      match width_spec with
-      | I32 => regInt32 x
-      | I64 => regInt64 x
-      end.
-
-    Definition iconst (x: word width): IConst width.
-      refine (
-        if width_dec
-        then (convert constInt32 _) x
-        else (convert constInt64 _) x);
-      abstract (rewrite _H; intuition).
-    Defined.
-
-    Definition stack (x: nat): Stack width :=
-      match width_spec with
-      | I32 => stack32 x
-      | I64 => stack64 (2 * x)
-      end.
-
-    Fixpoint maxIndex (prog: M.Program): nat :=
-      match prog with
-      | MSkip => O
-      | MSeq f g => max (maxIndex f) (maxIndex g)
-      | MAssign (MAVar a b) => max a b
-      | MAssign (MAConst a _) => a
-      | MOp (MIOpConst io a c) => a
-      | MOp (MIOpReg io a b) => max a b
-      | MOp (MDOpReg duo a b (Some x)) => max a (max b x)
-      | MOp (MDOpReg duo a b None) => max a b
-      | MOp (MOpRot _ a _) => a
-      | MCond _ f g => max (maxIndex f) (maxIndex g)
-      | MFunexp e f => maxIndex f
-      end.
-
-    Fixpoint convertState (st: AlmostQhasm.State): option M.State :=
-      let try_cons := fun (k: nat) (x: option N) (m: DefMap) =>
-        match x with | Some x' => NatM.add k x' m | _ => m end in
-
-      let get (n: nat): option N :=
-        match (getIntReg (ireg n) st, getStack (stack n) st) with
-        | (Some v, _) => Some (wordToN v)
-        | (_, Some v) => Some (wordToN v)
-        | _ => None
-        end in
-
-      Some (
-        (fix cs' (n: nat) :=
-         try_cons n (get n)
-           (match n with | O => NatM.empty N | S m => cs' m end))
-         vars).
-
-    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.
-
-    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):
-        option AlmostQhasm.Program :=
-      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.
diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v
index f4caed529..7afb3facb 100644
--- a/src/Assembly/PipelineExample.v
+++ b/src/Assembly/PipelineExample.v
@@ -1,35 +1,41 @@
 
-Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
-Require Import PseudoConversion AlmostConversion StringConversion.
+Require Import Pseudo Qhasm AlmostQhasm Medial Conversion Language.
+Require Import PseudoMedialConversion AlmostConversion StringConversion.
 
 Extraction Language Ocaml.
 Require Import ExtrOcamlString ExtrOcamlBasic.
 Require Import Coq.Strings.String.
 
 Module Progs.
-  Module P64 := Pseudo PseudoUnary64.
-  Module C64 := PseudoConversion PseudoUnary64.
+  Module Arch := PseudoUnary64.
+  Module C64 := PseudoMedialConversion Arch.
 
   Import C64.P.
 
-  Definition prog0: Pseudo 1 1.
-    refine (PBin _ Wplus
+  Definition prog0: C64.P.Program.
+    refine
+      (PBin _ IPlus (PComb _ _ _
         (PVar 1 (exist _ 0 _))
-        (PConst _ (natToWord _ 1)));
-        abstract intuition.
+        (PConst _ (natToWord _ 1)))); abstract intuition.
   Defined.
 
-  Definition prog1: option AlmostQhasm.Program :=
-    C64.Conv.convertProgram prog0.
+  Definition prog1: option C64.M.Program :=
+    C64.PseudoConversion.convertProgram prog0.
 
-  Definition prog2: option Qhasm.Program :=
+  Definition prog2: option AlmostQhasm.Program :=
     match prog1 with
-    | Some p => AlmostConversion.convertProgram p
+    | Some p => C64.MedialConversion.convertProgram p
     | None => None
     end.
 
-  Definition prog3: string :=
+  Definition prog3: option Qhasm.Program :=
     match prog2 with
+    | Some p => AlmostConversion.convertProgram p
+    | None => None
+    end.
+
+  Definition prog4: string :=
+    match prog3 with
     | Some p =>
         match (StringConversion.convertProgram p) with
         | Some s => s
@@ -39,7 +45,7 @@ Module Progs.
     end.
 
   Definition result: string.
-    let res := eval vm_compute in prog3 in exact res.
+    let res := eval vm_compute in prog4 in exact res.
   Defined.
 
   Open Scope string_scope.
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
deleted file mode 100644
index 97cf9cad1..000000000
--- a/src/Assembly/PseudoConversion.v
+++ /dev/null
@@ -1,133 +0,0 @@
-
-Require Export Language Conversion QhasmCommon QhasmUtil.
-Require Export AlmostQhasm Pseudo Medial State.
-Require Export Bedrock.Word NArith NPeano.
-Require Export List Sumbool.
-Require Vector.
-
-Module PseudoConversion (Arch: PseudoMachine).
-  Import QhasmCommon AlmostQhasm State Util.
-  Import ListNotations.
-
-  Module P := Pseudo Arch.
-  Module M := Medial Arch.
-
-  Module Conv <: Conversion P M.
-    Import P M Arch.
-
-    Fixpoint convertState (st: M.State): option P.State :=
-      let try_cons := fun {T} (x: option T) (l: list T) =>
-        match x with | Some x' => cons x' l | _ => l end in
-
-      let res := (fix cs' (n: nat) :=
-         try_cons (option_map (NToWord width) (NatM.find n st))
-           (match n with | O => [] | S m => cs' m end)) vars in
-
-      if (Nat.eq_dec (length res) vars)
-      then Some res
-      else None.
-
-    Definition omap {A B} (x: option A) (f: A -> option B) :=
-        match x with | Some y => f y | _ => None end.
-
-    Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
-
-    Fixpoint range (start len: nat): list nat :=
-      match len with
-      | O => []
-      | S len' => start :: (range (S start) len')
-      end.
-
-    Fixpoint list_split {A} (n: nat) (lst: list A): (list A) * (list A) :=
-      match n with
-      | O => ([], lst)
-      | S m =>
-        match lst with
-        | [] => ([], [])
-        | l :: ls =>
-          match list_split m ls with
-          | (a, b) => (cons l a, b)
-          end
-        end
-      end.
-
-    Fixpoint convertProgram' {n m}
-          (prog: Pseudo n m) (inMap outMap: list nat) (start: nat):
-        option (Medial * nat) :=
-
-      match prog with
-      | PVar n i =>
-        min <- nth_error inMap i;
-        mout <- nth_error outMap 0;
-
-        if (Nat.eq_dec min mout)
-        then Some (MSkip, start)
-        else Some ((MAssign (MAVar mout min)), start)
-
-      | PConst n c =>
-        mout <- nth_error outMap 0;
-        Some (MAssign (MAConst mout c), start)
-
-      | PBin n o p =>
-        t <- convertProgram' p inMap (outMap ++ [start]) (S start);
-        a <- nth_error outMap 0;
-
-        Some (MSeq (fst t) (MOp (MIOpReg o a start)), (snd t))
-
-      | PDual n o p =>
-        match outMap with
-        | [a; b] =>
-          x <- nth_error inMap 1;
-          t <- convertProgram' p inMap [a; x] start;
-          Some (MSeq (fst t) (MOp (MDOpReg o a b (Some x))), snd t)
-
-        | _ => None
-        end
-
-      | PShift n o a x =>
-        t <- convertProgram' x inMap outMap start;
-        b <- nth_error outMap 0;
-        Some (MSeq (fst t) (MOp (MOpRot o b a)), snd t)
-
-      | PLet n k m f g =>
-        let medMap := range start k in
-        ft <- convertProgram' f inMap medMap (start + k);
-        gt <- convertProgram' g (inMap ++ medMap) outMap (snd ft);
-        Some (MSeq (fst ft) (fst gt), (snd gt))
-
-      | PComp n k m f g =>
-        let medMap := range start k in
-        ft <- convertProgram' f inMap medMap (start + k);
-        gt <- convertProgram' g medMap outMap (snd ft);
-        Some (MSeq (fst ft) (fst gt), (snd gt))
-
-      | PComb n a b f g => 
-        let outt := list_split a outMap in
-        ft <- convertProgram' f inMap (fst outt) start;
-        gt <- convertProgram' g inMap (snd outt) (snd ft);
-        Some (MSeq (fst ft) (fst gt), snd gt)
-
-      | PIf n m o i0 i1 l r => 
-        lt <- convertProgram' l inMap outMap start;
-        rt <- convertProgram' r inMap outMap start;
-        c0 <- nth_error inMap i0;
-        c1 <- nth_error inMap i1;
-        Some (MCond (MC o c0 c1) (fst lt) (fst rt), (max (snd rt) (snd lt)))
-
-      | PFunExp n f e => 
-        ft <- convertProgram' f inMap outMap start;
-        Some (MFunexp e (fst ft), (snd ft))
-      end.
-
-    Definition convertProgram (prog: Pseudo vars vars): option Medial :=
-      let m := range O vars in
-      option_map (@fst Medial nat) (convertProgram' prog m m vars).
-
-    Lemma convert_spec:  forall a a' b b' prog prog',
-      convertProgram prog = Some prog' ->
-      convertState a = Some a' -> convertState b = Some b' ->
-      M.evaluatesTo prog' a b <-> P.evaluatesTo prog a' b'.
-    Admitted.
-
-  End Conv.
-End PseudoConversion.
diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v
new file mode 100644
index 000000000..5e671775c
--- /dev/null
+++ b/src/Assembly/PseudoMedialConversion.v
@@ -0,0 +1,358 @@
+
+Require Export Language Conversion QhasmCommon QhasmUtil.
+Require Export Pseudo Medial AlmostQhasm State.
+Require Export Bedrock.Word NArith NPeano.
+Require Export List Sumbool.
+Require Vector.
+
+Module PseudoMedialConversion (Arch: PseudoMachine).
+  Import QhasmCommon AlmostQhasm State Util.
+  Import ListNotations.
+
+  Module P := Pseudo Arch.
+  Module M := Medial Arch.
+
+  Inductive Mapping (n: nat) :=
+    | regM: forall (r: IReg n) (v: nat), v = getIRegIndex r -> Mapping n
+    | stackM: forall (r: Stack n) (v: nat), v = getStackIndex r -> Mapping n
+    | constM: forall (r: IConst n) (v: nat), v = getIConstValue r -> Mapping n.
+
+  Definition wordToM {n: nat} {spec: ISize n} (w: word n): Mapping n.
+    destruct spec; first [
+      refine (@constM 32 (constInt32 w) (wordToNat w) _)
+    | refine (@constM 64 (constInt64 w) (wordToNat w) _)];
+      abstract intuition.
+  Defined.
+
+  Definition regToM {n: nat} {spec: ISize n} (r: IReg n): Mapping n.
+    destruct spec; refine (@regM _ r (getIRegIndex r) _); abstract intuition.
+  Defined.
+
+  Definition stackToM {n: nat} {spec: ISize n} (s: Stack n): Mapping n.
+    destruct spec; refine (@stackM _ s (getStackIndex s) _); abstract intuition.
+  Defined.
+
+  Definition constToM {n: nat} {spec: ISize n} (c: IConst n): Mapping n.
+    destruct spec; refine (@constM _ c (getIConstValue c) _); abstract intuition.
+  Defined.
+
+  Definition mapping_dec {n} (a b: Mapping n): {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.
+
+  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.
+
+  Fixpoint usedStackEntries {n} (lst: list (Mapping n)): list nat :=
+    match lst with
+    | nil => []
+    | cons c cs =>
+      match c with
+      | stackM _ v _ => cons v (usedStackEntries cs)
+      | _ => usedStackEntries cs
+      end
+    end.
+
+  (******************    Material Conversions    ************************)
+
+  Module PseudoConversion <: Conversion P M.
+    Import P M Arch.
+
+    Fixpoint convertState (st: M.State): option P.State :=
+      let try_cons := fun {T} (x: option T) (l: list T) =>
+        match x with | Some x' => cons x' l | _ => l end in
+
+      let res := (fix cs' (n: nat) :=
+         try_cons (option_map (NToWord width) (NatM.find n st))
+           (match n with | O => [] | S m => cs' m end)) vars in
+
+      if (Nat.eq_dec (length res) vars)
+      then Some res
+      else None.
+
+    Definition omap {A B} (x: option A) (f: A -> option B) :=
+        match x with | Some y => f y | _ => None end.
+
+    Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
+
+    Fixpoint range (start len: nat): list nat :=
+      match len with
+      | O => []
+      | S len' => start :: (range (S start) len')
+      end.
+
+    Fixpoint list_split {A} (n: nat) (lst: list A): (list A) * (list A) :=
+      match n with
+      | O => ([], lst)
+      | S m =>
+        match lst with
+        | [] => ([], [])
+        | l :: ls =>
+          match list_split m ls with
+          | (a, b) => (cons l a, b)
+          end
+        end
+      end.
+
+    Fixpoint convertProgram' {n m}
+          (prog: Pseudo n m) (inMap outMap: list nat) (start: nat):
+        option (Medial * nat) :=
+
+      match prog with
+      | PVar n i =>
+        min <- nth_error inMap i;
+        mout <- nth_error outMap 0;
+
+        if (Nat.eq_dec min mout)
+        then Some (MSkip, start)
+        else Some ((MAssign (MAVar mout min)), start)
+
+      | PConst n c =>
+        mout <- nth_error outMap 0;
+        Some (MAssign (MAConst mout c), start)
+
+      | PBin n o p =>
+        t <- convertProgram' p inMap (outMap ++ [start]) (S start);
+        a <- nth_error outMap 0;
+
+        Some (MSeq (fst t) (MOp (MIOpReg o a start)), (snd t))
+
+      | PDual n o p =>
+        match outMap with
+        | [a; b] =>
+          x <- nth_error inMap 1;
+          t <- convertProgram' p inMap [a; x] start;
+          Some (MSeq (fst t) (MOp (MDOpReg o a b (Some x))), snd t)
+
+        | _ => None
+        end
+
+      | PShift n o a x =>
+        t <- convertProgram' x inMap outMap start;
+        b <- nth_error outMap 0;
+        Some (MSeq (fst t) (MOp (MOpRot o b a)), snd t)
+
+      | PLet n k m f g =>
+        let medMap := range start k in
+        ft <- convertProgram' f inMap medMap (start + k);
+        gt <- convertProgram' g (inMap ++ medMap) outMap (snd ft);
+        Some (MSeq (fst ft) (fst gt), (snd gt))
+
+      | PComp n k m f g =>
+        let medMap := range start k in
+        ft <- convertProgram' f inMap medMap (start + k);
+        gt <- convertProgram' g medMap outMap (snd ft);
+        Some (MSeq (fst ft) (fst gt), (snd gt))
+
+      | PComb n a b f g => 
+        let outt := list_split a outMap in
+        ft <- convertProgram' f inMap (fst outt) start;
+        gt <- convertProgram' g inMap (snd outt) (snd ft);
+        Some (MSeq (fst ft) (fst gt), snd gt)
+
+      | PIf n m o i0 i1 l r => 
+        lt <- convertProgram' l inMap outMap start;
+        rt <- convertProgram' r inMap outMap start;
+        c0 <- nth_error inMap i0;
+        c1 <- nth_error inMap i1;
+        Some (MCond (MC o c0 c1) (fst lt) (fst rt), (max (snd rt) (snd lt)))
+
+      | PFunExp n f e => 
+        ft <- convertProgram' f inMap outMap start;
+        Some (MFunexp e (fst ft), (snd ft))
+      end.
+
+    Definition convertProgram (prog: Pseudo vars vars): option M.Program :=
+      let m := range O vars in
+      option_map (@fst Medial nat) (convertProgram' prog m m vars).
+
+    Lemma convert_spec:  forall a a' b b' prog prog',
+      convertProgram prog = Some prog' ->
+      convertState a = Some a' -> convertState b = Some b' ->
+      M.evaluatesTo prog' a b <-> P.evaluatesTo prog a' b'.
+    Admitted.
+
+  End PseudoConversion.
+
+  Module MedialConversion <: Conversion M AlmostQhasm.
+
+    Import Arch M.
+
+    Definition width_dec : {width = 32} + {width = 64}.
+      destruct width_spec; first [
+        left; abstract intuition
+        | right; abstract intuition].
+    Defined.
+
+    Definition ireg (x: nat): IReg width :=
+      match width_spec with
+      | I32 => regInt32 x
+      | I64 => regInt64 x
+      end.
+
+    Definition iconst (x: word width): IConst width.
+      refine (
+        if width_dec
+        then (convert constInt32 _) x
+        else (convert constInt64 _) x);
+        abstract (rewrite _H; intuition).
+    Defined.
+
+    Definition stack (x: nat): Stack width :=
+      match width_spec with
+      | I32 => stack32 x
+      | I64 => stack64 (2 * x)
+      end.
+
+    Fixpoint convertState (st: AlmostQhasm.State): option M.State :=
+      let try_cons := fun (k: nat) (x: option N) (m: DefMap) =>
+        match x with | Some x' => NatM.add k x' m | _ => m end in
+
+      let get (n: nat): option N :=
+        match (getIntReg (ireg n) st, getStack (stack n) st) with
+        | (Some v, _) => Some (wordToN v)
+        | (_, Some v) => Some (wordToN v)
+        | _ => None
+        end in
+
+      Some (
+        (fix cs' (n: nat) :=
+         try_cons n (get n)
+           (match n with | O => NatM.empty N | S m => cs' m end))
+         vars).
+
+    Fixpoint convertProgram'
+             (prog: M.Program)
+             (mapF: nat -> Mapping width)
+             (nextFree tmp: nat):
+        option AlmostQhasm.Program :=
+
+      let omap := fun {A B} (x: option A) (f: A -> option B) =>
+        match x with | Some y => f y | _ => None end in
+
+      match prog with
+      | MSkip => Some ASkip
+
+      | MSeq a b =>
+        omap (convertProgram' a mapF nextFree tmp) (fun aprog =>
+          omap (convertProgram' b mapF nextFree tmp) (fun bprog =>
+            Some (ASeq aprog bprog)))
+
+      | MAssign a =>
+        match a with
+        | MAVar x y => 
+          match (mapF x, mapF y) with
+          | (regM rx _ _, regM ry _ _) =>
+            Some (AAssign (ARegRegInt _ rx ry))
+          | (stackM sx _ _, regM ry _ _) =>
+            Some (AAssign (AStackRegInt _ sx ry))
+          | (regM rx _ _, stackM sy _ _) =>
+            Some (AAssign (ARegStackInt _ rx sy))
+          | (regM rx _ _, constM cy _ _) =>
+            Some (AAssign (AConstInt _ rx cy))
+          | _ => None
+          end
+
+        | MAConst x c =>
+          match (mapF x) with
+          | (regM rx _ _) =>
+            Some (AAssign (AConstInt _ rx (iconst c)))
+          | _ => None
+          end
+        end
+
+      | MOp o =>
+        match o with
+        | MIOpConst io a c =>
+          match (mapF a) with
+          | (regM ra _ _) =>
+            Some (AOp (IOpConst _ io ra (iconst c)))
+          | _ => None
+          end
+
+        | MIOpReg io a b =>
+          match (mapF a, mapF b) with
+          | (regM ra _ _, regM rb _ _) =>
+            Some (AOp (IOpReg _ io ra rb))
+          | _ => None
+          end
+
+        | MDOpReg duo a b (Some x) =>
+          match (mapF a, mapF b, mapF x) with
+          | (regM ra _ _, regM rb _ _, regM rx _ _) =>
+            Some (AOp (DOpReg _ duo ra rb (Some rx)))
+          | _ => None
+          end
+
+        | MDOpReg duo a b None =>
+          match (mapF a, mapF b) with
+          | (regM ra _ _, regM rb _ _) =>
+            Some (AOp (DOpReg _ duo ra rb None))
+          | _ => None
+          end
+
+        | MOpRot ro a c =>
+          match (mapF a) with
+          | (regM ra _ _) =>
+            Some (AOp (OpRot _ ro ra c))
+          | _ => None
+          end
+        end
+
+      | MCond (MC to i0 i1) a b =>
+        let c := (fun x => convertProgram' x mapF nextFree tmp) in
+
+        omap (c a) (fun aprog => omap (c b) (fun bprog =>
+          match (mapF i0, mapF i1) with
+          | (regM r0 _ _, regM r1 _ _) =>
+            Some (ACond (TestInt _ to r0 r1) aprog bprog)
+          | _ => None
+          end))
+
+      | MFunexp e a =>
+        let c := (fun x => convertProgram' x mapF (S nextFree) tmp) in
+        omap (c a) (fun aprog =>
+          match (mapF nextFree, mapF tmp) with
+          | (regM rf _ _, regM rt _ _) =>
+
+            Some (ASeq (ASeq
+              (AAssign (AConstInt _ rf (iconst (natToWord _ O))))
+              (AAssign (AConstInt _ rt (iconst (natToWord _ e)))))
+              (AWhile (TestInt _ TLt rf rt)
+                (ASeq aprog (ASeq 
+                (AOp (IOpConst _ IPlus rf (iconst (natToWord _ 1))))
+                (AAssign (AConstInt _ rt (iconst (natToWord _ e))))))))
+          | _ => None
+          end)
+      end.
+
+    (* TODO (rsloan): make these into parameters *)
+    Definition convertProgram (prog: M.Program): option AlmostQhasm.Program :=
+      convertProgram' prog (fun x => @regToM width width_spec (ireg x)) 100 100.
+
+    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 <-> M.evaluatesTo prog a' b'.
+    Admitted.
+
+  End MedialConversion.
+End PseudoMedialConversion.
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index f213dc9a4..5e2077c5a 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -4,7 +4,6 @@ Require Export Bedrock.Word.
 (* A formalization of x86 qhasm *)
 Definition Label := nat.
 Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
-Definition Invert := bool.
 
 (* Sugar and Tactics *)