Add Pseudize, Vectorize, Wordize to the build process

4 files changed, 66 insertions, 41 deletions

diff --git a/_CoqProject b/_CoqProject
index c9d56d0fc..a8e3d66ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,3 +57,6 @@ src/Assembly/PseudoConversion.v
 src/Assembly/AlmostConversion.v
 src/Assembly/StringConversion.v
 src/Assembly/Pipeline.v
+src/Assembly/Vectorize.v
+src/Assembly/Wordize.v
+src/Assembly/Pseudize.v
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
index 3a66484ee..0ef1dd765 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 Compare_dec.
+Require Import NArith NPeano List Sumbool Compare_dec Omega.
 Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State.
 Require Export Wordize Vectorize.
 
@@ -9,6 +9,16 @@ Module Conversion.
   Hint Unfold setList getList getVar setCarry setCarryOpt getCarry
        getMem setMem overflows.
 
+  Lemma eval_in_length: forall {w s n m} x M c x' M' c' p,
+      @pseudoEval n m w s p (x, M, c) = Some (x', M', c')
+    -> Datatypes.length x = n.
+  Admitted.
+
+  Lemma eval_out_length: forall {w s n m} x M c x' M' c' p,
+      @pseudoEval n m w s p (x, M, c) = Some (x', M', c')
+    -> Datatypes.length x' = m.
+  Admitted.
+
   Lemma pseudo_var: forall {w s n} b k x v m c,
       (k < n)%nat
     -> nth_error x k = Some v
@@ -24,7 +34,7 @@ Module Conversion.
 
     autounfold; simpl.
     destruct (nth_error x k); simpl; try inversion H0; intuition.
-  Qed.
+  Admitted.
 
   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)
@@ -47,7 +57,7 @@ Module Conversion.
   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) =
+    -> pseudoEval (PBin n IAdd p) (x, m0, c0) =
         Some ([out0 ^+ out1], m1,
           Some (proj1_sig (bool_of_sumbool
                (overflows w (&out0 + &out1)%N)%w))).
@@ -62,7 +72,7 @@ Module Conversion.
 
   Lemma pseudo_bin:
     forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1 op,
-      op <> Add
+      op <> IAdd
     -> pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
     -> pseudoEval (PBin n op p) (x, m0, c0) =
         Some ([fst (evalIntOp op out0 out1)], m1, c1).
@@ -78,11 +88,11 @@ Module Conversion.
   Lemma pseudo_and:
     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 And p) (x, m0, c0) =
+    -> pseudoEval (PBin n IAnd p) (x, m0, c0) =
         Some ([out0 ^& out1], m1, c1).
   Proof.
     intros.
-    replace (out0 ^& out1) with (fst (evalIntOp And out0 out1)).
+    replace (out0 ^& out1) with (fst (evalIntOp IAnd out0 out1)).
     - apply pseudo_bin; intuition; inversion H0.
     - unfold evalIntOp; simpl; intuition.
   Qed.
@@ -164,24 +174,33 @@ Module Conversion.
 
   Lemma pseudo_let_var:
     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,
+      input a f m0 m1 m2 c0 c1 c2,
       pseudoEval p0 (input, m0, c0) = Some ([a], m1, c1)
     -> pseudoEval p1 (input ++ [a], m1, c1) = Some (f (nth n (input ++ [a]) (wzero _)), m2, c2)
     -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) =
         Some (let x := a in f a, m2, c2).
   Proof.
-    intros; cbv beta; simpl in *; apply pseudo_let.
+    intros; cbv zeta.
+    eapply pseudo_let; try eassumption.
+    replace (f a) with (f (nth n (input ++ [a]) (wzero w))); try assumption.
+    apply f_equal.
+    assert (Datatypes.length input = 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_let_list:
     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,
+      input lst f m0 m1 m2 c0 c1 c2,
       pseudoEval p0 (input, m0, c0) = Some (lst, m1, c1)
     -> pseudoEval p1 (input ++ lst, m1, c1) = Some (f lst, m2, c2)
     -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) =
-        Some (let x := lst in f a, m2, c2).
+        Some (let x := lst in f x, m2, c2).
   Proof.
-    intros; cbv beta; simpl in *; apply pseudo_let.
+    intros; cbv zeta.
+    eapply pseudo_let; try eassumption.
   Qed.
 
   Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := 
@@ -205,6 +224,13 @@ Module Conversion.
 
   Ltac pseudo_step :=
     match goal with
+    | [ |- pseudoEval ?p _ = Some ((let _ := ?b in _), _, _) ] =>
+      is_evar p;
+      match (type of b) with
+      | word _ => eapply pseudo_let_var
+      | list _ => eapply pseudo_let_list
+      end
+
     | [ |- pseudoEval ?p _ = Some ([?x ^& ?y], _, _) ] =>
       is_evar p; eapply pseudo_and
     | [ |- pseudoEval ?p _ = Some ([?x ^+ ?y], _, _) ] =>
@@ -229,11 +255,10 @@ Module Conversion.
       let b := nth 0 v (wzero _) in
       [a ^& b]).
 
-    cbv zeta; pseudo_solve.
-
+    pseudo_solve.
   Defined.
 
-  Eval simpl in (proj1_sig convert_example).
+  (* Eval simpl in (proj1_sig convert_example). *)
 
 End Conversion.
 
diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v
index f8139bf92..aeb47f960 100644
--- a/src/Assembly/Vectorize.v
+++ b/src/Assembly/Vectorize.v
@@ -1,7 +1,6 @@
 Require Export Bedrock.Word Bedrock.Nomega.
 Require Import NPeano NArith PArith Ndigits Compare_dec Arith.
-Require Import ProofIrrelevance Ring List.
-Require Import MultiBoundedWord.
+Require Import ProofIrrelevance Ring List Omega.
 
 Section Vector.
   Import ListNotations.
@@ -13,9 +12,13 @@ Section Vector.
       match (proj1_sig x) as x' return (proj1_sig x) = x' -> _ with
       | [] => fun _ => _
       | x0 :: xs => fun _ => nth (proj1_sig i) (proj1_sig x) x0
-      end eq_refl); abstract (
+      end eq_refl);
+    abstract (
       destruct x as [x xp], i as [i ip]; destruct x as [|x0 xs];
-      simpl in xp; subst; inversion _H; clear _H; omega).
+      simpl in *; subst; try omega;
+      match goal with
+      | [H: _ = @nil _ |- _] => inversion H
+      end).
   Defined.
 
   Lemma vget_spec: forall {T n} (x: vec T n) (i: {v: nat | (v < n)%nat}) (d: T),
diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v
index e5ad3f066..bac25db71 100644
--- a/src/Assembly/Wordize.v
+++ b/src/Assembly/Wordize.v
@@ -1,6 +1,7 @@
 
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec Compare_dec.
+Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec.
+Require Import Compare_dec Omega.
 Require Import FunctionalExtensionality ProofIrrelevance.
 Require Import QhasmUtil QhasmEvalCommon.
 
@@ -108,15 +109,15 @@ Section WordizeUtil.
 
   Lemma natToWord_convS: forall {n m} (x: word n) p,
       & x = & @convS (word n) (word m) x p.
-  Proof. admit. Qed.
+  Proof. Admitted.
 
   Lemma natToWord_combine: forall {n} (x: word n) k,
       & x = & combine x (wzero k).
-  Proof. admit. Qed.
+  Proof. Admitted.
 
   Lemma natToWord_split1: forall {n} (x: word n) p,
       & x = & split1 n 0 (convS x p).
-  Proof. admit. Qed.
+  Proof. Admitted.
 
   Lemma extend_bound: forall k n (p: (k <= n)%nat) (w: word k),
     (& (extend p w) < Npow2 k)%N.
@@ -141,7 +142,7 @@ Section WordizeUtil.
       + admit.
 
     - intros; rewrite <- natToWord_combine; intuition.
-  Qed.
+  Admitted.
 
   Lemma Npow2_split: forall a b,
     (Npow2 (a + b) = (Npow2 a) * (Npow2 b))%N.
@@ -160,7 +161,7 @@ Section WordizeUtil.
 
   Lemma Npow2_ignore: forall {n} (x: word n),
     x = NToWord _ (& x + Npow2 n).
-  Proof. intros. Admitted.
+  Proof. Admitted.
 
 End WordizeUtil.
 
@@ -244,15 +245,11 @@ Section Wordization.
         + admit.
         + admit.
         + admit.
-  Qed.
+  Admitted.
 
   Lemma wordize_shiftr: forall {n} (x: word n) (k: nat),
     (N.shiftr_nat (&x) k) = & (shiftr x k).
-  Proof.
-    intros.
-
-    admit.
-  Qed.
+  Proof. Admitted.
 
 End Wordization.
 
@@ -285,12 +282,12 @@ Section Bounds.
       | Lt => fun _ => left _
       | _ => fun _ => right _
       end eq_refl);
-      abstract (unfold c in *; try first [
-        apply N.compare_eq_iff in _H
-      | apply N.compare_lt_iff in _H
-      | pose proof (N.compare_antisym x y) as _H0;
-        rewrite _H in _H0; simpl in _H0;
-        apply N.compare_lt_iff in _H0 ]; nomega).
+    abstract (
+      unfold c, N.ge, N.lt in *; intuition; subst;
+      match goal with
+      | [H0: ?x = _, H1: ?x = _ |- _] =>
+        rewrite H0 in H1; inversion H1
+      end).
   Defined.
 
   Theorem wplus_bound : forall {n} (w1 w2 : word n) b1 b2,
@@ -336,15 +333,12 @@ Section Bounds.
       - unfold N.le, N.lt in *; rewrite H; intuition; inversion H0.
 
       - revert IHbits;
-          generalize (nat_iter bits N.div2 (& w)),
-                     (nat_iter bits N.div2 b);
-          clear; intros x y H.
 
        admit. (* Monotonicity of N.div2 *)
     }
 
     apply N.le_lteq in H0; destruct H0; nomega.
-  Qed.
+  Admitted.
 
   Theorem mask_bound : forall {n} (w : word n) m,
     (n > 1)%nat ->
@@ -378,7 +372,7 @@ Section Bounds.
 
         * admit.
         * admit.
-  Qed.
+  Admitted.
 
   Theorem mask_update_bound : forall {n} (w : word n) b m,
       (n > 1)%nat