From 44e58f0a06fbbf641dea6615278200411c3658cb Mon Sep 17 00:00:00 2001
From: Robert Sloan <varomodt@gmail.com>
Date: Sat, 4 Jun 2016 20:54:39 -0400
Subject: Huge Language / Conversion refactors

---
 src/Assembly/AlmostQhasm.v            |   9 +-
 src/Assembly/Conversion.v             |  15 +-
 src/Assembly/Language.v               |   7 +-
 src/Assembly/Medial.v                 | 175 -------------
 src/Assembly/Pipeline.v               |  33 +++
 src/Assembly/Pseudo.v                 | 163 ++++++-------
 src/Assembly/PseudoConversion.v       | 220 +++++++++++++++++
 src/Assembly/PseudoMedialConversion.v | 445 ----------------------------------
 src/Assembly/Qhasm.v                  |  19 +-
 src/Assembly/QhasmCommon.v            |   2 +-
 src/Assembly/QhasmEvalCommon.v        |  46 +---
 src/Assembly/State.v                  |  37 +--
 src/Assembly/StringConversion.v       |  20 +-
 13 files changed, 375 insertions(+), 816 deletions(-)
 delete mode 100644 src/Assembly/Medial.v
 create mode 100644 src/Assembly/Pipeline.v
 create mode 100644 src/Assembly/PseudoConversion.v
 delete mode 100644 src/Assembly/PseudoMedialConversion.v

(limited to 'src/Assembly')

diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
index e33186bea..5a3f1beea 100644
--- a/src/Assembly/AlmostQhasm.v
+++ b/src/Assembly/AlmostQhasm.v
@@ -6,7 +6,8 @@ Module AlmostQhasm <: Language.
   Import QhasmEval.
 
   (* Program Types *)
-  Definition State := State.
+  Definition Params := unit.
+  Definition State := fun (_: Params) => State.
 
   Inductive AlmostProgram: Set :=
     | ASkip: AlmostProgram
@@ -20,7 +21,7 @@ Module AlmostQhasm <: Language.
 
   Hint Constructors AlmostProgram.
 
-  Definition Program := AlmostProgram.
+  Definition Program := fun (_: Params) => AlmostProgram.
 
   Fixpoint inline (l: nat) (f prog: AlmostProgram) :=
     match prog with
@@ -38,7 +39,7 @@ Module AlmostQhasm <: Language.
     | _ => prog
     end.
 
-  Inductive AlmostEval: AlmostProgram -> State -> State -> Prop :=
+  Inductive AlmostEval {x: Params}: Program x -> State x -> State x -> Prop :=
     | AESkip: forall s, AlmostEval ASkip s s
     | AESeq: forall p p' s s' s'',
         AlmostEval p s s'
@@ -70,7 +71,7 @@ Module AlmostQhasm <: Language.
         AlmostEval (inline l f p) s s'
         -> AlmostEval (ADef l f p) s s'.
 
-  Definition evaluatesTo := AlmostEval.
+  Definition evaluatesTo := @AlmostEval.
 
   (* world peace *)
 End AlmostQhasm.
diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v
index 9811d5f43..239bd6b71 100644
--- a/src/Assembly/Conversion.v
+++ b/src/Assembly/Conversion.v
@@ -3,12 +3,15 @@ Require Export Language.
 
 Module Type Conversion (A B: Language).
 
-  Parameter convertProgram: A.Program -> option B.Program.
-  Parameter convertState: B.State -> option A.State.
+  Parameter convertProgram: forall (x: A.Params) (y: B.Params),
+    A.Program x -> option (B.Program y).
+  Parameter convertState: forall (x: A.Params) (y: B.Params),
+    B.State y -> option (A.State x).
 
-  Axiom convert_spec: forall a a' b b' prog prog',
-    convertProgram prog = Some prog' ->
-    convertState a = Some a' -> convertState b = Some b' ->
-    B.evaluatesTo prog' a b <-> A.evaluatesTo prog a' b'.
+  Axiom convert_spec: forall pa pb a a' b b' prog prog',
+    convertProgram pa pb prog = Some prog' ->
+    convertState pa pb a = Some a' ->
+    convertState pa pb b = Some b' ->
+    B.evaluatesTo pb prog' a b <-> A.evaluatesTo pa prog a' b'.
 
 End Conversion.
diff --git a/src/Assembly/Language.v b/src/Assembly/Language.v
index 35338b48b..460aff5fe 100644
--- a/src/Assembly/Language.v
+++ b/src/Assembly/Language.v
@@ -1,7 +1,8 @@
 
 Module Type Language.
-  Parameter Program: Type.
-  Parameter State: Type.
+  Parameter Params: Type.
+  Parameter Program: Params -> Type.
+  Parameter State: Params -> Type.
 
-  Parameter evaluatesTo: Program -> State -> State -> Prop.
+  Parameter evaluatesTo: forall x: Params, Program x -> State x -> State x -> Prop.
 End Language.
diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v
deleted file mode 100644
index 5f082aa12..000000000
--- a/src/Assembly/Medial.v
+++ /dev/null
@@ -1,175 +0,0 @@
-Require Import QhasmEvalCommon Pseudo.
-Require Import Language.
-Require Import List.
-
-Module Medial (Arch: PseudoMachine) <: Language.
-  Import MedState EvalUtil Arch.
-
-  Definition W := word width.
-
-  (* Program Types *)
-  Definition State := MedState width.
-  Transparent State.
-
-  Inductive MAssignment : Type :=
-    | MAVar: nat -> nat -> MAssignment 
-    | MAMem: forall m, nat -> nat -> Index m -> MAssignment 
-    | MAConst: nat -> W -> MAssignment.
-
-  Inductive MOperation :=
-    | MIOpConst: IntOp -> nat -> W -> MOperation
-    | MIOpReg: IntOp -> nat -> nat -> MOperation
-    | MCOpReg: CarryOp -> nat -> nat -> MOperation
-    | MDOpReg: DualOp -> nat -> nat -> option nat -> MOperation
-    | MOpRot: RotOp -> nat -> Index width -> MOperation.
-
-  Inductive MConditional :=
-    | MZ: nat -> MConditional
-    | MCReg: TestOp -> nat -> nat -> MConditional
-    | MCConst: TestOp -> nat -> W -> 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
-    | MDef: nat -> Medial -> Medial -> Medial
-    | MCall: nat -> Medial.
-
-  Definition Program := Medial.
-
-  Fixpoint inline (l: nat) (f p: Medial) :=
-    match p with
-    | MSeq a b => MSeq (inline l f a) (inline l f b)
-    | MCond c a b => MCond c (inline l f a) (inline l f b)
-    | MFunexp e a => MFunexp e (inline l f a)
-    | MDef l' f' p' =>
-      if (Nat.eq_dec l l')
-      then p
-      else MDef l' (inline l f f') (inline l f p')
-    | MCall l' =>
-      if (Nat.eq_dec l l')
-      then f
-      else p
-    | _ => p
-    end.
-
-  Fixpoint inlineAll (p: Medial) :=
-    match p with
-    | MSeq a b => MSeq (inlineAll a) (inlineAll b)
-    | MCond c a b => MCond c (inlineAll a) (inlineAll b)
-    | MFunexp e a => MFunexp e (inlineAll a)
-    | MDef l' f' p' => inline l' f' (inlineAll p')
-    | _ => p
-    end.
-
-  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 (getVar y st) with
-        | Some v => Some (setVar x v st)
-        | _ => None
-        end
-
-      | MAMem _ x y i =>
-        match (getMem y i st) with
-        | Some v => Some (setVar x v st)
-        | _ => None
-        end
-
-      | MAConst x c => Some (setVar x c st)
-      end
-
-    | MOp o =>
-      match o with
-      | MIOpConst io a c =>
-        omap (getVar a st) (fun v =>
-          let (res, c') := evalIntOp io v c in
-          Some (setVar a res (setCarryOpt c' st)))
-
-      | MIOpReg io a b =>
-        omap (getVar a st) (fun va =>
-          omap (getVar b st) (fun vb =>
-            let (res, c') := evalIntOp io va vb in
-            Some (setVar a res (setCarryOpt c' st))))
-
-      | MCOpReg o a b =>
-        omap (getVar a st) (fun va =>
-          omap (getVar b st) (fun vb =>
-            let c := match (snd st) with | Some b => b | _ => false end in
-            let (res, c') := evalCarryOp o va vb c in
-            Some (setVar a res (setCarry c' st))))
-
-      | MDOpReg duo a b (Some x) =>
-        omap (getVar a st) (fun va =>
-          omap (getVar b st) (fun vb =>
-            let (low, high) := evalDualOp duo va vb in
-            Some (setVar a low (setVar x high st))))
-
-      | MDOpReg duo a b None =>
-        omap (getVar a st) (fun va =>
-          omap (getVar b st) (fun vb =>
-            let (low, high) := evalDualOp duo va vb in
-            Some (setVar a low st)))
-
-      | MOpRot ro a x =>
-        omap (getVar a st) (fun v =>
-          let res := evalRotOp ro v (proj1_sig x) in
-          Some (setVar a res st))
-      end
-
-    | MCond c a b =>
-      match c with
-      | MCConst t x y =>
-        omap (getVar x st) (fun vx =>
-          if (evalTest t vx y)
-          then meval a st
-          else meval b st)
-
-      | MCReg t x y =>
-        omap (getVar x st) (fun vx =>
-
-          (* TODO: why can't we infer width here? *)
-          omap (@getVar width y st) (fun vy =>
-            if (evalTest t vx vy)
-            then meval a st
-            else meval b st))
-
-      | MZ x =>
-        omap (getVar x st) (fun vx =>
-          if (evalTest TEq vx (wzero width))
-          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
-
-    | _ => None
-    end.
-
-  Definition evaluatesTo := fun m st0 st1 => meval (inlineAll m) st0 = Some st1.
-
-  (* world peace *)
-End Medial.
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
new file mode 100644
index 000000000..b0cd4018e
--- /dev/null
+++ b/src/Assembly/Pipeline.v
@@ -0,0 +1,33 @@
+
+Require Import QhasmCommon QhasmEvalCommon.
+Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
+Require Import PseudoConversion AlmostConversion StringConversion.
+
+Module Pipeline.
+  Export Pseudo Util.
+
+  Definition toAlmost (p: Pseudo inVars outVars): option AlmostQhasm.Program :=
+    PseudoConversion.convertProgram p.
+
+  Definition toQhasm (p: Pseudo inVars outVars): option Qhasm.Program :=
+    omap (toAlmost p) AlmostConversion.convertProgram.
+
+  Definition toString (p: Pseudo inVars outVars): option string :=
+    omap (toQhasm p) StringConversion.convertProgram.
+End Pipeline.
+
+Module PipelineExample.
+  Import Pipeline.
+
+  Program Definition asdf: Program Unary32 := ($0 :+: $0)%p.
+
+  Definition exStr := Pipeline.toString ex.
+    | Some x => x
+    | None => EmptyString
+    end.
+  Defined.
+
+Open Scope string_scope.
+Print Result.
+
+Extraction "Result.ml" Result.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index 1f127f665..c4249804d 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -2,42 +2,43 @@ Require Import QhasmEvalCommon QhasmUtil State.
 Require Import Language.
 Require Import List.
 
-Module Type PseudoMachine.
-  Parameter width: nat.
-  Parameter vars: nat.
-  Parameter width_spec: Width width.
-End PseudoMachine.
+Module Pseudo <: Language.
+  Import EvalUtil ListState Util.
 
-Module Pseudo (M: PseudoMachine) <: Language.
-  Import EvalUtil ListState Util M.
-
-  Definition const: Type := word width.
-
-  (* Program Types *)
-  Inductive Pseudo: nat -> nat -> Type :=
-    (* Some true for registers, false for stack, None for default *)
+  Inductive Pseudo {w: nat} {spec: Width w}: nat -> nat -> Type :=
     | PVar: forall n, option bool -> Index n -> Pseudo n 1
     | PMem: forall n m, Index n -> Index m -> Pseudo n 1
-    | PConst: forall n, const -> Pseudo n 1
-
+    | PConst: forall n, word w -> Pseudo n 1
     | PBin: forall n, IntOp -> Pseudo n 2 -> Pseudo n 1
     | PDual: forall n, DualOp -> Pseudo n 2 -> Pseudo n 2
     | PCarry: forall n, CarryOp -> Pseudo n 2 -> Pseudo n 1
-    | PShift: forall n, RotOp -> Index width -> Pseudo n 1 -> Pseudo n 1
-
+    | PShift: forall n, RotOp -> Index w -> Pseudo n 1 -> Pseudo n 1
     | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m
     | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n
-
     | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m
     | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b)
     | PCall: forall n m, Label -> Pseudo n m -> Pseudo n m.
 
   Hint Constructors Pseudo.
 
-  Definition Program := Pseudo vars vars.
-  Definition State := ListState width.
+  Record Params': Type := mkParams {
+    width: nat;
+    spec: Width width;
+    inputs: nat;
+    outputs: nat
+  }.
 
-  Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State :=
+  Definition Params := Params'.
+  Definition State (p: Params): Type := ListState (width p).
+  Definition Program (p: Params): Type :=
+    @Pseudo (width p) (spec p) (inputs p) (outputs p).
+
+  Definition Unary32: Params := mkParams 32 W32 1 1.
+  Definition Unary64: Params := mkParams 64 W64 1 1.
+
+  (* Evaluation *)
+
+  Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w): option (ListState w) :=
     match prog with
     | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st))
     | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st))
@@ -94,7 +95,7 @@ Module Pseudo (M: PseudoMachine) <: Language.
           else pseudoEval r st ))
 
     | PFunExp n p e =>
-      (fix funexpseudo (e': nat) (st': State) := 
+      (fix funexpseudo (e': nat) (st': ListState w) := 
         match e' with
         | O => Some st'
         | S e'' =>
@@ -105,94 +106,74 @@ Module Pseudo (M: PseudoMachine) <: Language.
     | PCall n m _ p => pseudoEval p st
     end.
 
-  Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st').
-
-  Module Notations.
-    Delimit Scope pseudo_notations with p.
-    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).
-    Defined.
+  Definition evaluatesTo (p: Params) (prog: Program p) (st st': State p) :=
+      pseudoEval prog st = Some st'.
 
-    Notation "% A" := (PVar _ (Some false) (indexize _ _ A))
-      (at level 20, right associativity) : pseudo_notations.
+  Delimit Scope pseudo_notations with p.
+  Open Scope pseudo_notations.
 
-    Notation "$ A" := (PVar _ (Some true) (indexize _ _ A))
-      (at level 20, right associativity) : 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).
+  Defined.
 
-    Notation "'MEM' ( A , B )" :=  (PMem _ _ (indexize _ _ A) (indexize _ _ B))
-      (at level 20, right associativity) : pseudo_notations.
+  Notation "% A" := (PVar _ (Some false) (indexize _ _ A))
+    (at level 20, right associativity) : pseudo_notations.
 
-    Notation "# A" := (PConst _ (natToWord _ A))
-      (at level 20, right associativity) : pseudo_notations.
+  Notation "$ A" := (PVar _ (Some true) (indexize _ _ A))
+    (at level 20, right associativity) : pseudo_notations.
 
-    Notation "A :+: B" := (PBin _ Add (PComb _ _ _ A B))
-      (at level 60, right associativity) : pseudo_notations.
+  Notation "'MEM' ( A , B )" :=  (PMem _ _ (indexize _ _ A) (indexize _ _ B))
+    (at level 20, right associativity) : pseudo_notations.
 
-    Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B))
-      (at level 60, right associativity) : pseudo_notations.
+  Notation "# A" := (PConst _ (natToWord _ A))
+    (at level 20, right associativity) : pseudo_notations.
 
-    Notation "A :-: B" := (PBin _ Sub (PComb _ _ _ A B))
-      (at level 60, right associativity) : pseudo_notations.
+  Notation "A :+: B" := (PBin _ Add (PComb _ _ _ A B))
+    (at level 60, right associativity) : pseudo_notations.
 
-    Notation "A :&: B" := (PBin _ And (PComb _ _ _ A B))
-      (at level 45, right associativity) : pseudo_notations.
+  Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B))
+    (at level 60, right associativity) : pseudo_notations.
 
-    Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B))
-      (at level 45, right associativity) : pseudo_notations.
+  Notation "A :-: B" := (PBin _ Sub (PComb _ _ _ A B))
+    (at level 60, right associativity) : pseudo_notations.
 
-    Notation "A :|: B" := (PBin _ Or (PComb _ _ _ A B))
-      (at level 60, right associativity) : pseudo_notations.
+  Notation "A :&: B" := (PBin _ And (PComb _ _ _ A B))
+    (at level 45, right associativity) : pseudo_notations.
 
-    Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A)
-      (at level 60, right associativity) : pseudo_notations.
+  Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B))
+    (at level 45, right associativity) : pseudo_notations.
 
-    Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A)
-      (at level 60, right associativity) : pseudo_notations.
+  Notation "A :|: B" := (PBin _ Or (PComb _ _ _ A B))
+    (at level 60, right associativity) : pseudo_notations.
 
-    Notation "A :**: B" := (PDual _ Mult (PComb _ _ _ A B))
-      (at level 55, right associativity) : pseudo_notations.
+  Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A)
+    (at level 60, right associativity) : pseudo_notations.
 
-    Notation "'IF' O ( A , B ) 'THEN' L 'ELSE' R" :=
-      (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R)
-      (at level 70, left associativity) : pseudo_notations.
+  Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A)
+    (at level 60, right associativity) : pseudo_notations.
 
-    Notation "'EXP' ( e ) ( F )" :=
-      (PFunExp _ F e)
-      (at level 70, left associativity) : pseudo_notations.
+  Notation "A :**: B" := (PDual _ Mult (PComb _ _ _ A B))
+    (at level 55, right associativity) : pseudo_notations.
 
-    Notation "'LET' E 'IN' F" :=
-      (PLet _ _ _ E F)
-      (at level 70, left associativity) : pseudo_notations.
+  Notation "'IF' O ( A , B ) 'THEN' L 'ELSE' R" :=
+    (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R)
+    (at level 70, left associativity) : pseudo_notations.
 
-    Notation "A | B" :=
-      (PComb _ _ _ A B)
-      (at level 65, left associativity) : pseudo_notations.
+  Notation "'EXP' ( e ) ( F )" :=
+    (PFunExp _ F e)
+    (at level 70, left associativity) : pseudo_notations.
 
-    Notation "'CALL' n ::: A" :=
-      (PCall _ _ n A)
-      (at level 65, left associativity) : pseudo_notations.
+  Notation "'LET' E 'IN' F" :=
+    (PLet _ _ _ E F)
+    (at level 70, left associativity) : pseudo_notations.
 
-    Definition p0: Pseudo 1 2.
-      refine (CALL 0 ::: %0 :**: $0); intuition.
-    Defined.
-  End Notations.
+  Notation "A | B" :=
+    (PComb _ _ _ A B)
+    (at level 65, left associativity) : pseudo_notations.
 
-  (* world peace *)
+  Notation "'CALL' n ::: A" :=
+    (PCall _ _ n A)
+    (at level 65, left associativity) : pseudo_notations.
 End Pseudo.
 
-Module PseudoUnary32 <: PseudoMachine.
-  Definition width := 32.
-  Definition vars := 1.
-  Definition width_spec := W32.
-  Definition const: Type := word width.
-End PseudoUnary32.
-
-Module PseudoUnary64 <: PseudoMachine.
-  Definition width := 64.
-  Definition vars := 1.
-  Definition width_spec := W64.
-  Definition const: Type := word width.
-End PseudoUnary64.
\ No newline at end of file
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
new file mode 100644
index 000000000..39b655e47
--- /dev/null
+++ b/src/Assembly/PseudoConversion.v
@@ -0,0 +1,220 @@
+
+Require Export Language Conversion QhasmEvalCommon QhasmUtil.
+Require Export Pseudo AlmostQhasm State.
+Require Export Bedrock.Word NArith NPeano Euclid.
+Require Export List Sumbool Vector.
+
+Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
+  Import QhasmCommon AlmostQhasm EvalUtil Util Pseudo StateCommon.
+  Import ListNotations.
+
+  Definition MMap {w} := NatM.t (Mapping w).
+  Definition mempty {w} := NatM.empty (Mapping w).
+
+  Definition FMap {w} := NatM.t (AlmostProgram * (list (Mapping w))).
+  Definition fempty {w} := NatM.empty (AlmostProgram * (list (Mapping w))).
+
+  Definition getStart {w s n m} (prog: @Pseudo w s n m) :=
+    let ns := (fix getStart' {n' m'} (p': @Pseudo w s n' m') :=
+      match p' with
+      | PVar _ _ i => [proj1_sig i]
+      | PBin _ _ p => getStart' p
+      | PDual _ _ p => getStart' p
+      | PCarry _ _ p => getStart' p
+      | PShift _ _ _ p => getStart' p
+      | PIf _ _ _ _ _ l r => (getStart' l) ++ (getStart' r)
+      | PFunExp _ p _ => getStart' p
+      | PLet _ k _ a b => (n + k) :: (getStart' a) ++ (getStart' b)
+      | PComb _ _ _ a b => (getStart' a) ++ (getStart' b)
+      | PCall _ _ _ p => getStart' p
+      | _ => []
+      end) _ _ prog in
+
+    maxN (n :: m :: ns).
+
+  Definition addMap {T} (a b: NatM.t T): NatM.t T :=
+    (fix add' (m: NatM.t T) (elts: list (nat * T)%type) :=
+      match elts with
+      | [] => m
+      | (k, v) :: elts' => add' (NatM.add k v m) elts'
+      end) a (NatM.elements b).
+
+  Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat) (M: MMap) (F: FMap):
+      option (AlmostProgram * (list (Mapping width)) * MMap * FMap) :=
+    let rM := fun (x: nat) => regM _ (reg width_spec x) in
+    let sM := fun (x: nat) => stackM _ (stack width_spec x) in
+
+    let reg' := reg width_spec in
+    let stack' := stack width_spec in
+    let const' := const width_spec in
+
+    let G := fun (k: nat) =>
+      match (NatM.find k M) with
+      | Some v => v
+      | _ => rM k (* TODO: more intelligent defaults *)
+      end in
+
+    let madd := fun (k: nat) (f: nat -> Mapping width) => NatM.add k (f k) in
+    let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping width)) => NatM.add k (f, r) 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) 
+
+    | PConst n c => Some (AAssign (AConstInt (reg' start) (const' c)),
+                         [rM start], madd start rM M, F)
+
+    | PMem n m v i => Some (AAssign (ARegMem (reg' start) (mem width_spec v) i),
+                           [rM start], 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')
+
+      | 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')
+
+      | 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')
+
+      | 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')
+
+      | _ => None
+      end
+
+    | PCarry n o p =>
+      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')
+
+      | _ => None
+      end
+
+    | PDual n o p =>
+      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')
+
+      | _ => None
+      end
+
+    | PShift n o x p =>
+      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')
+
+      | _ => None
+      end
+
+    | PLet n k m f g =>
+      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
+      end
+
+    | PComb n a b f g => 
+      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, fm ++ gm, M'', F'')
+        end
+      end
+
+    | PIf n m o i0 i1 l r => 
+      match (convertProgram' l start M F) with
+      | None => None
+      | Some (lp, lr, lM, lF) =>
+
+        match (convertProgram' r start lM lF) with
+        | None => None
+        | Some (rp, rr, M', F') =>
+
+          if (list_eq_dec mapping_dec lr rr)
+          then
+            match (G (proj1_sig i0), G (proj1_sig i1)) 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
+            end
+          else None
+        end
+      end
+
+    | PFunExp n f e => 
+      match (convertProgram' f (S start) M F) with
+      | Some (fp, fr, M', F') => 
+        let a := start in
+        Some (ASeq
+          (AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
+          (AWhile (CConst _ TLt (reg' a) (const' (natToWord _ e)))
+            (ASeq fp (AOp (IOpConst Add (reg' a) (const' (natToWord _ 1)))))),
+          fr, madd a rM M', F')
+
+      | _ => None
+      end
+ 
+    | PCall n m lbl f =>
+      match (convertProgram' f start M F) with
+      | Some (fp, fr, M', F') =>
+        let F'' := NatM.add lbl (fp, fr) F' in
+        Some (ACall lbl, fr, M', F'')
+      | None => None
+      end
+    end.
+
+  Definition convertProgram (prog: Pseudo inVars outVars): option AlmostProgram := 
+    match (convertProgram' prog (max inVars outVars) mempty fempty) with
+    | Some (prog', _, M, F) =>
+      Some (fold_left
+           (fun p0 t => match t with | (k, (v, _)) => ADef k v p0 end)
+           prog'
+           (of_list (NatM.elements F)))
+    | _ => None
+    end.
+
+  Fixpoint convertState (st: AlmostQhasm.State): option State :=
+    let vars := max inVars outVars in
+
+    let try_cons := fun {T} (x: option T) (l: list T) =>
+      match x with | Some x' => x' :: l | _ => l end in
+
+    let get := fun i =>
+      match (FullState.getReg (reg width_spec i) st,
+             FullState.getStack (stack width_spec i) st) with
+      | (Some v, _) => Some v
+      | (_, Some v) => Some v
+      | _ => None
+      end in
+
+    let varList := (fix cs' (n: nat) :=
+      try_cons (get (vars - n)) (match n with | O => [] | S m => cs' m end)) vars in
+
+    match st with
+    | FullState.fullState _ _ memState _ carry =>
+      if (Nat.eq_dec (length varList) vars)
+      then Some (varList, memState, carry)
+      else 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 <-> evaluatesTo prog a' b'.
+  Admitted.
+End PseudoConversion.
diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v
deleted file mode 100644
index a2ec6fe40..000000000
--- a/src/Assembly/PseudoMedialConversion.v
+++ /dev/null
@@ -1,445 +0,0 @@
-
-Require Export Language Conversion QhasmEvalCommon QhasmUtil.
-Require Export Pseudo AlmostQhasm State.
-Require Export Bedrock.Word NArith NPeano Euclid.
-Require Export List Sumbool Vector.
-
-Module PseudoConversion (Arch: PseudoMachine).
-  Import QhasmCommon AlmostQhasm EvalUtil Util.
-  Import ListNotations.
-
-  Module P := Pseudo Arch.
-  (* Module M := Medial Arch. *)
-
-  (******************    Material Conversions    ************************)
-
-  Module PseudoConversion <: Conversion P AlmostQhasm.
-    Import P (* M *) Arch StateCommon.
-
-    (* Fixpoint convertState (st: M.State): option P.State :=
-      let try_cons := fun {T} (x: option T) (l: list T) =>
-        match x with | Some x' => x' :: l | _ => l end in
-
-      match st with
-      | (v, m, c) =>
-        let varList := (fix cs' (n: nat) :=
-          try_cons (option_map (NToWord width) (NatM.find n v))
-            (match n with | O => [] | S m => cs' m end)) vars in
-
-        if (Nat.eq_dec (length varList) vars)
-        then Some (varList, m, c)
-        else None
-      end. *)
-
-    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) => (l :: a, b)
-          end
-        end
-      end.
-
-    Fixpoint maxN (lst: list nat): nat :=
-      match lst with
-      | x :: xs => max x (maxN xs)
-      | [] => O
-      end.
-
-    Definition MMap := NatM.t (Mapping width).
-    Definition mempty := NatM.empty (Mapping width).
-
-    Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat) (M: MMap):
-        option (AlmostProgram * (list (Mapping width)) * MMap) :=
-      let rM := fun (x: nat) => regM _ (reg width_spec x) in
-      let sM := fun (x: nat) => stackM _ (stack width_spec x) in
-
-      let g := fun (k: nat) =>
-        match (NatM.find k M) with
-        | Some v => v
-        | _ => rM k (* TODO: more intelligent defaults *)
-        end in
-
-      let madd := fun (k: nat) (f: nat -> Mapping width) => NatM.add k (f k) M in
-
-      match prog with
-      | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM)
-      | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM)
-      | PVar n None i => Some (ASkip, [g i], M) 
-      | PConst n c => Some (AAssign (AConstInt (rM start) c), [rM start], madd start rM)
-      | PMem n m v i => Some (AAssign (ARegMem (rM start) v i), madd start rM)
-      | _ => None
-      end.
-
-
-      | PBin n o p =>
-        match (convertProgram' p start) with
-        | Some (p', [a; b]) =>
-          Some (MSeq p' (MOp (MIOpReg o a b)), [a])
-        | _ => None
-        end
-
-      | PCarry n o p =>
-        match (convertProgram' p start) with
-        | Some (p', [a; b]) =>
-          Some (MSeq p' (MOp (MCOpReg o a b)), [a])
-        | _ => None
-        end
-
-      | PDual n o p =>
-        match (convertProgram' p start) with
-        | Some (p', [a; b]) =>
-          let nextOpen := S (maxN [a; b]) in
-          Some (MSeq p' (MOp (MDOpReg o a b (Some nextOpen))), [a; nextOpen])
-        | _ => None
-        end
-
-      | PShift n o a x =>
-        match (convertProgram' x start) with
-        | Some (p', [r]) =>
-          Some (MSeq p' (MOp (MOpRot o r a)), [proj1_sig a])
-        | _ => None
-        end
-
-      | PLet n k m f g =>
-        ft <- convertProgram' f (start + k);
-        gt <- convertProgram' g (S (maxN (snd ft)));
-
-        match (ft, gt) with
-        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, gr)
-        end
-
-      | PComb n a b f g => 
-        ft <- convertProgram' f start;
-        gt <- convertProgram' g (S (maxN (snd ft)));
-        match (ft, gt) with
-        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, fr ++ gr)
-        end
-
-      | PIf n m o i0 i1 l r => 
-        lt <- convertProgram' l start;
-        rt <- convertProgram' r start;
-        match (lt, rt) with
-        | ((lp, lr), (rp, rr)) => Some (MCond (MCReg o i0 i1) lp rp, lr)
-        end
-        (* TODO: prove that all (Pseudo n m) will return the same list *)
-
-      | PFunExp n f e => 
-        match (convertProgram' f start) with
-        | Some (fp, fr) => Some (MFunexp e fp, fr)
-        | _ => None
-        end
- 
-      | PCall n m lbl _ => Some (MCall lbl, range n m)
-      end.
-
-    (* Results are in the locations described by the
-       returned list. start is the next known open address *)
-    Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat):
-        option (Medial * (list nat)) :=
-
-      match prog with
-      | PVar n i => Some (MSkip, [start])
-      | PConst n c => Some (MAssign (MAConst start c), [start])
-      | PMem n m v i => Some (MAssign (MAMem _ start v i), [start])
-
-      | PBin n o p =>
-        match (convertProgram' p start) with
-        | Some (p', [a; b]) =>
-          Some (MSeq p' (MOp (MIOpReg o a b)), [a])
-        | _ => None
-        end
-
-      | PCarry n o p =>
-        match (convertProgram' p start) with
-        | Some (p', [a; b]) =>
-          Some (MSeq p' (MOp (MCOpReg o a b)), [a])
-        | _ => None
-        end
-
-      | PDual n o p =>
-        match (convertProgram' p start) with
-        | Some (p', [a; b]) =>
-          let nextOpen := S (maxN [a; b]) in
-          Some (MSeq p' (MOp (MDOpReg o a b (Some nextOpen))), [a; nextOpen])
-        | _ => None
-        end
-
-      | PShift n o a x =>
-        match (convertProgram' x start) with
-        | Some (p', [r]) =>
-          Some (MSeq p' (MOp (MOpRot o r a)), [proj1_sig a])
-        | _ => None
-        end
-
-      | PLet n k m f g =>
-        ft <- convertProgram' f (start + k);
-        gt <- convertProgram' g (S (maxN (snd ft)));
-
-        match (ft, gt) with
-        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, gr)
-        end
-
-      | PComb n a b f g => 
-        ft <- convertProgram' f start;
-        gt <- convertProgram' g (S (maxN (snd ft)));
-        match (ft, gt) with
-        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, fr ++ gr)
-        end
-
-      | PIf n m o i0 i1 l r => 
-        lt <- convertProgram' l start;
-        rt <- convertProgram' r start;
-        match (lt, rt) with
-        | ((lp, lr), (rp, rr)) => Some (MCond (MCReg o i0 i1) lp rp, lr)
-        end
-        (* TODO: prove that all (Pseudo n m) will return the same list *)
-
-      | PFunExp n f e => 
-        match (convertProgram' f start) with
-        | Some (fp, fr) => Some (MFunexp e fp, fr)
-        | _ => None
-        end
- 
-      | PCall n m lbl _ => Some (MCall lbl, range n m)
-      end.
-
-    Definition addFunMap {T} (a b: TripleM.t T): TripleM.t T :=
-      (fix add' (m: TripleM.t T) (elts: list ((nat * nat * nat) * T)%type) :=
-        match elts with
-        | [] => m
-        | (k, v) :: elts' => add' (TripleM.add k v m) elts'
-        end) a (TripleM.elements b).
-
-    Definition convertProgram (prog: Pseudo vars vars): option M.Program :=
-      let defs: TripleM.t M.Program :=
-        (fix allDefs {n m: nat} (prog: Pseudo n m): TripleM.t M.Program :=
-          match prog with
-          | PBin n o p => allDefs p
-          | PCarry n o p => allDefs p
-          | PDual n o p => allDefs p
-          | PShift n o a x => allDefs x
-          | PLet n k m f g => addFunMap (allDefs f) (allDefs g)
-          | PComb n a b f g => addFunMap (allDefs f) (allDefs g)
-          | PIf n m t i0 i1 l r => addFunMap (allDefs l) (allDefs r)
-          | PFunExp n p e => allDefs p
-          | PCall n m l p =>
-            match (convertProgram' p n) with
-            | Some (mp, _) => TripleM.add (n, m, l) mp (allDefs p)
-            | _ => allDefs p
-            end
-          | _ => TripleM.empty M.Program
-          end) _ _ prog in
-
-     let foldF := fun (p: M.Program) (t: (nat * nat * nat) * M.Program) =>
-       match t with
-       | ((n', m', lbl), p') => MDef lbl p' p
-       end in
-
-     let f: M.Program -> option M.Program := fun x =>
-       Some (fold_left foldF x (of_list (TripleM.elements defs))) in
-
-     match (convertProgram' prog vars) with
-     | Some (p', _) => f p'
-     | _ => None
-     end.
-
-    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 FullState.
-
-    Definition ireg (x: nat): Reg width := reg width_spec x.
-    Definition iconst (x: word width): Const width := const width_spec x.
-    Definition istack (x: nat): Stack width := stack width_spec x.
-
-    Definition tmpMap: nat -> Mapping width := (fun x => regM width (ireg x)).
-
-    Definition getMapping (m: Mapping width) (st: AlmostQhasm.State): option (word width) :=
-      match m with
-      | regM r => getReg r st
-      | stackM s => getStack s st
-      | _ => None
-      end.
-
-    Definition convertState' (mapF: nat -> Mapping width) (st: AlmostQhasm.State): option M.State :=
-      let tryAddVar := fun (k: nat) (x: option (word width)) (st: M.State) =>
-        match x with | Some x' => MedState.setVar k x' st | _ => st end in
-
-      Some ((fix cs' (n: nat) :=
-           tryAddVar n (getMapping (mapF n) st)
-           (match n with | O => MedState.emptyState | S m => cs' m end))
-         vars).
-
-    Definition convertState (st: AlmostQhasm.State): option M.State :=
-      convertState' tmpMap st.
-
-    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 (ARegReg rx ry))
-          | (stackM sx, regM ry) =>
-            Some (AAssign (AStackReg sx ry))
-          | (regM rx, stackM sy) =>
-            Some (AAssign (ARegStack 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
-
-        | MAMem m x v i =>
-          match (mapF x) with
-          | (regM rx) => Some (AAssign (ARegMem rx (@mem _ m width_spec v) i))
-          | _ => 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
-
-        | MCOpReg co a b =>
-          match (mapF a, mapF b) with
-          | (regM ra, regM rb) =>
-            Some (AOp (COp co 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 (DOp duo ra rb (Some rx)))
-          | _ => None
-          end
-
-        | MDOpReg duo a b None =>
-          match (mapF a, mapF b) with
-          | (regM ra, regM rb) =>
-            Some (AOp (DOp duo ra rb None))
-          | _ => None
-          end
-
-        | MOpRot ro a c =>
-          match (mapF a) with
-          | (regM ra) =>
-            Some (AOp (ROp ro ra c))
-          | _ => None
-          end
-        end
-
-      | MCond c a b =>
-
-        let conv := (fun x => convertProgram' x mapF nextFree tmp) in
-
-        omap (conv a) (fun aprog => omap (conv b) (fun bprog =>
-          match c with
-          | MCReg t x y =>
-            match (mapF x, mapF y) with
-            | (regM r0, regM r1) =>
-              Some (ACond (CReg _ t r0 r1) aprog bprog)
-            | _ => None
-            end
-
-          | MCConst t x y =>
-            match (mapF x) with
-            | (regM r) =>
-              Some (ACond (CConst _ t r (iconst y)) aprog bprog)
-            | _ => None
-            end
-
-          | MZ x =>
-            match (mapF x) with
-            | (regM r) =>
-              Some (ACond (CZero _ r) aprog bprog)
-            | _ => None
-            end
-          end))
-
-      | MFunexp e a =>
-        let conv := (fun x => convertProgram' x mapF (S nextFree) tmp) in
-        omap (conv 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 (CReg _ TLt rf rt)
-                (ASeq aprog (ASeq 
-                (AOp (IOpConst Add rf (iconst (natToWord _ 1))))
-                (AAssign (AConstInt rt (iconst (natToWord _ e))))))))
-          | _ => None
-          end)
-
-      | MDef lbl f a =>
-        omap (convertProgram' f mapF nextFree tmp) (fun fprog =>
-          omap (convertProgram' a mapF (S nextFree) tmp) (fun aprog =>
-            Some (ADef lbl fprog aprog)))
-      | MCall lbl => Some (ACall lbl)
-      end.
-
-    (* TODO (rsloan): make these into parameters *)
-    Definition convertProgram (prog: M.Program): option AlmostQhasm.Program :=
-      convertProgram' prog tmpMap 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/Qhasm.v b/src/Assembly/Qhasm.v
index 9558f23ae..8dd2b9e78 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -7,7 +7,10 @@ Module Qhasm <: Language.
   Import QhasmEval.
 
   (* A constant upper-bound on the number of operations we run *)
-  Definition State := State.
+  Definition Params := unit.
+  Definition State := fun (_: Params) => State.
+
+  Transparent Params.
 
   (* Program Types *)
   Inductive QhasmStatement :=
@@ -20,25 +23,25 @@ Module Qhasm <: Language.
 
   Hint Constructors QhasmStatement.
 
-  Definition Program := list QhasmStatement.
+  Definition Program := fun (_: Params) => list QhasmStatement.
 
   (* Only execute while loops a fixed number of times.
      TODO (rsloan): can we do any better? *)
 
-  Fixpoint getLabelMap' (prog: Program) (cur: LabelMap) (index: nat): LabelMap :=
+  Fixpoint getLabelMap' {x} (prog: Program x) (cur: LabelMap) (index: nat): LabelMap :=
     match prog with
     | p :: ps =>
       match p with
-      | QLabel label => getLabelMap' ps (NatM.add label index cur) (S index)
-      | _ => getLabelMap' ps cur (S index)
+      | QLabel label => @getLabelMap' x ps (NatM.add label index cur) (S index)
+      | _ => @getLabelMap' x ps cur (S index)
       end
     | [] => cur
     end.
 
-  Definition getLabelMap (prog: Program): LabelMap :=
+  Definition getLabelMap {x} (prog: Program x): LabelMap :=
     getLabelMap' prog (NatM.empty nat) O.
 
-  Inductive QhasmEval: nat -> Program -> LabelMap -> State -> State -> Prop :=
+  Inductive QhasmEval {x}: nat -> Program x -> LabelMap -> State x -> State x -> Prop :=
     | QEOver: forall p n m s, (n > (length p))%nat -> QhasmEval n p m s s
     | QEZero: forall p s m, QhasmEval O p m s s
     | QEAssign: forall n p m a s s' s'',
@@ -77,7 +80,7 @@ Module Qhasm <: Language.
       -> QhasmEval (S n) p m s s'
       -> QhasmEval n p m s s'.
 
-  Definition evaluatesTo := fun p => QhasmEval O p (getLabelMap p).
+  Definition evaluatesTo := fun (x: Params) p => @QhasmEval x O p (getLabelMap p).
 
   (* world peace *)
 End Qhasm.
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 8a9d0d51f..21f846cb5 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -93,7 +93,7 @@ Inductive Conditional :=
 Inductive Mapping (n: nat) :=
   | regM: forall (r: Reg n), Mapping n
   | stackM: forall (s: Stack n), Mapping n
-  | memM: forall {m} (x: Mem n m), Mapping n
+  | memM: forall {m} (x: Mem n m) (i: Index m), Mapping n
   | constM: forall (x: Const n), Mapping n.
 
 (* Parameter Accessors *)
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 83ef5b701..b12e27e19 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,7 +1,7 @@
 Require Export QhasmCommon QhasmUtil State.
 Require Export ZArith Sumbool.
 Require Export Bedrock.Word.
-Require Import Logic.Eqdep_dec.
+Require Import Logic.Eqdep_dec ProofIrrelevance.
 
 Import Util.
 
@@ -116,12 +116,11 @@ Module EvalUtil.
         then left _
         else right _
 
-    | (memM _ v, memM _ v') => fun _ => 
+    | (memM _ v i, memM _ v' i') => fun _ => 
         if (Nat.eq_dec (memName v) (memName v')) 
         then if (Nat.eq_dec (memLength v) (memLength v'))
-        then left _
-        else right _
-        else right _
+        then if (Nat.eq_dec (proj1_sig i) (proj1_sig i'))
+        then left _ else right _ else right _ else right _
 
     | _ => fun _ => right _
     end (eq_refl (a, b))); abstract (
@@ -137,6 +136,8 @@ Module EvalUtil.
           rewrite _H0
         | apply (inj_pair2_eq_dec _ Nat.eq_dec) in H3
         | inversion H; subst; intuition
+        | destruct i, i'; simpl in _H2; subst;
+          replace l with l0 by apply proof_irrelevance
         | intuition ]).
   Defined.
 
@@ -170,41 +171,6 @@ Module EvalUtil.
       end
     end.
 
-    (* Mapping Identifier-Triples *)
-
-  Definition mappingId {n} (x: Mapping n): nat * nat * nat :=
-    match x with
-    | regM (reg n _ v) => (0, n, v)
-    | stackM (stack n _ v) => (1, n, v)
-    | constM (const n _ w) => (2, n, wordToNat w)
-    | memM _ (mem n m _ v) => (3, m, v)
-    end.
-
-  Lemma id_equal: forall {n: nat} (x y: Mapping n),
-    x = y <-> mappingId x = mappingId y.
-  Proof.
-    intros; split; intros; try abstract (rewrite H; intuition);
-      destruct x as [x | x | x | x], y as [y | y | y | y];
-      destruct x, y; unfold mappingId in H; simpl in H;
-
-      repeat match goal with
-      | [X: (_, _, _) = (_, _, _) |- _ ] =>
-        apply Triple_as_OT.conv in X
-      | [X: _ /\ _ /\ _ |- _ ] => destruct X
-      | [X: _ /\ _ |- _ ] => destruct X
-      | [A: Width _, B: Width _ |- _ ] =>
-        replace A with B by (apply width_eq)
-      | [X: context[match ?a with | _ => _ end] |- _ ] =>
-        destruct a
-      end; try subst; try omega; intuition.
-
-    rewrite <- (natToWord_wordToNat w0);
-      rewrite <- (natToWord_wordToNat w2);
-      rewrite H1; intuition.
-  Qed.
-
-  Definition id_dec := Triple_as_OT.eq_dec.
-
 End EvalUtil.
 
 Module QhasmEval.
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 7d1edcf6b..9e96a0f31 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -190,9 +190,9 @@ End StateCommon.
 Module ListState.
   Export StateCommon.
 
-  Definition ListState (n: nat) := ((list (word n)) * PairNMap * (option bool))%type.
+  Definition ListState (n: nat) := ((list (word n)) * TripleNMap * (option bool))%type.
 
-  Definition emptyState {n}: ListState n := ([], PairM.empty N, None).
+  Definition emptyState {n}: ListState n := ([], TripleM.empty N, None).
 
   Definition getVar {n: nat} (name: nat) (st: ListState n): option (word n) :=
     nth_error (fst (fst st)) name.
@@ -204,10 +204,10 @@ Module ListState.
     (lst, snd (fst st), snd st).
 
   Definition getMem {n: nat} (name index: nat) (st: ListState n): option (word n) :=
-    omap (PairM.find (name, index) (snd (fst st))) (fun v => Some (NToWord n v)).
+    omap (TripleM.find (n, name, index) (snd (fst st))) (fun v => Some (NToWord n v)).
 
   Definition setMem {n: nat} (name index: nat) (v: word n) (st: ListState n): ListState n :=
-    (fst (fst st), PairM.add (name, index) (wordToN v) (snd (fst st)), snd st).
+    (fst (fst st), TripleM.add (n, name, index) (wordToN v) (snd (fst st)), snd st).
 
   Definition getCarry {n: nat} (st: ListState n): option bool := (snd st).
 
@@ -219,34 +219,6 @@ Module ListState.
 
 End ListState.
 
-Module MedState.
-  Export StateCommon.
-
-  Definition MedState (n: nat) := (NatNMap * PairNMap * (option bool))%type.
-
-  Definition emptyState {n}: MedState n := (NatM.empty N, PairM.empty N, None).
-
-  Definition getVar {n: nat} (name: nat) (st: MedState n): option (word n) :=
-    omap (NatM.find name (fst (fst st))) (fun v => Some (NToWord n v)).
-
-  Definition setVar {n: nat} (name: nat) (v: word n) (st: MedState n): MedState n :=
-    (NatM.add name (wordToN v) (fst (fst st)), snd (fst st), snd st).
-
-  Definition getMem {n: nat} (name index: nat) (st: MedState n): option (word n) :=
-    omap (PairM.find (name, index) (snd (fst st))) (fun v => Some (NToWord n v)).
-
-  Definition setMem {n: nat} (name index: nat) (v: word n) (st: MedState n): MedState n :=
-    (fst (fst st), PairM.add (name, index) (wordToN v) (snd (fst st)), snd st).
-
-  Definition getCarry {n: nat} (st: MedState n): option bool := (snd st).
-
-  Definition setCarry {n: nat} (v: bool) (st: MedState n): MedState n :=
-    (fst st, Some v).
-
-  Definition setCarryOpt {n: nat} (v: option bool) (st: MedState n): MedState n :=
-    (fst st, v).
-End MedState.
-
 Module FullState.
   Export StateCommon.
 
@@ -351,5 +323,4 @@ Module FullState.
     | Some c' => setCarry c' state
     | _ => state
     end.
-
 End FullState.
\ No newline at end of file
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 46fce9b60..151eaa3f7 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -188,7 +188,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
 
     Arguments regM [n] r.
     Arguments stackM [n] s.
-    Arguments memM [n m] x.
+    Arguments memM [n m] x i.
     Arguments constM [n] x.
 
     Fixpoint entries (width: nat) (prog: Program): list (Mapping width) :=
@@ -199,8 +199,8 @@ Module StringConversion <: Conversion Qhasm QhasmString.
           match a with
           | ARegStack n r s => convM [regM r; stackM s]
           | AStackReg n s r => convM [regM r; stackM s]
-          | ARegMem n m a b i => convM [regM a; memM b]
-          | AMemReg n m a i b => convM [memM a; regM b]
+          | ARegMem n m a b i => convM [regM a; memM b i]
+          | AMemReg n m a i b => convM [memM a i; regM b]
           | ARegReg n a b => convM [regM a; regM b]
           | AConstInt n r c => convM [regM r; constM c]
           end
@@ -209,7 +209,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
           | IOpConst _ o a c => convM [regM a; constM c]
           | IOpReg _ o a b => convM [regM a; regM b]
           | IOpStack _ o a b => convM [regM a; stackM b]
-          | IOpMem _ _ o a b i => convM [regM a; memM b]
+          | IOpMem _ _ o a b i => convM [regM a; memM b i]
           | DOp _ o a b (Some x) => convM [regM a; regM b; regM x]
           | DOp _ o a b None => convM [regM a; regM b]
           | ROp _ o a i => convM [regM a]
@@ -254,7 +254,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
 
     Definition getMemNames (n: nat) (lst: list (Mapping n)): list nat :=
       flatMapOpt (dedup lst) (fun e =>
-        match e with | memM _ (mem _ _ _ x) => Some x | _ => None end).
+        match e with | memM _ (mem _ _ _ x) _ => Some x | _ => None end).
 
     Fixpoint getInputs' (n: nat) (prog: list QhasmStatement) (init: list (Mapping n)): list (Mapping n) :=
       let f := fun rs => filter (fun x =>
@@ -268,8 +268,8 @@ Module StringConversion <: Conversion Qhasm QhasmString.
           match a with
           | ARegStack n r s   => g ([stackM s], [regM r; stackM s])
           | AStackReg n s r   => g ([regM r], [regM r; stackM s])
-          | ARegMem n m r x i => g ([memM x], [regM r; memM x])
-          | AMemReg n m x i r => g ([regM r], [regM r; memM x])
+          | ARegMem n m r x i => g ([memM x i], [regM r; memM x i])
+          | AMemReg n m x i r => g ([regM r], [regM r; memM x i])
           | ARegReg n a b     => g ([regM b], [regM a; regM b])
           | AConstInt n r c   => g ([], [regM r])
           end
@@ -278,7 +278,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
           | IOpConst _ o a c     => g ([regM a], [regM a])
           | IOpReg _ o a b       => g ([regM a], [regM a; regM b])
           | IOpStack _ o a b     => g ([regM a], [regM a; stackM b])
-          | IOpMem _ _ o a b i   => g ([regM a], [regM a; memM b])
+          | IOpMem _ _ o a b i   => g ([regM a], [regM a; memM b i])
           | DOp _ o a b (Some x) => g ([regM a; regM b], [regM a; regM b; regM x])
           | DOp _ o a b None     => g ([regM a; regM b], [regM a; regM b])
           | ROp _ o a i          => g ([regM a], [regM a])
@@ -313,7 +313,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
         | W64 => Some ("stack64 " ++ (stack w x))%string
         end
 
-      | memM _ (mem _ m w x) =>
+      | memM _ (mem _ m w x) _ =>
         match w with
         | W32 => Some ("stack32 " ++ (@mem _ m w x))%string
         | W64 => Some ("stack64 " ++ (@mem _ m w x))%string
@@ -326,7 +326,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       match x with
       | regM r => Some ("input " ++ r)%string
       | stackM s => Some ("input " ++ s)%string
-      | memM _ m => Some ("input " ++ m)%string
+      | memM _ m i => Some ("input " ++ m)%string
       | _ => None
       end.
 
-- 
cgit v1.2.3