1 files changed, 65 insertions, 26 deletions

diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
index b5d1a2b95..af234fdb3 100644
--- a/src/Assembly/Pseudize.v
+++ b/src/Assembly/Pseudize.v
@@ -1,39 +1,78 @@
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NArith List.
-Require Import Pseudo State Wordize.
+Require Import NArith NPeano List Sumbool.
+Require Import QhasmCommon QhasmUtil Pseudo State Wordize.
 
 Module Conversion.
   Import Pseudo ListNotations StateCommon.
 
-  Definition run {n m w s} (prog: @Pseudo w s n m) (inList: list (word w)) : list (word w) :=  
-    match (pseudoEval prog (inList, TripleM.empty N, None)) with
-    | Some (outList, _, _) => outList
-    | _ => []
-    end.
-
-  Lemma pseudo_plus: forall {w s n} (p0 p1: @Pseudo w s n 1) x out0 out1 b,
-      (b <= Npow2 w)%N
-    -> ((&out0)%w < b)%N
-    -> ((&out1)%w < (Npow2 w - b))%N
-    -> run p0 x = [out0]
-    -> run p1 x = [out1]
-    -> run (p0 :+: p1)%p x = [out0 ^+ out1].
+  Hint Unfold ListState.setList ListState.getList ListState.getVar
+       ListState.setCarry ListState.setCarryOpt ListState.getCarry
+       ListState.getMem ListState.setMem overflows.
+
+  Lemma pseudo_var: forall {w s n} x k v b p m c,
+      nth_error x k = Some v
+    -> pseudoEval (@PVar w s n b (exist _ k p)) (x, m, c) = Some ([v], m, c).
+  Proof.
+    intros; simpl; autounfold; simpl.
+    destruct (nth_error x k); simpl; try inversion H; intuition.
+  Qed.
+
+  Lemma pseudo_mem: forall {w s} n v m c x name len index p0 p1,
+      TripleM.find (w, name mod n, index mod len)%nat m = Some (@wordToN w v)
+    -> pseudoEval (@PMem w s n len (indexize _ p0 name) (indexize _ p1 index)) (x, m, c) = Some ([v], m, c).
+  Proof.
+    intros; autounfold; simpl.
+    unfold ListState.getMem; simpl.
+    rewrite H; autounfold; simpl.
+    rewrite NToWord_wordToN; intuition.
+  Qed.
+
+  Lemma pseudo_const: forall {w s n} x v m c,
+      pseudoEval (@PConst w s n v) (x, m, c) = Some ([v], m, c).
+  Proof. intros; simpl; intuition. Qed.
+
+  Lemma pseudo_plus:
+    forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1,
+      pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
+    -> pseudoEval (PBin n Add p) (x, m0, c0) =
+        Some ([out0 ^+ out1], m1,
+          Some (proj1_sig (bool_of_sumbool (overflows out0 out1)))).
   Proof.
-    intros; unfold run in *; simpl.
-    destruct (pseudoEval p0 _) as [r0|], (pseudoEval p1 _) as [r1|].
-    destruct r0 as [r0 rc0], r1 as [r1 rc1].
-    destruct r0 as [r0 rm0], r1 as [r1 rm1].
+    intros; simpl; rewrite H; simpl.
 
-    - subst; simpl.
-      destruct ((& out0)%w + (& out1)%w ?= Npow2 w)%N; simpl;
-        rewrite (wordize_plus out0 out1 b); try assumption;
-        rewrite NToWord_wordToN; intuition.
+    pose proof (wordize_plus out0 out1).
+    destruct (overflows out0 out1); autounfold; simpl; try rewrite H0;
+      try rewrite <- (@Npow2_ignore w (out0 ^+ out1));
+      try rewrite NToWord_wordToN; intuition.
+  Qed.
 
-    - inversion H3.
+  Lemma pseudo_plus:
+    forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1 op,
+      op ⋄ Add
+    → pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
+    → pseudoEval (PBin n op p) (x, m0, c0) =
+        Some ([out0 ^+ out1], m1,
+          Some (proj1_sig (bool_of_sumbool (overflows out0 out1)))).
+  Proof.
+    intros; simpl; rewrite H; simpl.
 
-    - inversion H2.
+    pose proof (wordize_plus out0 out1).
+    destruct (overflows out0 out1); autounfold; simpl; try rewrite H0;
+      try rewrite <- (@Npow2_ignore w (out0 ^+ out1));
+      try rewrite NToWord_wordToN; intuition.
+  Qed.
 
-    - inversion H2.
+  Lemma pseudo_comb:
+    forall {w s n a b} (p0: @Pseudo w s n a) (p1: @Pseudo w s n b)
+      input out0 out1 m0 m1 m2 c0 c1 c2,
+       pseudoEval p0 (input, m0, c0) = Some (out0, m1, c1)
+    -> pseudoEval p1 (input, m1, c1) = Some (out1, m2, c2)
+    -> pseudoEval (@PComb w s n _ _ p0 p1) (input, m0, c0) =
+        Some (out0 ++ out1, m2, c2).
+  Proof.
+    intros; autounfold; simpl.
+    rewrite H; autounfold; simpl.
+    rewrite H0; autounfold; simpl; intuition.
   Qed.
 
   Program Definition ex0: Program Unary32 := ($0 :-: $0)%p.