Module-based reorganization of Qhasm code

12 files changed, 831 insertions, 706 deletions

diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v
new file mode 100644
index 000000000..16638af78
--- /dev/null
+++ b/src/Assembly/AlmostConversion.v
@@ -0,0 +1,51 @@
+
+Require Import NArith.
+Require Export Qhasm AlmostQhasm Conversion.
+
+Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
+  Import QhasmCommon AlmostQhasm Qhasm.
+  Import ListNotations.
+
+  Fixpoint almostToQhasm' (prog: AlmostProgram) (startLabel: N): Qhasm.Program :=
+    let label0 := N.shiftl 1 startLabel in
+    let label1 := N.succ label0 in
+
+    match prog with
+    | ASkip => []
+    | ASeq a b => (almostToQhasm' a label0) ++ (almostToQhasm' b label1)
+    | AAssign a => [ QAssign a ]
+    | AOp a => [ QOp a ]
+    | ACond c a b =>
+      let els := N.to_nat (N.shiftl 1 label0) in
+      let finish := S els in
+      [QJmp (invertConditional c) els] ++
+      (almostToQhasm' a label1) ++
+      [QJmp TestTrue finish] ++
+      [QLabel els] ++
+      (almostToQhasm' b label1) ++
+      [QLabel finish]
+    | AWhile c a =>
+      let start := N.to_nat (N.shiftl 1 label0) in
+      let finish := S start in
+      [ QJmp (invertConditional c) finish ;
+        QLabel start ] ++
+        (almostToQhasm' a label1) ++
+      [ QJmp c start;
+        QLabel finish ]
+    end.
+
+  Definition convertProgram (prog: AlmostQhasm.Program) := Some (almostToQhasm' prog 0%N).
+  Definition convertState (st: Qhasm.State): option AlmostQhasm.State := Some st.
+
+  Lemma convert_spec: forall st' prog,
+    match ((convertProgram prog), (convertState st')) with
+    | (Some prog', Some st) =>
+      match (Qhasm.eval prog' st') with
+      | Some st'' => AlmostQhasm.eval prog st = (convertState st'')
+      | _ => True
+      end
+    | _ => True
+    end.
+  Admitted.
+
+End AlmostConversion.
diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
new file mode 100644
index 000000000..31128fbfb
--- /dev/null
+++ b/src/Assembly/AlmostQhasm.v
@@ -0,0 +1,57 @@
+Require Import QhasmEvalCommon.
+Require Import Language.
+Require Import List.
+
+Module AlmostQhasm <: Language.
+  Import ListNotations.
+
+  (* A constant upper-bound on the number of operations we run *)
+  Definition maxOps: nat := 1000.
+
+  (* Program Types *)
+  Definition State := State.
+
+  Inductive AlmostProgram: Set :=
+    | ASkip: AlmostProgram
+    | ASeq: AlmostProgram -> AlmostProgram -> AlmostProgram
+    | AAssign: Assignment -> AlmostProgram
+    | AOp: Operation -> AlmostProgram
+    | ACond: Conditional -> AlmostProgram -> AlmostProgram -> AlmostProgram
+    | AWhile: Conditional -> AlmostProgram -> AlmostProgram.
+
+  Hint Constructors AlmostProgram.
+
+  Definition Program := AlmostProgram.
+
+  (* Only execute while loops a fixed number of times.
+     TODO (rsloan): can we do any better? *)
+
+  (* TODO: make this inductive *)
+  Fixpoint almostEvalWhile (cond: Conditional) (prog: Program) (state: State) (horizon: nat): option State :=
+    match horizon with
+    | (S m) =>
+      if (evalCond cond state)
+      then almostEvalWhile cond prog state m
+      else Some state
+    | O => None
+    end.
+
+  Fixpoint eval (prog: Program) (state: State): option State :=
+    match prog with
+    | ASkip => Some state
+    | ASeq a b =>
+      match (eval a state) with
+      | (Some st') => eval b st'
+      | _ => None
+      end
+    | AAssign a => Some (evalAssignment a state)
+    | AOp a => Some (evalOperation a state)
+    | ACond c a b =>
+      if (evalCond c state)
+      then eval a state
+      else eval b state
+    | AWhile c a => almostEvalWhile c a state maxOps
+    end.
+
+  (* world peace *)
+End AlmostQhasm.
diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v
new file mode 100644
index 000000000..eb378d437
--- /dev/null
+++ b/src/Assembly/Conversion.v
@@ -0,0 +1,19 @@
+
+Require Export Language.
+
+Module Type Conversion (A B: Language).
+
+  Parameter convertProgram: A.Program -> option B.Program.
+  Parameter convertState: B.State -> option A.State.
+
+  Axiom convert_spec: forall st' prog,
+    match ((convertProgram prog), (convertState st')) with
+    | (Some prog', Some st) =>
+      match (B.eval prog' st') with
+      | Some st'' => A.eval prog st = (convertState st'')
+      | _ => True
+      end
+    | _ => True
+    end.
+
+End Conversion.
diff --git a/src/Assembly/GallinaConversion.v b/src/Assembly/GallinaConversion.v
new file mode 100644
index 000000000..0419ec3e1
--- /dev/null
+++ b/src/Assembly/GallinaConversion.v
@@ -0,0 +1,60 @@
+
+Require Export Language Conversion.
+Require Export AlmostQhasm QhasmCommon.
+Require Export Bedrock.Word.
+Require Export List.
+Require Vector.
+
+Module Type GallinaFunction <: Language.
+  Parameter len: nat.
+  Definition Vec := Vector.t (word 32) len.
+
+  Definition Program := Vec -> Vec.
+  Definition State := Vec.
+
+  Definition eval (p: Program) (s: Vec) := Some (p s).
+End GallinaFunction.
+
+Module GallinaConversion (S: GallinaFunction) <: Conversion S AlmostQhasm.
+  Import QhasmCommon AlmostQhasm.
+  Import ListNotations.
+  Import S.
+
+  Fixpoint convertState' (st: AlmostQhasm.State) (rem: nat): list (word 32) :=
+    match rem with
+    | O => []
+    | S m =>
+      match (getStack (stack32 rem) st) with
+      | Some e => e
+      | None => (wzero 32) 
+      end :: (convertState' st m)
+    end.
+
+  Lemma convertState'_len: forall st rem, length (convertState' st rem) = rem.
+  Proof.
+    intros; induction rem; simpl; intuition.
+  Qed.
+
+  Definition convertState (st: AlmostQhasm.State): option S.State.
+    unfold State, Vec.
+    replace len with (length (convertState' st len))
+      by abstract (apply convertState'_len).
+    refine (Some (Vector.of_list (convertState' st len))).
+  Defined.
+
+  (* TODO (rsloan): implement conversion *)
+  Definition convertProgram (prog: S.Program): option AlmostQhasm.Program :=
+    Some ASkip.
+
+  Lemma convert_spec: forall st' prog,
+    match ((convertProgram prog), (convertState st')) with
+    | (Some prog', Some st) =>
+      match (AlmostQhasm.eval prog' st') with
+      | Some st'' => S.eval prog st = (convertState st'')
+      | _ => True
+      end
+    | _ => True
+    end.
+  Admitted.
+
+End GallinaConversion.
diff --git a/src/Assembly/HighLevel.v b/src/Assembly/HighLevel.v
deleted file mode 100644
index bae67f312..000000000
--- a/src/Assembly/HighLevel.v
+++ /dev/null
@@ -1,9 +0,0 @@
-
-Inductive Const32 : Set = | const32: word 32 -> Const32.
-
-Inductive HL :=
-  | Input: Const32 -> HL
-  | Variable: Const32 -> HL
-  | Let: forall m, nat -> HL -> HL -> HL
-  | Lift1: (Const32 -> Const32) -> HL -> HL
-  | Lift2: (Const32 -> Const32 -> Const32) -> HL -> HL -> HL.
diff --git a/src/Assembly/Language.v b/src/Assembly/Language.v
new file mode 100644
index 000000000..d04393b51
--- /dev/null
+++ b/src/Assembly/Language.v
@@ -0,0 +1,7 @@
+
+Module Type Language.
+  Parameter Program: Type.
+  Parameter State: Type.
+
+  Parameter eval: Program -> State -> option State.
+End Language.
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
index 8921b6e4b..05e607462 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -1,674 +1,73 @@
+Require Import QhasmEvalCommon.
+Require Import Language.
+Require Import List NPeano.
+
+Module Qhasm <: Language.
+  Import ListNotations.
+
+  (* A constant upper-bound on the number of operations we run *)
+  Definition maxOps: nat := 1000.
+  Definition State := State.
+
+  (* Program Types *)
+  Inductive QhasmStatement :=
+    | QAssign: Assignment -> QhasmStatement
+    | QOp: Operation -> QhasmStatement
+    | QJmp: Conditional -> Label -> QhasmStatement
+    | QLabel: Label -> QhasmStatement.
+
+  Hint Constructors QhasmStatement.
+
+  Definition Program := list QhasmStatement.
+
+  (* Only execute while loops a fixed number of times.
+     TODO (rsloan): can we do any better? *)
+
+  Fixpoint getLabelMap' (prog: Program) (cur: LabelMap) (index: nat): LabelMap :=
+    match prog with
+    | p :: ps =>
+      match p with
+      | QLabel label => getLabelMap' ps (NatM.add label index cur) (S index)
+      | _ => getLabelMap' ps cur (S index)
+      end
+    | [] => cur
+    end.
+
+  Definition getLabelMap (prog: Program): LabelMap :=
+    getLabelMap' prog (NatM.empty nat) O.
+
+  Fixpoint eval' (prog: Program) (state: State) (loc: nat) (horizon: nat) (labelMap: LabelMap) (maxLoc: nat): option State :=
+    match horizon with
+    | (S h) =>
+      match (nth_error prog loc) with
+      | Some stmt =>
+        let (nextState, jmp) :=
+          match stmt with
+          | QAssign a => (evalAssignment a state, None)
+          | QOp o => (evalOperation o state, None)
+          | QLabel l => (state, None)
+          | QJmp c l =>
+            if (evalCond c state)
+            then (state, Some l)
+            else (state, None)
+          end
+        in
+          match jmp with
+          | None =>
+            if (Nat.eq_dec loc maxLoc)
+            then Some nextState
+            else eval' prog nextState (S loc) h labelMap maxLoc
+          | Some nextLoc =>
+            eval' prog nextState nextLoc h labelMap nextLoc
+          end
+      | None => None
+      end
+    | O => None
+    end.
+
+  Definition eval (prog: Program) (state: State): option State :=
+    eval' prog state O maxOps (getLabelMap prog) ((length prog) - 1).
+
+  (* world peace *)
+End Qhasm.
 
-Require Import String List.
-Require Import Bedrock.Word.
-Require Import ZArith NArith NPeano.
-Require Import Coq.Structures.OrderedTypeEx.
-
-Require Import FMapAVL FMapList.
-
-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.
-
-(* A formalization of x86 qhasm *)
-
-(* Basic Types *)
-Definition Label := nat.
-Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
-Definition Invert := bool.
-
-Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
-Coercion indexToNat : Index >-> nat.
-
-(* A constant upper-bound on the number of operations we run *)
-Definition maxOps: nat := 1000.
-
-(* Datatypes *)
-Inductive Const: nat -> Set :=
-  | const32: word 32 -> Const 32
-  | const64: word 64 -> Const 64
-  | const128: word 128 -> Const 128.
-
-Inductive Reg: nat -> Set :=
-  | reg32: nat -> Reg 32
-  | reg3232: nat -> Reg 64
-  | reg6464: nat -> Reg 128
-  | reg80: nat -> Reg 80.
-
-Inductive Stack: nat -> Set :=
-  | stack32: nat -> Stack 32
-  | stack64: nat -> Stack 64
-  | stack128: nat -> Stack 128.
-
-(* Assignments *)
-Inductive Assignment : Set :=
-  | Assign32Stack32: Reg 32 -> Stack 32 -> Assignment
-  | Assign32Stack16: Reg 32 -> Stack 32 -> Index 2 -> Assignment
-  | Assign32Stack8: Reg 32 -> Stack 32 -> Index 4 -> Assignment
-  | Assign32Stack64: Reg 32 -> Stack 64 -> Index 2 -> Assignment
-  | Assign32Stack128: Reg 32 -> Stack 128 -> Index 2 -> Assignment
-
-  | Assign32Reg32: Reg 32 -> Reg 32 -> Assignment
-  | Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment
-  | Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment
-  | Assign32Reg64: Reg 32 -> Reg 64 -> Index 2 -> Assignment
-  | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment
-
-  | Assign3232Stack32: Reg 64 -> Index 2 -> Stack 32 -> Assignment
-  | Assign3232Stack64: Reg 64 -> Stack 64 -> Assignment
-  | Assign3232Stack128: Reg 64 -> Stack 128 -> Index 2 -> Assignment
-
-  | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment
-  | Assign3232Reg64: Reg 64 -> Reg 64 -> Assignment
-  | Assign3232Reg128: Reg 64 -> Reg 128 -> Index 2 -> Assignment
-
-  | Assign6464Reg32: Reg 128 -> Index 4 -> Reg 32 -> Assignment
-  | Assign6464Reg64: Reg 128 -> Index 2 -> Reg 64 -> Assignment
-  | Assign6464Reg128: Reg 128 -> Reg 128 -> Assignment
-
-  | AssignConstant: Reg 32 -> Const 32 -> Assignment.
-
-Hint Constructors Assignment.
-
-(* Operations *)
-
-Inductive BinOp :=
-  | Plus: BinOp | Minus: BinOp | Mult: BinOp
-  | Div: BinOp | Xor: BinOp | And: BinOp | Or: BinOp.
-
-Inductive RotOp :=
-  | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp.
-
-Inductive Operation :=
-  | OpReg32Constant: BinOp -> Reg 32 -> Const 32 -> Operation
-  | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation
-  | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation
-
-  | OpReg64Constant: BinOp -> Reg 64 -> Const 64 -> Operation
-  | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation
-
-  | OpReg128Constant: BinOp -> Reg 128 -> Const 32 -> Operation
-  | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation.
-
-Hint Constructors Operation.
-
-(* Control Flow *)
-
-Inductive TestOp :=
-  | TEq: TestOp
-  | TLt: TestOp
-  | TUnsignedLt: TestOp
-  | TGt: TestOp
-  | TUnsignedGt: TestOp.
-
-Inductive Conditional :=
-  | TestTrue: Conditional
-  | TestFalse: Conditional
-  | TestReg32Reg32: TestOp -> Invert -> Reg 32 -> Reg 32 -> Conditional
-  | TestReg32Const: TestOp -> Invert -> Reg 32 -> Const 32 -> Conditional.
-
-Definition invertConditional (c: Conditional): Conditional :=
-  match c with
-  | TestTrue => TestFalse
-  | TestFalse => TestFalse
-  | TestReg32Reg32 o i r0 r1 => TestReg32Reg32 o (negb i) r0 r1
-  | TestReg32Const o i r c => TestReg32Const o (negb i) r c
-  end.
-
-Hint Constructors Conditional.
-
-(* Program Types *)
-
-Inductive AlmostQhasm :=
-  | ASeq: AlmostQhasm -> AlmostQhasm -> AlmostQhasm
-  | AAssign: Assignment -> AlmostQhasm
-  | AOp: Operation -> AlmostQhasm 
-  | ACond: Conditional -> AlmostQhasm -> AlmostQhasm
-  | AWhile: Conditional -> AlmostQhasm -> AlmostQhasm.
-
-Hint Constructors AlmostQhasm.
-
-Inductive QhasmStatement :=
-  | QAssign: Assignment -> QhasmStatement
-  | QOp: Operation -> QhasmStatement
-  | QJmp: Conditional -> Label -> QhasmStatement
-  | QLabel: Label -> QhasmStatement.
-
-Hint Constructors QhasmStatement.
-
-Definition Qhasm := list QhasmStatement.
-
-Import ListNotations.
-
-(* AlmostQhasm -> Qhasm Conversion *)
-
-Fixpoint almostToQhasm' (prog: AlmostQhasm) (startLabel: N): Qhasm :=
-  let label0 := N.shiftl 1 startLabel in
-  let label1 := N.succ label0 in
-
-  match prog with
-  | ASeq a b => (almostToQhasm' a label0) ++ (almostToQhasm' b label1)
-  | AAssign a => [ QAssign a ]
-  | AOp a => [ QOp a ]
-  | ACond c a =>
-    [QJmp (invertConditional c) (N.to_nat label0)] ++
-    (almostToQhasm' a label1) ++
-    [QLabel (N.to_nat label0)]
-  | AWhile c a =>
-    let start := N.to_nat (N.shiftl 1 label0) in
-    let finish := S start in
-    [ QJmp (invertConditional c) finish ;
-      QLabel start ] ++
-      (almostToQhasm' a label1) ++
-    [ QJmp c start;
-      QLabel finish ]
-  end.
-
-Definition almostToQhasm (prog: AlmostQhasm) := almostToQhasm' prog 0%N.
-
-(* Machine State *)
-
-Inductive State :=
-| fullState (regState: StateMap) (stackState: StateMap): State.
-
-Definition getReg {n} (reg: Reg n) (state: State): option (word n).
-  destruct state; inversion reg as [L H | L H | L H | L H];
-    destruct (NatM.find n regState) as [map |];
-    first [ destruct (NatM.find L map) as [n0 |] | exact None ];
-    first [ rewrite H; exact (Some (NToWord n n0)) | exact None ].
-Defined.
-
-Definition setReg {n} (reg: Reg n) (value: word n) (state: State): State.
-  inversion state; inversion reg as [L H | L H | L H | L H];
-    destruct (NatM.find n regState) as [map |];
-    first [
-       exact
-         (fullState
-           (NatM.add n
-             (NatM.add L (wordToN value) map) regState)
-             stackState)
-     | exact state ].
-Defined.
-
-Definition getStack {n} (entry: Stack n) (state: State): option (word n).
-  destruct state; inversion entry as [L H | L H | L H];
-    destruct (NatM.find n stackState) as [map |];
-    first [ destruct (NatM.find L map) as [n0 |] | exact None ];
-    first [ rewrite H; exact (Some (NToWord n n0)) | exact None ].
-Defined.
-
-Definition setStack {n} (entry: Stack n) (value: word n) (state: State): State.
-  inversion state; inversion entry as [L H | L H | L H];
-    destruct (NatM.find n stackState) as [map |];
-    first [
-       exact
-         (fullState regState
-           (NatM.add n
-             (NatM.add L (wordToN value) map) regState))
-     | exact state ].
-Defined.
-
-Definition emptyState: State :=
-  fullState (NatM.empty DefMap) (NatM.empty DefMap).
-
-(* 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))).
-
-(* State Evaluation *)
-
-Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool :=
-  xorb invert
-  match o with
-  | TEq => weqb a b
-  | TLt =>
-    match (Z.compare (wordToZ a) (wordToZ b)) with
-    | Lt => true
-    | _ => false
-    end
-  | TUnsignedLt =>
-    match (N.compare (wordToN a) (wordToN b)) with
-    | Lt => true
-    | _ => false
-    end
-  | TGt =>
-    match (Z.compare (wordToZ a) (wordToZ b)) with
-    | Gt => true
-    | _ => false
-    end
-  | TUnsignedGt =>
-    match (N.compare (wordToN a) (wordToN b)) with
-    | Gt => true
-    | _ => false
-    end
-  end.
-
-
-Definition evalCond (c: Conditional) (state: State): option bool :=
-  match c with
-  | TestTrue => Some true
-  | TestFalse => Some false
-  | TestReg32Reg32 o i r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r0 state) with
-      | Some v1 => Some (evalTest o i v0 v1)
-      | _ => None
-      end
-    | _ => None
-    end
-  | TestReg32Const o i r x =>
-    match (getReg r state) with
-    | Some v0 =>
-      match x with
-      | const32 v1 => Some (evalTest o i v0 v1)
-      end
-    | _ => None
-    end
-  end.
-
-Definition evalBinOp {n} (o: BinOp) (a b: word n): word n :=
-  match o with
-  | Plus => wplus a b
-  | Minus => wminus a b
-  | Mult => wmult a b
-  | Div => NToWord n ((wordToN a) / (wordToN b))%N
-  | Or => wor a b
-  | Xor => wxor a b
-  | And => wand a b
-  end.
-
-Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n :=
-  match o with
-  | Shl => NToWord n (N.shiftl_nat (wordToN a) m)
-  | Shr => NToWord n (N.shiftr_nat (wordToN a) m)
-
-  (* TODO (rsloan): not actually rotate operations *)
-  | Rotl => NToWord n (N.shiftl_nat (wordToN a) m) 
-  | Rotr => NToWord n (N.shiftr_nat (wordToN a) m)
-  end.
-
-Definition evalOperation (o: Operation) (state: State): 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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    end
-  | RotReg32 b r m =>
-    match (getReg r state) with
-    | Some v0 => setReg r (evalRotOp b v0 m) state
-    | None => state
-    end
-
-  | OpReg64Constant b r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const64 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
-      end
-    | None => state
-    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
-      end
-    | None => state
-    end
-
-  | OpReg128Constant b r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const128 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
-      end
-    | None => state
-    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
-      end
-    | None => state
-    end
-  end.
-
-Definition evalAssignment (a: Assignment) (state: State): 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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    end
-
-  | Assign32Reg32 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => state
-      end
-    | None => state
-    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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    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
-      end
-    | None => state
-    end
-
-  | Assign3232Stack32 r0 i s =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign3232Stack64 r s =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r v1 state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign3232Stack128 r s i =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r (getIndex v1 64 i) state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign3232Reg32 r0 i r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign3232Reg64 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign3232Reg128 r0 r1 i =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (getIndex v1 64 i) state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign6464Reg32 r0 i r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign6464Reg64 r0 i r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | Assign6464Reg128 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => state
-      end
-    | None => state
-    end
-
-  | AssignConstant r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const32 v1 => setReg r v1 state
-      | _ => state
-      end
-    | None => state
-    end
-  end.
-
-(* AlmostQhasm Evaluation *)
-
-
-(* Only execute while loops a fixed number of times.
-   TODO (rsloan): can we do any better? *)
-
-Fixpoint almostEvalWhile (cond: Conditional) (prog: AlmostQhasm) (state: State) (horizon: nat): State :=
-  match horizon with
-  | (S m) => 
-    if (evalCond cond state)
-    then almostEvalWhile cond prog state m
-    else state 
-  | O => state
-  end.
-
-Fixpoint almostEval (prog: AlmostQhasm) (state: State): State :=
-  match prog with
-  | ASeq a b => almostEval b (almostEval a state)
-  | AAssign a => evalAssignment a state
-  | AOp a => evalOperation a state
-  | ACond c a =>
-    if (evalCond c state)
-    then almostEval a state
-    else state 
-  | AWhile c a => almostEvalWhile c a state maxOps
-  end.
-
-Definition almostEvalReg {n} (prog: AlmostQhasm) (reg: Reg n): option (word n) :=
-  getReg reg (almostEval prog emptyState).
-
-Definition almostEvalStack {n} (prog: AlmostQhasm) (stack: Stack n): option (word n) :=
-  getStack stack (almostEval prog emptyState).
-
-(* Qhasm Evaluation *)
-
-Fixpoint getLabelMap' (prog: Qhasm) (cur: LabelMap) (index: nat): LabelMap :=
-  match prog with
-  | p :: ps =>
-    match p with
-    | QLabel label => getLabelMap' ps (NatM.add label index cur) (S index)
-    | _ => getLabelMap' ps cur (S index)
-    end
-  | [] => cur
-  end.
-
-Definition getLabelMap (prog: Qhasm): LabelMap :=
-  getLabelMap' prog (NatM.empty nat) O.
-
-Fixpoint eval' (prog: Qhasm) (state: State) (loc: nat) (horizon: nat) (labelMap: LabelMap) (maxLoc: nat): option State :=
-  match horizon with
-  | (S h) =>
-    match (nth_error prog loc) with
-    | Some stmt =>
-      let (nextState, jmp) :=
-        match stmt with
-        | QAssign a => (evalAssignment a state, None)
-        | QOp o => (evalOperation o state, None)
-        | QLabel l => (state, None)
-        | QJmp c l =>
-          if (evalCond c state)
-          then (state, Some l)
-          else (state, None)
-        end
-      in
-        match jmp with
-        | None =>
-          if (Nat.eq_dec loc maxLoc)
-          then Some nextState
-          else eval' prog nextState (S loc) h labelMap maxLoc
-        | Some nextLoc =>
-          eval' prog nextState nextLoc h labelMap nextLoc
-        end
-    | None => None
-    end
-  | O => None
-  end.
-
-Definition eval (prog: Qhasm) (state: State): option State :=
-  eval' prog state O maxOps (getLabelMap prog) ((length prog) - 1).
-
-Definition evalReg {n} (prog: Qhasm) (reg: Reg n): option (word n) :=
-  match (eval prog emptyState) with
-  | Some st => getReg reg st
-  | None => None
-  end.
-
-Definition evalStack {n} (prog: Qhasm) (stack: Stack n): option (word n) :=
-  match (eval prog emptyState) with
-  | Some st => getStack stack st
-  | None => None
-  end.
-
-(* world peace *)
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
new file mode 100644
index 000000000..2d3567a44
--- /dev/null
+++ b/src/Assembly/QhasmCommon.v
@@ -0,0 +1,157 @@
+Require Export String List.
+Require Export Bedrock.Word.
+
+Require Import ZArith NArith NPeano.
+Require Import Coq.Structures.OrderedTypeEx.
+Require Import FMapAVL FMapList.
+
+Require Import QhasmUtil.
+
+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.
+
+(* A formalization of x86 qhasm *)
+
+(* A constant upper-bound on the number of operations we run *)
+Definition maxOps: nat := 1000.
+
+(* Datatypes *)
+Inductive Const: nat -> Set :=
+  | const32: word 32 -> Const 32
+  | const64: word 64 -> Const 64
+  | const128: word 128 -> Const 128.
+
+Inductive Reg: nat -> Set :=
+  | reg32: nat -> Reg 32
+  | reg3232: nat -> Reg 64
+  | reg6464: nat -> Reg 128
+  | reg80: nat -> Reg 80.
+
+Inductive Stack: nat -> Set :=
+  | stack32: nat -> Stack 32
+  | stack64: nat -> Stack 64
+  | stack128: nat -> Stack 128.
+
+(* Assignments *)
+Inductive Assignment : Set :=
+  | Assign32Stack32: Reg 32 -> Stack 32 -> Assignment
+  | Assign32Stack16: Reg 32 -> Stack 32 -> Index 2 -> Assignment
+  | Assign32Stack8: Reg 32 -> Stack 32 -> Index 4 -> Assignment
+  | Assign32Stack64: Reg 32 -> Stack 64 -> Index 2 -> Assignment
+  | Assign32Stack128: Reg 32 -> Stack 128 -> Index 2 -> Assignment
+
+  | Assign32Reg32: Reg 32 -> Reg 32 -> Assignment
+  | Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment
+  | Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment
+  | Assign32Reg64: Reg 32 -> Reg 64 -> Index 2 -> Assignment
+  | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment
+
+  | Assign3232Stack32: Reg 64 -> Index 2 -> Stack 32 -> Assignment
+  | Assign3232Stack64: Reg 64 -> Stack 64 -> Assignment
+  | Assign3232Stack128: Reg 64 -> Stack 128 -> Index 2 -> Assignment
+
+  | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment
+  | Assign3232Reg64: Reg 64 -> Reg 64 -> Assignment
+  | Assign3232Reg128: Reg 64 -> Reg 128 -> Index 2 -> Assignment
+
+  | Assign6464Reg32: Reg 128 -> Index 4 -> Reg 32 -> Assignment
+  | Assign6464Reg64: Reg 128 -> Index 2 -> Reg 64 -> Assignment
+  | Assign6464Reg128: Reg 128 -> Reg 128 -> Assignment
+
+  | AssignConstant: Reg 32 -> Const 32 -> Assignment.
+
+Hint Constructors Assignment.
+
+(* Operations *)
+
+Inductive BinOp :=
+  | Plus: BinOp | Minus: BinOp | Mult: BinOp
+  | Div: BinOp | Xor: BinOp | And: BinOp | Or: BinOp.
+
+Inductive RotOp :=
+  | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp.
+
+Inductive Operation :=
+  | OpReg32Constant: BinOp -> Reg 32 -> Const 32 -> Operation
+  | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation
+  | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation
+
+  | OpReg64Constant: BinOp -> Reg 64 -> Const 64 -> Operation
+  | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation
+
+  | OpReg128Constant: BinOp -> Reg 128 -> Const 32 -> Operation
+  | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation.
+
+Hint Constructors Operation.
+
+(* Control Flow *)
+
+Inductive TestOp :=
+  | TEq: TestOp
+  | TLt: TestOp
+  | TUnsignedLt: TestOp
+  | TGt: TestOp
+  | TUnsignedGt: TestOp.
+
+Inductive Conditional :=
+  | TestTrue: Conditional
+  | TestFalse: Conditional
+  | TestReg32Reg32: TestOp -> Invert -> Reg 32 -> Reg 32 -> Conditional
+  | TestReg32Const: TestOp -> Invert -> Reg 32 -> Const 32 -> Conditional.
+
+Definition invertConditional (c: Conditional): Conditional :=
+  match c with
+  | TestTrue => TestFalse
+  | TestFalse => TestTrue
+  | TestReg32Reg32 o i r0 r1 => TestReg32Reg32 o (negb i) r0 r1
+  | TestReg32Const o i r c => TestReg32Const o (negb i) r c
+  end.
+
+Hint Constructors Conditional.
+
+(* Machine State *)
+
+Inductive State :=
+| fullState (regState: StateMap) (stackState: StateMap): State.
+
+Definition getReg {n} (reg: Reg n) (state: State): option (word n).
+  destruct state; inversion reg as [L H | L H | L H | L H];
+    destruct (NatM.find n regState) as [map |];
+    first [ destruct (NatM.find L map) as [n0 |] | exact None ];
+    first [ rewrite H; exact (Some (NToWord n n0)) | exact None ].
+Defined.
+
+Definition setReg {n} (reg: Reg n) (value: word n) (state: State): State.
+  inversion state; inversion reg as [L H | L H | L H | L H];
+    destruct (NatM.find n regState) as [map |];
+    first [
+       exact
+         (fullState
+           (NatM.add n
+             (NatM.add L (wordToN value) map) regState)
+             stackState)
+     | exact state ].
+Defined.
+
+Definition getStack {n} (entry: Stack n) (state: State): option (word n).
+  destruct state; inversion entry as [L H | L H | L H];
+    destruct (NatM.find n stackState) as [map |];
+    first [ destruct (NatM.find L map) as [n0 |] | exact None ];
+    first [ rewrite H; exact (Some (NToWord n n0)) | exact None ].
+Defined.
+
+Definition setStack {n} (entry: Stack n) (value: word n) (state: State): State.
+  inversion state; inversion entry as [L H | L H | L H];
+    destruct (NatM.find n stackState) as [map |];
+    first [
+       exact
+         (fullState regState
+           (NatM.add n
+             (NatM.add L (wordToN value) map) regState))
+     | exact state ].
+Defined.
+
+Definition emptyState: State :=
+  fullState (NatM.empty DefMap) (NatM.empty DefMap).
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
new file mode 100644
index 000000000..312f30e03
--- /dev/null
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -0,0 +1,334 @@
+Require Export QhasmCommon.
+Require Export QhasmUtil.
+
+Require Export ZArith.
+
+Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool :=
+  xorb invert
+  match o with
+  | TEq => weqb a b
+  | TLt =>
+    match (Z.compare (wordToZ a) (wordToZ b)) with
+    | Lt => true
+    | _ => false
+    end
+  | TUnsignedLt =>
+    match (N.compare (wordToN a) (wordToN b)) with
+    | Lt => true
+    | _ => false
+    end
+  | TGt =>
+    match (Z.compare (wordToZ a) (wordToZ b)) with
+    | Gt => true
+    | _ => false
+    end
+  | TUnsignedGt =>
+    match (N.compare (wordToN a) (wordToN b)) with
+    | Gt => true
+    | _ => false
+    end
+  end.
+
+Definition evalCond (c: Conditional) (state: State): option bool :=
+  match c with
+  | TestTrue => Some true
+  | TestFalse => Some false
+  | TestReg32Reg32 o i r0 r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r0 state) with
+      | Some v1 => Some (evalTest o i v0 v1)
+      | _ => None
+      end
+    | _ => None
+    end
+  | TestReg32Const o i r x =>
+    match (getReg r state) with
+    | Some v0 =>
+      match x with
+      | const32 v1 => Some (evalTest o i v0 v1)
+      end
+    | _ => None
+    end
+  end.
+
+Definition evalBinOp {n} (o: BinOp) (a b: word n): word n :=
+  match o with
+  | Plus => wplus a b
+  | Minus => wminus a b
+  | Mult => wmult a b
+  | Div => NToWord n ((wordToN a) / (wordToN b))%N
+  | Or => wor a b
+  | Xor => wxor a b
+  | And => wand a b
+  end.
+
+Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n :=
+  match o with
+  | Shl => NToWord n (N.shiftl_nat (wordToN a) m)
+  | Shr => NToWord n (N.shiftr_nat (wordToN a) m)
+
+  (* TODO (rsloan): not actually rotate operations *)
+  | Rotl => NToWord n (N.shiftl_nat (wordToN a) m)
+  | Rotr => NToWord n (N.shiftr_nat (wordToN a) m)
+  end.
+
+Definition evalOperation (o: Operation) (state: State): 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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    end
+  | RotReg32 b r m =>
+    match (getReg r state) with
+    | Some v0 => setReg r (evalRotOp b v0 m) state
+    | None => state
+    end
+
+  | OpReg64Constant b r c =>
+    match (getReg r state) with
+    | Some v0 =>
+      match c with
+      | const64 v1 => setReg r (evalBinOp b v0 v1) state
+      | _ => state
+      end
+    | None => state
+    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
+      end
+    | None => state
+    end
+
+  | OpReg128Constant b r c =>
+    match (getReg r state) with
+    | Some v0 =>
+      match c with
+      | const128 v1 => setReg r (evalBinOp b v0 v1) state
+      | _ => state
+      end
+    | None => state
+    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
+      end
+    | None => state
+    end
+  end.
+
+Definition evalAssignment (a: Assignment) (state: State): 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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    end
+
+  | Assign32Reg32 r0 r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 v1 state
+      | _ => state
+      end
+    | None => state
+    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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    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
+      end
+    | None => state
+    end
+
+  | Assign3232Stack32 r0 i s =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getStack s state) with
+      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign3232Stack64 r s =>
+    match (getReg r state) with
+    | Some v0 =>
+      match (getStack s state) with
+      | Some v1 => setReg r v1 state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign3232Stack128 r s i =>
+    match (getReg r state) with
+    | Some v0 =>
+      match (getStack s state) with
+      | Some v1 => setReg r (getIndex v1 64 i) state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign3232Reg32 r0 i r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign3232Reg64 r0 r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 v1 state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign3232Reg128 r0 r1 i =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 (getIndex v1 64 i) state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign6464Reg32 r0 i r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign6464Reg64 r0 i r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | Assign6464Reg128 r0 r1 =>
+    match (getReg r0 state) with
+    | Some v0 =>
+      match (getReg r1 state) with
+      | Some v1 => setReg r0 v1 state
+      | _ => state
+      end
+    | None => state
+    end
+
+  | AssignConstant r c =>
+    match (getReg r state) with
+    | Some v0 =>
+      match c with
+      | const32 v1 => setReg r v1 state
+      | _ => state
+      end
+    | None => state
+    end
+  end.
diff --git a/src/Assembly/QhasmExtraction.v b/src/Assembly/QhasmExtraction.v
deleted file mode 100644
index 0584553fc..000000000
--- a/src/Assembly/QhasmExtraction.v
+++ /dev/null
@@ -1,24 +0,0 @@
-
-
-(*
-- Define an evaluation function over the QH type, which can be terribly inefficient. This function will be parametrized in the following way:  
-  
-    evalReg x InputRegs OutputRegs
-    evalStack x InputStack OutputStack
-
-Then, produce a lemma which shows that evaluating a given QH will perform an appropriate register operation. This will not check side-effects, which should be okay since we’re synthesizing in a very controlled manner.
-
-- Work on {x: QH | eval x _ _ = AST}, like the bounding code  
-
-- Introduce all Inputs as StackX 
-
-- Replace upward as:  
-
-    + Lifted functions by lemma (as above)
-    + Conditionals as QCond, by lemma
-
-- Then we can convert to string:  
-
-    + We can introduce stack inputs, etc. by traversing the AST
-    + QSeq, QStatement, QAssign are convertible directly
-    + QCond, QWhile are fixed assembly wrappers *)
\ No newline at end of file
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
new file mode 100644
index 000000000..0528d0738
--- /dev/null
+++ b/src/Assembly/QhasmUtil.v
@@ -0,0 +1,44 @@
+
+Require Import ZArith NArith NPeano.
+Require Export Bedrock.Word.
+
+Definition Label := nat.
+Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
+Definition Invert := bool.
+
+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))).
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
new file mode 100644
index 000000000..0504ed3a6
--- /dev/null
+++ b/src/Assembly/StringConversion.v
@@ -0,0 +1,30 @@
+Require Export Qhasm Language Conversion.
+Require Export String.
+
+Module QhasmString <: Language.
+  Definition Program := string.
+  Definition State := unit.
+
+  Definition eval (p: Program) (s: State): option State := Some tt.
+End QhasmString.
+
+Module StringConversion <: Conversion Qhasm QhasmString.
+
+  Definition convertState (st: QhasmString.State): option Qhasm.State := None.
+
+  (* TODO (rsloan): Actually implement string conversion *)
+  Definition convertProgram (prog: Qhasm.Program): option string :=
+    Some EmptyString.
+
+  Lemma convert_spec: forall st' prog,
+    match ((convertProgram prog), (convertState st')) with
+    | (Some prog', Some st) =>
+      match (QhasmString.eval prog' st') with
+      | Some st'' => Qhasm.eval prog st = (convertState st'')
+      | _ => True
+      end
+    | _ => True
+    end.
+  Admitted.
+
+End StringConversion.