Pushing through changes

3 files changed, 87 insertions, 27 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 6b40c9d2a..2f4d7f9be 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -11,14 +11,21 @@ Definition maxOps: nat := 1000.
 
 (* Float Datatype *)
 
-Record Float (n: nat) (fractionBits: nat) := mkFloat {
+Record Float (floatBits: nat) (fractionBits: nat) := mkFloat {
   FloatType: Set;
 
   wordToFloat: word fractionBits -> FloatType;
   floatToWord: FloatType -> word fractionBits;
 
+  wordToFloat_spec : forall x, floatToWord (wordToFloat x) = x;
+
+  serialize: FloatType -> N;
+  deserialize: N -> FloatType;
+
+  serialize_spec1 : forall x, serialize (deserialize x) = x;
+  serialize_spec2 : forall x, deserialize (serialize x) = x;
+
   floatPlus: FloatType -> FloatType -> FloatType;
-  floatMult: FloatType -> FloatType -> FloatType;
 
   floatPlus_wordToFloat : forall n m,
       (wordToN n < (Npow2 (fractionBits - 1)))%N ->
@@ -26,27 +33,26 @@ Record Float (n: nat) (fractionBits: nat) := mkFloat {
       floatPlus (wordToFloat n) (wordToFloat m)
         = wordToFloat (wplus n m);
 
+  floatMult: FloatType -> FloatType -> FloatType;
+
   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);
-
-  wordToFloat_spec : forall x, 
-      floatToWord (wordToFloat x) = x
+        = wordToFloat (wmult n m)
 }.
 
 Parameter Float32: Float 32 23.
 
-Parameter Float64: Float 64 53.
+Parameter Float64: Float 64 52.
 
 (* Asm Types *)
 Inductive IConst: nat -> Type :=
   | constInt32: word 32 -> IConst 32.
 
 Inductive FConst: nat -> Type :=
-  | constFloat32: forall b, Float 32 b -> FConst 32
-  | constFloat64: forall b, Float 64 b -> FConst 64.
+  | constFloat32: (FloatType _ _ Float32) -> FConst 32
+  | constFloat64: (FloatType _ _ Float64) -> FConst 64.
 
 Inductive IReg: nat -> Type :=
   | regInt32: nat -> IReg 32.
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 774dc50b8..60b3b49a0 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -10,6 +10,21 @@ 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 :=
+      match reg with
+      | regFloat32 _ => 23
+      | regFloat64 _ => 52
+      end.
+
+    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; intuition.
+    Defined.
+
     (* Magical Bitwise Manipulations *)
 
     (* Force w to be m bits long, by truncation or zero-extension *)
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index c61a408c3..432af2fbf 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -38,18 +38,21 @@ Module State.
     (* The Big Definition *)
 
     Inductive State :=
-      | fullState (regState: StateMap) (stackState: DefMap) (carryBit: CarryState): State.
+    | fullState (intRegState: StateMap)
+                (floatRegState: StateMap)
+                (stackState: DefMap)
+                (carryBit: CarryState): State.
 
-    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N) None.
+    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,30 +60,67 @@ 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 regState stackState carryState =>
-        match (NatM.find n regState) with
+      | fullState intRegState floatRegState stackState carryState =>
+        match (NatM.find n intRegState) with
         | Some map =>
             Some (fullState
-                    (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map) regState)
+                    (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 (getFractionalBits reg)).
+      refine match state with
+      | fullState _ floatRegState _ _ =>
+        match (NatM.find n floatRegState) with
+        | Some map =>
+          match (NatM.find (getFRegIndex reg) map) with
+          | Some m =>
+            let f := getFloatInstance reg in
+            let b := getFractionalBits reg in
+            Some (floatToWord n b f (deserialize n b f m))
+          | _ => None
+          end
+        | None => None
+        end
+      end; abstract (unfold getFractionalBits, f, b; destruct reg; simpl; intuition).
+    Defined.
+
+    Definition setFloatReg {n} (reg: FReg n) (value: word (getFractionalBits reg)) (state: State): option State.
+      refine match state with
+      | fullState intRegState floatRegState stackState carryState =>
+        match (NatM.find n floatRegState) with
+        | Some map =>
+            let f := getFloatInstance reg in
+            let b := getFractionalBits reg in
+            Some (fullState
+              intRegState
+              (NatM.add n (NatM.add (getFRegIndex reg)
+                 (serialize n b f (wordToFloat n b f value)) map) floatRegState)
+              stackState
+              carryState)
+        | None => None
+        end
+      end; abstract (unfold getFractionalBits, f, b; destruct reg; simpl; intuition).
+    Defined.
+
     (* Carry State Manipulations *)
 
-    Definition getCarry {n} (reg: Reg n) (state: State): CarryState :=
+    Definition getCarry (state: State): CarryState :=
       match state with
-      | fullState _ _ b => b
+      | fullState _ _ _ b => b
       end.
 
     Definition setCarry (value: bool) (state: State): State :=
       match state with
-      | fullState regState stackState carryState =>
-        fullState regState stackState (Some value)
+      | fullState intRegState floatRegState stackState carryState =>
+        fullState intRegState floatRegState stackState (Some value)
       end.
 
 
@@ -88,7 +128,7 @@ Module State.
 
     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
@@ -100,11 +140,10 @@ Module State.
 
     Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State :=
     match state with
-    | fullState regState stackState carryState =>
+    | fullState intRegState floatRegState stackState carryState =>
         match entry with
         | stack32 loc =>
-          (Some (fullState
-                   regState
+          (Some (fullState intRegState floatRegState
                    (NatM.add loc (wordToN value) stackState)
                    carryState))
         end