Simpler QhasmCommon grammar

updating QhasmCommon

Pushing through changes

Pushing through changes

Pushing through changes

Pushing through changes

Pushing through changes

Pushing through changes

5 files changed, 376 insertions, 461 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 46e2664ad..aeeb0746f 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -1,4 +1,4 @@
-Require Export String List.
+Require Export String List NPeano NArith.
 Require Export Bedrock.Word.
 
 (* A formalization of x86 qhasm *)
@@ -6,113 +6,158 @@ 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.
+(* Sugar and Tactics *)
 
-(* Datatypes *)
-Inductive Const: nat -> Set :=
-  | const32: word 32 -> Const 32
-  | const64: word 64 -> Const 64
-  | const128: word 128 -> Const 128.
+Definition convert {A B: Type} (x: A) (H: A = B): B :=
+  eq_rect A (fun B0 : Type => B0) x B H.
 
-Inductive Reg: nat -> Set :=
-  | reg32: nat -> Reg 32
-  | reg3232: nat -> Reg 64
-  | reg6464: nat -> Reg 128
-  | reg80: nat -> Reg 80.
+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.
 
-Inductive Stack: nat -> Set :=
+Obligation Tactic := abstract intuition.
+
+(* Float Datatype *)
+
+Record Float (floatBits: nat) (fractionBits: nat) := mkFloat {
+  validFloat: word floatBits -> Prop;
+
+  wordToFloat: word fractionBits -> {w: word floatBits | validFloat w};
+  floatToWord: {w: word floatBits | validFloat w} -> word fractionBits;
+
+  wordToFloat_spec : forall x, floatToWord (wordToFloat x) = x;
+
+  serialize: {w: word floatBits | validFloat w} -> N;
+  deserialize: N -> {w: word floatBits | validFloat w};
+
+  serialize_spec1 : forall x, serialize (deserialize x) = x;
+  serialize_spec2 : forall x, deserialize (serialize x) = x;
+
+  floatPlus: {w: word floatBits | validFloat w}
+          ->  {w: word floatBits | validFloat w}
+          ->  {w: word floatBits | validFloat w};
+
+  floatPlus_wordToFloat : forall n m,
+      (wordToN n < (Npow2 (fractionBits - 1)))%N ->
+      (wordToN m < (Npow2 (fractionBits - 1)))%N ->
+      floatPlus (wordToFloat n) (wordToFloat m)
+        = wordToFloat (wplus n m);
+
+  floatMult: {w: word floatBits | validFloat w}
+          ->  {w: word floatBits | validFloat w}
+          ->  {w: word floatBits | validFloat w};
+
+  floatMult_wordToFloat : forall n m,
+      (wordToN n < (Npow2 (fractionBits / 2)%nat))%N ->
+      (wordToN m < (Npow2 (fractionBits / 2)%nat))%N ->
+      floatMult (wordToFloat n) (wordToFloat m)
+        = wordToFloat (wmult n m);
+
+  floatAnd:  {w: word floatBits | validFloat w}
+          ->  {w: word floatBits | validFloat w}
+          ->  {w: word floatBits | validFloat w};
+
+  floatAnd_wordToFloat : forall n m,
+    floatAnd (wordToFloat n) (wordToFloat m) = wordToFloat (wand n m)
+}.
+
+Parameter Float32: Float 32 23.
+
+Parameter Float64: Float 64 52.
+
+(* Asm Types *)
+Inductive IConst: nat -> Type :=
+  | constInt32: word 32 -> IConst 32.
+
+Inductive FConst: nat -> Type :=
+  | constFloat32: word 32 -> FConst 32
+  | constFloat64: word 64 -> FConst 64.
+
+Inductive IReg: nat -> Type :=
+  | regInt32: nat -> IReg 32.
+
+Inductive FReg: nat -> Type :=
+  | regFloat32: nat -> FReg 32
+  | regFloat64: nat -> FReg 64.
+
+Inductive Stack: nat -> Type :=
   | stack32: nat -> Stack 32
   | stack64: nat -> Stack 64
-  | stack128: nat -> Stack 128
-  | stack256: nat -> Stack 256
-  | stack512: nat -> Stack 512.
+  | 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
+Definition CarryState := option bool.
 
-  | 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
+(* Assignments *)
+Inductive Assignment : Type :=
+  | ARegStackInt: forall n, IReg n -> Stack n -> Assignment
+  | ARegStackFloat: forall n, FReg n -> Stack n -> Assignment
 
-  | Assign3232Stack32: Reg 64 -> Index 2 -> Stack 32 -> Assignment
-  | Assign3232Stack64: Reg 64 -> Stack 64 -> Assignment
-  | Assign3232Stack128: Reg 64 -> Stack 128 -> Index 2 -> Assignment
+  | AStackRegInt: forall n, Stack n -> IReg n -> Assignment
+  | AStackRegFloat: forall n, Stack n -> FReg n -> Assignment
 
-  | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment
-  | Assign3232Reg64: Reg 64 -> Reg 64 -> Assignment
-  | Assign3232Reg128: Reg 64 -> Reg 128 -> Index 2 -> Assignment
+  | ARegRegInt: forall n, IReg n -> IReg n -> Assignment
+  | ARegRegFloat: forall n, FReg n -> FReg n -> Assignment
 
-  | Assign6464Reg32: Reg 128 -> Index 4 -> Reg 32 -> Assignment
-  | Assign6464Reg64: Reg 128 -> Index 2 -> Reg 64 -> Assignment
-  | Assign6464Reg128: Reg 128 -> Reg 128 -> Assignment
+  | AConstInt: forall n, IReg n -> IConst n -> Assignment
+  | AConstFloat: forall n, FReg n -> FConst n -> Assignment
 
-  | AssignConstant: Reg 32 -> Const 32 -> Assignment.
+  | AIndex: forall n m, IReg n -> IReg m -> Index (n/m)%nat -> Assignment
+  | APtr: forall n, IReg 32 -> Stack n -> Assignment.
 
 Hint Constructors Assignment.
 
 (* Operations *)
 
-Inductive BinOp :=
-  | Plus: BinOp | Minus: BinOp | Mult: BinOp
-  | Div: BinOp | Xor: BinOp | And: BinOp | Or: BinOp.
+Inductive IntOp :=
+  | IPlus: IntOp | IMinus: IntOp
+  | IXor: IntOp  | IAnd: IntOp | IOr: IntOp.
+
+Inductive FloatOp :=
+  | FPlus: FloatOp | FMult: FloatOp | FAnd: FloatOp.
 
 Inductive RotOp :=
-  | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp.
+  | Shl: RotOp | Shr: RotOp.
 
 Inductive Operation :=
-  | OpReg32Constant: BinOp -> Reg 32 -> Const 32 -> Operation
-  | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation
-  | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation
+  | IOpConst: IntOp -> IReg 32 -> IConst 32 -> Operation
+  | IOpReg: IntOp -> IReg 32 -> IReg 32 -> Operation
+
+  | FOpConst32: FloatOp -> FReg 32 -> FConst 32 -> Operation
+  | FOpReg32: FloatOp -> FReg 32 -> FReg 32 -> Operation
 
-  | OpReg64Constant: BinOp -> Reg 64 -> Const 64 -> Operation
-  | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation
+  | FOpConst64: FloatOp -> FReg 64 -> FConst 64 -> Operation
+  | FOpReg64: FloatOp -> FReg 64 -> FReg 64 -> Operation
 
-  | OpReg128Constant: BinOp -> Reg 128 -> Const 32 -> Operation
-  | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation.
+  | OpRot: RotOp -> IReg 32 -> Index 32 -> Operation.
 
 Hint Constructors Operation.
 
 (* Control Flow *)
 
 Inductive TestOp :=
-  | TEq: TestOp
-  | TLt: TestOp
-  | TUnsignedLt: TestOp
-  | TGt: TestOp
-  | TUnsignedGt: TestOp.
+  | TEq: TestOp   | TLt: TestOp  | TLe: TestOp
+  | TGt: TestOp   | TGe: 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.
+  | TestInt: forall n, TestOp -> IReg n -> IReg n -> Conditional
+  | TestFloat: forall n, TestOp -> FReg n -> FReg n -> Conditional.
 
 Hint Constructors Conditional.
 
 (* Reg, Stack, Const Utilities *)
 
-Definition getRegWords {n} (x: Reg n) :=
+Definition getIRegWords {n} (x: IReg n) :=
+  match x with
+  | regInt32 loc => 1
+  end.
+
+Definition getFRegWords {n} (x: FReg n) :=
   match x with
-  | reg32 loc => 1
-  | reg3232 loc => 2
-  | reg6464 loc => 4
-  | reg80 loc => 2
+  | regFloat32 loc => 1
+  | regFloat64 loc => 2
   end.
 
 Definition getStackWords {n} (x: Stack n) :=
@@ -120,16 +165,17 @@ Definition getStackWords {n} (x: Stack n) :=
   | stack32 loc => 1
   | stack64 loc => 2
   | stack128 loc => 4
-  | stack256 loc => 8
-  | stack512 loc => 16
   end.
 
-Definition getRegIndex {n} (x: Reg n): nat :=
+Definition getIRegIndex {n} (x: IReg n): nat :=
+  match x with
+  | regInt32 loc => loc
+  end.
+
+Definition getFRegIndex {n} (x: FReg n): nat :=
   match x with
-  | reg32 loc => loc
-  | reg3232 loc => loc
-  | reg6464 loc => loc
-  | reg80 loc => loc
+  | regFloat32 loc => loc
+  | regFloat64 loc => loc
   end.
 
 Definition getStackIndex {n} (x: Stack n): nat :=
@@ -137,15 +183,18 @@ Definition getStackIndex {n} (x: Stack n): nat :=
   | stack32 loc => loc
   | stack64 loc => loc
   | stack128 loc => loc
-  | stack256 loc => loc
-  | stack512 loc => loc
   end.
 
 (* For register allocation checking *)
-Definition regCount (base: nat): nat :=
+Definition intRegCount (base: nat): nat :=
   match base with
-  | 32 => 7   | 64 => 8
-  | 128 => 8  | 80 => 8
+  | 32 => 7
   | _ => 0
   end.
 
+Definition floatRegCount (base: nat): nat :=
+  match base with
+  | 32 => 8
+  | 64 => 8
+  | _ => 0
+  end.
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 009bcbd1e..92c27bb72 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,322 +1,170 @@
 Require Export QhasmCommon QhasmUtil State.
-Require Export ZArith.
+Require Export ZArith Sumbool.
 Require Export Bedrock.Word.
 
 Import State.
 Import Util.
 
-Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool :=
-  xorb invert
+Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
+  let c := (N.compare (wordToN a) (wordToN b)) in
+
+  let eqBit := match c with | Eq => true | _ => false end in
+  let ltBit := match c with | Lt => true | _ => false end in
+  let gtBit := match c with | Gt => true | _ => false end in
+
   match o with
-  | TEq => 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
+  | TEq => eqBit
+  | TLt => ltBit
+  | TLe => orb (eqBit) (ltBit)
+  | TGt => gtBit
+  | TGe => orb (eqBit) (gtBit)
   end.
 
-Definition evalCond (c: Conditional) (state: State): option bool :=
-  match c with
+Definition evalCond (c: Conditional) (state: State): option bool.
+  refine 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)
+  | 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
-  | TestReg32Const o i r x =>
-    match (getReg r state) with
-    | Some v0 =>
-      match x with
-      | const32 v1 => Some (evalTest o i v0 v1)
+
+  | TestFloat n t a b =>
+    let aOpt := (getFloatReg a state) in
+    let bOpt := convert (getFloatReg a state) _ in
+
+    match aOpt with
+    | Some va =>
+      match bOpt with
+      | Some vb => Some (evalTest t va vb)
+      | _ => None
       end
     | _ => None
     end
-  end.
+  end; abstract (
+    inversion a; inversion b;
+    unfold aOpt, getFractionalBits;
+    simpl; intuition).
+Defined.
+
+Definition evalOperation (o: Operation) (state: State): option State.
+  refine (
+  let evalIOp := fun {b} (io: IntOp) (x y: word b) =>
+    match io with
+    | IPlus => wplus x y
+    | IMinus => wminus x y
+    | IXor => wxor x y
+    | IAnd => wand x y
+    | IOr => wor x y
+    end in
+
+  let evalFOp := fun {b} (fo: FloatOp) (x y: word b) =>
+    match fo with
+    | FAnd => wand x y
+    | FPlus => wplus x y
+    | FMult => wmult x y
+    end in
+
+  let evalRotOp := fun {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 in
+
+  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
 
-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.
+  | IOpConst o r c =>
+    liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
+      (getIntReg r state)
+      (match c with | constInt32 v => Some v 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)
+  | IOpReg o a b =>
+    liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
+      (getIntReg a state) (getIntReg b state)
 
-  (* 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.
+  | FOpConst32 o r c =>
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state)
+      (match c with | constFloat32 v => Some (convert v _) end)
 
-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
-      end
-    | None => None
-    end
+  | FOpReg32 o a b =>
+    liftOpt (fun x y => setFloatReg a (evalFOp o x y) state)
+      (getFloatReg a state) (convert (getFloatReg b state) _)
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  | FOpConst64 o r c =>
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state)
+      (match c with | constFloat64 v => Some (convert v _) end)
 
-  | RotReg32 b r m =>
-    match (getReg r state) with
-    | Some v0 => setReg r (evalRotOp b v0 m) state
-    | None => None
-    end
+  | FOpReg64 o a b =>
+    liftOpt (fun x y => setFloatReg a (evalFOp o x y) state)
+      (getFloatReg a state) (convert (getFloatReg b state) _)
 
-  | OpReg64Constant b r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const64 v1 => setReg r (evalBinOp b v0 v1) state
-      end
+  | OpRot o r i =>
+   match (getIntReg r state) with
+    | Some va => setIntReg r (evalRotOp o va i) state
     | None => None
     end
+  end); abstract intuition.
+Defined.
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+Definition getIConst {n} (c: IConst n): word n :=
+  match c with
+  | constInt32 v => v
+  end.
 
-  (* Don't implement the 128-wide ops yet:
-     I think x86 doesn't do them like this *)
-  | _ => None end.
+Definition getFConst {n} (c: FConst n): word n :=
+  match c with
+  | constFloat32 v => v
+  | constFloat64 v => v
+  end.
 
 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | None => None
-    end
-
-  | Assign32Reg32 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | None => None
-    end
+  let liftOpt := fun {A B} (f: A -> option B) (xo: option A) =>
+    match xo with
+    | (Some x') => f x'
+    | _ => None
+    end in
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  match a with
+  | ARegStackInt n r s =>
+    liftOpt (fun x => setIntReg r x state) (getStack s state)
 
-  | Assign3232Stack64 r s =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r v1 state
-      | _ => None
-      end
-    | None => None
-    end
+  | ARegStackFloat n r s =>
+    liftOpt (fun x => setFloatReg r x state) (getStack s state)
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  | AStackRegInt n s r =>
+    liftOpt (fun x => setStack s x state) (getIntReg r state)
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  | AStackRegFloat n s r =>
+    liftOpt (fun x => setStack s x state) (getFloatReg r state)
 
-  | Assign3232Reg64 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => None
-      end
-    | None => None
-    end
+  | ARegRegInt n a b =>
+    liftOpt (fun x => setIntReg a x state) (getIntReg b state)
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  | ARegRegFloat n a b =>
+    liftOpt (fun x => setFloatReg a x state) (getFloatReg b state)
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  | AConstInt n r c => setIntReg r (getIConst c) state
 
-  | 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
-      | _ => None
-      end
-    | None => None
-    end
+  | AConstFloat n r c => setFloatReg r (getFConst c) state
 
-  | Assign6464Reg128 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => None
-      end
-    | None => None
+  | AIndex n m a b i =>
+    match (getIntReg b state) with
+    | Some v => setIntReg a (trunc n (getIndex v m i)) state
+    | _ => None
     end
 
-  | AssignConstant r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const32 v1 => setReg r v1 state
-      end
-    | None => None
-    end
+  | APtr n r s =>
+    setIntReg r (NToWord 32 (N.of_nat (getStackIndex s))) state 
   end.
-
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 774dc50b8..70c3e4218 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -10,11 +10,24 @@ Module Util.
     Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
     Coercion indexToNat : Index >-> nat.
 
+    (* Float Manipulations *)
+
+    Definition getFractionalBits {n} (reg: FReg n): nat :=
+      if (Nat.eq_dec n 32) then 23 else
+      if (Nat.eq_dec n 64) then 52 else 0.
+
+    Definition getFloatInstance {n} (reg: FReg n): Float n (getFractionalBits reg).
+      refine match reg with
+      | regFloat32 _ => (eq_rect _ id Float32 _ _)
+      | regFloat64 _ => (eq_rect _ id Float64 _ _)
+      end; abstract intuition.
+    Defined.
+
     (* 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].
+      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)).
@@ -49,11 +62,11 @@ Module Util.
     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.
+      intros; destruct x; simpl; intuition.
     Defined.
 
     Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n.
-    intros; destruct x; simpl; intuition.
+      intros; destruct x; simpl; intuition.
     Defined.
 
  End Util.
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 16b9b12d3..2e030d242 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -23,33 +23,24 @@ Module State.
     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.
+    | fullState (intRegState: StateMap)
+                (floatRegState: StateMap)
+                (stackState: DefMap)
+                (carryBit: CarryState): State.
 
-    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N).
+    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty DefMap) (NatM.empty N) None.
 
     (* Register State Manipulations *)
 
-    Definition getReg {n} (reg: Reg n) (state: State): option (word n) :=
+    Definition getIntReg {n} (reg: IReg n) (state: State): option (word n) :=
       match state with
-      | fullState regState stackState =>
-        match (NatM.find n regState) with
+      | fullState intRegState _ _ _ =>
+        match (NatM.find n intRegState) with
         | Some map =>
-            match (NatM.find (getRegIndex reg) map) with
+            match (NatM.find (getIRegIndex reg) map) with
             | Some m => Some (NToWord n m)
             | _ => None
             end
@@ -57,23 +48,66 @@ Module State.
         end
       end.
 
-    Definition setReg {n} (reg: Reg n) (value: word n) (state: State): option State :=
+    Definition setIntReg {n} (reg: IReg n) (value: word n) (state: State): option State :=
+      match state with
+      | fullState intRegState floatRegState stackState carryState =>
+        match (NatM.find n intRegState) with
+        | Some map =>
+            Some (fullState
+                    (NatM.add n (NatM.add (getIRegIndex reg) (wordToN value) map) intRegState)
+                    floatRegState
+                    stackState
+                    carryState)
+        | None => None
+        end
+      end.
+
+    Definition getFloatReg {n} (reg: FReg n) (state: State): option (word n) :=
+      match state with
+      | fullState _ floatRegState _ _ =>
+        match (NatM.find n floatRegState) with
+        | Some map =>
+          match (NatM.find (getFRegIndex reg) map) with
+          | Some v => Some (NToWord n v)
+          | None => None
+          end
+        | None => None
+        end
+      end.
+
+    Definition setFloatReg {n} (reg: FReg n) (value: word n) (state: State): option State :=
       match state with
-      | fullState regState stackState =>
-        match (NatM.find n regState) with
+      | fullState intRegState floatRegState stackState carryState =>
+        match (NatM.find n floatRegState) with
         | Some map =>
             Some (fullState
-                    (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map) regState)
-                    stackState)
+              intRegState
+              (NatM.add n (NatM.add (getFRegIndex reg) (wordToN value) map) floatRegState)
+              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 floatRegState stackState carryState =>
+        fullState intRegState floatRegState stackState (Some value)
+      end.
+
+
     (* Per-word Stack Operations *)
 
     Definition getStack32 (entry: Stack 32) (state: State): option (word 32) :=
       match state with
-      | fullState regState stackState =>
+      | fullState _ _ stackState _ =>
         match entry with
         | stack32 loc =>
           match (NatM.find loc stackState) with
@@ -85,11 +119,12 @@ Module State.
 
     Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State :=
     match state with
-    | fullState regState stackState =>
+    | fullState intRegState floatRegState stackState carryState =>
         match entry with
         | stack32 loc =>
-        (Some (fullState regState
-              (NatM.add loc (wordToN value) stackState)))
+          (Some (fullState intRegState floatRegState
+                   (NatM.add loc (wordToN value) stackState)
+                   carryState))
         end
     end.
 
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index d1b273c98..d44dbfcbf 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -1,6 +1,5 @@
 Require Export Language Conversion.
-Require Export Qhasm.
-Require Import QhasmCommon QhasmEvalCommon QhasmUtil.
+Require Import QhasmCommon QhasmEvalCommon QhasmUtil Qhasm.
 Require Export String Ascii.
 Require Import NArith NPeano.
 Require Export Bedrock.Word.
@@ -53,81 +52,56 @@ Module StringConversion <: Conversion Qhasm QhasmString.
 
   Section Elements.
     Local Open Scope string_scope.
+    Import Util.
 
     Definition nameSuffix (n: nat): string := 
       (nToHex (N.of_nat n)).
 
-    Definition wordToString {n} (w: word n): string := 
+    Coercion wordToString {n} (w: word n): string := 
       "0x" ++ (nToHex (wordToN w)).
 
-    Coercion wordToString : word >-> string.
-
-    Definition constToString {n} (c: Const n): string :=
+    Coercion constToString {n} (c: Const n): string :=
       match c with
       | const32 w => "0x" ++ w
       | const64 w => "0x" ++ w
       | const128 w => "0x" ++ w
       end.
 
-    Coercion constToString : Const >-> string.
-
-    Definition indexToString {n} (i: Index n): string :=
+    Coercion indexToString {n} (i: Index n): string :=
       "0x" ++ (nToHex (N.of_nat i)).
 
-    Coercion indexToString : Index >-> string.
-
-    Definition regToString {n} (r: Reg n): option string :=
-      Some match r with
+    Coercion regToString {n} (r: Reg n): string :=
+      match r with
       | reg32 n => "ex" ++ (nameSuffix n)
       | reg3232 n => "mm" ++ (nameSuffix n)
       | reg6464 n => "xmm" ++ (nameSuffix n)
       | reg80 n => "st" ++ (nameSuffix n)
       end.
 
-    Definition stackToString {n} (s: Stack n): option string :=
-      Some match s with
+    Coercion stackToString {n} (s: Stack n): string :=
+      match s with
       | stack32 n => "word" ++ (nameSuffix n)
       | stack64 n => "double" ++ (nameSuffix n)
       | stack128 n => "quad" ++ (nameSuffix n)
+      | stack256 n => "stack256n" ++ (nameSuffix n)
+      | stack512 n => "stack512n" ++ (nameSuffix n)
       end.
 
+    Coercion stringToSome (x: string): option string := Some x.
+
     Definition stackLocation {n} (s: Stack n): word 32 :=
       combine (natToWord 8 n) (natToWord 24 n).
 
     Definition assignmentToString (a: Assignment): option string :=
       match a with
-      | Assign32Stack32 r s =>
-        match (regToString r, stackToString s) with
-        | (Some s0, Some s1) => s0 ++ " = " ++ s1
-        | _ => None
-        end.
-      | Assign32Stack16 r s i => r0 ++ " = " ++ r1
-      | Assign32Stack8 r s i =>
-      | Assign32Stack64 r s i =>
-      | Assign32Stack128 r s i =>
-
-      | Assign32Reg32 r0 r1 => r0 ++ " = " ++ r1 
-      | Assign32Reg16 r0 r1 i =>
-      | Assign32Reg8 r0 r1 i =>
-      | Assign32Reg64 r0 r1 i =>
-      | Assign32Reg128 r0 r1 i =>
-
-      | Assign3232Stack32 r i s =>
-      | Assign3232Stack64 r s =>
-      | Assign3232Stack128 r s i =>
-
-      | Assign3232Reg32 r0 i r1 =>
-      | Assign3232Reg64 r0 r1 =>
-      | Assign3232Reg128 r0 r1 i =>
-
-      | Assign6464Reg32 r0 i r1 =>
-      | Assign6464Reg64 r0 i r1 =>
-      | Assign6464Reg128 r0 r1 =>
-
-      | AssignConstant r c =>
+
+      (* r = s *)
+      | Assign32Stack32 r s => r ++ " = " ++ s
+
+      | _ => None
       end.
 
-    Definition binOpToString (b: BinOp): string :=
+    Coercion binOpToString (b: BinOp): string :=
       match b with
       | Plus => "+"
       | Minus => "-"
@@ -138,7 +112,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       | Or => "|"
       end.
 
-    Definition rotOpToString (r: RotOp): string :=
+    Coercion rotOpToString (r: RotOp): string :=
       match r with
       | Shl => "<<"
       | Shr => ">>"
@@ -146,41 +120,37 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       | Rotr => ">>>"
       end.
 
-    Definition operationToString (o: Operation): string :=
+    Definition operationToString (o: Operation): option string :=
       match o with
       | OpReg32Constant b r c =>
-        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+        r ++ " " ++ b ++ "= " ++ c
       | OpReg32Reg32 b r0 r1 =>
-        (regToString r0) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString r1)
+        r0 ++ " " ++ b ++ "= " ++ r1
       | RotReg32 o r i =>
-        (regToString r) ++ " " ++ (rotOpToString o) ++ "= " ++ (constToString i)
-
+        r ++ " " ++ o ++ "= " ++ i
       | OpReg64Constant b r c =>
-        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+        r ++ " " ++ b ++ "= " ++ c
       | OpReg64Reg64 b r0 r1 =>
-        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
-
-      | OpReg128Constant b r c =>
-        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
-      | OpReg128Reg128 b r0 r1 =>
-        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+        r0 ++ " " ++ b ++ "= " ++ r1
+      | _ => None
       end.
 
-    Definition testOpToString (t: TestOp): string :=
+    Coercion testOpToString (t: TestOp): string :=
       match t with
-      | TEq =>
-      | TLt =>
-      | TUnsignedLt =>
-      | TGt =>
-      | TUnsignedGt =>
+      | TEq => "="
+      | TLt => "<"
+      | TUnsignedLt => "unsigned<"
+      | TGt => ">"
+      | TUnsignedGt => "unsigned>"
       end.
 
     Definition conditionalToString (c: Conditional): string :=
+      let f := fun (i: bool) => if i then "!" else "" in
       match c with
-      | TestTrue =>
-      | TestFalse =>
-      | TestReg32Reg32 o i r0 r1 =>
-      | TestReg32Const o i r c =>
+      | TestTrue => ""
+      | TestFalse => ""
+      | TestReg32Reg32 o i r0 r1 => (f i) ++ o ++ "?" ++ r0 ++ " " ++ r1
+      | TestReg32Const o i r c =>(f i) ++ o ++ "?" ++ r ++ " " ++ c
       end.
 
   End Elements.
@@ -188,9 +158,9 @@ Module StringConversion <: Conversion Qhasm QhasmString.
   Section Parsing.
 
     Inductive Entry :=
-      | regEntry: forall n, Reg n => Entry
-      | stackEntry: forall n, Stack n => Entry
-      | constEntry: forall n, Const n => Entry.
+      | regEntry: forall n, Reg n -> Entry
+      | stackEntry: forall n, Stack n -> Entry
+      | constEntry: forall n, Const n -> Entry.
 
     Definition allRegs (prog: Qhasm.Program): list Entry := [(* TODO *)]