1 files changed, 446 insertions, 15 deletions

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index d4bc73aeb..f0e6ef335 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.NArith.NArith.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Bedrock.Word.
@@ -8,6 +9,9 @@ Require Import Coq.Program.Program.
 Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
 Require Import Coq.micromega.Psatz.
 
+Require Import Crypto.Assembly.WordizeUtil.
+Require Import Crypto.Assembly.Bounds.
+
 Local Open Scope nat_scope.
 
 Create HintDb pull_wordToN discriminated.
@@ -17,6 +21,20 @@ Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN.
 
 Ltac word_util_arith := omega.
 
+Ltac destruct_min :=
+  match goal with
+  | [|- context[Z.min ?a ?b]] =>
+    let g := fresh in
+    destruct (Z.min_dec a b) as [g|g]; rewrite g; clear g
+  end.
+
+Ltac destruct_max :=
+  match goal with
+  | [|- context[Z.max ?a ?b]] =>
+    let g := fresh in
+    destruct (Z.max_dec a b) as [g|g]; rewrite g; clear g
+  end.
+
 Lemma pow2_id : forall n, pow2 n = 2 ^ n.
 Proof.
   induction n; intros; simpl; auto.
@@ -34,6 +52,175 @@ Proof.
   auto.
 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.
+
+Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N.
+Proof.
+  induction n.
+
+  - simpl; intuition.
+
+  - rewrite Nat2N.inj_succ.
+    rewrite N.pow_succ_r; try apply N_ge_0.
+    rewrite <- IHn.
+    simpl; intuition.
+Qed.
+
+Lemma Npow2_Zlog2 : forall x n,
+    (Z.log2 (Z.of_N x) < Z.of_nat n)%Z
+ -> (x < Npow2 n)%N.
+Proof.
+  intros.
+  apply N2Z.inj_lt.
+  rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
+  destruct (N.eq_dec x 0%N) as [e|e].
+
+  - rewrite e.
+    apply Z.pow_pos_nonneg; [cbv; reflexivity|apply Nat2Z.is_nonneg].
+
+  - apply Z.log2_lt_pow2; [|assumption].
+    apply N.neq_0_lt_0, N2Z.inj_lt in e.
+    assumption.
+Qed.
+
+Lemma Z_land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z.
+Proof.
+  intros; apply Z.ldiff_le; [assumption|].
+  rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc.
+  rewrite <- Z.land_0_l with (a := y); f_equal.
+  rewrite Z.land_comm, Z.land_lnot_diag.
+  reflexivity.
+Qed.
+
+Lemma Z_lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z.
+Proof.
+  intros; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
+  rewrite Z.ldiff_land.
+  apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
+  rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec;
+    [|apply Z.ge_le; assumption].
+  induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity.
+Qed.
+
+Lemma Z_lor_le : forall x y z,
+     (0 <= x)%Z
+  -> (x <= y)%Z
+  -> (y <= z)%Z
+  -> (Z.lor x y <= (2 ^ Z.log2_up (z+1)) - 1)%Z.
+Proof.
+  intros; apply Z.ldiff_le.
+
+  - apply Z.le_add_le_sub_r.
+    replace 1%Z with (2 ^ 0)%Z by (cbv; reflexivity).
+    rewrite Z.add_0_l.
+    apply Z.pow_le_mono_r; [cbv; reflexivity|].
+    apply Z.log2_up_nonneg.
+
+  - destruct (Z_lt_dec 0 z).
+
+    + assert (forall a, a - 1 = Z.pred a)%Z as HP by (intro; omega);
+        rewrite HP, <- Z.ones_equiv; clear HP.
+      apply Z.ldiff_ones_r_low; [apply Z.lor_nonneg; split; omega|].
+      rewrite Z.log2_up_eqn, Z.log2_lor; try omega.
+      apply Z.lt_succ_r.
+      destruct_max; apply Z.log2_le_mono; omega.
+
+    + replace z with 0%Z by omega.
+      replace y with 0%Z by omega.
+      replace x with 0%Z by omega.
+      cbv; reflexivity.
+Qed.
+
+Lemma Z_inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y).
+Proof.
+  intros.
+  apply Z.bits_inj_iff'; intros k Hpos.
+  rewrite Z2N.inj_testbit; [|assumption].
+  rewrite Z.shiftl_spec; [|assumption].
+
+  assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by (
+    unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left];
+    intro H; inversion H).
+
+  destruct g as [g|g];
+  [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le]
+  | rewrite N.shiftl_spec_low]; try assumption.
+
+  - rewrite <- N2Z.inj_testbit; f_equal.
+    rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption].
+
+  - apply N2Z.inj_lt in g.
+    rewrite Z2N.id in g; [symmetry|assumption].
+    apply Z.testbit_neg_r; omega.
+Qed.
+
+Lemma Z_inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y).
+Proof.
+  intros.
+  apply Z.bits_inj_iff'; intros k Hpos.
+  rewrite Z2N.inj_testbit; [|assumption].
+  rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption.
+  rewrite <- N2Z.inj_testbit; f_equal.
+  rewrite N2Z.inj_add; f_equal.
+  apply Z2N.id; assumption.
+Qed.
+
+Lemma Z_pow2_ge_0: forall a, (0 <= 2 ^ a)%Z.
+Proof.
+  intros; apply Z.pow_nonneg; omega.
+Qed.
+
+Lemma Z_pow2_gt_0: forall a, (0 <= a)%Z -> (0 < 2 ^ a)%Z.
+Proof.
+  intros; apply Z.pow_pos_nonneg; [|assumption]; omega.
+Qed.
+
+Local Ltac solve_pow2 :=
+  repeat match goal with
+  | [|- _ /\ _] => split
+  | [|- (0 < 2 ^ _)%Z] => apply Z_pow2_gt_0
+  | [|- (0 <= 2 ^ _)%Z] => apply Z_pow2_ge_0
+  | [|- (2 ^ _ <= 2 ^ _)%Z] => apply Z.pow_le_mono_r
+  | [|- (_ <= _)%Z] => omega
+  | [|- (_ < _)%Z] => omega
+  end.
+
+Lemma Z_shiftr_le_mono: forall a b c d,
+    (0 <= a)%Z
+ -> (0 <= d)%Z
+ -> (a <= c)%Z
+ -> (d <= b)%Z
+ -> (Z.shiftr a b <= Z.shiftr c d)%Z.
+Proof.
+  intros.
+  repeat rewrite Z.shiftr_div_pow2; [|omega|omega].
+  etransitivity; [apply Z.div_le_compat_l | apply Z.div_le_mono]; solve_pow2.
+Qed.
+
+Lemma Z_shiftl_le_mono: forall a b c d,
+    (0 <= a)%Z
+ -> (0 <= b)%Z
+ -> (a <= c)%Z
+ -> (b <= d)%Z
+ -> (Z.shiftl a b <= Z.shiftl c d)%Z.
+Proof.
+  intros.
+  repeat rewrite Z.shiftl_mul_pow2; [|omega|omega].
+  etransitivity; [apply Z.mul_le_mono_nonneg_l|apply Z.mul_le_mono_nonneg_r]; solve_pow2.
+Qed.
+
 Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
   wordToN (NToWord sz n) = n.
 Proof.
@@ -281,47 +468,291 @@ Proof.
            end.
 Qed.
 
-Local Notation bounds_2statement wop Zop
-  := (forall {sz} (x y : word sz),
-         (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))
-          -> Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz
-          -> Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))))%Z).
+Local Notation bounds_2statement wop Zop := (forall {sz} (x y : word sz),
+     (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))
+  -> (Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz)
+  -> (Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))))%Z).
 
 Lemma wordToN_wplus : bounds_2statement (@wplus _) Z.add.
 Proof.
-  admit.
-Admitted.
+  intros.
+  rewrite <- wordize_plus; [rewrite N2Z.inj_add; reflexivity|].
+  destruct (N.eq_dec (wordToN x + wordToN y) 0%N) as [e|e];
+    [rewrite e; apply Npow2_gt0|].
+  apply N.neq_0_lt_0 in e.
+  apply N2Z.inj_lt in e.
+  apply N2Z.inj_lt.
+  rewrite N2Z.inj_add in *.
+  rewrite Npow2_N.
+  rewrite N2Z.inj_pow.
+  replace (Z.of_N 2%N) with 2%Z by auto.
+  apply Z.log2_lt_pow2; [auto|].
+  rewrite nat_N_Z.
+  assumption.
+Qed.
+
 Hint Rewrite @wordToN_wplus using word_util_arith : push_wordToN.
 Hint Rewrite <- @wordToN_wplus using word_util_arith : pull_wordToN.
 
 Lemma wordToN_wminus : bounds_2statement (@wminus _) Z.sub.
 Proof.
-  admit.
-Admitted.
+  intros sz x y H ?.
+  assert (wordToN y <= wordToN x)%N. {
+    apply N2Z.inj_le.
+    rewrite <- (Z.add_0_l (Z.of_N (wordToN y))).
+    apply Z.le_add_le_sub_r; assumption.
+  }
+
+  rewrite <- N2Z.inj_sub; [|assumption].
+  rewrite <- wordize_minus; [reflexivity|apply N.le_ge; assumption].
+Qed.
+
 Hint Rewrite @wordToN_wminus using word_util_arith : push_wordToN.
 Hint Rewrite <- @wordToN_wminus using word_util_arith : pull_wordToN.
 
 Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul.
 Proof.
-  admit.
-Admitted.
+  intros.
+  rewrite <- wordize_mult; [rewrite N2Z.inj_mul; reflexivity|].
+  destruct (N.eq_dec (wordToN x * wordToN y) 0%N) as [e|e];
+    [rewrite e; apply Npow2_gt0|].
+  apply N.neq_0_lt_0 in e.
+  apply N2Z.inj_lt in e.
+  apply N2Z.inj_lt.
+  rewrite N2Z.inj_mul in *.
+  rewrite Npow2_N.
+  rewrite N2Z.inj_pow.
+  replace (Z.of_N 2%N) with 2%Z by auto.
+  apply Z.log2_lt_pow2; [auto|].
+  rewrite nat_N_Z.
+  assumption.
+Qed.
+
 Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN.
 Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN.
 
 Lemma wordToN_wand : bounds_2statement (@wand _) Z.land.
 Proof.
-  admit.
-Admitted.
+  intros.
+  rewrite wordize_and.
+  apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
+  rewrite Z.land_spec.
+  rewrite Z2N.inj_testbit; [|apply Z.ge_le; assumption].
+  rewrite N.land_spec.
+  repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]).
+  reflexivity.
+Qed.
 Hint Rewrite @wordToN_wand using word_util_arith : push_wordToN.
 Hint Rewrite <- @wordToN_wand using word_util_arith : pull_wordToN.
 
 Lemma wordToN_wor : bounds_2statement (@wor _) Z.lor.
 Proof.
-  admit.
-Admitted.
+  intros.
+  rewrite wordize_or.
+  apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
+  rewrite Z.lor_spec.
+  rewrite Z2N.inj_testbit; [|apply Z.ge_le; assumption].
+  rewrite N.lor_spec.
+  repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]).
+  reflexivity.
+Qed.
 Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN.
 Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN.
 
+Local Notation bound n lower value upper := (
+    (0 <= lower)%Z
+  /\ (lower <= Z.of_N (@wordToN n value))%Z
+  /\ (Z.of_N (@wordToN n value) <= upper)%Z
+  /\ (Z.log2 upper < Z.of_nat n)%Z).
+
+Definition valid_update n lowerF valueF upperF : Prop :=
+  forall lower0 value0 upper0
+    lower1 value1 upper1,
+
+    bound n lower0 value0 upper0
+  -> bound n lower1 value1 upper1
+  -> (0 <= lowerF lower0 upper0 lower1 upper1)%Z
+  -> (Z.log2 (upperF lower0 upper0 lower1 upper1) < Z.of_nat n)%Z
+  -> bound n (lowerF lower0 upper0 lower1 upper1)
+            (valueF value0 value1)
+            (upperF lower0 upper0 lower1 upper1).
+
+Local Ltac add_mono := 
+  etransitivity; [| apply Z.add_le_mono_r; eassumption]; omega.
+
+Lemma add_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => l0 + l1)%Z
+      (@wplus n)
+      (fun l0 u0 l1 u1 => u0 + u1)%Z.
+Proof.
+  unfold valid_update; intros until upper1; intros B0 B1 H0 H1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1.
+  repeat split; [add_mono| | |assumption]; (
+    rewrite wordToN_wplus; [add_mono|add_mono|];
+    eapply Z.le_lt_trans; [| eassumption];
+    apply Z.log2_le_mono; add_mono).
+Qed.
+
+Local Ltac sub_mono :=
+  etransitivity;
+  [| apply Z.sub_le_mono_r]; eauto;
+  first [ reflexivity
+        | apply Z.sub_le_mono_l; assumption
+        | apply Z.le_add_le_sub_l; etransitivity; [|eassumption];
+          repeat rewrite Z.add_0_r; assumption].
+
+Lemma sub_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => l0 - u1)%Z
+      (@wminus n)
+      (fun l0 u0 l1 u1 => u0 - l1)%Z.
+Proof.
+  unfold valid_update; intros until upper1; intros B0 B1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1.
+  repeat split; [sub_mono| | |assumption]; (
+   rewrite wordToN_wminus; [sub_mono|omega|];
+   eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]; sub_mono).
+Qed.
+
+Local Ltac mul_mono := 
+  etransitivity; [|apply Z.mul_le_mono_nonneg_r];
+  repeat first
+  [ eassumption
+  | reflexivity
+  | apply Z.mul_le_mono_nonneg_l
+  | rewrite Z.mul_0_l
+  | omega].
+
+Lemma mul_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => l0 * l1)%Z
+      (@wmult n)
+      (fun l0 u0 l1 u1 => u0 * u1)%Z.
+Proof.
+  unfold valid_update; intros until upper1; intros B0 B1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1.
+  repeat split; [mul_mono| | |assumption]; (
+    rewrite wordToN_wmult; [mul_mono|mul_mono|];
+    eapply Z.le_lt_trans; [| eassumption];
+    apply Z.log2_le_mono; mul_mono).
+Qed.
+
+Local Ltac solve_land_ge0 :=
+  apply Z.land_nonneg; left; etransitivity; [|eassumption]; assumption.
+
+Local Ltac land_mono :=
+  first [assumption | etransitivity; [|eassumption]; assumption].
+
+Lemma land_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => 0)%Z
+      (@wand n)
+      (fun l0 u0 l1 u1 => Z.min u0 u1)%Z.
+Proof.
+  unfold valid_update; intros until upper1; intros B0 B1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
+  repeat split; [reflexivity|apply N2Z.is_nonneg| |assumption].
+  rewrite wordToN_wand; [|solve_land_ge0|].
+
+  - destruct_min;
+      (etransitivity; [|eassumption]); [|rewrite Z.land_comm];
+      (apply Z_land_le; land_mono).
+
+  - eapply Z.le_lt_trans; [apply Z.log2_land; land_mono|destruct_min]; (
+      eapply Z.le_lt_trans; [apply Z.log2_le_mono; eassumption|];
+      assumption).
+Qed.
+
+Local Ltac lor_mono :=
+  first [assumption | etransitivity; [|eassumption]; assumption].
+
+Local Ltac lor_trans :=
+  destruct_max; (
+    eapply Z.le_lt_trans; [apply Z.log2_le_mono; eassumption|];
+    assumption).
+
+Lemma lor_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => Z.max l0 l1)%Z
+      (@wor n)
+      (fun l0 u0 l1 u1 => 2^(Z.max (Z.log2_up (u0+1)) (Z.log2_up (u1+1))) - 1)%Z.
+Proof.
+  unfold valid_update; intros until upper1; intros B0 B1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
+  repeat split; [destruct_max; assumption| | |assumption].
+
+  - rewrite wordToN_wor;
+    [ destruct_max; [|rewrite Z.lor_comm];
+        (etransitivity; [|apply Z_lor_lower]; lor_mono)
+    | apply Z.lor_nonneg; split; lor_mono|].
+
+    rewrite Z.log2_lor; [lor_trans|lor_mono|lor_mono].
+
+  - rewrite wordToN_wor; [
+    | apply Z.lor_nonneg; split; lor_mono
+    | rewrite Z.log2_lor; [lor_trans|lor_mono|lor_mono]].
+
+    destruct (Z_ge_dec upper0 upper1) as [g|g].
+
+    + apply Z.ge_le in g; pose proof g as g'.
+      apply -> (Z.add_le_mono_r upper1 upper0 1) in g'.
+      apply Z.log2_up_le_mono, Z.max_l in g'.
+      rewrite g'; clear g'.
+
+      destruct (Z.le_ge_cases (Z.of_N (wordToN value0)) (Z.of_N (wordToN value1)));
+        [|rewrite Z.lor_comm];
+        apply Z_lor_le; lor_mono.
+
+    + assert (upper1 >= upper0)%Z as g'' by omega; clear g.
+      pose proof g'' as g; pose proof g'' as g'; clear g''.
+      apply Z.ge_le in g; apply Z.ge_le in g'.
+      apply -> (Z.add_le_mono_r upper0 upper1 1) in g'.
+      apply Z.log2_up_le_mono, Z.max_r in g'.
+      rewrite g'; clear g'.
+
+      destruct (Z.le_ge_cases (Z.of_N (wordToN value0)) (Z.of_N (wordToN value1)));
+        [|rewrite Z.lor_comm];
+        apply Z_lor_le; lor_mono.
+Qed.
+
+Local Ltac shift_mono := repeat progress first
+  [ eassumption
+  | etransitivity; [|eassumption]].
+
+Lemma shr_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => Z.shiftr l0 u1)%Z
+      (@wordBin N.shiftr n)
+      (fun l0 u0 l1 u1 => Z.shiftr u0 l1)%Z.
+Proof.
+  unfold valid_update, wordBin; intros until upper1; intros B0 B1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
+
+  repeat split; [assumption| | |assumption];
+    (rewrite wordToN_NToWord; [|apply Npow2_Zlog2]; rewrite Z_inj_shiftr);
+    [ | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]
+    | | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]];
+    apply Z_shiftr_le_mono; shift_mono.
+Qed.
+
+Lemma shl_valid_update: forall n,
+    valid_update n
+      (fun l0 u0 l1 u1 => Z.shiftl l0 l1)%Z
+      (@wordBin N.shiftl n)
+      (fun l0 u0 l1 u1 => Z.shiftl u0 u1)%Z.
+Proof.
+  unfold valid_update, wordBin; intros until upper1; intros B0 B1.
+  do 2 destruct B0 as [? B0], B1 as [? B1]; destruct B0, B1; intros.
+
+  repeat split; [assumption| | |assumption];
+    (rewrite wordToN_NToWord; [|apply Npow2_Zlog2]; rewrite Z_inj_shiftl);
+    [ | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]
+    | | eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]];
+    apply Z_shiftl_le_mono; shift_mono.
+Qed.
+
+
 Axiom wlast : forall sz, word (sz+1) -> bool. Arguments wlast {_} _.
 Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _.
 Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)),