Assembly converted except String and Gallina conversions

5 files changed, 78 insertions, 94 deletions

diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v
index 16638af78..4b66c8128 100644
--- a/src/Assembly/AlmostConversion.v
+++ b/src/Assembly/AlmostConversion.v
@@ -16,36 +16,31 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
     | 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] ++
+      let tru := N.to_nat (N.shiftl 1 label0) in
+      let finish := S tru in
+      [QJmp c tru] ++
       (almostToQhasm' b label1) ++
+      [QJmp TestTrue finish] ++
+      [QLabel tru] ++
+      (almostToQhasm' a 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 ;
+      let test := S start in
+      [ QJmp TestTrue test ;
         QLabel start ] ++
         (almostToQhasm' a label1) ++
-      [ QJmp c start;
-        QLabel finish ]
+      [ QLabel test;
+        QJmp c start ]
     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.
+  Lemma convert_spec:  forall a a' b b' prog prog',
+    convertProgram prog = Some prog' ->
+    convertState a = Some a' -> convertState b = Some b' ->
+    Qhasm.evaluatesTo prog' a b <-> AlmostQhasm.evaluatesTo prog a' b'.
   Admitted.
 
 End AlmostConversion.
diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
index 0ec47fc37..7e18edfe0 100644
--- a/src/Assembly/AlmostQhasm.v
+++ b/src/Assembly/AlmostQhasm.v
@@ -24,35 +24,36 @@ Module AlmostQhasm <: Language.
 
   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 => evalAssignment a state
-    | AOp a => 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.
+  Inductive AlmostEval: AlmostProgram -> State -> State -> Prop :=
+    | AESkip: forall s, AlmostEval ASkip s s
+    | AESeq: forall p p' s s' s'',
+        AlmostEval p s s'
+      -> AlmostEval p' s' s''
+      -> AlmostEval (ASeq p p') s s''
+    | AEAssign a: forall s s',
+        evalAssignment a s = Some s'
+      -> AlmostEval (AAssign a) s s'
+    | AEOp: forall s s' a,
+        evalOperation a s = Some s'
+      -> AlmostEval (AOp a) s s'
+    | AECondFalse: forall c a b s s',
+        evalCond c s = Some false
+      -> AlmostEval b s s'
+      -> AlmostEval (ACond c a b) s s'
+    | AECondTrue: forall c a b s s',
+        evalCond c s = Some true
+      -> AlmostEval a s s'
+      -> AlmostEval (ACond c a b) s s'
+    | AEWhileRun: forall c a s s' s'',
+        evalCond c s = Some true
+      -> AlmostEval a s s'
+      -> AlmostEval (AWhile c a) s' s''
+      -> AlmostEval (AWhile c a) s s''
+    | AEWhileSkip: forall c a s,
+        evalCond c s = Some false
+      -> AlmostEval (AWhile c a) s s.
+
+  Definition evaluatesTo := AlmostEval.
 
   (* world peace *)
 End AlmostQhasm.
diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v
index eb378d437..9811d5f43 100644
--- a/src/Assembly/Conversion.v
+++ b/src/Assembly/Conversion.v
@@ -6,14 +6,9 @@ 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.
+  Axiom convert_spec: forall a a' b b' prog prog',
+    convertProgram prog = Some prog' ->
+    convertState a = Some a' -> convertState b = Some b' ->
+    B.evaluatesTo prog' a b <-> A.evaluatesTo prog a' b'.
 
 End Conversion.
diff --git a/src/Assembly/Language.v b/src/Assembly/Language.v
index d04393b51..35338b48b 100644
--- a/src/Assembly/Language.v
+++ b/src/Assembly/Language.v
@@ -3,5 +3,5 @@ Module Type Language.
   Parameter Program: Type.
   Parameter State: Type.
 
-  Parameter eval: Program -> State -> option State.
+  Parameter evaluatesTo: Program -> State -> State -> Prop.
 End Language.
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
index 00961a49a..c911b00ee 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -37,43 +37,36 @@ Module Qhasm <: Language.
   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 => (Some state, None)
-          | QJmp c l =>
-            if (evalCond c state)
-            then (Some state, Some l)
-            else (Some state, None)
-          end
-        in
-          match jmp with
-          | None =>
-            if (Nat.eq_dec loc maxLoc)
-            then nextState
-            else match nextState with
-              | Some st' => eval' prog st' (S loc) h labelMap maxLoc
-              | _ => None
-              end
-          | Some nextLoc =>
-            match nextState with
-            | Some st' => eval' prog st' nextLoc h labelMap maxLoc
-            | _ => None
-            end
-          end
-      | None => None
-      end
-    | O => None
-    end.
+  Inductive QhasmEval: nat -> Program -> LabelMap -> State -> State -> Prop :=
+    | QEOver: forall p n m s, (n > (length p))%nat -> QhasmEval n p m s s
+    | QEZero: forall p s m, QhasmEval O p m s s
+    | QEAssign: forall n p m a s s' s'',
+        (nth_error p n) = Some (QAssign a)
+      -> evalAssignment a s = Some s'
+      -> QhasmEval (S n) p m s' s''
+      -> QhasmEval n p m s s''
+    | QEOp: forall n p m a s s' s'',
+        (nth_error p n) = Some (QOp a)
+      -> evalOperation a s = Some s'
+      -> QhasmEval (S n) p m s' s''
+      -> QhasmEval n p m s s''
+    | QEJmpTrue: forall (n loc next: nat) p m c l s s',
+        (nth_error p n) = Some (QJmp c l)
+      -> evalCond c s = Some true
+      -> NatM.find l m = Some loc
+      -> QhasmEval loc p m s s'
+      -> QhasmEval n p m s s'
+    | QEJmpFalse: forall (n loc next: nat) p m c l s s',
+        (nth_error p n) = Some (QJmp c l)
+      -> evalCond c s = Some false
+      -> QhasmEval (S n) p m s s'
+      -> QhasmEval n p m s s'
+    | QELabel: forall n p m l s s',
+        (nth_error p n) = Some (QLabel l)
+      -> QhasmEval (S n) p m s s'
+      -> QhasmEval n p m s s'.
 
-  Definition eval (prog: Program) (state: State): option State :=
-    eval' prog state O maxOps (getLabelMap prog) ((length prog) - 1).
+  Definition evaluatesTo := fun p => QhasmEval O p (getLabelMap p).
 
   (* world peace *)
 End Qhasm.