Major language refactoring to support Memory and AddWithCarry

4 files changed, 155 insertions, 89 deletions

diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
index 929eeaba5..d50e3a6bd 100644
--- a/src/Assembly/AlmostQhasm.v
+++ b/src/Assembly/AlmostQhasm.v
@@ -15,12 +15,30 @@ Module AlmostQhasm <: Language.
     | AAssign: Assignment -> AlmostProgram
     | AOp: Operation -> AlmostProgram
     | ACond: Conditional -> AlmostProgram -> AlmostProgram -> AlmostProgram
-    | AWhile: Conditional -> AlmostProgram -> AlmostProgram.
+    | AWhile: Conditional -> AlmostProgram -> AlmostProgram
+    | ADef: Label -> AlmostProgram -> AlmostProgram -> AlmostProgram
+    | ACall: Label -> AlmostProgram.
 
   Hint Constructors AlmostProgram.
 
   Definition Program := AlmostProgram.
 
+  Fixpoint inline (l: nat) (f prog: AlmostProgram) :=
+    match prog with
+    | ASeq a b => ASeq (inline l f a) (inline l f b)
+    | ACond c a b => ACond c (inline l f a) (inline l f b)
+    | AWhile c a => AWhile c (inline l f a)
+    | ADef l' f' p' =>
+      if (Nat.eq_dec l l')
+      then prog
+      else ADef l' (inline l f f') (inline l f p')
+    | ACall l' =>
+      if (Nat.eq_dec l l')
+      then f
+      else prog
+    | _ => prog
+    end.
+
   Inductive AlmostEval: AlmostProgram -> State -> State -> Prop :=
     | AESkip: forall s, AlmostEval ASkip s s
     | AESeq: forall p p' s s' s'',
@@ -48,7 +66,10 @@ Module AlmostQhasm <: Language.
       -> AlmostEval (AWhile c a) s s''
     | AEWhileSkip: forall c a s,
         evalCond c s = Some false
-      -> AlmostEval (AWhile c a) s s.
+        -> AlmostEval (AWhile c a) s s
+    | AEFun: forall l f p s s',
+        AlmostEval (inline l f p) s s'
+        -> AlmostEval (ADef l f p) s s'.
 
   Definition evaluatesTo := AlmostEval.
 
diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v
index aea77932d..90f6afd73 100644
--- a/src/Assembly/Medial.v
+++ b/src/Assembly/Medial.v
@@ -10,15 +10,24 @@ Module Medial (M: PseudoMachine) <: Language.
   Definition W := word width.
 
   (* Program Types *)
-  Definition State := DefMap.
+  Definition State := (NatNMap * PairNMap * (option bool))%type.
+
+  Definition varS (st: State) := fst (fst st).
+  Definition memS (st: State) := snd (fst st).
+  Definition carryS (st: State) := snd st.
+
+  Definition var (i: nat) (st: State) := NatM.find i (varS st).
+  Definition mem (v i: nat) (st: State) := PairM.find (v, i) (memS st).
 
   Inductive MAssignment : Type :=
     | MAVar: nat -> nat -> MAssignment 
+    | MAMem: nat -> nat -> nat -> MAssignment 
     | MAConst: nat -> W -> MAssignment.
 
   Inductive MOperation :=
     | MIOpConst: IntOp -> nat -> W -> MOperation
     | MIOpReg: IntOp -> nat -> nat -> MOperation
+    | MCOpReg: CarryOp -> nat -> nat -> MOperation
     | MDOpReg: DualOp -> nat -> nat -> option nat -> MOperation
     | MOpRot: RotOp -> nat -> Index width -> MOperation.
 
@@ -31,65 +40,112 @@ Module Medial (M: PseudoMachine) <: Language.
     | MAssign: MAssignment -> Medial
     | MOp: MOperation -> Medial
     | MCond: MConditional -> Medial -> Medial -> Medial
-    | MFunexp: nat -> Medial -> Medial.
+    | MFunexp: nat -> Medial -> Medial
+    | MDef: nat -> Medial -> Medial -> Medial
+    | MCall: nat -> Medial.
 
   Definition Program := Medial.
 
+  Fixpoint inline (l: nat) (f p: Medial) :=
+    match p with
+    | MSeq a b => MSeq (inline l f a) (inline l f b)
+    | MCond c a b => MCond c (inline l f a) (inline l f b)
+    | MFunexp e a => MFunexp e (inline l f a)
+    | MDef l' f' p' =>
+      if (Nat.eq_dec l l')
+      then p
+      else MDef l' (inline l f f') (inline l f p')
+    | MCall l' =>
+      if (Nat.eq_dec l l')
+      then f
+      else p
+    | _ => p
+    end.
+
+  Fixpoint inlineAll (p: Medial) :=
+    match p with
+    | MSeq a b => MSeq (inlineAll a) (inlineAll b)
+    | MCond c a b => MCond c (inlineAll a) (inlineAll b)
+    | MFunexp e a => MFunexp e (inlineAll a)
+    | MDef l' f' p' => inline l' f' (inlineAll p')
+    | _ => p
+    end.
+
   Fixpoint meval (m: Medial) (st: State): option State :=
     let omap := fun {A B} (x: option A) (f: A -> option B) =>
       match x with | Some y => f y | _ => None end in
+
     match m with
     | MSkip => Some st
+
     | MSeq a b => omap (meval a st) (fun s => meval b s)
+
     | MAssign a =>
       match a with
       | MAVar x y =>
-        match (NatM.find y st) with
-        | (Some v) => Some (NatM.add x v st)
+        match (var y st) with
+        | Some v => Some (NatM.add x v (varS st), memS st, carryS st)
         | _ => None
         end
-      | MAConst x c => Some (NatM.add x (wordToN c) st)
+
+      | MAMem x y i =>
+        match (mem y i st) with
+        | Some v => Some (NatM.add x v (varS st), memS st, carryS st)
+        | _ => None
+        end
+
+      | MAConst x c => Some (NatM.add x (wordToN c) (varS st), memS st, carryS st)
       end
+
     | MOp o =>
       match o with
       | MIOpConst io a c =>
-        omap (NatM.find a st) (fun v =>
-          let res := evalIOp io (NToWord _ v) c in
-          Some (NatM.add a (wordToN res) st))
+        omap (var a st) (fun v =>
+          let (res, c') := evalIntOp io (NToWord _ v) c in
+          Some (NatM.add a (wordToN res) (varS st), memS st, c'))
 
       | MIOpReg io a b =>
-        omap (NatM.find a st) (fun va =>
-          omap (NatM.find b st) (fun vb =>
-            let res := evalIOp io (NToWord width va) (NToWord width vb) in
-            Some (NatM.add a (wordToN res) st)))
+        omap (var a st) (fun va =>
+          omap (var b st) (fun vb =>
+            let (res, c') := evalIntOp io (NToWord width va) (NToWord width vb) in
+            Some (NatM.add a (wordToN res) (varS st), memS st, c')))
+
+      | MCOpReg o a b =>
+        omap (var a st) (fun va =>
+          omap (var b st) (fun vb =>
+            let c := match (carryS st) with | Some b => b | _ => false end in
+            let (res, c') := evalCarryOp o (NToWord width va) (NToWord width vb) c in
+            Some (NatM.add a (wordToN res) (varS st), memS st, Some c')))
 
       | MDOpReg duo a b (Some x) =>
-        omap (NatM.find a st) (fun va =>
-          omap (NatM.find b st) (fun vb =>
+        omap (var a st) (fun va =>
+          omap (var b st) (fun vb =>
             let res := evalDualOp duo (NToWord width va) (NToWord width vb) in
             Some (NatM.add a (wordToN (fst res))
-                   (NatM.add x (wordToN (snd res)) st))))
+                   (NatM.add x (wordToN (snd res)) (varS st)), memS st, carryS st)))
 
       | MDOpReg duo a b None =>
-        omap (NatM.find a st) (fun va =>
-          omap (NatM.find b st) (fun vb =>
+        omap (var a st) (fun va =>
+          omap (var b st) (fun vb =>
             let res := evalDualOp duo (NToWord width va) (NToWord width vb) in
-            Some (NatM.add a (wordToN (fst res)) st)))
+            Some (NatM.add a (wordToN (fst res)) (varS st), memS st, carryS st)))
 
       | MOpRot ro a x =>
-        omap (NatM.find a st) (fun v =>
+        omap (var a st) (fun v =>
           let res := evalRotOp ro (NToWord width v) (proj1_sig x) in
-          Some (NatM.add a (wordToN res) st))
+          Some (NatM.add a (wordToN res) (varS st), memS st, carryS st))
       end
+
     | MCond c a b =>
       match c with
       | MC t x y =>
-        omap (NatM.find x st) (fun vx =>
-          omap (NatM.find y st) (fun vy =>
+        omap (var x st) (fun vx =>
+          omap (var y st) (fun vy =>
             if (evalTest t (NToWord width vx) (NToWord width vy))
             then meval a st
             else meval b st))
       end
+
     | MFunexp n a =>
       (fix fexp (m: nat) (f: State -> option State) (s: State) :=
         match m with
@@ -101,9 +157,11 @@ Module Medial (M: PseudoMachine) <: Language.
           end
         end
       ) n (meval a) st
+
+    | _ => None
     end.
 
-  Definition evaluatesTo := fun m st0 st1 => meval m st0 = Some st1.
+  Definition evaluatesTo := fun m st0 st1 => meval (inlineAll m) st0 = Some st1.
 
   (* world peace *)
 End Medial.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index 6bb619910..af5dd3891 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -1,11 +1,11 @@
-Require Import QhasmEvalCommon QhasmUtil.
+Require Import QhasmEvalCommon QhasmUtil State.
 Require Import Language.
 Require Import List.
 
 Module Type PseudoMachine.
   Parameter width: nat.
   Parameter vars: nat.
-  Parameter width_spec: ISize width.
+  Parameter width_spec: Width width.
 End PseudoMachine.
 
 Module Pseudo (M: PseudoMachine) <: Language.
@@ -14,104 +14,90 @@ Module Pseudo (M: PseudoMachine) <: Language.
   Definition const: Type := word width.
 
   (* Program Types *)
-  Definition State := list const.
+  Definition State := ((list const) * (list (list const)) * (option bool))%type.
+
+  Definition var (st: State)  := fst (fst st).
+  Definition mem (st: State)  := snd (fst st).
+  Definition carry (st: State) := snd st.
 
   Inductive Pseudo: nat -> nat -> Type :=
     | PVar: forall n, Index n -> Pseudo n 1
+    | PMem: forall n m, Index n -> Index m -> Pseudo n 1
     | PConst: forall n, const -> Pseudo n 1
 
     | PBin: forall n, IntOp -> Pseudo n 2 -> Pseudo n 1
     | PDual: forall n, DualOp -> Pseudo n 2 -> Pseudo n 2
+    | PCarry: forall n, CarryOp -> Pseudo n 2 -> Pseudo n 1
     | PShift: forall n, RotOp -> Index width -> Pseudo n 1 -> Pseudo n 1
 
+    | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m
+    | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n
+
     | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m
     | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b)
-
-    | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m
-    | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n.
+    | PCall: forall n m, Pseudo n m -> Pseudo n m.
 
   Hint Constructors Pseudo.
 
   Definition Program := Pseudo vars vars.
 
-  Definition applyBin (op: IntOp) (a b: word width): const :=
-    match op with
-    | IPlus => wplus a b
-    | IMinus => wminus a b
-    | IAnd => wand a b
-    | IXor => wxor a b
-    | IOr => wor a b
-    end.
-
-  Definition applyDual (op: DualOp) (a b: word width): list const :=
-    match op with
-    | Wmult =>
-      let wres := natToWord (width + width)
-        (N.to_nat ((wordToN a) * (wordToN b))) in
-      [split1 _ _ wres; split2 _ _ wres]
-    end.
-
-  Definition applyShift (op: RotOp) (v: const) (n: Index width): const.
-    refine match op with
-    | Shl => convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _
-    | Shr => convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _
-    end; abstract (
-      unfold const;
-      destruct n; simpl;
-      replace (width - x + x) with width;
-      replace (x + (width - x)) with width;
-      intuition ).
-  Defined.
-
   Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State :=
-    let option_map' := fun {A B: Type} (x: option A) (f: A -> option B) =>
-      match x with
-      | Some x' =>
-        match (f x') with
-        | Some res => Some res
-        | None => None
-        end
-      | _ => None
-      end in
-
     match prog with
-    | PVar n i => option_map' (nth_error st i) (fun x => Some [x])
-    | PConst n c => Some ([c])
+    | PVar n i =>
+      omap (nth_error (var st) i) (fun x =>
+        Some ([x], mem st, carry st))
+
+    | PMem n m v i =>
+      omap (nth_error (mem st) v) (fun vec =>
+        omap (nth_error vec i) (fun x =>
+          Some ([x], mem st, carry st)))
+
+    | PConst n c => Some ([c], mem st, carry st)
 
     | PBin n o p =>
-      option_map' (pseudoEval p st) (fun sp =>
+      omap (pseudoEval p st) (fun sp =>
         match sp with
-        | [wa; wb] => Some [applyBin o wa wb]
+        | ([wa; wb], m', _) =>
+          let (v, c) := evalIntOp o wa wb in Some ([v], m', c)
+        | _ => None
+        end)
+
+    | PCarry n o p =>
+      omap (pseudoEval p st) (fun sp =>
+        match sp with
+        | ([wa; wb], m', Some c) =>
+          let (v, c') := evalCarryOp o wa wb c in Some ([v], m', Some c')
         | _ => None
         end)
 
     | PDual n o p =>
-      option_map' (pseudoEval p st) (fun sp =>
+      omap (pseudoEval p st) (fun sp =>
         match sp with
-        | [wa; wb] => Some (applyDual o wa wb)
+        | ([wa; wb], m', co) =>
+          let (low, high) := evalDualOp o wa wb in Some ([low; high], m', co)
         | _ => None
         end)
 
     | PShift n o a x =>
-      option_map' (pseudoEval x st) (fun sx =>
+      omap (pseudoEval x st) (fun sx =>
         match sx with
-        | [wx] => Some [applyShift o wx a]
+        | ([wx], m', co) => Some ([evalRotOp o wx a], m', co)
         | _ => None
         end)
 
     | PLet n k m f g =>
-      option_map' (pseudoEval f st) (fun sf =>
-        option_map' (pseudoEval g (st ++ sf))
+      omap (pseudoEval f st) (fun sf =>
+        omap (pseudoEval g ((var st) ++ (var sf), mem sf, carry sf))
           (fun sg => Some sg))
 
     | PComb n a b f g =>
-      option_map' (pseudoEval f st) (fun sf =>
-        option_map' (pseudoEval g st) (fun sg =>
-          Some (sf ++ sg)))
+      omap (pseudoEval f st) (fun sf =>
+        omap (pseudoEval g st) (fun sg =>
+          Some ((var sf) ++ (var sg), mem sg, carry sg)))
 
     | PIf n m t i0 i1 l r =>
-      option_map' (nth_error st i0) (fun v0 =>
-        option_map' (nth_error st i1) (fun v1 =>
+      omap (nth_error (var st) i0) (fun v0 =>
+        omap (nth_error (var st) i1) (fun v1 =>
           if (evalTest t v0 v1)
           then pseudoEval l st
           else pseudoEval r st ))
@@ -121,9 +107,11 @@ Module Pseudo (M: PseudoMachine) <: Language.
         match e' with
         | O => Some st'
         | S e'' =>
-          option_map' (pseudoEval p st') (fun st'' =>
+          omap (pseudoEval p st') (fun st'' =>
             funexpseudo e'' st'')
         end) e st
+
+    | PCall n m p => pseudoEval p st
     end.
 
   Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st').
@@ -134,14 +122,14 @@ End Pseudo.
 Module PseudoUnary32 <: PseudoMachine.
   Definition width := 32.
   Definition vars := 1.
-  Definition width_spec := I32.
+  Definition width_spec := W32.
   Definition const: Type := word width.
 End PseudoUnary32.
 
 Module PseudoUnary64 <: PseudoMachine.
   Definition width := 64.
   Definition vars := 1.
-  Definition width_spec := I64.
+  Definition width_spec := W64.
   Definition const: Type := word width.
 End PseudoUnary64.
  
\ No newline at end of file
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
index c911b00ee..193114d14 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -7,7 +7,6 @@ Module Qhasm <: Language.
   Import State.
 
   (* A constant upper-bound on the number of operations we run *)
-  Definition maxOps: nat := 1000.
   Definition State := State.
 
   (* Program Types *)