Major language refactoring to support Memory and AddWithCarry

7 files changed, 500 insertions, 534 deletions

diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v
index 6d2fa1b50..339a36bbc 100644
--- a/src/Assembly/AlmostConversion.v
+++ b/src/Assembly/AlmostConversion.v
@@ -17,7 +17,7 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
     | AOp a => [ QOp a ]
     | ACond c a b =>
       let tru := N.to_nat (N.shiftl 1 label0) in
-      let finish := S tru in
+      let finish := S tru 
       [QJmp c tru] ++
       (almostToQhasm' b label1) ++
       [QJmp TestTrue finish] ++
diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v
index 5e671775c..79653136c 100644
--- a/src/Assembly/PseudoMedialConversion.v
+++ b/src/Assembly/PseudoMedialConversion.v
@@ -12,11 +12,6 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
   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) _)
@@ -88,11 +83,6 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
       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 => []
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 5e2077c5a..fe6746382 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -1,72 +1,79 @@
 Require Export String List NPeano NArith.
 Require Export Bedrock.Word.
 
-(* A formalization of x86 qhasm *)
+(* Utilities *)
 Definition Label := nat.
+
 Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
+Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
 
-(* Sugar and Tactics *)
+Inductive Either A B :=
+  | xleft: A -> Either A B
+  | xright: B -> Either A B.
 
 Definition convert {A B: Type} (x: A) (H: A = B): B :=
   eq_rect A (fun B0 : Type => B0) x B H.
 
-Notation "'always' A" := (fun _ => A) (at level 90) : state_scope.
-Notation "'cast' e" := (convert e _) (at level 20) : state_scope.
-Notation "'lift' e" := (exist _ e _) (at level 20) : state_scope.
-Notation "'contra'" := (False_rec _ _) : state_scope.
-
-Obligation Tactic := abstract intuition.
-
 (* Asm Types *)
-Inductive ISize: nat -> Type :=
-  | I32: ISize 32
-  | I64: ISize 64.
+Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64.
 
-Inductive IConst: nat -> Type :=
-  | constInt32: word 32 -> IConst 32
-  | constInt64: word 64 -> IConst 64.
+(* A constant value *)
+Inductive Const: nat -> Type :=
+  | const: forall {n}, Width n -> word n -> Const n.
 
-Inductive IReg: nat -> Type :=
-  | regInt32: nat -> IReg 32
-  | regInt64: nat -> IReg 64.
+(* A variable in any register *)
+Inductive Reg: nat -> Type :=
+  | reg: forall {n}, Width n -> nat -> Reg n.
 
+(* A variable on the stack. We should use this sparingly. *)
 Inductive Stack: nat -> Type :=
-  | stack32: nat -> Stack 32
-  | stack64: nat -> Stack 64
-  | stack128: nat -> Stack 128.
+  | stack: forall {n}, Width n -> nat -> Stack n.
 
-Definition CarryState := option bool.
+(* A pointer to a memory block. Called as:
+     mem width index length
+   where length is in words of size width.
+
+   All Mem pointers will be declared as Stack arguments in the
+   resulting qhasm output *)
+Inductive Mem: nat -> nat -> Type :=
+  | mem: forall {n m}, Width n -> nat -> Mem n m.
+
+(* The state of the carry flag:
+   1       = Some true
+   0       = Some false
+   unknown = None *)
+Definition Carry := option bool.
 
 (* Assignments *)
-Inductive Assignment : Type :=
-  | ARegStackInt: forall n, IReg n -> Stack n -> Assignment
-  | AStackRegInt: forall n, Stack n -> IReg n -> Assignment
-  | ARegRegInt: forall n, IReg n -> IReg n -> Assignment
-  | AConstInt: forall n, IReg n -> IConst n -> Assignment
-  | AIndex: forall n m, IReg n -> Stack m -> Index (m/n)%nat -> Assignment
-  | APtr: forall n, IReg 32 -> Stack n -> Assignment.
 
-Hint Constructors Assignment.
+Inductive Assignment : Type :=
+  | ARegMem: forall {n m}, Reg n -> Mem n m -> Index m -> Assignment
+  | AMemReg: forall {n m}, Mem n m -> Index m -> Reg n -> Assignment
+  | AStackReg: forall {n}, Stack n -> Reg n -> Assignment
+  | ARegStack: forall {n}, Reg n -> Stack n -> Assignment
+  | ARegReg: forall {n}, Reg n -> Reg n -> Assignment
+  | AConstInt: forall {n}, Reg n -> Const n -> Assignment.
 
 (* Operations *)
 
 Inductive IntOp :=
-  | IPlus: IntOp | IMinus: IntOp
-  | IXor: IntOp  | IAnd: IntOp | IOr: IntOp.
+  | Add: IntOp  | Sub: IntOp
+  | Xor: IntOp  | And: IntOp
+  | Or: IntOp.
 
-Inductive DualOp :=
-  | IMult: DualOp.
+Inductive CarryOp := | AddWithCarry: CarryOp.
 
-Inductive RotOp :=
-  | Shl: RotOp | Shr: RotOp.
+Inductive DualOp := | Mult: DualOp.
 
-Inductive Operation :=
-  | IOpConst: forall n, IntOp -> IReg n -> IConst n -> Operation
-  | IOpReg: forall n, IntOp -> IReg n -> IReg n -> Operation
-  | DOpReg: forall n, DualOp -> IReg n -> IReg n -> option (IReg n) -> Operation
-  | OpRot: forall n, RotOp -> IReg n -> Index n -> Operation.
+Inductive RotOp := | Shl: RotOp | Shr: RotOp.
 
-Hint Constructors Operation.
+Inductive Operation :=
+  | IOpConst: forall {n}, IntOp -> Reg n -> Const n -> Operation
+  | IOpReg: forall {n}, IntOp -> Reg n -> Reg n -> Operation
+  | IOpMem: forall {n m}, IntOp -> Reg n -> Mem n m -> Index m -> Operation
+  | DOp: forall {n}, DualOp -> Reg n -> Reg n -> option (Reg n) -> Operation
+  | ROp: forall {n}, RotOp -> Reg n -> Index n -> Operation
+  | COp: forall {n}, CarryOp -> Reg n -> Reg n -> Operation.
 
 (* Control Flow *)
 
@@ -75,50 +82,47 @@ Inductive TestOp :=
   | TGt: TestOp   | TGe: TestOp.
 
 Inductive Conditional :=
-  | TestTrue: Conditional
-  | TestFalse: Conditional
-  | TestInt: forall n, TestOp -> IReg n -> IReg n -> Conditional.
-
-Hint Constructors Conditional.
-
-(* Reg, Stack, Const Utilities *)
-
-Definition getIRegWords {n} (x: IReg n) :=
-  match x with
-  | regInt32 loc => 1
-  | regInt64 loc => 2
-  end.
-
-Definition getStackWords {n} (x: Stack n) :=
-  match x with
-  | stack32 loc => 1
-  | stack64 loc => 2
-  | stack128 loc => 4
-  end.
-
-Definition getIConstValue {n} (x: IConst n): nat :=
-  match x with
-  | constInt32 v => wordToNat v
-  | constInt64 v => wordToNat v
-  end.
-
-Definition getIRegIndex {n} (x: IReg n): nat :=
-  match x with
-  | regInt32 loc => loc
-  | regInt64 loc => loc
-  end.
-
-Definition getStackIndex {n} (x: Stack n): nat :=
-  match x with
-  | stack32 loc => loc
-  | stack64 loc => loc
-  | stack128 loc => loc
-  end.
-
-(* For register allocation checking *)
-Definition intRegCount (base: nat): nat :=
-  match base with
-  | 32 => 7
-  | 64 => 8
-  | _ => 0
-  end.
+  | CTrue: Conditional 
+  | CZero: forall n, Reg n -> Conditional 
+  | CReg: forall n, TestOp -> Reg n -> Reg n -> Conditional 
+  | CConst: forall n, TestOp -> Reg n -> Const n -> Conditional.
+
+(* Generalized Variable Entry *)
+
+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
+  | constM: forall (x: Const n), Mapping n.
+
+(* Parameter Accessors *)
+
+Definition constWidth {n} (x: Const n): nat := n.
+
+Definition regWidth {n} (x: Reg n): nat := n.
+
+Definition stackWidth {n} (x: Stack n): nat := n.
+
+Definition memWidth {n m} (x: Mem n m): nat := n.
+
+Definition memLength {n m} (x: Mem n m): nat := m.
+
+Definition constValueW {n} (x: Const n): word n :=
+  match x with | @const n _ v => v end.
+
+Definition constValueN {n} (x: Const n): nat :=
+  match x with | @const n _ v => wordToNat v end.
+
+Definition regName {n} (x: Reg n): nat :=
+  match x with | @reg n _ v => v end.
+
+Definition stackName {n} (x: Stack n): nat :=
+  match x with | @stack n _ v => v end.
+
+Definition memName {n m} (x: Mem n m): nat :=
+  match x with | @mem n m _ v => v end.
+
+(* Hints *)
+Hint Constructors
+     Reg Stack Const Mem Mapping
+     Assignment Operation Conditional.
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index b6261d1c6..ea39a04ac 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -22,112 +22,123 @@ Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
 
 Definition evalCond (c: Conditional) (state: State): option bool :=
   match c with
-  | TestTrue => Some true
-  | TestFalse => Some false
-  | TestInt n t a b => 
-    match (getIntReg a state) with
-    | Some va =>
-      match (getIntReg b state) with
-      | Some vb => Some (evalTest t va vb)
-      | _ => None
-      end
-    | _ => None
-    end
+  | 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 evalIOp {b} (io: IntOp) (x y: word b) :=
+Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool :=
   match io with
-  | IPlus => wplus x y
-  | IMinus => wminus x y
-  | IXor => wxor x y
-  | IAnd => wand x y
-  | IOr => wor x y
+  | 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 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)
+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
-  | IMult =>
-    let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in
+  | 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 evalOperation (o: Operation) (state: State): option State :=
-  let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) =>
-    match (xo, yo) with
-    | (Some x, Some y) => f x y
-    | _ => None
-    end in
-
-  match o with
-  | IOpConst n o r c =>
-    liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
-      (getIntReg r state)
-      (match c with | constInt32 v => Some v | constInt64 v => Some v end)
-
-  | IOpReg n o a b =>
-    liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
-      (getIntReg a state) (getIntReg b state)
-
-  | DOpReg n o a b h =>
-    liftOpt (fun x y =>
-        match (evalDualOp o x y) with
-        | (lw, hw) =>
-          match (setIntReg a lw state) with
-          | Some st' =>
-            match h with
-            | Some hr => setIntReg hr hw st'
-            | _ => Some st'
-            end
-          | None => None
-          end
-        end)
-      (getIntReg a state) (getIntReg b state)
-
-  | OpRot n o r i =>
-   match (getIntReg r state) with
-    | Some va => setIntReg r (evalRotOp o va i) state
-    | None => None
-    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 getIConst {n} (c: IConst n): word n :=
-  match c with
-  | constInt32 v => v
-  | constInt64 v => v
+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 :=
-  let liftOpt := fun {A B} (f: A -> option B) (xo: option A) =>
-    match xo with
-    | (Some x') => f x'
-    | _ => None
-    end in
-
   match a with
-  | ARegStackInt n r s =>
-    liftOpt (fun x => setIntReg r x state) (getStack s state)
-
-  | AStackRegInt n s r =>
-    liftOpt (fun x => setStack s x state) (getIntReg r state)
-
-  | ARegRegInt n a b =>
-    liftOpt (fun x => setIntReg a x state) (getIntReg b state)
-
-  | AConstInt n r c => setIntReg r (getIConst c) state
-
-  | AIndex n m a b i =>
-    match (getStack b state) with
-    | Some v => setIntReg a (trunc n (getIndex v m i)) state
-    | _ => None
-    end
-
-  | APtr n r s =>
-    setIntReg r (NToWord 32 (N.of_nat (getStackIndex s))) state 
+  | 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.
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index dea937ac1..2dc3f6ade 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -4,56 +4,43 @@ Require Import QhasmCommon.
 Require Export Bedrock.Word.
 
 Module Util.
-
-    Inductive Either A B := | xleft: A -> Either A B | xright: B -> Either A B.
-
-    Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
-    Coercion indexToNat : Index >-> nat.
-
-    (* Magical Bitwise Manipulations *)
-
-    (* Force w to be m bits long, by truncation or zero-extension *)
-    Definition trunc {n} (m: nat) (w: word n): word m.
-      destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
-
-    - replace m with (n + (m - n)) by abstract intuition.
-        refine (zext w (m - n)).
-
-    - rewrite <- s; assumption.
-
-    - replace n with (m + (n - m)) in w by abstract intuition.
-        refine (split1 m (n-m) w).
-    Defined.
-
-    (* Get the index-th m-bit block of w *)
-    Definition getIndex {n} (w: word n) (m index: nat): word m.
-      replace n with
-        ((min n (m * index)) + (n - (min n (m * index))))%nat
-        in w by abstract (
-        assert ((min n (m * index)) <= n)%nat
-            by apply Nat.le_min_l;
-        intuition).
-
-      refine
-        (trunc m
-        (split2 (min n (m * index)) (n - min n (m * index)) w)).
-    Defined.
-
-    (* set the index-th m-bit block of w to s *)
-    Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n :=
-      (w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat)))))
-         ^| (trunc n (combine s (wzero (index * m)%nat))).
-
-    (* Iterating Stack Operations *)
-    Lemma getStackWords_spec: forall {n} (x: Stack n), n = 32 * (getStackWords x).
-    Proof. intros; destruct x; simpl; intuition. Qed.
-
-    Definition segmentStackWord {n} (x: Stack n) (w: word n): word (32 * (getStackWords x)).
-      intros; destruct x; simpl; intuition.
-    Defined.
-
-    Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n.
-      intros; destruct x; simpl; intuition.
-    Defined.
-
- End Util.
+  (* Magical Bitwise Manipulations *)
+
+  (* Force w to be m bits long, by truncation or zero-extension *)
+  Definition trunc {n} (m: nat) (w: word n): word m.
+    destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
+
+  - replace m with (n + (m - n)) by abstract intuition.
+    refine (zext w (m - n)).
+
+  - rewrite <- s; assumption.
+
+  - replace n with (m + (n - m)) in w by abstract intuition.
+    refine (split1 m (n-m) w).
+  Defined.
+
+  (* Get the index-th m-bit block of w *)
+  Definition getIndex {n} (w: word n) (m index: nat): word m.
+    replace n with
+      ((min n (m * index)) + (n - (min n (m * index))))%nat
+      in w by abstract (
+      assert ((min n (m * index)) <= n)%nat
+          by apply Nat.le_min_l;
+      intuition).
+
+    refine
+      (trunc m
+      (split2 (min n (m * index)) (n - min n (m * index)) w)).
+  Defined.
+
+  (* set the index-th m-bit block of w to s *)
+  Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n :=
+    (w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat)))))
+       ^| (trunc n (combine s (wzero (index * m)%nat))).
+
+  (* Option utilities *)
+  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).
+End Util.
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 0840538bc..df8bc97c1 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -1,274 +1,278 @@
 Require Export String List Logic.
 Require Export Bedrock.Word.
 
-Require Import ZArith NArith NPeano.
-Require Import Coq.Structures.OrderedTypeEx.
-Require Import FMapAVL FMapList.
-Require Import JMeq.
+Require Import ZArith NArith NPeano Ndec.
+Require Import Compare_dec Omega.
+Require Import OrderedType Coq.Structures.OrderedTypeEx.
+Require Import FMapAVL FMapList JMeq.
 
 Require Import QhasmUtil QhasmCommon.
 
-(* There's a lot in here.
-   We don't want to automatically give it all to the client. *)
+(* We want to use pairs and triples as map keys: *)
+
+Module Pair_as_OT <: UsualOrderedType.
+  Definition t := (nat * nat)%type.
+
+  Definition eq := @eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
+
+  Definition lt (a b: t) :=
+    if (Nat.eq_dec (fst a) (fst b))
+    then lt (snd a) (snd b)
+    else lt (fst a) (fst b).
+
+  Lemma conv: forall {x0 x1 y0 y1: nat},
+    (x0 = y0 /\ x1 = y1) <-> (x0, x1) = (y0, y1).
+  Proof.
+    intros; split; intros.
+  - destruct H; destruct H0; subst; intuition.
+  - inversion_clear H; intuition.
+  Qed.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+    intros; destruct x as [x0 x1], y as [y0 y1], z as [z0 z1];
+      unfold lt in *; simpl in *;
+      destruct (Nat.eq_dec x0 y0), (Nat.eq_dec y0 z0), (Nat.eq_dec x0 z0);
+      omega.
+  Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+    intros; destruct x as [x0 x1], y as [y0 y1];
+      unfold lt, eq in *; simpl in *;
+      destruct (Nat.eq_dec x0 y0); subst; intuition;
+      inversion H0; subst; omega.
+  Qed.
+
+  Definition compare x y : Compare lt eq x y.
+    destruct x as [x0 x1], y as [y0 y1];
+      destruct (Nat_as_OT.compare x0 y0);
+      unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
+
+    - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
+
+    - destruct (Nat_as_OT.compare x1 y1);
+        unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
+
+      + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
+      + apply EQ; abstract (unfold lt; simpl; subst; intuition).
+      + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+
+    - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+  Defined.
+
+  Definition eq_dec (a b: t): {a = b} + {a <> b}.
+    destruct (compare a b);
+      destruct a as [a0 a1], b as [b0 b1].
+
+    - right; abstract (
+        unfold lt in *; simpl in *;
+        destruct (Nat.eq_dec a0 b0); intuition;
+        inversion H; intuition).
+
+    - left; abstract (inversion e; intuition).
+
+    - right; abstract (
+        unfold lt in *; simpl in *;
+        destruct (Nat.eq_dec b0 a0); intuition;
+        inversion H; intuition).
+  Defined.
+End Pair_as_OT.
+
+Module Triple_as_OT <: UsualOrderedType.
+  Definition t := (nat * nat * nat)%type.
+
+  Definition get0 (x: t) := fst (fst x).
+  Definition get1 (x: t) := snd (fst x).
+  Definition get2 (x: t) := snd x.
+
+  Definition eq := @eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
+
+  Definition lt (a b: t) :=
+    if (Nat.eq_dec (get0 a) (get0 b))
+    then
+      if (Nat.eq_dec (get1 a) (get1 b))
+      then lt (get2 a) (get2 b)
+      else lt (get1 a) (get1 b)
+    else lt (get0 a) (get0 b).
+
+  Lemma conv: forall {x0 x1 x2 y0 y1 y2: nat},
+      (x0 = y0 /\ x1 = y1 /\ x2 = y2) <-> (x0, x1, x2) = (y0, y1, y2).
+  Proof.
+    intros; split; intros.
+    - destruct H; destruct H0; subst; intuition.
+    - inversion_clear H; intuition.
+  Qed.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+    intros; unfold lt in *;
+    destruct (Nat.eq_dec (get0 x) (get0 y)),
+             (Nat.eq_dec (get1 x) (get1 y)),
+             (Nat.eq_dec (get0 y) (get0 z)),
+             (Nat.eq_dec (get1 y) (get1 z)),
+             (Nat.eq_dec (get0 x) (get0 z)),
+             (Nat.eq_dec (get1 x) (get1 z));
+      omega.
+  Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+    intros; unfold lt, eq in *;
+      destruct (Nat.eq_dec (get0 x) (get0 y)),
+               (Nat.eq_dec (get1 x) (get1 y));
+      subst; intuition;
+      inversion H0; subst; omega.
+  Qed.
+
+  Definition compare x y : Compare lt eq x y.
+    destruct (Nat_as_OT.compare (get0 x) (get0 y)).
+
+    Ltac compare_tmp x y :=
+      abstract (
+        unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *;
+        destruct (Nat.eq_dec (get0 x) (get0 y));
+        destruct (Nat.eq_dec (get1 x) (get1 y));
+        simpl; intuition).
+
+    Ltac compare_eq x y :=
+      abstract (
+        unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq, get0, get1 in *;
+        destruct x as [x x2], y as [y y2];
+        destruct x as [x0 x1], y as [y0 y1];
+        simpl in *; subst; intuition).
+
+    - apply LT; compare_tmp x y.
+    - destruct (Nat_as_OT.compare (get1 x) (get1 y)).
+      + apply LT; compare_tmp x y.
+      + destruct (Nat_as_OT.compare (get2 x) (get2 y)).
+        * apply LT; compare_tmp x y.
+        * apply EQ; compare_eq x y.
+        * apply GT; compare_tmp y x.
+      + apply GT; compare_tmp y x.
+    - apply GT; compare_tmp y x.
+  Defined.
+
+  Definition eq_dec (a b: t): {a = b} + {a <> b}.
+    destruct (compare a b);
+      destruct a as [a a2], b as [b b2];
+      destruct a as [a0 a1], b as [b0 b1].
+
+    - right; abstract (
+        unfold lt, get0, get1, get2 in *; simpl in *;
+        destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1);
+        intuition; inversion H; intuition).
+
+    - left; abstract (inversion e; intuition).
+
+    - right; abstract (
+        unfold lt, get0, get1, get2 in *; simpl in *;
+        destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1);
+        intuition; inversion H; intuition).
+  Defined.
+End Triple_as_OT.
 
 Module State.
-    Import ListNotations.
-    Import Util.
-
-    Module NatM := FMapAVL.Make(Nat_as_OT).
-    Definition DefMap: Type := NatM.t N.
-    Definition StateMap: Type := NatM.t DefMap.
-    Definition LabelMap: Type := NatM.t nat.
-
-    Delimit Scope state_scope with state.
-    Local Open Scope state_scope.
-
-    (* The Big Definition *)
-
-    Inductive State :=
-    | fullState (intRegState: StateMap)
-                (stackState: DefMap)
-                (carryBit: CarryState): State.
-
-    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N) None.
-
-    (* Register State Manipulations *)
-
-    Definition getIntReg {n} (reg: IReg n) (state: State): option (word n) :=
-      match state with
-      | fullState intRegState _ _ =>
-        match (NatM.find n intRegState) with
-        | Some map =>
-            match (NatM.find (getIRegIndex reg) map) with
-            | Some m => Some (NToWord n m)
-            | _ => None
-            end
-        | None => None
-        end
-      end.
-
-    Definition setIntReg {n} (reg: IReg n) (value: word n) (state: State): option State :=
-      match state with
-      | fullState intRegState stackState carryState =>
-        match (NatM.find n intRegState) with
-        | Some map =>
-            Some (fullState
-                    (NatM.add n (NatM.add (getIRegIndex reg) (wordToN value) map) intRegState)
-                    stackState
-                    carryState)
-        | None => None
-        end
-      end.
-
-    (* Carry State Manipulations *)
-
-    Definition getCarry (state: State): CarryState :=
-      match state with
-      | fullState _ _ b => b
-      end.
-
-    Definition setCarry (value: bool) (state: State): State :=
-      match state with
-      | fullState intRegState stackState carryState =>
-        fullState intRegState stackState (Some value)
-      end.
-
-    (* Per-word Stack Operations *)
-
-    Definition getStack32 (entry: Stack 32) (state: State): option (word 32) :=
-      match state with
-      | fullState _ stackState _ =>
-        match entry with
-        | stack32 loc =>
-          match (NatM.find loc stackState) with
-          | Some n => Some (NToWord 32 n)
-          | _ => None
-          end
-        end
-      end.
-
-    Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State :=
+  Import ListNotations Util.
+
+  Module NatM := FMapAVL.Make(Nat_as_OT).
+  Module PairM := FMapAVL.Make(Pair_as_OT).
+  Module TripleM := FMapAVL.Make(Triple_as_OT).
+
+  Definition NatNMap: Type := NatM.t N.
+  Definition PairNMap: Type := PairM.t N.
+  Definition TripleNMap: Type := TripleM.t N.
+  Definition LabelMap: Type := NatM.t nat.
+
+  Delimit Scope state_scope with state.
+  Open Scope state_scope.
+
+  (* The Big Definition *)
+
+  Inductive State :=
+    | fullState (regState: PairNMap)
+                (stackState: PairNMap)
+                (memState: TripleNMap)
+                (carry: Carry): State.
+
+  Definition emptyState: State :=
+    fullState (PairM.empty N) (PairM.empty N) (TripleM.empty N) None.
+
+  (* Register *)
+
+  Definition getReg {n} (r: Reg n) (state: State): option (word n) :=
+    match state with
+    | fullState regS _ _ _ =>
+      match (PairM.find (n, regName r) regS) with
+      | Some v => Some (NToWord n v)
+      | None => None
+      end
+    end.
+
+  Definition setReg {n} (r: Reg n) (value: word n) (state: State): State :=
+    match state with
+    | fullState regS stackS memS carry =>
+      fullState (PairM.add (n, regName r) (wordToN value) regS)
+                stackS memS carry
+    end.
+
+  (* Stack *)
+
+  Definition getStack {n} (s: Stack n) (state: State): option (word n) :=
+    match state with
+    | fullState _ stackS _ _ =>
+      match (PairM.find (n, stackName s) stackS) with
+      | Some v => Some (NToWord n v)
+      | None => None
+      end
+    end.
+
+  Definition setStack {n} (s: Stack n) (value: word n) (state: State): State :=
+    match state with
+    | fullState regS stackS memS carry =>
+      fullState regS
+                (PairM.add (n, stackName s) (wordToN value) stackS)
+                memS carry
+    end.
+
+  (* Memory *)
+
+  Definition getMem {n m} (x: Mem n m) (i: Index m) (state: State): option (word n) :=
+    match state with
+    | fullState _ _ memS _ =>
+      match (TripleM.find (n, memName x, proj1_sig i) memS) with
+      | Some v => Some (NToWord n v)
+      | None => None
+      end
+    end.
+
+  Definition setMem {n m} (x: Mem n m) (i: Index m) (value: word n) (state: State): State :=
+    match state with
+    | fullState regS stackS memS carry =>
+      fullState regS stackS
+                (TripleM.add (n, memName x, proj1_sig i) (wordToN value) memS)
+                carry
+    end.
+
+  (* Carry State Manipulations *)
+
+  Definition getCarry (state: State): Carry :=
+    match state with
+    | fullState _ _ _ b => b
+    end.
+
+  Definition setCarry (value: bool) (state: State): State :=
     match state with
-    | fullState intRegState stackState carryState =>
-        match entry with
-        | stack32 loc =>
-          (Some (fullState intRegState 
-                   (NatM.add loc (wordToN value) stackState)
-                   carryState))
-        end
+    | fullState regS stackS memS carry =>
+      fullState regS stackS memS (Some value)
     end.
 
-    (* Inductive Word Manipulations*)
-
-    Definition getWords' {n} (st: (list (word 32)) * word (32 * n)) :
-        Either (list (word 32)) ((list (word 32)) * word (32 * (n - 1))).
-
-      destruct (Nat.eq_dec n 0) as [H | H];
-        destruct st as [lst w].
-
-    - refine (xleft _ _ lst).
-
-    - refine (xright _ _
-             (cons (split1 32 (32 * (n - 1)) (cast w)) lst,
-             (split2 32 (32 * (n - 1)) (cast w))));
-      intuition.
-    Defined.
-
-    Section GetWords.
-      Program Fixpoint getWords'_iter (n: nat) (st: (list (word 32)) * word (32 * n)): list (word 32) :=
-        match n with
-        | O => fst st
-        | S m =>
-            match (getWords' st) with
-            | xleft lst => lst
-            | xright st => cast (getWords'_iter m st)
-            end
-        end.
-
-      Definition getWords {len} (wd: word (32 * len)): list (word 32) :=
-        getWords'_iter len ([], wd).
-    End GetWords.
-
-    Section JoinWords.
-
-        Inductive Any (U: nat -> Type) (lim: nat) := | any: forall n, (n <= lim)%nat -> U n -> Any U lim.
-
-        Definition getAnySize {U lim} (a: Any U lim) :=
-          match a as a' return a = a' -> _ with
-          | any n p v => fun _ => n
-          end (eq_refl a).
-
-        Lemma lim_prop: forall (n lim: nat), (n <= lim)%nat -> ((n - 1) <= lim)%nat.
-        Proof. intros; intuition. Qed.
-
-        Lemma zero_prop: forall (n m: nat), n = S m -> n <> 0.
-        Proof. intros; intuition. Qed.
-
-        Fixpoint anyExp {U: nat -> Type}
-            {lim: nat}
-            (f: forall n, (n <> 0)%nat -> (n <= lim)%nat -> U n -> U (n - 1))
-            (rem: nat)
-            (cur: Any U lim): option {a: Any U lim | getAnySize a = 0}.
-
-          refine match rem with
-          | O => None
-          | S rem' =>
-            match cur as c' return cur = c' -> _ with
-            | any n p v => always
-              match (Nat.eq_dec n 0) with
-              | left peq => Some (lift cur)
-              | right pneq =>
-                anyExp U lim f rem' (any U lim (n - 1) (lim_prop n lim p) (f n pneq p v))
-              end
-            end (eq_refl cur)
-          end.
-
-          subst; unfold getAnySize; intuition.
-
-        Defined.
-
-        Definition JoinWordType (len: nat): nat -> Type := fun n => option (word (32 * (len - n))).
-
-        Definition joinWordUpdate (len: nat) (wds: list (option (word 32))):
-            forall n, (n <> 0)%nat -> (n <= len)%nat -> JoinWordType len n -> JoinWordType len (n - 1).
-
-          intros n H0 Hlen v; unfold JoinWordType in v.
-          refine match v with
-            | Some cur =>
-              match (nth_error wds n) with
-              | Some (Some w) => Some (cast (combine w cur))
-              | _ => None
-              end
-            | _ => None
-            end.
-
-          abstract (replace (32 + 32 * (len - n)) with (32 * (len - (n - 1))); intuition).
-        Defined.
-
-        Definition joinWordOpts (wds: list (option (word 32))): option (word (32 * (length wds))).
-          refine (
-            let len := (length wds) in
-            let start := (any (JoinWordType len) len len _ (cast (Some (wzero 0)))) in
-            let aopt := anyExp (cast (joinWordUpdate len wds)) (length wds) start in
-            match aopt as aopt' return aopt = aopt' -> _ with
-            | Some a => always
-              match (proj1_sig a) as a' return (proj1_sig a) = a' -> _ with
-              | any n p v => always (cast v)
-              end (eq_refl (proj1_sig a))
-            | _ => always None
-            end (eq_refl aopt)
-          ); try abstract intuition.
-
-          - abstract ( unfold JoinWordType; replace (32 * (len-len)) with 0; intuition).
-
-          - destruct a; simpl in _H0; destruct x, aopt.
-
-            + abstract (
-                destruct s; unfold getAnySize in e; simpl in e; subst;
-                inversion _H0;
-                unfold JoinWordType;
-                replace (len - 0) with len by intuition;
-                unfold len; intuition ).
-
-            + inversion _H.
-        Defined.
-
-    End JoinWords.
-
-    (* Stack Manipulations *)
-
-    Fixpoint getStack_iter (rem: nat) (loc: nat) (state: State): list (option (word 32)) :=
-      match rem with
-      | O => []
-      | (S rem') =>
-        (getStack32 (stack32 loc) state) ::
-        (getStack_iter rem' (loc + 32) state)
+  Definition setCarryOpt (value: option bool) (state: State): State :=
+    match value with
+    | Some c' => setCarry c' state
+    | _ => state
     end.
 
-    Lemma getStack_iter_length: forall rem loc state,
-        length (getStack_iter rem loc state) = rem.
-    Proof.
-      induction rem; intuition.
-
-      replace (getStack_iter (S rem) loc state) with 
-        ((getStack32 (stack32 loc) state) ::
-        (getStack_iter rem (loc + 32) state)) by intuition.
-
-      replace (Datatypes.length _) with
-        (1 + Datatypes.length (getStack_iter rem (loc + 32) state)) by intuition.
-
-      rewrite IHrem; intuition.
-    Qed.
-
-    Definition getStack {n} (entry: Stack n) (state: State) : option (word n).
-
-      refine (
-        let m := getStackWords entry in
-        let i := getStackIndex entry in
-        let wos := (getStack_iter m i state) in
-        let joined := (joinWordOpts wos) in
-
-        match joined as j return j = joined -> _ with
-        | Some w => always Some (cast w)
-        | None => always None
-        end (eq_refl joined)
-      ); abstract (
-        intuition;
-        unfold wos;
-        rewrite getStack_iter_length;
-        destruct entry; simpl; intuition).
-
-    Defined.
-
-    Definition setStack {n} (entry: Stack n) (value: word n) (state: State) : option State :=
-      (fix setStack_iter (wds: list (word 32)) (nextLoc: nat) (state: State) :=
-        match wds with
-        | [] => Some state
-        | w :: ws =>
-        match (setStack32 (stack32 nextLoc) w state) with 
-        | Some st' => setStack_iter ws (S nextLoc) st'
-        | None => None
-        end
-        end) (getWords (segmentStackWord entry value)) (getStackIndex entry) state.
-
-End State.
+End State.
\ No newline at end of file
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 9eeb0f2ca..abd5b9367 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -187,36 +187,6 @@ Module StringConversion <: Conversion Qhasm QhasmString.
         simpl in H; inversion H; intuition.
     Qed.
 
-    Lemma triple_conv: forall {x0 x1 x2 y0 y1 y2: nat},
-      (x0 = y0 /\ x1 = y1 /\ x2 = y2) <-> (x0, x1, x2) = (y0, y1, y2).
-    Proof.
-      intros; split; intros.
-
-      - destruct H; destruct H0; subst; intuition.
-
-      - inversion_clear H; intuition.
-    Qed.
-
-    Definition triple_dec (x y: nat * nat * nat): {x = y} + {x <> y}.
-      refine (match x as x' return x' = _ -> _ with
-      | (x0, x1, x2) => fun _ =>
-        match y as y' return y' = _ -> _ with
-        | (y0, y1, y2) => fun _ =>
-           _ (Nat.eq_dec x0 y0) (Nat.eq_dec x1 y1) (Nat.eq_dec x2 y2)
-        end (eq_refl y)
-      end (eq_refl x));
-        rewrite <- _H, <- _H0;
-        clear _H _H0 x y p p0;
-        intros.
-
-      intros; destruct x6, x7, x8; first [
-        left; abstract (subst; intuition)
-      | right; abstract (intro;
-          apply triple_conv in H;
-          destruct H; destruct H0; intuition)
-      ].
-    Defined.
-
     Definition entry_dec (x y: Entry): {x = y} + {x <> y}.
       refine (_ (triple_dec (entryId x) (entryId y))).
       intros; destruct x0.