Pseudize Lemmas for Dual Operations

5 files changed, 168 insertions, 50 deletions

diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 9299d9d52..9d6c4c9da 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -22,21 +22,19 @@ Module Pipeline.
 End Pipeline.
 
 Module PipelineExample.
-  Import Pipeline ListNotations.
+  Import Pipeline ListNotations StateCommon EvalUtil ListState.
 
   Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40).
   Local Notation "$$ v" := (natToWord _ v) (at level 40).
 
   Definition example: @pseudeq 32 W32 1 1 (fun v =>
-      Let_In ($$ 1) (fun a =>
-        Let_In (v[[0]]) (fun b => [
-          a ^& b
-      ]))).
-
+      plet a := $$ 1 in
+      plet b := v[[0]] in
+      plet c := multHigh a b in
+      plet d := a ^* b in
+      [b ^& d]).
     pseudo_solve.
   Defined.
 
-  Definition exStr := Pipeline.toString (proj1_sig example).
-
-  (* Eval vm_compute in exStr. *)
+  Eval vm_compute in (Pipeline.toString (proj1_sig example)).
 End PipelineExample.
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
index fb3a8b81b..c167dd6a1 100644
--- a/src/Assembly/Pseudize.v
+++ b/src/Assembly/Pseudize.v
@@ -7,8 +7,6 @@ Import Pseudo ListNotations StateCommon EvalUtil ListState.
 
 Section Conversion.
 
-  Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
-
   Hint Unfold setList getList getVar setCarry setCarryOpt getCarry
        getMem setMem overflows.
 
@@ -130,15 +128,6 @@ Section Conversion.
     rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition.
   Qed.
 
-  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 ([out0 ^* out1; multHigh out0 out1], m1, c1).
-  Proof.
-    intros; simpl; rewrite H; autounfold; simpl; intuition.
-  Qed.
-
   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,
@@ -210,6 +199,54 @@ Section Conversion.
     eapply pseudo_let; try eassumption.
   Qed.
 
+  Lemma pseudo_mult_single:
+    forall {w s n m} (p0: @Pseudo w s n 2)
+                (p1: @Pseudo w s (n + 2) m)
+        out0 out1 f x m0 m1 m2 c0 c1 c2,
+      pseudoEval p0 (x, m0, c0) = Some ([out0; out1], m1, c1)
+    -> pseudoEval p1 (x ++ [out0 ^* out1; multHigh out0 out1], m1, c1) =
+        Some (f (nth n (x ++ [out0 ^* out1; multHigh out0 out1]) (wzero _)), m2, c2)
+    -> pseudoEval (@PLet w s n 2 m (PDual n Mult p0) p1) (x, m0, c0) =
+      Some (Let_In (out0 ^* out1) f, m2, c2).
+  Proof.
+    intros; simpl; rewrite H; autounfold; simpl; rewrite H0; simpl; intuition.
+    replace (nth n (x ++ _) _) with (out0 ^* out1); simpl; intuition.
+    assert (Datatypes.length x = n) as L by (
+      eapply eval_in_length; eassumption).
+    rewrite app_nth2; try rewrite L; intuition.
+    replace (n - n) with 0 by omega.
+    simpl; intuition.
+  Qed.
+
+  Lemma pseudo_mult_dual:
+    forall {w s n m} (p0: @Pseudo w s n 2)
+                (p1: @Pseudo w s (n + 2) m)
+        out0 out1 f x m0 m1 m2 c0 c1 c2,
+      pseudoEval p0 (x, m0, c0) = Some ([out0; out1], m1, c1)
+    -> pseudoEval p1 (x ++ [out0 ^* out1; multHigh out0 out1], m1, c1) =
+      Some (f (nth n (x ++ [out0 ^* out1; multHigh out0 out1]) (wzero _))
+              (nth (S n) (x ++ [out0 ^* out1; multHigh out0 out1]) (wzero _)),
+            m2, c2)
+    -> pseudoEval (@PLet w s n 2 m (PDual n Mult p0) p1) (x, m0, c0) =
+      Some (Let_In (multHigh out0 out1) (fun x =>
+            Let_In (out0 ^* out1) (fun y =>
+            f y x)), m2, c2).
+  Proof.
+    intros; simpl; rewrite H; autounfold; simpl; rewrite H0; simpl; intuition.
+    assert (Datatypes.length x = n) as L by (eapply eval_in_length; eassumption).
+
+    replace (nth n (x ++ _) _) with (out0 ^* out1); simpl; intuition.
+    replace (nth (S n) (x ++ _) _) with (multHigh out0 out1); simpl; intuition.
+
+    - rewrite app_nth2; try rewrite L; intuition.
+      replace (S n - n) with 1 by omega.
+      simpl; intuition.
+
+    - rewrite app_nth2; try rewrite L; intuition.
+      replace (n - n) with 0 by omega.
+      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',
@@ -232,21 +269,34 @@ Ltac autodestruct :=
 
 Ltac pseudo_step :=
   match goal with
-  | [ |- pseudoEval ?p _ = Some ((Let_In ?a ?f), _, _) ] =>
-    is_evar p;
-    match (type of a) with
-    | word _ => eapply pseudo_let_var
-    | list _ => eapply pseudo_let_list
-    end
+  | [ |- pseudoEval ?p _ = Some ((
+            Let_In (multHigh ?a ?b) (fun x =>
+            Let_In (?a ^* ?b) (fun y => _))), _, _) ] =>
+    is_evar p; eapply pseudo_mult_dual
+
+  | [ |- pseudoEval ?p _ = Some (Let_In (?a ^* ?b) _, _, _) ] =>
+    is_evar p; eapply pseudo_mult_single
 
   | [ |- 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 ?p _ = Some ((Let_In ?a ?f), _, _) ] =>
+    is_evar p;
+    match (type of a) with
+    | list _ => eapply pseudo_let_list
+    | word _ => eapply pseudo_let_var
+    | (_ * _)%type => rewrite detuple_let
+    end
+
   | [ |- @pseudoEval ?n _ _ _ ?P _ =
         Some ([nth ?i ?lst _], _, _)%p ] =>
     eapply (pseudo_var None i); simpl; intuition
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 9c3fda2a0..9959e5319 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -16,6 +16,8 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
     Definition FMap := NatM.t (AlmostProgram * (list (Mapping w))).
     Definition fempty := NatM.empty (AlmostProgram * (list (Mapping w))).
 
+    Transparent MMap FMap.
+
     Definition getStart {n m} (prog: @Pseudo w s n m) :=
       let ns := (fix getStart' {n' m'} (prog': @Pseudo w s n' m') :=
         match prog' with
@@ -54,48 +56,60 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
       let stack' := stack s in
       let const' := constant s in
 
-      let G := fun (k: nat) =>
-        match (NatM.find k M) with
+      let get := fun (k: nat) (default: nat -> Mapping w) (M': MMap) =>
+        match (NatM.find k M') with
         | Some v => v
-        | _ => rM k (* TODO: more intelligent defaults *)
+        | _ => default k
         end in
 
-      let madd := fun (k: nat) (f: nat -> Mapping w) =>
-        NatM.add k (f k) in
+      let madd := fun (a: nat) (default: nat -> Mapping w) (M': MMap) =>
+        NatM.add a (get a default M') M' in
 
       let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping w)) =>
         NatM.add k (f, r) in
 
+      let updateM := (
+        fix updateM' (k: nat) (mtmp: list (Mapping w)) (Miter: MMap) : MMap :=
+        match mtmp with
+        | [] => Miter
+        | a :: mtmp' => NatM.add k a (updateM' (S k) mtmp' Miter)
+        end) in
+
       match prog with
-      | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM M, F)
-      | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM M, F)
-      | PVar n None i => Some (ASkip, [G i], M, F) 
+      | PVar n (Some true) i =>
+        Some (ASkip, [get i rM M], madd i rM M, F)
+
+      | PVar n (Some false) i =>
+        Some (ASkip, [get i sM M], madd i sM M, F)
+
+      | PVar n None i => (* assign to register by default *)
+        Some (ASkip, [get i rM M], madd i rM M, F) 
 
       | PConst n c =>
         Some (AAssign (AConstInt (reg' start) (const' c)),
-                       [rM start], madd start rM M, F)
+              [get start rM M], madd start rM M, F)
 
       | PMem n m v i =>
         Some (AAssign (ARegMem (reg' start) (mem s v) i),
-                       [rM start], madd start rM M, F)
+              [get start rM M], madd start rM M, F)
 
       | PBin n o p =>
         match (convertProgram' p start M F) with
         | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
             Some (ASeq p' (AOp (IOpReg o (reg' a) (reg' b))),
-                [rM a], madd a rM (madd b rM M'), F')
+                [get a rM M'], madd a rM (madd b rM M'), F')
 
         | Some (p', [regM (reg _ _ a); constM c], M', F') =>
             Some (ASeq p' (AOp (IOpConst o (reg' a) c)),
-                [rM a], madd a rM M', F')
+                [get a rM M'], madd a rM M', F')
 
         | Some (p', [regM (reg _ _ a); memM _ b i], M', F') =>
             Some (ASeq p' (AOp (IOpMem o (reg' a) b i)),
-                [rM a], madd a rM M', F')
+                [get a rM M'], madd a rM M', F')
 
         | Some (p', [regM (reg _ _ a); stackM (stack _ _ b)], M', F') =>
             Some (ASeq p' (AOp (IOpStack o (reg' a) (stack' b))),
-                [rM a], madd a rM (madd b sM M'), F')
+                [get a rM M'], madd a rM (madd b sM M'), F')
 
         | _ => None
         end
@@ -104,7 +118,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
         match (convertProgram' p start M F) with
         | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
             Some (ASeq p' (AOp (COp o (reg' a) (reg' b))),
-                [rM a], madd a rM (madd b rM M'), F')
+                [get a rM M'], madd a rM (madd b rM M'), F')
 
         | _ => None
         end
@@ -113,7 +127,8 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
         match (convertProgram' p (S start) M F) with
         | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
             Some (ASeq p' (AOp (DOp o (reg' a) (reg' b) (Some (reg' start)))),
-                [rM a; rM start], madd a rM (madd b rM (madd start rM M')), F')
+                  [get a rM M'; get start rM M'],
+                  madd a rM (madd b rM (madd start rM M')), F')
 
         | _ => None
         end
@@ -122,7 +137,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
         match (convertProgram' p start M F) with
         | Some (p', [regM (reg _ _ a)], M', F') =>
             Some (ASeq p' (AOp (ROp o (reg' a) x)),
-                [rM a], madd a rM M', F')
+                [get a rM M'], madd a rM M', F')
 
         | _ => None
         end
@@ -131,10 +146,15 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
         match (convertProgram' f start M F) with
         | None => None
         | Some (fp, fm, M', F') =>
-            match (convertProgram' g (start + (length fm)) M' F') with
-            | None => None
-            | Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'')
-            end
+
+          (* Make sure all of the new variables are bound to their results *)
+          let M'' := updateM start fm M' in
+
+          (* Then convert the second program *)
+          match (convertProgram' g (start + (length fm)) M'' F') with
+          | None => None
+          | Some (gp, gm, M''', F'') => Some (ASeq fp gp, gm, M''', F'')
+          end
         end
 
       | PComb n a b f g => 
@@ -158,7 +178,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
 
             if (list_eq_dec mapping_dec lr rr)
             then
-                match (G (proj1_sig i0), G (proj1_sig i1)) with
+                match (get (proj1_sig i0) rM M, get (proj1_sig i1) rM M) with
                 | (regM r0, regM r1) => Some (ACond (CReg _ o r0 r1) lp rp, lr, M', F')
                 | (regM r, constM c) => Some (ACond (CConst _ o r c) lp rp, lr, M', F')
                 | _ => None
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 66a83cfa3..9f3908a26 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -127,7 +127,13 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       end.
  
     Definition operationToString (op: Operation): option string :=
-      let f := fun x => if (Nat.eq_dec x 32) then "32" else "64" in
+      let f := fun x => (
+        if (Nat.eq_dec x 32)
+        then "32"
+        else if (Nat.eq_dec x 64)
+          then "64"
+          else "128") in
+
       match op with
       | IOpConst n o r c => 
         r ++ " " ++ o ++ "= " ++ c
@@ -140,7 +146,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       | DOp n o a b x =>
         match x with
         | Some r =>
-          "inline " ++ r ++ " " ++ a ++ " " ++ o ++ "= " ++ b
+          "(int" ++ (f (2 * n)) ++ ") " ++ r ++ " " ++ a ++ " " ++ o ++ "= " ++ b
         | None => a ++ " " ++ o ++ "= " ++ b
         end
       | COp n o a b =>
diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v
index aeb47f960..d2fca3ce6 100644
--- a/src/Assembly/Vectorize.v
+++ b/src/Assembly/Vectorize.v
@@ -2,6 +2,11 @@ Require Export Bedrock.Word Bedrock.Nomega.
 Require Import NPeano NArith PArith Ndigits Compare_dec Arith.
 Require Import ProofIrrelevance Ring List Omega.
 
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x :=
+  let y := x in f y.
+
+Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)) (at level 60).
+
 Section Vector.
   Import ListNotations.
 
@@ -62,6 +67,45 @@ Section Vector.
   Defined.
 End Vector.
 
+Section Vectorization.
+  Import ListNotations.
+
+  Lemma detuple_let: forall {A B C} (y0: A) (y1: B) (z: (A * B) -> C),
+      Let_In (y0, y1) z =
+        Let_In y0 (fun x0 =>
+          Let_In y1 (fun x1 =>
+            z (x0, x1))).
+  Proof. intros; unfold Let_In; cbv zeta; intuition. Qed.
+
+  Lemma listize_let: forall {A B} (y d: A) (z: A -> B),
+      Let_In y z = Let_In [y] (fun x => z (nth 0 x d)).
+  Proof. intros; unfold Let_In; cbv zeta; intuition. Qed.
+
+  Lemma combine_let_lists: forall {A B} (a: list A) (b: list A) (d: A) (z: list A -> list A -> B),
+      Let_In a (fun x => Let_In b (z x)) =
+        Let_In (a ++ b) (fun x => z (firstn (length a) x) (skipn (length a) x)).
+  Proof.
+
+    intros; unfold Let_In; cbv zeta.
+
+    assert (forall b0, firstn (length a) (a ++ b0) = a) as HA. {
+      induction a; intros; simpl; try reflexivity.
+      apply f_equal; apply IHa.
+    }
+
+    assert (forall b0, skipn (length a) (a ++ b0) = b0) as HB. {
+      induction a; intros; simpl; try reflexivity.
+      apply IHa; intro; simpl in HA.
+      pose proof (HA b1) as HA'; inversion HA' as [HA''].
+      rewrite HA''.
+      assumption.
+    }
+
+    rewrite HA, HB; reflexivity.
+  Qed.
+
+End Vectorization.
+
 Ltac vectorize :=
   repeat match goal with
    | [ |- context[?a - 1] ] =>