Breaking out State into its own file

4 files changed, 327 insertions, 285 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index aeb5c0c10..46e2664ad 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -1,36 +1,10 @@
-Require Export String List Logic.
+Require Export String List.
 Require Export Bedrock.Word.
 
-Require Import ZArith NArith NPeano.
-Require Import Coq.Structures.OrderedTypeEx.
-Require Import FMapAVL FMapList.
-Require Import JMeq.
-
-Require Import QhasmUtil.
-
-Import ListNotations.
-
-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.
-
-(* Sugar *)
-
-Definition W := word 32.
-
-Definition convert {A B: Type} (x: A) (H: A = B): B :=
- eq_rect A (fun B0 : Type => B0) x B H.
-
-Ltac create X Y :=
-  let H := fresh in (
-    assert (exists X, X = Y) as H
-      by (exists Y; abstract intuition);
-    destruct H).
-
-Obligation Tactic := abstract intuition.
-
 (* A formalization of x86 qhasm *)
+Definition Label := nat.
+Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
+Definition Invert := bool.
 
 (* A constant upper-bound on the number of operations we run *)
 Definition maxOps: nat := 1000.
@@ -131,11 +105,6 @@ Definition invertConditional (c: Conditional): Conditional :=
 
 Hint Constructors Conditional.
 
-(* Machine State *)
-
-Inductive State :=
-| fullState (regState: StateMap) (stackState: DefMap): State.
-
 (* Reg, Stack, Const Utilities *)
 
 Definition getRegWords {n} (x: Reg n) :=
@@ -172,167 +141,6 @@ Definition getStackIndex {n} (x: Stack n): nat :=
   | stack512 loc => loc
   end.
 
-(* State Manipulations *)
-
-Definition getReg {n} (reg: Reg n) (state: State): option (word n) :=
-  match state with
-  | fullState regState stackState =>
-    match (NatM.find n regState) with
-      | Some map =>
-        match (NatM.find (getRegIndex reg) map) with
-        | Some m => Some (NToWord n m)
-        | _ => None
-        end
-      | None => None
-    end
-  end.
-
-Definition setReg {n} (reg: Reg n) (value: word n) (state: State): option State :=
-  match state with
-  | fullState regState stackState =>
-    match (NatM.find n regState) with
-      | Some map =>
-        Some (fullState
-          (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map)
-            regState) stackState)
-      | None => None
-    end
-  end.
-
-(* Per-word Stack Operations *)
-Definition getStack32 (entry: Stack 32) (state: State): option (word 32) :=
-  match state with
-  | fullState regState 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 :=
-  match state with
-  | fullState regState stackState =>
-    match entry with
-    | stack32 loc =>
-      (Some (fullState regState
-                       (NatM.add loc (wordToN value) stackState)))
-    end
-  end.
-
-Notation "'cast' e" := (convert e _) (at level 20).
-
-(* 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.
-
-Inductive Either A B := | xleft: A -> Either A B | xright: B -> Either A B.
-
-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.
-
-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).
-
-Definition joinWordOpts_expandTerm {n} (w: word (32 + 32 * n)): word (32 * S n).
-  replace (32 * S n) with (32 + 32 * n) by abstract intuition; assumption.
-Defined.
-
-Fixpoint joinWordOpts (wds: list (option (word 32))) (len: nat): option (word (32 * (length wds))).
-  refine match len with
-  | O => None
-  | S len' =>
-    match wds with
-    | nil => None
-    | (cons wo wos) =>
-        match wo with
-        | None => None
-        | Some w =>
-          let f := fun x =>
-            match x with 
-            | None => None
-            | (Some joined) => Some (cast (combine w joined))
-            end in
-
-          f (joinWordOpts wos len')
-        end
-    end
-  end; 
-    try replace (Datatypes.length (wo :: wos))
-           with (1 + (Datatypes.length wos))
-             by abstract intuition;
-    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.
-
-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)
-  end.
-
-Fixpoint 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
-    option_map (fun a => cast a) joined
-  ); intuition.
-
-  replace (Datatypes.length _) with (getStackWords entry); intuition.
-  unfold wds.
-  induction (getStackWords entry); simpl; intuition.
-  destruct entry.
-
-  simpl; intuition.
-Defined.
-
-Definition emptyState: State :=
-  fullState (NatM.empty DefMap) (NatM.empty DefMap).
-
 (* For register allocation checking *)
 Definition regCount (base: nat): nat :=
   match base with
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 312f30e03..ec54fdc47 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,7 +1,9 @@
-Require Export QhasmCommon.
-Require Export QhasmUtil.
-
+Require Export QhasmCommon QhasmUtil State.
 Require Export ZArith.
+Require Export Bedrock.Word.
+
+Import State.
+Import Util.
 
 Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool :=
   xorb invert
@@ -73,30 +75,30 @@ Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n :=
   | Rotr => NToWord n (N.shiftr_nat (wordToN a) m)
   end.
 
-Definition evalOperation (o: Operation) (state: State): State :=
+Definition evalOperation (o: Operation) (state: State): option State :=
   match o with
   | OpReg32Constant b r c =>
     match (getReg r state) with
     | Some v0 =>
       match c with
       | const32 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | OpReg32Reg32 b r0 r1 =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | RotReg32 b r m =>
     match (getReg r state) with
     | Some v0 => setReg r (evalRotOp b v0 m) state
-    | None => state
+    | None => None
     end
 
   | OpReg64Constant b r c =>
@@ -104,18 +106,18 @@ Definition evalOperation (o: Operation) (state: State): State :=
     | Some v0 =>
       match c with
       | const64 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | OpReg64Reg64 b r0 r1 =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | OpReg128Constant b r c =>
@@ -123,67 +125,67 @@ Definition evalOperation (o: Operation) (state: State): State :=
     | Some v0 =>
       match c with
       | const128 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | OpReg128Reg128 b r0 r1 =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   end.
 
-Definition evalAssignment (a: Assignment) (state: State): State :=
+Definition evalAssignment (a: Assignment) (state: State): option State :=
   match a with
   | Assign32Stack32 r s =>
     match (getReg r state) with
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Stack16 r s i =>
     match (getReg r state) with
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r (trunc 32 (getIndex v1 16 i)) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Stack8 r s i =>
     match (getReg r state) with
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r (trunc 32 (getIndex v1 8 i)) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Stack64 r s i =>
     match (getReg r state) with
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r (getIndex v1 32 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Stack128 r s i =>
     match (getReg r state) with
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r (getIndex v1 32 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign32Reg32 r0 r1 =>
@@ -191,45 +193,45 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Reg16 r0 r1 i =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (trunc 32 (getIndex v1 16 i)) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Reg8 r0 r1 i =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (trunc 32 (getIndex v1 8 i)) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Reg64 r0 r1 i =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (getIndex v1 32 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | Assign32Reg128 r0 r1 i =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (getIndex v1 32 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Stack32 r0 i s =>
@@ -237,9 +239,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Stack64 r s =>
@@ -247,9 +249,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Stack128 r s i =>
@@ -257,9 +259,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r (getIndex v1 64 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Reg32 r0 i r1 =>
@@ -267,9 +269,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Reg64 r0 r1 =>
@@ -277,9 +279,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Reg128 r0 r1 i =>
@@ -287,9 +289,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (getIndex v1 64 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign6464Reg32 r0 i r1 =>
@@ -297,9 +299,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign6464Reg64 r0 i r1 =>
@@ -307,9 +309,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign6464Reg128 r0 r1 =>
@@ -317,9 +319,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | AssignConstant r c =>
@@ -327,8 +329,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match c with
       | const32 v1 => setReg r v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   end.
+
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 0528d0738..774dc50b8 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -1,44 +1,59 @@
 
 Require Import ZArith NArith NPeano.
+Require Import QhasmCommon.
 Require Export Bedrock.Word.
 
-Definition Label := nat.
-Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
-Definition Invert := bool.
+Module Util.
 
-Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
-Coercion indexToNat : Index >-> nat.
+    Inductive Either A B := | xleft: A -> Either A B | xright: B -> Either A B.
 
-(* Magical Bitwise Manipulations *)
+    Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
+    Coercion indexToNat : Index >-> nat.
 
-(* 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].
+    (* Magical Bitwise Manipulations *)
 
-  - replace m with (n + (m - n)) by abstract intuition.
-    refine (zext w (m - n)).
+    (* 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].
 
-  - rewrite <- s; assumption.
+    - replace m with (n + (m - n)) by abstract intuition.
+        refine (zext w (m - n)).
 
-  - replace n with (m + (n - m)) in w by abstract intuition.
-    refine (split1 m (n-m) w).
-Defined.
+    - rewrite <- s; assumption.
 
-(* 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).
+    - replace n with (m + (n - m)) in w by abstract intuition.
+        refine (split1 m (n-m) w).
+    Defined.
 
-  refine
-    (trunc m
-      (split2 (min n (m * index)) (n - min n (m * index)) 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).
 
-(* 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))).
+      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.
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
new file mode 100644
index 000000000..3f80f7d33
--- /dev/null
+++ b/src/Assembly/State.v
@@ -0,0 +1,216 @@
+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 QhasmUtil QhasmCommon.
+
+(* There's a lot in here.
+   We don't want to automatically give it all to the client. *)
+
+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.
+
+    (* Sugar and Tactics *)
+
+    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.
+
+    (* The Big Definition *)
+
+    Inductive State :=
+      | fullState (regState: StateMap) (stackState: DefMap): State.
+
+    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N).
+
+    (* Register State Manipulations *)
+
+    Definition getReg {n} (reg: Reg n) (state: State): option (word n) :=
+      match state with
+      | fullState regState stackState =>
+        match (NatM.find n regState) with
+        | Some map =>
+            match (NatM.find (getRegIndex reg) map) with
+            | Some m => Some (NToWord n m)
+            | _ => None
+            end
+        | None => None
+        end
+      end.
+
+    Definition setReg {n} (reg: Reg n) (value: word n) (state: State): option State :=
+      match state with
+      | fullState regState stackState =>
+        match (NatM.find n regState) with
+        | Some map =>
+            Some (fullState
+                    (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map) regState)
+                    stackState)
+        | None => None
+        end
+      end.
+
+    (* Per-word Stack Operations *)
+
+    Definition getStack32 (entry: Stack 32) (state: State): option (word 32) :=
+      match state with
+      | fullState regState 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 :=
+    match state with
+    | fullState regState stackState =>
+        match entry with
+        | stack32 loc =>
+        (Some (fullState regState
+              (NatM.add loc (wordToN value) stackState)))
+        end
+    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.
+
+    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).
+
+    Definition joinWordOpts_expandTerm {n} (w: word (32 + 32 * n)): word (32 * S n).
+      replace (32 * S n) with (32 + 32 * n) by abstract intuition; assumption.
+    Defined.
+
+    Fixpoint joinWordOpts'
+            (len: nat)
+            (rem: nat)
+            (wds: list (option (word 32)))
+            (cont: word (32 * (len - rem)))
+        : (rem <= len)%nat -> (length wds = rem) -> option (word (32 * len)).
+
+      refine (fun remCorrect wdsCorrect =>
+      match rem as r return r = rem -> _ with
+      | O => always Some (cast cont)
+      | (S rem') => always
+        match wds as l return l = wds -> _ with
+        | nil => always None
+        | (cons wo wos) => always
+            match wo with
+            | None => None
+            | Some w => (joinWordOpts' len rem' wos (cast (combine w cont)) _ _)
+            end
+        end (eq_refl wds)
+      end (eq_refl rem)); intuition.
+
+      rewrite <- _H in wdsCorrect; rewrite <- _H0 in *;
+        replace (length (wo::wos)) with (1 + length wos) in wdsCorrect by abstract intuition;
+        intuition.
+
+    Admitted.
+
+    Definition joinWordOpts (wds: list (option (word 32))): option (word (32 * (length wds))).
+      refine (joinWordOpts' (length wds) (length wds) wds (cast (wzero 0)) _ _); intuition.
+    Defined.
+
+    (* 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)
+    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.
+
+    Fixpoint 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).
+
+    Admitted.
+
+    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.