Generalized and cleaned up state model

7 files changed, 412 insertions, 416 deletions

diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
index d50e3a6bd..e33186bea 100644
--- a/src/Assembly/AlmostQhasm.v
+++ b/src/Assembly/AlmostQhasm.v
@@ -3,8 +3,7 @@ Require Import Language.
 Require Import List.
 
 Module AlmostQhasm <: Language.
-  Import ListNotations.
-  Import State.
+  Import QhasmEval.
 
   (* Program Types *)
   Definition State := State.
diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v
index 90f6afd73..e46dd5547 100644
--- a/src/Assembly/Medial.v
+++ b/src/Assembly/Medial.v
@@ -2,22 +2,14 @@ Require Import QhasmEvalCommon Pseudo.
 Require Import Language.
 Require Import List.
 
-Module Medial (M: PseudoMachine) <: Language.
-  Import ListNotations.
-  Import State.
-  Import M.
+Module Medial (Arch: PseudoMachine) <: Language.
+  Import MedState EvalUtil Arch.
 
   Definition W := word width.
 
   (* Program Types *)
-  Definition State := (NatNMap * PairNMap * (option bool))%type.
-
-  Definition varS (st: State) := fst (fst st).
-  Definition memS (st: State) := snd (fst st).
-  Definition carryS (st: State) := snd st.
-
-  Definition var (i: nat) (st: State) := NatM.find i (varS st).
-  Definition mem (v i: nat) (st: State) := PairM.find (v, i) (memS st).
+  Definition State := MedState width.
+  Transparent State.
 
   Inductive MAssignment : Type :=
     | MAVar: nat -> nat -> MAssignment 
@@ -83,65 +75,66 @@ Module Medial (M: PseudoMachine) <: Language.
     | MAssign a =>
       match a with
       | MAVar x y =>
-        match (var y st) with
-        | Some v => Some (NatM.add x v (varS st), memS st, carryS st)
+        match (getVar y st) with
+        | Some v => Some (setVar x v st)
         | _ => None
         end
 
       | MAMem x y i =>
-        match (mem y i st) with
-        | Some v => Some (NatM.add x v (varS st), memS st, carryS st)
+        match (getMem y i st) with
+        | Some v => Some (setVar x v st)
         | _ => None
         end
 
-      | MAConst x c => Some (NatM.add x (wordToN c) (varS st), memS st, carryS st)
+      | MAConst x c => Some (setVar x c st)
       end
 
     | MOp o =>
       match o with
       | MIOpConst io a c =>
-        omap (var a st) (fun v =>
-          let (res, c') := evalIntOp io (NToWord _ v) c in
-          Some (NatM.add a (wordToN res) (varS st), memS st, 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 (var a st) (fun va =>
-          omap (var b st) (fun vb =>
-            let (res, c') := evalIntOp io (NToWord width va) (NToWord width vb) in
-            Some (NatM.add a (wordToN res) (varS st), memS st, c')))
+        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 (var a st) (fun va =>
-          omap (var b st) (fun vb =>
-            let c := match (carryS st) with | Some b => b | _ => false end in
-            let (res, c') := evalCarryOp o (NToWord width va) (NToWord width vb) c in
-            Some (NatM.add a (wordToN res) (varS st), memS st, Some c')))
+        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 (var a st) (fun va =>
-          omap (var 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)) (varS st)), memS st, carryS st)))
+        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 (var a st) (fun va =>
-          omap (var b st) (fun vb =>
-            let res := evalDualOp duo (NToWord width va) (NToWord width vb) in
-            Some (NatM.add a (wordToN (fst res)) (varS st), memS st, carryS st)))
+        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 (var a st) (fun v =>
-          let res := evalRotOp ro (NToWord width v) (proj1_sig x) in
-          Some (NatM.add a (wordToN res) (varS st), memS st, carryS st))
+        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
       | MC t x y =>
-        omap (var x st) (fun vx =>
-          omap (var y st) (fun vy =>
-            if (evalTest t (NToWord width vx) (NToWord width vy))
+        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))
       end
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index af5dd3891..a0ebf7255 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -9,17 +9,11 @@ Module Type PseudoMachine.
 End PseudoMachine.
 
 Module Pseudo (M: PseudoMachine) <: Language.
-  Import ListNotations State Util M.
+  Import EvalUtil ListState Util M.
 
   Definition const: Type := word width.
 
   (* Program Types *)
-  Definition State := ((list const) * (list (list const)) * (option bool))%type.
-
-  Definition var (st: State)  := fst (fst st).
-  Definition mem (st: State)  := snd (fst st).
-  Definition carry (st: State) := snd st.
-
   Inductive Pseudo: nat -> nat -> Type :=
     | PVar: forall n, Index n -> Pseudo n 1
     | PMem: forall n m, Index n -> Index m -> Pseudo n 1
@@ -40,64 +34,60 @@ Module Pseudo (M: PseudoMachine) <: Language.
   Hint Constructors Pseudo.
 
   Definition Program := Pseudo vars vars.
+  Definition State := ListState width.
 
   Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State :=
     match prog with
-    | PVar n i =>
-      omap (nth_error (var st) i) (fun x =>
-        Some ([x], mem st, carry st))
-
-    | PMem n m v i =>
-      omap (nth_error (mem st) v) (fun vec =>
-        omap (nth_error vec i) (fun x =>
-          Some ([x], mem st, carry st)))
-
-    | PConst n c => Some ([c], mem st, carry st)
-
+    | 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))
+    | PConst n c => Some (setList [c] st)
     | PBin n o p =>
       omap (pseudoEval p st) (fun sp =>
-        match sp with
-        | ([wa; wb], m', _) =>
-          let (v, c) := evalIntOp o wa wb in Some ([v], m', c)
+        match (getList sp) with
+        | [wa; wb] =>
+          let (v, c) := evalIntOp o wa wb in
+          Some (setList [v] (setCarryOpt c sp))
         | _ => None
         end)
 
     | PCarry n o p =>
       omap (pseudoEval p st) (fun sp =>
-        match sp with
-        | ([wa; wb], m', Some c) =>
-          let (v, c') := evalCarryOp o wa wb c in Some ([v], m', Some c')
+        match (getList sp, getCarry sp) with
+        | ([wa; wb], Some c) =>
+          let (v, c') := evalCarryOp o wa wb c in
+          Some (setList [v] (setCarry c' sp))
         | _ => None
         end)
 
     | PDual n o p =>
       omap (pseudoEval p st) (fun sp =>
-        match sp with
-        | ([wa; wb], m', co) =>
-          let (low, high) := evalDualOp o wa wb in Some ([low; high], m', co)
+        match (getList sp) with
+        | [wa; wb] =>
+          let (low, high) := evalDualOp o wa wb in
+          Some (setList [low; high] sp)
         | _ => None
         end)
 
     | PShift n o a x =>
       omap (pseudoEval x st) (fun sx =>
-        match sx with
-        | ([wx], m', co) => Some ([evalRotOp o wx a], m', co)
+        match (getList sx) with
+        | [wx] => Some (setList [evalRotOp o wx a] sx)
         | _ => None
         end)
 
     | PLet n k m f g =>
       omap (pseudoEval f st) (fun sf =>
-        omap (pseudoEval g ((var st) ++ (var sf), mem sf, carry sf))
+        omap (pseudoEval g (setList ((getList st) ++ (getList sf)) sf))
           (fun sg => Some sg))
 
     | PComb n a b f g =>
       omap (pseudoEval f st) (fun sf =>
         omap (pseudoEval g st) (fun sg =>
-          Some ((var sf) ++ (var sg), mem sg, carry sg)))
+          Some (setList ((getList sf) ++ (getList sg)) sg)))
 
     | PIf n m t i0 i1 l r =>
-      omap (nth_error (var st) i0) (fun v0 =>
-        omap (nth_error (var st) i1) (fun v1 =>
+      omap (getVar i0 st) (fun v0 =>
+        omap (getVar i1 st) (fun v1 =>
           if (evalTest t v0 v1)
           then pseudoEval l st
           else pseudoEval r st ))
diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v
index 79653136c..48625e011 100644
--- a/src/Assembly/PseudoMedialConversion.v
+++ b/src/Assembly/PseudoMedialConversion.v
@@ -12,60 +12,6 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
   Module P := Pseudo Arch.
   Module M := Medial Arch.
 
-  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.
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
index 193114d14..0f96b6bab 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -4,7 +4,7 @@ Require Import List NPeano.
 
 Module Qhasm <: Language.
   Import ListNotations.
-  Import State.
+  Import QhasmEval.
 
   (* A constant upper-bound on the number of operations we run *)
   Definition State := State.
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index fba8428ee..3e2411303 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -3,284 +3,291 @@ Require Export ZArith Sumbool.
 Require Export Bedrock.Word.
 Require Import Logic.Eqdep_dec.
 
-Import State.
 Import Util.
 
-Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
-  let c := (N.compare (wordToN a) (wordToN b)) in
-
-  let eqBit := match c with | Eq => true | _ => false end in
-  let ltBit := match c with | Lt => true | _ => false end in
-  let gtBit := match c with | Gt => true | _ => false end in
-
-  match o with
-  | TEq => eqBit
-  | TLt => ltBit
-  | TLe => orb (eqBit) (ltBit)
-  | TGt => gtBit
-  | TGe => orb (eqBit) (gtBit)
-  end.
-
-Definition evalCond (c: Conditional) (state: State): option bool :=
-  match c with
-  | CTrue => Some true
-  | CZero n r =>
-    omap (getReg r state) (fun v =>
-      if (Nat.eq_dec O (wordToNat v))
-      then Some true
-      else Some false) 
-  | CReg n o a b =>
-    omap (getReg a state) (fun va =>
-      omap (getReg b state) (fun vb =>
-        Some (evalTest o va vb)))
-  | CConst n o a c => 
-    omap (getReg a state) (fun va =>
-      Some (evalTest o va (constValueW c)))
-  end.
-
-Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool :=
-  match io with
-  | Add =>
-    let v := (wordToN x + wordToN y)%N in
-    let c := (N.compare v (Npow2 b)) in
-
-    match c as c' return c' = c -> _ with
-    | Lt => fun _ => (NToWord b v, Some false)
-    | _ => fun _ => (NToWord b v, Some true)
-    end eq_refl
-
-  | Sub => (wminus x y, None)
-  | Xor => (wxor x y, None)
-  | And => (wand x y, None)
-  | Or => (wor x y, None)
-  end.
-
-Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool :=
-  match io with
-  | AddWidthCarry =>
-    let v := (wordToN x + wordToN y + (if c then 1%N else 0%N))%N in
-    let c := (N.compare v (Npow2 b)) in
-
-    match c as c' return c' = c -> _ with
-    | Lt => fun _ => (NToWord b v, false)
-    | _ => fun _ => (NToWord b v, true)
-    end eq_refl
-  end.
-
-Definition evalDualOp {b} (duo: DualOp) (x y: word b) :=
-  match duo with
-  | Mult =>
-    let v := (wordToN x * wordToN y)%N in
-    let wres := NToWord (b + b) v in
-    (split1 b b wres, split2 b b wres)
-  end.
-
-Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
-  match ro with
-  | Shl => NToWord b (N.shiftl_nat (wordToN x) n)
-  | Shr => NToWord b (N.shiftr_nat (wordToN x) n)
-  end.
-
-Definition evalOperation (o: Operation) (state: State): option State :=
-  match o with
-  | IOpConst _ o r c =>
-    omap (getReg r state) (fun v =>
-      let (v', co) := (evalIntOp o v (constValueW c)) in
-      Some (setCarryOpt co (setReg r v' state)))
-
-  | IOpReg _ o a b =>
-    omap (getReg a state) (fun va =>
-      omap (getReg b state) (fun vb =>
-        let (v', co) := (evalIntOp o va vb) in
-        Some (setCarryOpt co (setReg a v' state))))
-
-  | IOpMem _ _ o r m i => 
-    omap (getReg r state) (fun va =>
-      omap (getMem m i state) (fun vb =>
-        let (v', co) := (evalIntOp o va vb) in
-        Some (setCarryOpt co (setReg r v' state))))
-
-  | DOp _ o a b (Some x) => 
-    omap (getReg a state) (fun va =>
-      omap (getReg b state) (fun vb =>
-        let (low, high) := (evalDualOp o va vb) in
-        Some (setReg x high (setReg a low state))))
-
-  | DOp _ o a b None => 
-    omap (getReg a state) (fun va =>
-      omap (getReg b state) (fun vb =>
-        let (low, high) := (evalDualOp o va vb) in
-        Some (setReg a low state)))
-
-  | ROp _ o r i => 
-    omap (getReg r state) (fun v =>
-      let v' := (evalRotOp o v i) in
-      Some (setReg r v' state))
-
-  | COp _ o a b => 
-    omap (getReg a state) (fun va =>
-      omap (getReg b state) (fun vb =>
-        match (getCarry state) with
-        | None => None
-        | Some c0 => 
-          let (v', c') := (evalCarryOp o va vb c0) in
-          Some (setCarry c' (setReg a v' state))
-        end))
-  end.
-
-Definition evalAssignment (a: Assignment) (state: State): option State :=
-  match a with
-  | ARegMem _ _ r m i => 
-    omap (getMem m i state) (fun v => Some (setReg r v state))
-  | AMemReg _ _ m i r =>
-    omap (getReg r state) (fun v => Some (setMem m i v state))
-  | AStackReg _ a b =>
-    omap (getReg b state) (fun v => Some (setStack a v state))
-  | ARegStack _ a b =>
-    omap (getStack b state) (fun v => Some (setReg a v state))
-  | ARegReg _ a b => 
-    omap (getReg b state) (fun v => Some (setReg a v state))
-  | AConstInt _ r c =>
-    Some (setReg r (constValueW c) state)
-  end.
-
-(* Width decideability *)
-
-Definition getWidth (n: nat): option (Width n) :=
-  match n with
-  | 32 => Some W32
-  | 64 => Some W64
-  | _ => None
-  end.
-
-Lemma getWidth_eq {n} (a: Width n): Some a = getWidth n.
-Proof. induction a; unfold getWidth; simpl; intuition. Qed.
-
-Lemma width_eq {n} (a b: Width n): a = b.
-Proof. 
-  assert (Some a = Some b) as H by (
-    replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition);
-    replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition);
-    intuition).
-  inversion H; intuition.
-Qed. 
-
-(* Mapping Conversions *)
-
-Definition wordToM {n: nat} {spec: Width n} (w: word n): Mapping n :=
-  constM _ (const spec w).
-
-Definition regToM {n: nat} {spec: Width n} (r: Reg n): Mapping n :=
-  regM _ r.
-
-Definition stackToM {n: nat} {spec: Width n} (s: Stack n): Mapping n :=
-  stackM _ s.
-
-Definition constToM {n: nat} {spec: Width n} (c: Const n): Mapping n :=
-  constM _ c.
-
-Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}.
-  refine (match (a, b) as p' return (a, b) = p' -> _ with
-  | (regM v, regM v') => fun _ => 
-    if (Nat.eq_dec (regName v) (regName v'))
-    then left _
-    else right _
-
-  | (stackM v, stackM v') => fun _ => 
-    if (Nat.eq_dec (stackName v) (stackName v'))
-    then left _
-    else right _
-
-  | (constM v, constM v') => fun _ => 
-    if (Nat.eq_dec (constValueN v) (constValueN v'))
-    then left _
-    else right _
-
-  | (memM _ v, memM _ v') => fun _ => 
-    if (Nat.eq_dec (memName v) (memName v')) 
-    then if (Nat.eq_dec (memLength v) (memLength v'))
-      then left _
-      else right _
-    else right _
-
-  | _ => fun _ => right _
-  end (eq_refl (a, b))); abstract (
-    inversion_clear _H;
-    unfold regName, stackName, constValueN, memName, memLength in *;
-    intuition; try inversion H;
-    destruct v, v'; subst;
-    try assert (w = w0) by (apply width_eq); do 3 first [
-      contradict _H0; inversion H1
-    | rewrite <- (natToWord_wordToNat w0);
+Module EvalUtil.
+  Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
+    let c := (N.compare (wordToN a) (wordToN b)) in
+
+    let eqBit := match c with | Eq => true | _ => false end in
+    let ltBit := match c with | Lt => true | _ => false end in
+    let gtBit := match c with | Gt => true | _ => false end in
+
+    match o with
+    | TEq => eqBit
+    | TLt => ltBit
+    | TLe => orb (eqBit) (ltBit)
+    | TGt => gtBit
+    | TGe => orb (eqBit) (gtBit)
+    end.
+
+  Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool :=
+    match io with
+    | Add =>
+      let v := (wordToN x + wordToN y)%N in
+      let c := (N.compare v (Npow2 b)) in
+
+      match c as c' return c' = c -> _ with
+      | Lt => fun _ => (NToWord b v, Some false)
+      | _ => fun _ => (NToWord b v, Some true)
+      end eq_refl
+
+    | Sub => (wminus x y, None)
+    | Xor => (wxor x y, None)
+    | And => (wand x y, None)
+    | Or => (wor x y, None)
+    end.
+
+  Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool :=
+    match io with
+    | AddWidthCarry =>
+      let v := (wordToN x + wordToN y + (if c then 1%N else 0%N))%N in
+      let c := (N.compare v (Npow2 b)) in
+
+      match c as c' return c' = c -> _ with
+      | Lt => fun _ => (NToWord b v, false)
+      | _ => fun _ => (NToWord b v, true)
+      end eq_refl
+    end.
+
+  Definition evalDualOp {b} (duo: DualOp) (x y: word b) :=
+    match duo with
+    | Mult =>
+      let v := (wordToN x * wordToN y)%N in
+      let wres := NToWord (b + b) v in
+      (split1 b b wres, split2 b b wres)
+    end.
+
+  Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
+    match ro with
+    | Shl => NToWord b (N.shiftl_nat (wordToN x) n)
+    | Shr => NToWord b (N.shiftr_nat (wordToN x) n)
+    end.
+
+  (* Width decideability *)
+
+  Definition getWidth (n: nat): option (Width n) :=
+    match n with
+    | 32 => Some W32
+    | 64 => Some W64
+    | _ => None
+    end.
+
+  Lemma getWidth_eq {n} (a: Width n): Some a = getWidth n.
+  Proof. induction a; unfold getWidth; simpl; intuition. Qed.
+
+  Lemma width_eq {n} (a b: Width n): a = b.
+  Proof. 
+    assert (Some a = Some b) as H by (
+      replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition);
+      replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition);
+      intuition).
+    inversion H; intuition.
+  Qed. 
+
+  (* Mapping Conversions *)
+
+  Definition wordToM {n: nat} {spec: Width n} (w: word n): Mapping n :=
+    constM _ (const spec w).
+
+  Definition regToM {n: nat} {spec: Width n} (r: Reg n): Mapping n :=
+    regM _ r.
+
+  Definition stackToM {n: nat} {spec: Width n} (s: Stack n): Mapping n :=
+    stackM _ s.
+
+  Definition constToM {n: nat} {spec: Width n} (c: Const n): Mapping n :=
+    constM _ c.
+
+  Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}.
+    refine (match (a, b) as p' return (a, b) = p' -> _ with
+    | (regM v, regM v') => fun _ => 
+        if (Nat.eq_dec (regName v) (regName v'))
+        then left _
+        else right _
+
+    | (stackM v, stackM v') => fun _ => 
+        if (Nat.eq_dec (stackName v) (stackName v'))
+        then left _
+        else right _
+
+    | (constM v, constM v') => fun _ => 
+        if (Nat.eq_dec (constValueN v) (constValueN v'))
+        then left _
+        else right _
+
+    | (memM _ v, memM _ v') => fun _ => 
+        if (Nat.eq_dec (memName v) (memName v')) 
+        then if (Nat.eq_dec (memLength v) (memLength v'))
+        then left _
+        else right _
+        else right _
+
+    | _ => fun _ => right _
+    end (eq_refl (a, b))); abstract (
+      inversion_clear _H;
+      unfold regName, stackName, constValueN, memName, memLength in *;
+      intuition; try inversion H;
+      destruct v, v'; subst;
+      try assert (w = w0) by (apply width_eq); do 3 first [
+          contradict _H0; inversion H1
+        | rewrite <- (natToWord_wordToNat w0);
+          rewrite <- (natToWord_wordToNat w2);
+          assert (w = w1) by (apply width_eq); subst;
+          rewrite _H0
+        | apply (inj_pair2_eq_dec _ Nat.eq_dec) in H3
+        | inversion H; subst; intuition
+        | intuition ]).
+  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 stackNames {n} (lst: list (Mapping n)): list nat :=
+    match lst with
+    | nil => nil
+    | cons c cs =>
+      match c with
+      | stackM v => cons (stackName v) (stackNames cs)
+      | _ => stackNames cs
+      end
+    end.
+
+  Fixpoint regNames {n} (lst: list (Mapping n)): list nat :=
+    match lst with
+    | nil => nil
+    | cons c cs =>
+      match c with
+      | regM v => cons (regName v) (regNames cs)
+      | _ => regNames cs
+      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);
-      assert (w = w1) by (apply width_eq); subst;
-      rewrite _H0
-    | apply (inj_pair2_eq_dec _ Nat.eq_dec) in H3
-    | inversion H; subst; intuition
-    | intuition ]).
-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 stackNames {n} (lst: list (Mapping n)): list nat :=
-  match lst with
-  | nil => nil
-  | cons c cs =>
-    match c with
-    | stackM v => cons (stackName v) (stackNames cs)
-    | _ => stackNames cs
-    end
-  end.
-
-Fixpoint regNames {n} (lst: list (Mapping n)): list nat :=
-  match lst with
-  | nil => nil
-  | cons c cs =>
+      rewrite H1; intuition.
+  Qed.
+
+  Definition id_dec := Triple_as_OT.eq_dec.
+
+End EvalUtil.
+
+Module QhasmEval.
+  Export EvalUtil FullState.
+
+  Definition evalCond (c: Conditional) (state: State): option bool :=
     match c with
-    | regM v => cons (regName v) (regNames cs)
-    | _ => regNames cs
-    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.
+    | CTrue => Some true
+    | CZero n r =>
+      omap (getReg r state) (fun v =>
+        if (Nat.eq_dec O (wordToNat v))
+        then Some true
+        else Some false) 
+    | CReg n o a b =>
+      omap (getReg a state) (fun va =>
+        omap (getReg b state) (fun vb =>
+          Some (evalTest o va vb)))
+    | CConst n o a c => 
+      omap (getReg a state) (fun va =>
+        Some (evalTest o va (constValueW c)))
+    end.
+
+  Definition evalOperation (o: Operation) (state: State): option State :=
+    match o with
+    | IOpConst _ o r c =>
+      omap (getReg r state) (fun v =>
+        let (v', co) := (evalIntOp o v (constValueW c)) in
+        Some (setCarryOpt co (setReg r v' state)))
+
+    | IOpReg _ o a b =>
+      omap (getReg a state) (fun va =>
+        omap (getReg b state) (fun vb =>
+            let (v', co) := (evalIntOp o va vb) in
+            Some (setCarryOpt co (setReg a v' state))))
+
+    | IOpMem _ _ o r m i => 
+      omap (getReg r state) (fun va =>
+        omap (getMem m i state) (fun vb =>
+            let (v', co) := (evalIntOp o va vb) in
+            Some (setCarryOpt co (setReg r v' state))))
+
+    | DOp _ o a b (Some x) => 
+      omap (getReg a state) (fun va =>
+        omap (getReg b state) (fun vb =>
+            let (low, high) := (evalDualOp o va vb) in
+            Some (setReg x high (setReg a low state))))
+
+    | DOp _ o a b None => 
+      omap (getReg a state) (fun va =>
+        omap (getReg b state) (fun vb =>
+            let (low, high) := (evalDualOp o va vb) in
+            Some (setReg a low state)))
+
+    | ROp _ o r i => 
+      omap (getReg r state) (fun v =>
+        let v' := (evalRotOp o v i) in
+        Some (setReg r v' state))
+
+    | COp _ o a b => 
+      omap (getReg a state) (fun va =>
+        omap (getReg b state) (fun vb =>
+            match (getCarry state) with
+            | None => None
+            | Some c0 => 
+            let (v', c') := (evalCarryOp o va vb c0) in
+            Some (setCarry c' (setReg a v' state))
+            end))
+    end.
+
+  Definition evalAssignment (a: Assignment) (state: State): option State :=
+    match a with
+    | ARegMem _ _ r m i => 
+      omap (getMem m i state) (fun v => Some (setReg r v state))
+    | AMemReg _ _ m i r =>
+      omap (getReg r state) (fun v => Some (setMem m i v state))
+    | AStackReg _ a b =>
+      omap (getReg b state) (fun v => Some (setStack a v state))
+    | ARegStack _ a b =>
+      omap (getStack b state) (fun v => Some (setReg a v state))
+    | ARegReg _ a b => 
+      omap (getReg b state) (fun v => Some (setReg a v state))
+    | AConstInt _ r c =>
+      Some (setReg r (constValueW c) state)
+    end.
+
+End QhasmEval.
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index df8bc97c1..33ab6efde 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -174,8 +174,8 @@ Module Triple_as_OT <: UsualOrderedType.
   Defined.
 End Triple_as_OT.
 
-Module State.
-  Import ListNotations Util.
+Module StateCommon.
+  Export ListNotations Util.
 
   Module NatM := FMapAVL.Make(Nat_as_OT).
   Module PairM := FMapAVL.Make(Pair_as_OT).
@@ -185,9 +185,70 @@ Module State.
   Definition PairNMap: Type := PairM.t N.
   Definition TripleNMap: Type := TripleM.t N.
   Definition LabelMap: Type := NatM.t nat.
+End StateCommon.
 
-  Delimit Scope state_scope with state.
-  Open Scope state_scope.
+Module ListState.
+  Export StateCommon.
+
+  Definition ListState (n: nat) := ((list (word n)) * PairNMap * (option bool))%type.
+
+  Definition emptyState {n}: ListState n := ([], PairM.empty N, None).
+
+  Definition getVar {n: nat} (name: nat) (st: ListState n): option (word n) :=
+    nth_error (fst (fst st)) name.
+
+  Definition getList {n: nat} (st: ListState n): list (word n) :=
+    fst (fst st).
+
+  Definition setList {n: nat} (lst: list (word n)) (st: ListState n): ListState n :=
+    (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)).
+
+  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).
+
+  Definition getCarry {n: nat} (st: ListState n): option bool := (snd st).
+
+  Definition setCarry {n: nat} (v: bool) (st: ListState n): ListState n :=
+    (fst st, Some v).
+
+  Definition setCarryOpt {n: nat} (v: option bool) (st: ListState n): ListState n :=
+    (fst st, v).
+
+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.
 
   (* The Big Definition *)
 
@@ -275,4 +336,4 @@ Module State.
     | _ => state
     end.
 
-End State.
\ No newline at end of file
+End FullState.
\ No newline at end of file