Decent machinery for automatic pseudo-conversion

6 files changed, 164 insertions, 105 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.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index fb9402523..e0412fcf1 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -3,7 +3,7 @@ Require Import Language.
 Require Import List.
 
 Module Pseudo <: Language.
-  Import EvalUtil ListState Util.
+  Import EvalUtil ListState.
 
   Inductive Pseudo {w: nat} {s: Width w}: nat -> nat -> Type :=
     | PVar: forall n, option bool -> Index n -> Pseudo n 1
@@ -85,7 +85,7 @@ Module Pseudo <: Language.
 
     | PComb n a b f g =>
       omap (pseudoEval f st) (fun sf =>
-        omap (pseudoEval g st) (fun sg =>
+        omap (pseudoEval g (setList (getList st) sf)) (fun sg =>
           Some (setList ((getList sf) ++ (getList sg)) sg)))
 
     | PIf n m t i0 i1 l r =>
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 566d7b892..b05318ebc 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -3,8 +3,6 @@ Require Export ZArith Sumbool.
 Require Export Bedrock.Word.
 Require Import Logic.Eqdep_dec ProofIrrelevance.
 
-Import Util.
-
 Module EvalUtil.
   Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
     let c := (N.compare (wordToN a) (wordToN b)) in
@@ -25,11 +23,11 @@ Module EvalUtil.
     match io with
     | Add =>
       let v := (wordToN x + wordToN y)%N in
-      let c := (N.compare v (Npow2 b)) in
+      let c := (overflows x y) in
 
       match c as c' return c' = c -> _ with
-      | Lt => fun _ => (NToWord b v, Some false)
-      | _ => fun _ => (NToWord b v, Some true)
+      | right _ => fun _ => (NToWord b v, Some false)
+      | left _ => fun _ => (NToWord b v, Some true)
       end eq_refl
 
     | Sub => (wminus x y, None)
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 2dc3f6ade..269dc384c 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -3,44 +3,70 @@ Require Import ZArith NArith NPeano.
 Require Import QhasmCommon.
 Require Export Bedrock.Word.
 
-Module Util.
-  (* Magical Bitwise Manipulations *)
+Delimit Scope nword_scope with w.
+Local Open Scope nword_scope.
 
-  (* Force w to be m bits long, by truncation or zero-extension *)
-  Definition trunc {n} (m: nat) (w: word n): word m.
-    destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
+Notation "& x" := (wordToN x) (at level 30) : nword_scope.
+Notation "** x" := (NToWord _ x) (at level 30) : nword_scope.
 
-  - replace m with (n + (m - n)) by abstract intuition.
-    refine (zext w (m - n)).
+Section Util.
+  Definition convS {A B: Set} (x: A) (H: A = B): B :=
+    eq_rect A (fun B0 : Set => B0) x B H.
 
-  - rewrite <- s; assumption.
+  Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
+    refine (split1 k (n - k) (convS w _)).
+    abstract (replace n with (k + (n - k)) by omega; intuition).
+  Defined.
+
+  Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
+    refine (split2 (n - k) k (convS w _)).
+    abstract (replace n with (k + (n - k)) by omega; intuition).
+  Defined.
 
-  - replace n with (m + (n - m)) in w by abstract intuition.
-    refine (split1 m (n-m) w).
+  Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
+    refine (convS (zext w (n - k)) _).
+    abstract (replace (k + (n - k)) with n by omega; intuition).
   Defined.
 
-  (* Get the index-th m-bit block of w *)
-  Definition getIndex {n} (w: word n) (m index: nat): word m.
-    replace n with
-      ((min n (m * index)) + (n - (min n (m * index))))%nat
-      in w by abstract (
-      assert ((min n (m * index)) <= n)%nat
-          by apply Nat.le_min_l;
-      intuition).
-
-    refine
-      (trunc m
-      (split2 (min n (m * index)) (n - min n (m * index)) w)).
+  Definition shiftr {n} (w: word n) (k: nat): word n :=
+    match (le_dec k n) with
+    | left p => extend p (high p w)
+    | right _ => wzero n
+    end.
+
+  Definition mask {n} (k: nat) (w: word n): word n :=
+    match (le_dec k n) with
+    | left p => extend p (low p w)
+    | right _ => w
+    end.
+
+  Definition overflows {n} (out0 out1: word n) :
+      {(&out0 + &out1 >= Npow2 n)%N} + {(&out0 + &out1 < Npow2 n)%N}.
+    refine (
+      let c := ((& out0)%w + (& out1)%w ?= Npow2 n)%N in
+      match c as c' return c = c' -> _ with
+      | Lt => fun _ => right _
+      | _ => fun _ => left _
+      end eq_refl); abstract (
+        unfold c in *; unfold N.lt, N.ge;
+        rewrite _H in *; intuition; try inversion H).
   Defined.
 
-  (* set the index-th m-bit block of w to s *)
-  Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n :=
-    (w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat)))))
-       ^| (trunc n (combine s (wzero (index * m)%nat))).
+  Definition break {n} (m: nat) (x: word n): word m * word (n - m).
+    refine match (le_dec m n) with
+    | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x))
+    | right p => (extend _ x, _)
+    end; try abstract intuition.
+
+    replace (n - m) with O by abstract omega; exact WO.
+  Defined.
 
   (* Option utilities *)
   Definition omap {A B} (x: option A) (f: A -> option B) :=
     match x with | Some y => f y | _ => None end.
 
   Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
+
 End Util.
+
+Close Scope nword_scope.
\ No newline at end of file
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 9e96a0f31..ea7628bb7 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -175,7 +175,7 @@ Module Triple_as_OT <: UsualOrderedType.
 End Triple_as_OT.
 
 Module StateCommon.
-  Export ListNotations Util.
+  Export ListNotations.
 
   Module NatM := FMapAVL.Make(Nat_as_OT).
   Module PairM := FMapAVL.Make(Pair_as_OT).
diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v
index 8d0b86e8a..d17df7543 100644
--- a/src/Assembly/Wordize.v
+++ b/src/Assembly/Wordize.v
@@ -2,50 +2,22 @@
 Require Export Bedrock.Word Bedrock.Nomega.
 Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec Compare_dec.
 Require Import FunctionalExtensionality ProofIrrelevance.
+Require Import QhasmUtil.
 
 Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add
              Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N.
 
-Delimit Scope wordize_scope with w.
-Local Open Scope wordize_scope.
-
-Notation "& x" := (wordToN x) (at level 30) : wordize_scope.
-Notation "** x" := (NToWord _ x) (at level 30) : wordize_scope.
-
-Section Definitions.
-  Definition convS {A B: Set} (x: A) (H: A = B): B :=
-    eq_rect A (fun B0 : Set => B0) x B H.
-
-  Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
-    refine (split1 k (n - k) (convS w _)).
-    abstract (replace n with (k + (n - k)) by omega; intuition).
-  Defined.
-
-  Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
-    refine (split2 (n - k) k (convS w _)).
-    abstract (replace n with (k + (n - k)) by omega; intuition).
-  Defined.
-
-  Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
-    refine (convS (zext w (n - k)) _).
-    abstract (replace (k + (n - k)) with n by omega; intuition).
-  Defined.
-
-  Definition shiftr {n} (w: word n) (k: nat): word n :=
-    match (le_dec k n) with
-    | left p => extend p (high p w)
-    | right _ => wzero n
-    end.
-
-  Definition mask {n} (k: nat) (w: word n): word n :=
-    match (le_dec k n) with
-    | left p => extend p (low p w)
-    | right _ => w
-    end.
-
-End Definitions.
+Open Scope nword_scope.
 
 Section WordizeUtil.
+  Lemma break_spec: forall (m n: nat) (x: word n) low high,
+      (low, high) = break m x
+    -> &x = (&high * Npow2 m + &low)%N.
+  Proof.
+    intros; unfold break in *; destruct (le_dec m n);
+      inversion H; subst; clear H; simpl.
+  Admitted.
+ 
   Lemma mask_wand : forall (n: nat) (x: word n) m b,
       (& (mask (N.to_nat m) x) < b)%N
     -> (& (x ^& (@NToWord n (N.ones m))) < b)%N.
@@ -186,13 +158,17 @@ Section WordizeUtil.
       rewrite Pos.mul_xO_r; intuition.
   Qed.
 
+  Lemma Npow2_ignore: forall {n} (x: word n),
+    x = NToWord _ (& x + Npow2 n).
+  Proof. intros. Admitted.
+
 End WordizeUtil.
 
 (** Wordization Lemmas **)
 
 Section Wordization.
 
-  Lemma wordize_plus: forall {n} (x y: word n) (b: N),
+  Lemma wordize_plus': forall {n} (x y: word n) (b: N),
       (b <= Npow2 n)%N
     -> (&x < b)%N
     -> (&y < (Npow2 n - b))%N
@@ -215,7 +191,20 @@ Section Wordization.
         apply N.lt_le_incl; assumption.
   Qed.
 
-  Lemma wordize_mult: forall {n} (x y: word n) (b: N),
+  Lemma wordize_plus: forall {n} (x y: word n),
+    if (overflows x y)
+    then (&x + &y)%N = (& (x ^+ y) + Npow2 n)%N
+    else (&x + &y)%N = & (x ^+ y).
+  Proof.
+    intros; induction (overflows x y).
+
+    - admit.
+
+    - admit.
+
+  Qed.
+
+  Lemma wordize_mult': forall {n} (x y: word n) (b: N),
       (1 < n)%nat -> (0 < b)%N
     -> (&x < b)%N
     -> (&y < (Npow2 n) / b)%N
@@ -230,6 +219,13 @@ Section Wordization.
     - apply N.mul_div_le; nomega.
   Qed.
 
+  Definition highBits {n} (m: nat) (x: word n) := snd (break m x).
+
+  Lemma wordize_mult: forall {n} (x y: word n) (b: N),
+    (&x * &y)%N = (&(x ^* y) +
+      &((highBits (n/2) x) ^* (highBits (n/2) y)) * Npow2 n)%N.
+  Proof. intros. Admitted.
+
   Lemma wordize_and: forall {n} (x y: word n),
     N.land (&x) (&y) = & (x ^& y).
   Proof.
@@ -308,7 +304,7 @@ Section Bounds.
     intros.
 
     destruct (Nlt_dec (b1 + b2)%N (Npow2 n));
-      rewrite <- wordize_plus with (b := b1);
+      rewrite <- wordize_plus' with (b := b1);
       try apply N.add_lt_mono;
       try assumption.
 
@@ -323,7 +319,7 @@ Section Bounds.
   Proof.
     intros.
     destruct (Nlt_dec (b1 * b2)%N (Npow2 n));
-      rewrite <- wordize_mult with (b := b1);
+      rewrite <- wordize_mult' with (b := b1);
       try apply N.mul_lt_mono;
       try assumption;
       try nomega.
@@ -405,8 +401,8 @@ End Bounds.
 
 Ltac wordize_ast :=
   repeat match goal with
-  | [ H: (& ?x < ?b)%N |- context[((& ?x) + (& ?y))%N] ] => rewrite (wordize_plus x y b)
-  | [ H: (& ?x < ?b)%N |- context[((& ?x) * (& ?y))%N] ] => rewrite (wordize_mult x y b)
+  | [ H: (& ?x < ?b)%N |- context[((& ?x) + (& ?y))%N] ] => rewrite (wordize_plus' x y b)
+  | [ H: (& ?x < ?b)%N |- context[((& ?x) * (& ?y))%N] ] => rewrite (wordize_mult' x y b)
   | [ |- context[N.land (& ?x) (& ?y)] ] => rewrite (wordize_and x y)
   | [ |- context[N.shiftr (& ?x) ?k] ] => rewrite (wordize_shiftr x k)
   | [ |- (_ < _ / _)%N ] => unfold N.div; simpl
@@ -511,4 +507,4 @@ Module WordizationExamples.
 
 End WordizationExamples.
 
-Close Scope wordize_scope.
+Close Scope nword_scope.