Full automation for relevant parts of pseudo conversion except lets

4 files changed, 87 insertions, 48 deletions

diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
index 164fc8866..af311963d 100644
--- a/src/Assembly/Pseudize.v
+++ b/src/Assembly/Pseudize.v
@@ -1,5 +1,5 @@
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NArith NPeano List Sumbool.
+Require Import NArith NPeano List Sumbool Compare_dec.
 Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State.
 Require Export Wordize Vectorize.
 
@@ -9,22 +9,35 @@ Module Conversion.
   Hint Unfold setList getList getVar setCarry setCarryOpt getCarry
        getMem 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).
+  Lemma pseudo_var: forall {w s n} b k x v m c,
+      (k < n)%nat
+    -> nth_error x k = Some v
+    -> pseudoEval (@PVar w s n b (indexize k)) (x, m, c) = Some ([v], m, c).
   Proof.
-    intros; simpl; autounfold; simpl.
-    destruct (nth_error x k); simpl; try inversion H; intuition.
+    intros; autounfold; simpl; unfold indexize.
+    destruct (le_dec n 0); simpl. {
+      replace k with 0 in * by omega; autounfold; simpl in *.
+      rewrite H0; simpl; intuition.
+    }
+
+    replace (k mod n) with k by admit. (* TODO (rsloan): find lemma name *)
+
+    autounfold; simpl.
+    destruct (nth_error x k); simpl; try inversion H0; intuition.
   Qed.
 
-  Lemma pseudo_mem: forall {w s} n v m c x name len index p0 p1,
+  Lemma pseudo_mem: forall {w s} n v m c x name len index,
       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).
+    -> pseudoEval (@PMem w s n len (indexize name) (indexize index)) (x, m, c) = Some ([v], m, c).
   Proof.
     intros; autounfold; simpl.
-    unfold getMem; simpl.
-    rewrite H; autounfold; simpl.
-    rewrite NToWord_wordToN; intuition.
+    unfold indexize;
+      destruct (le_dec n 0), (le_dec len 0);
+      try replace n with 0 in * by intuition;
+      try replace len with 0 in * by intuition;
+      autounfold; simpl in *; rewrite H;
+      autounfold; simpl; rewrite NToWord_wordToN;
+      intuition.
   Qed.
 
   Lemma pseudo_const: forall {w s n} x v m c,
@@ -100,14 +113,13 @@ Module Conversion.
     rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition.
   Qed.
 
-  Lemma pseudo_dual:
-    forall {w s n} (p: @Pseudo w s n 1) x out0 out1 m0 m1 c0 c1 k,
+  Lemma pseudo_mult:
+    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 (PDual n Mult p) (x, m0, c0) =
-      Some ([x ^* y; (highBits (n/2) x) ^* (highBits (n/2) y)], m1, c1).
+      Some ([out0 ^* out1; multHigh out0 out1], m1, c1).
   Proof.
-    intros; simpl; rewrite H; autounfold; simpl.
-    rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition.
+    intros; simpl; rewrite H; autounfold; simpl; intuition.
   Qed.
 
   Lemma pseudo_comb:
@@ -137,14 +149,24 @@ Module Conversion.
     apply (pseudo_comb p0 p1 input _ _ m0 m1 m2 c0 c1 c2); intuition.
   Qed.
 
+  Lemma pseudo_let:
+    forall {w s n k m} (p0: @Pseudo w s n k) (p1: @Pseudo w s (n + k) m)
+      input out0 out1 m0 m1 m2 c0 c1 c2,
+      pseudoEval p0 (input, m0, c0) = Some (out0, m1, c1)
+    -> pseudoEval p1 (input ++ out0, m1, c1) = Some (out1, m2, c2)
+    -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) =
+        Some (out1, m2, c2).
+  Proof.
+    intros; autounfold; simpl.
+    rewrite H; autounfold; simpl.
+    rewrite H0; autounfold; simpl; intuition.
+  Qed.
+
   Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := 
     {p: @Pseudo w s n m | forall x: (list (word w)),
       List.length x = n -> exists m' c',
       pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}.
 
-  Definition example (v: list (word 32)) : list (word 32) :=
-      [(natToWord _ 1) ^& (nth 0 v (wzero _))].
-
   Ltac autodestruct :=
     repeat match goal with
     | [H: context[Datatypes.length (cons _ _)] |- _] => simpl in H
@@ -159,23 +181,34 @@ Module Conversion.
       end
     end.
 
-  Definition convert_example: @pseudeq 32 W32 1 1 example.
-    repeat eexists; unfold example; autounfold; autodestruct.
-
-    eapply pseudo_and.
-    eapply pseudo_cons.
-    eapply pseudo_const.
-    eapply pseudo_var.
+  Ltac pseudo_step :=
+    match goal with
+    | [ |- pseudoEval ?p _ = Some ([?x ^& ?y], _, _) ] =>
+      is_evar p; eapply pseudo_and
+    | [ |- pseudoEval ?p _ = Some ([?x ^+ ?y], _, _) ] =>
+      is_evar p; eapply pseudo_plus
+    | [ |- pseudoEval ?p _ = Some (cons ?x (cons _ _), _, _) ] =>
+      is_evar p; eapply pseudo_cons; try reflexivity
+    | [ |- pseudoEval ?p _ = Some ([natToWord _ ?x], _, _)%p ] =>
+      is_evar p; eapply pseudo_const
+    | [ |- @pseudoEval ?n _ _ _ ?P (?lst, _, _) =
+            Some ([nth ?i ?lst _], _, _)%p ] =>
+      eapply (pseudo_var None); simpl; intuition
+    end.
 
-    (* leftovers *)
+  Ltac pseudo_solve :=
+    repeat eexists;
+    autounfold;
+    autodestruct;
+    repeat pseudo_step.
 
-    instantiate (1 := 0); simpl; intuition.
-    reflexivity.
+  Definition convert_example: @pseudeq 32 W32 1 1 (fun v =>
+      let a := natToWord _ 1 in
+      let b := nth 0 v (wzero _) in
+      [a ^& b]).
 
-    Grab Existential Variables.
+    cbv zeta; pseudo_solve.
 
-    abstract (simpl; intuition).
-    exact None.
   Defined.
 
   Eval simpl in (proj1_sig convert_example).
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index 6102b9642..48e642151 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -1,6 +1,6 @@
 Require Import QhasmUtil QhasmCommon QhasmEvalCommon QhasmUtil State.
 Require Import Language.
-Require Import List.
+Require Import List Compare_dec.
 
 Module Pseudo <: Language.
   Import EvalUtil ListState.
@@ -113,18 +113,21 @@ Module Pseudo <: Language.
   Delimit Scope pseudo_notations with p.
   Local Open Scope pseudo_notations.
 
-  Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n.
-    intros; exists (x mod n);
-      abstract (pose proof (mod_bound_pos x n); omega).
+  Definition indexize {n: nat} (x: nat): Index n.
+    intros; destruct (le_dec n 0).
+
+    - exists 0; abstract intuition.
+    - exists (x mod n); abstract (
+        pose proof (mod_bound_pos x n); omega).
   Defined.
 
-  Notation "% A" := (PVar _ (Some false) (indexize _ _ A))
+  Notation "% A" := (PVar _ (Some false) (indexize A))
     (at level 20, right associativity) : pseudo_notations.
 
-  Notation "$ A" := (PVar _ (Some true) (indexize _ _ A))
+  Notation "$ A" := (PVar _ (Some true) (indexize A))
     (at level 20, right associativity) : pseudo_notations.
 
-  Notation "A :[ B ]:" :=  (PMem _ _ (indexize _ _ A) (indexize _ _ B))
+  Notation "A :[ B ]:" :=  (PMem _ _ (indexize A) (indexize B))
     (at level 20, right associativity) : pseudo_notations.
 
   Notation "# A" := (PConst _ (natToWord _ A))
@@ -145,17 +148,17 @@ Module Pseudo <: Language.
   Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B))
     (at level 45, right associativity) : pseudo_notations.
 
-  Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A)
+  Notation "A :>>: B" := (PShift _ Shr (indexize B) A)
     (at level 60, right associativity) : pseudo_notations.
 
-  Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A)
+  Notation "A :<<: B" := (PShift _ Shl (indexize B) A)
     (at level 60, right associativity) : pseudo_notations.
 
   Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B))
     (at level 55, right associativity) : pseudo_notations.
 
   Notation "O :( A , B ): :?: L ::: R" :=
-    (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R)
+    (PIf _ _ O (indexize A) (indexize B) L R)
     (at level 70, right associativity) : pseudo_notations.
 
   Notation "F :**: e" :=
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 654f109f3..ccec401d2 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -4,7 +4,7 @@ Require Export Bedrock.Word.
 (* Utilities *)
 Definition Label := nat.
 
-Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
+Definition Index (limit: nat) := {x: nat | (x <= (pred limit))%nat}.
 Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
 
 Inductive Either A B :=
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index e7e9b0c7d..dbd46b1b4 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -50,13 +50,16 @@ Module EvalUtil.
 
   Definition highBits {n} (m: nat) (x: word n) := snd (break m x).
 
-  Definition evalDualOp {n} (duo: DualOp) (x y: word n): word n * word n.
-    refine match duo with
-    | Mult => (x ^* y,
-        @extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y)))
-    end; abstract omega.
+  Definition multHigh {n} (x y: word n): word n.
+    refine (@extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y)));
+      abstract omega.
   Defined.
 
+  Definition evalDualOp {n} (duo: DualOp) (x y: word n) :=
+    match duo with
+    | Mult => (x ^* y, multHigh x y)
+    end.
+
   Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
     match ro with
     | Shl => NToWord b (N.shiftl_nat (wordToN x) n)