Merging wordization and bounding together in Wordize.v

2 files changed, 296 insertions, 293 deletions

diff --git a/src/Assembly/BoundedWord.v b/src/Assembly/BoundedWord.v
index 744c10755..3c5684793 100644
--- a/src/Assembly/BoundedWord.v
+++ b/src/Assembly/BoundedWord.v
@@ -3,12 +3,11 @@ Require Import Bedrock.Word Bedrock.Nomega.
 Require Import NArith PArith Ndigits Compare_dec Arith.
 Require Import ProofIrrelevance.
 Require Import Ring.
+Require Import Wordize.
 
 Section BoundedWord.
 
-  Delimit Scope Bounded_scope with bounded.
-
-  Open Scope Bounded_scope.
+  Local Open Scope wordize_scope.
 
   Context {n: nat}.
 
@@ -50,10 +49,6 @@ Section BoundedWord.
   Defined.
 
   (* Definitions of Inequality and simple bounds. *)
-  Definition wordLeN {n: nat} (a: word n) (b: N): Prop :=
-    (wordToN a <= b)%N.
-
-  Notation "A <= B" := (wordLeN A B) (at level 70) : Bounded_scope.
 
   Lemma le_ge : forall n m, (n <= m -> m >= n)%nat.
   Proof.
diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v
index 17c077cb0..0e88ada75 100644
--- a/src/Assembly/Wordize.v
+++ b/src/Assembly/Wordize.v
@@ -1,291 +1,299 @@
 
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NPeano NArith PArith Ndigits Nnat Pnat.
-Require Import Arith Ring List Compare_dec Bool.
+Require Import NArith PArith Ndigits Nnat NPow Compare_dec.
 Require Import FunctionalExtensionality.
 
+Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add
+             Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N.
+
 Delimit Scope wordize_scope with wordize.
-Local Open Scope wordize_scope.
-
-Notation "& x" := (wordToNat x) (at level 30) : wordize_scope.
-
-Lemma word_size_bound : forall {n} (w: word n),
-  (& w <= pow2 n - 1)%nat.
-Proof. intros; assert (B := wordToNat_bound w); omega. Qed.
-
-Lemma pow2_gt0 : forall x, (pow2 x > 0)%nat.
-Proof. intros; induction x; simpl; intuition. Qed.
-
-Lemma wordize_plus: forall {n} (x y: word n) (b: nat),
-    (&x <= b)%nat
-  -> (&y <= (pow2 n - b - 1))%nat
-  -> (&x + &y) = wordToNat (x ^+ y).
-Proof.
-  intros; unfold wplus, wordBin;
-    repeat rewrite wordToN_nat in *;
-    repeat rewrite NToWord_nat in *;
-    rewrite <- Nat2N.inj_add; rewrite Nat2N.id.
-
-  destruct (wordToNat_natToWord n (&x + &y)) as [k HW];
-    destruct HW as [HW HK]; rewrite HW; clear HW.
-
-  assert ((&x) + (&y) <= (pow2 n - 1))%nat by (
-    pose proof (word_size_bound x);
-    pose proof (word_size_bound y);
-    omega).
-
-  assert (k * pow2 n <= pow2 n - 1)%nat by omega.
-
-  destruct k; subst; simpl in *; intuition;
-    clear H H0 H1 HK;
-    contradict H2.
-
-  pose proof (pow2_gt0 n).
-  induction k; simpl; intuition.
-Qed.
-
-Lemma wordize_mult: forall {n} (x y: word n) (b: nat),
-    (1 <= n)%nat
-  -> (&x <= b)%nat
-  -> (&y <= (pow2 n - 1) / b)%nat
-  -> (&x * &y)%nat = wordToNat (x ^* y).
-Proof.
-  intros; unfold wmult, wordBin;
-    repeat rewrite wordToN_nat in *;
-    repeat rewrite NToWord_nat in *;
-    rewrite <- Nat2N.inj_mul; rewrite Nat2N.id.
-
-  destruct (wordToNat_natToWord n (&x * &y)) as [k HW];
-    destruct HW as [HW HK]; rewrite HW; clear HW.
-
-  assert ((&x) * (&y) <= (pow2 n - 1))%nat. {
-    destruct (Nat.eq_dec b 0); subst;
-      try abstract (replace (&x) with 0 by intuition; omega).
-
-    transitivity ((&x * (pow2 n - 1)) / b). {
-      transitivity (&x * ((pow2 n - 1) / b)).
-
-      + apply Nat.mul_le_mono_nonneg_l; intuition.
-      + apply Nat.div_mul_le; assumption.
-    }
-
-    transitivity ((b * (pow2 n - 1)) / (b * 1)). {
-      rewrite Nat.div_mul_cancel_l; intuition.
-      rewrite Nat.div_1_r.
-      apply Nat.div_le_upper_bound; intuition.
-      apply Nat.mul_le_mono_pos_r; intuition.
-      induction n; try inversion H; simpl; intuition.
-      pose proof (pow2_gt0 n).
-      omega.
-    }
-
-    rewrite Nat.div_mul_cancel_l; intuition.
-    rewrite Nat.div_1_r; intuition.
-  }
-
-  assert (k * (pow2 n) <= pow2 n - 1)%nat by omega.
-
-  induction k; try omega.
-
-  assert (pow2 n - 1 < S k * (pow2 n))%nat. {
-    destruct n; try inversion H; simpl; try omega.
-    pose proof (pow2_gt0 n).
-    induction k; try omega.
-    
-    transitivity (pow2 n + pow2 n + pow2 n); try omega.
-    replace (pow2 n + (pow2 n + 0) + S k * _)
-      with (pow2 n + pow2 n + pow2 n +
-           (pow2 n + k * (pow2 n + (pow2 n + 0)))).
-    apply Nat.lt_add_pos_r.
-    apply Nat.add_pos_nonneg; try omega; intuition.
-
-    simpl; omega.
-  }
-
-  contradict H3; omega.
-Qed.
-
-Definition even_dec (x: nat): {exists x', x = 2*x'} + {exists x', x = 2*x' + 1}.
-  refine (if (bool_dec (odd x) true) then right _ else left _).
-
-  - apply odd_spec in _H; destruct _H; exists x0. abstract intuition.
-  - unfold odd in _H.
-    assert (even x = true) by abstract (destruct (even x); intuition).
-    apply even_spec in H; destruct H; exists x0; abstract intuition.
-Defined.
-
-Lemma testbit_spec: forall (n x y: nat), (x < pow2 n)%nat -> (y < pow2 n)%nat -> 
-    (forall k, (k < n)%nat -> testbit x k = testbit y k) -> x = y.
-Proof.
-  intro n; induction n; intros. simpl in *; omega.
-  destruct (even_dec x) as [px|px], (even_dec y) as [py|py];
-    destruct px as [x' px], py as [y' py];
-    rewrite px in *; rewrite py in *;
-    clear x y px py;
-    replace (pow2 (S n)) with (2 * (pow2 n)) in * by intuition;
-    assert (x' < pow2 n)%nat by intuition;
-    assert (y' < pow2 n)%nat by intuition.
-
-  - apply Nat.mul_cancel_l; intuition.
-    apply IHn; intuition.
-    assert (S k < S n)%nat as Z by intuition.
-    pose proof (H1 (S k) Z); intuition.
-    repeat rewrite testbit_even_succ in H5; intuition.
-
-  - assert (0 < S n)%nat as Z by intuition.
-    apply (H1 0) in Z.
-    rewrite testbit_even_0 in Z;
-      rewrite testbit_odd_0 in Z;
-      inversion Z.
-
-  - assert (0 < S n)%nat as Z by intuition.
-    apply (H1 0) in Z.
-    rewrite testbit_even_0 in Z;
-      rewrite testbit_odd_0 in Z;
-      inversion Z.
-
-  - apply Nat.add_cancel_r; apply Nat.mul_cancel_l; intuition.
-    apply IHn; intuition.
-    assert (S k < S n)%nat as Z by intuition.
-    pose proof (H1 (S k) Z); intuition.
-    repeat rewrite testbit_odd_succ in H5; intuition.
-Qed. 
-
-Inductive BinF := | binF: forall (a b c d: bool), BinF.
-
-Definition applyBinF (f: BinF) (x y: bool) :=
-  match f as f' return f = f' -> _ with
-  | binF a b c d => fun _ =>
-    if x
-    then if y
-      then a
-      else b
-    else if y
-      then c
-      else d
-  end eq_refl.
-
-Definition boolToBinF (f: bool -> bool -> bool): {g: BinF | f = applyBinF g}.
-  intros; exists (binF (f true true) (f true false) (f false true) (f false false));
-    abstract (
-      apply functional_extensionality; intro x;
-      apply functional_extensionality; intro y;
-      destruct x, y; unfold applyBinF; simpl; intuition).
-Qed.
-
-Lemma testbit_odd_succ': forall x k, testbit (S (x * 2)) (S k) = testbit x k.
-  intros.
-  replace (S (x * 2)) with ((2 * x) + 1) by omega.
-  apply testbit_odd_succ.
-Qed. 
-
-Lemma testbit_even_succ': forall x k, testbit (x * 2) (S k) = testbit x k.
-  intros; replace (x * 2) with (2 * x) by omega; apply testbit_even_succ.
-Qed. 
-
-Lemma testbit_odd_zero': forall x, testbit (S (x * 2)) 0 = true.
-  intros.
-  replace (S (x * 2)) with ((2 * x) + 1) by omega.
-  apply testbit_odd_0.
-Qed. 
-
-Lemma testbit_even_zero': forall x, testbit (x * 2) 0 = false.
-  intros; replace (x * 2) with (2 * x) by omega; apply testbit_even_0.
-Qed. 
-
-Lemma testbit_bitwp: forall {n} (x y: word n) f k, (k < n)%nat ->
-  testbit (wordToNat (bitwp f x y)) k = f (testbit (&x) k) (testbit (&y) k).
-Proof.
-  intros.
-
-  pose proof (shatter_word x);
-    pose proof (shatter_word y);
-    simpl in *.
-
-  induction n. inversion H. clear IHn; rewrite H0, H1; clear H0 H1; simpl.
-
-  replace f with (applyBinF (proj1_sig (boolToBinF f))) in *
-    by (destruct (boolToBinF f); simpl; intuition);
-    generalize (boolToBinF f) as g; intro g;
-    destruct g as [g pg]; simpl; clear pg f.
-
-  revert x y H; generalize k n; clear k n; induction k, n;
-    intros; try omega. 
-
-  - destruct g as [a b c d], (whd x), (whd y);
-      destruct a, b, c, d; unfold applyBinF in *; clear H;
-      repeat rewrite testbit_odd_zero';
-      repeat rewrite testbit_even_zero';
-      reflexivity.
-
-  - destruct g as [a b c d], (whd x), (whd y);
-      destruct a, b, c, d; unfold applyBinF in *; clear H;
-      repeat rewrite testbit_odd_zero';
-      repeat rewrite testbit_even_zero';
-      reflexivity.
-
-  - assert (k < S n)%nat as HB by omega;
-      pose proof (IHk n (wtl x) (wtl y) HB) as Z; clear HB IHk.
-
-    assert (forall {m} (w: word (S m)),
-      &w = if whd w
-           then S (& wtl w * 2)
-           else & wtl w * 2) as r0. {
-      clear H Z x y; intros.
-      pose proof (shatter_word w); simpl in H; rewrite H; clear H; simpl.
-      destruct (whd w); intuition.
-    } repeat rewrite <- r0 in Z; clear r0.
-
-    assert (forall {m} (a b: word (S m)),
-      & bitwp (applyBinF g) a b
-         = if applyBinF g (whd a) (whd b)
-           then S (& bitwp (applyBinF g) (wtl a) (wtl b) * 2)
-           else & bitwp (applyBinF g) (wtl a) (wtl b) * 2) as r1. {
-      clear H Z x y; intros.
-      pose proof (shatter_word a); pose proof (shatter_word b);
-        simpl in *; rewrite H; rewrite H0; clear H H0; simpl.
-      destruct (applyBinF g (whd a) (whd b)); intuition.
-    } repeat rewrite <- r1 in Z; clear r1.
-
-    destruct g as [a b c d], (whd x), (whd y);
-      destruct a, b, c, d; unfold applyBinF in *; clear H;
-      repeat rewrite testbit_odd_succ';
-      repeat rewrite testbit_even_succ';
-      assumption.
-Qed.
-
-(* (forall k, testbit x k = testbit y k) <-> x = y. *)
-Lemma wordize_and: forall {n} (x y: word n),
-  (Nat.land (&x) (&y))%nat = & (x ^& y).
-Proof.
-  intros n x y.
-  pose proof (pow2_gt0 n).
-  assert (&x < pow2 n)%nat by (pose proof (word_size_bound x); intuition).
-  assert (&y < pow2 n)%nat by (pose proof (word_size_bound y); intuition).
-  apply (testbit_spec n).
-
-  - induction n.
-
-    + simpl in *; intuition.
-      replace (&x) with 0 by intuition.
-      replace (&y) with 0 by intuition.
-      simpl; intuition.
-
-    + admit.
-
-  - pose (word_size_bound (x ^& y)); intuition.
-
-  - intros; rewrite land_spec.
-    unfold wand; rewrite testbit_bitwp; intuition.
-Qed.
-
-Definition take (k n: nat) (p: (k <= n)%nat) (w: word n): word k.
-  replace n with (k + (n - k)) in * by abstract omega.
-  refine (split1 k _ w).
-Defined.
-
-Lemma wordize_shiftr: forall {n} (x: word n) (k: nat) (p: (k <= n)%nat),
-  (Nat.shiftr (&x) k)%nat = & (take k n p x).
-Proof.
-  intros.
-Admitted.
+Open Scope wordize_scope.
+
+Notation "& x" := (wordToN x) (at level 30) : wordize_scope.
+Notation "** x" := (NToWord _ x) (at level 30) : wordize_scope.
+Notation "$ x" := (natToWord x) (at level 30) : wordize_scope.
+
+Section Definitions.
+
+  Definition take (k n: nat) (p: (k <= n)%nat) (w: word n): word k.
+    replace n with (k + (n - k)) in * by abstract omega.
+    refine (split1 k _ w).
+  Defined.
+
+  Definition shiftr {n} (w: word n) (k: nat): word n.
+    destruct (le_dec k n).
+
+    - replace n with (k + (n - k)) in * by abstract intuition.
+        refine (sext (take k (k + (n - k)) l w) _).
+
+    - exact (wzero n).
+  Defined.
+
+  Definition mask {n} (m: nat) (w: word n): word n.
+    destruct (le_dec m n).
+
+    - replace n with (m + (n - m)) in * by (abstract intuition).
+        refine (w ^& (zext (wones m) (n - m))).
+
+    - exact w.
+  Defined.
+
+End Definitions.
+
+Section WordizeUtil.
+
+  Lemma to_nat_lt: forall x b, (x < b)%N <-> (N.to_nat x < N.to_nat b)%nat.
+  Proof. (* via Nat2N.inj_compare *) Admitted.
+
+  Lemma of_nat_lt: forall x b, (x < b)%nat <-> (N.of_nat x < N.of_nat b)%N.
+  Proof. (* via N2Nat.inj_compare *) Admitted.
+
+  Lemma Npow2_spec : forall n, Npow2 n = N.pow 2 (N.of_nat n).
+  Proof. (* by induction and omega *) Admitted.
+
+  Lemma NToWord_wordToN: forall sz x, NToWord sz (wordToN x) = x.
+  Proof.
+    intros.
+    rewrite NToWord_nat.
+    rewrite wordToN_nat.
+    rewrite Nat2N.id.
+    rewrite natToWord_wordToNat.
+    intuition.
+  Qed.
+
+  Lemma wordToN_NToWord: forall sz x, (x < Npow2 sz)%N -> wordToN (NToWord sz x) = x.
+  Proof.
+    intros.
+    rewrite NToWord_nat.
+    rewrite wordToN_nat.
+    rewrite <- (N2Nat.id x).
+    apply Nat2N.inj_iff.
+    rewrite Nat2N.id.
+    apply natToWord_inj with (sz:=sz);
+        try rewrite natToWord_wordToNat;
+        intuition.
+
+    - apply wordToNat_bound.
+    - rewrite <- Npow2_nat; apply to_nat_lt; assumption.
+  Qed.
+
+  Lemma word_size_bound : forall {n} (w: word n), (&w < Npow2 n)%N.
+  Proof.
+    intros; pose proof (wordToNat_bound w) as B;
+        rewrite of_nat_lt in B;
+        rewrite <- Npow2_nat in B;
+        rewrite N2Nat.id in B;
+        rewrite <- wordToN_nat in B;
+        assumption.
+  Qed.
+
+  Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N.
+  Proof.
+    intros; induction x.
+
+    - simpl; apply N.lt_1_r; intuition.
+
+    - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition.
+        apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0.
+
+        + intuition; inversion H.
+
+        + apply N.neq_0_lt_0 in IHx; intuition.
+  Qed.
+
+End WordizeUtil.
+
+(** Wordization Lemmas **)
+
+Section Wordization.
+
+  Lemma wordize_plus: forall {n} (x y: word n) (b: N),
+      (b <= Npow2 n)%N
+    -> (&x < b)%N
+    -> (&y < (Npow2 n - b))%N
+    -> (&x + &y)%N = & (x ^+ y).
+  Proof.
+    intros.
+    unfold wplus, wordBin.
+    rewrite wordToN_NToWord; intuition.
+    apply (N.lt_le_trans _ (b + &y)%N _).
+
+    - apply N.add_lt_le_mono; try assumption; intuition.
+
+    - replace (Npow2 n) with (b + Npow2 n - b)%N by nomega.
+        replace (b + Npow2 n - b)%N with (b + (Npow2 n - b))%N by (
+        replace (b + (Npow2 n - b))%N with ((Npow2 n - b) + b)%N by nomega;
+        rewrite (N.sub_add b (Npow2 n)) by assumption;
+        nomega).
+
+        apply N.add_le_mono_l; try nomega.
+        apply N.lt_le_incl; assumption.
+  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
+    -> (&x * &y)%N = & (x ^* y).
+  Proof.
+    intros; unfold wmult, wordBin.
+    rewrite wordToN_NToWord; intuition.
+    apply (N.lt_le_trans _ (b * ((Npow2 n) / b))%N _).
+
+    - apply N.mul_lt_mono; assumption.
+
+    - apply N.mul_div_le; nomega.
+  Qed.
+
+  Lemma wordize_and: forall {n} (x y: word n),
+    N.land (&x) (&y) = & (x ^& y).
+  Proof.
+    intros; pose proof (Npow2_gt0 n).
+    pose proof (word_size_bound x).
+    pose proof (word_size_bound y).
+
+    induction n.
+
+    - rewrite (shatter_word_0 x) in *.
+        rewrite (shatter_word_0 y) in *.
+        simpl; intuition.
+
+    - rewrite (shatter_word x) in *.
+        rewrite (shatter_word y) in *.
+        induction (whd x), (whd y).
+
+        + admit.
+        + admit.
+        + admit.
+        + admit.
+  Qed.
+
+  Lemma wordize_shiftr: forall {n} (x: word n) (k: nat),
+    (N.shiftr_nat (&x) k) = & (shiftr x k).
+  Proof.
+    intros.
+    admit.
+  Qed.
+
+End Wordization.
+
+Section Bounds.
+
+  Theorem constant_bound_N : forall {n} (k: word n),
+    (& k < & k + 1)%N.
+  Proof. intros; nomega. Qed.
+
+  Lemma let_bound : forall {n} (x: word n) (f: word n -> word n) xb fb,
+      (& x < xb)%N
+    -> (forall x', & x' < xb -> & (f x') < fb)%N
+    -> ((let k := x in &(f k)) < fb)%N.
+  Proof. intros; eauto. Qed.
+
+  Definition Nlt_dec (x y: N): {(x < y)%N} + {(x >= y)%N}.
+    refine (
+      let c := N.compare x y in
+      match c as c' return c = c' -> _ with
+      | Lt => fun _ => left _
+      | _ => fun _ => right _
+      end eq_refl); admit.
+  Defined.
+
+  Theorem wplus_bound : forall {n} (w1 w2 : word n) b1 b2,
+      (&w1 < b1)%N
+    -> (&w2 < b2)%N
+    -> (&(w1 ^+ w2) < b1 + b2)%N.
+  Proof.
+    intros.
+
+    destruct (N.compare (b1 + b2)%N (Npow2 n));
+      rewrite <- wordize_plus with (b := b1);
+      try apply N.add_lt_mono;
+      try assumption.
+
+    - apply N.add_lt_mono; assumption.
+
+    - admit. 
+    - admit.
+
+    - apply N.add_lt_mono; assumption.
+    - apply N.add_lt_mono; assumption.
+
+  Qed.
+
+  Theorem wmult_bound : forall (w1 w2 : word n) b1 b2,
+    w1 <= b1
+    -> w2 <= b2
+    -> w1 ^* w2 <= b1 * b2.
+  Proof.
+    preomega.
+    destruct (le_lt_dec (pow2 n) (N.to_nat b1 * N.to_nat b2)).
+
+    specialize (wordToNat_bound (w1 ^* w2)); nomega.
+
+    rewrite wmult_alt.
+    unfold wmultN, wordBinN.
+    rewrite wordToNat_natToWord_idempotent.
+    ge_to_le_nat.
+
+    apply Mult.mult_le_compat; nomega.
+    pre_nomega.
+    apply Lt.le_lt_trans with (N.to_nat b1 * N.to_nat b2); auto.
+    apply Mult.mult_le_compat; nomega.
+  Qed.
+
+  Theorem shiftr_bound : forall (w : word n) b bits,
+    w <= b
+    -> shiftr w bits <= N.shiftr b (N.of_nat bits).
+  Proof.
+    admit.
+  Qed.
+
+  Theorem mask_bound : forall (w : word n) m,
+    mask m w <= Npow2 m - 1.
+  Proof.
+    admit.
+  Qed.
+
+  Theorem mask_update_bound : forall (w : word n) b m,
+    w <= b
+    -> mask m w <= (N.min b (Npow2 m - 1)).
+  Proof.
+    admit.
+  Qed.
+
+End Bounds.
+
+(** Wordization Tactics **)
+
+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)
+  | [ |- 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
+  | [ |- context[Npow2 _] ] => simpl
+  | [ |- (?x < ?c)%N ] => assumption
+  | [ |- _ = _ ] => reflexivity
+  end.
+
+Ltac lt_crush := try abstract (clear; vm_compute; intuition).
+
+(** Bounding Tactics **)
+
+(** Examples **)
+
+Module WordizationExamples.
+
+  Lemma wordize_example0: forall (x y z: word 16),
+    (wordToN x < 10)%N ->
+    (wordToN y < 10)%N ->
+    (wordToN z < 10)%N ->
+    & (x ^* y) = (&x * &y)%N.
+  Proof.
+    intros.
+    wordize_ast; lt_crush.
+    transitivity 10%N; try assumption; lt_crush.
+  Qed.
+
+End WordizationExamples.
\ No newline at end of file