Remove WordUtil

Remove Util/NUtil.v and Util/WordUtil.v. This code is no longer in use.

3 files changed, 0 insertions, 1485 deletions

diff --git a/_CoqProject b/_CoqProject
index 40df1fb72..6e7e43e64 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -151,7 +151,6 @@ src/Util/LetInMonad.v
 src/Util/ListUtil.v
 src/Util/Logic.v
 src/Util/Loops.v
-src/Util/NUtil.v
 src/Util/NatUtil.v
 src/Util/Notations.v
 src/Util/NumTheoryUtil.v
@@ -177,7 +176,6 @@ src/Util/TagList.v
 src/Util/Tower.v
 src/Util/Tuple.v
 src/Util/Unit.v
-src/Util/WordUtil.v
 src/Util/ZBounded.v
 src/Util/ZRange.v
 src/Util/ZUtil.v
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
deleted file mode 100644
index 1d78e3276..000000000
--- a/src/Util/NUtil.v
+++ /dev/null
@@ -1,121 +0,0 @@
-Require Import Coq.NArith.NArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
-Require Export Crypto.Util.NUtil.WithoutReferenceToZ.
-Require bbv.WordScope.
-Require Import bbv.NatLib.
-Require Crypto.Util.WordUtil.
-Require Import Crypto.Util.ZUtil.Z2Nat.
-Require Import Crypto.Util.ZUtil.Shift.
-
-Module N.
-  Lemma shiftr_size : forall n bound, N.size_nat n <= bound ->
-    N.shiftr_nat n bound = 0%N.
-  Proof.
-    intros n bound H.
-    rewrite <- (Nat2N.id bound).
-    rewrite Nshiftr_nat_equiv.
-    destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
-    apply N.shiftr_eq_0.
-    rewrite N.size_nat_equiv in *.
-    rewrite N.size_log2 in * by auto.
-    apply N.le_succ_l.
-    rewrite <- N.compare_le_iff.
-    rewrite N2Nat.inj_compare.
-    rewrite <- Compare_dec.nat_compare_le.
-    rewrite Nat2N.id.
-    auto.
-  Qed.
-
-  Hint Rewrite
-    N.succ_double_spec
-    N.add_1_r
-    Nat2N.inj_succ
-    Nat2N.inj_mul
-    N2Nat.id: N_nat_conv
- .
-
-  Lemma succ_double_to_nat : forall n,
-    N.succ_double n = N.of_nat (S (2 * N.to_nat n)).
-  Proof.
-    intros.
-    replace 2 with (N.to_nat 2) by auto.
-    autorewrite with N_nat_conv.
-    reflexivity.
-  Qed.
-
-  Lemma double_to_nat : forall n,
-    N.double n = N.of_nat (2 * N.to_nat n).
-  Proof.
-    intros.
-    replace 2 with (N.to_nat 2) by auto.
-    autorewrite with N_nat_conv.
-    reflexivity.
-  Qed.
-
-  Lemma shiftr_succ : forall n i,
-    N.to_nat (N.shiftr_nat n i) =
-    if N.testbit_nat n i
-    then S (2 * N.to_nat (N.shiftr_nat n (S i)))
-    else (2 * N.to_nat (N.shiftr_nat n (S i))).
-  Proof.
-    intros n i.
-    rewrite Nshiftr_nat_S.
-    case_eq (N.testbit_nat n i); intro testbit_i;
-      pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd;
-      rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd;
-      rewrite testbit_i in shiftr_n_odd.
-    + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
-      rewrite succ_double_to_nat in Nsucc_double_shift.
-      apply Nat2N.inj.
-      rewrite Nsucc_double_shift.
-      apply N2Nat.id.
-    + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
-      rewrite double_to_nat in Nsucc_double_shift.
-      apply Nat2N.inj.
-      rewrite Nsucc_double_shift.
-      apply N2Nat.id.
-  Qed.
-
-  Section ZN.
-    Import Coq.ZArith.ZArith.
-    Lemma ZToN_NPow2_lt : forall z n, (0 <= z < 2 ^ Z.of_nat n)%Z ->
-                                      (Z.to_N z < Npow2 n)%N.
-    Proof.
-      intros.
-      apply WordUtil.bound_check_nat_N.
-      apply Znat.Nat2Z.inj_lt.
-      rewrite Znat.Z2Nat.id by omega.
-      rewrite Z.pow_Zpow.
-      replace (Z.of_nat 2) with 2%Z by reflexivity.
-      omega.
-    Qed.
-
-    Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x).
-    Lemma combine_ZNWord : forall sz1 sz2 z1 z2,
-        (0 <= Z.of_nat sz1)%Z ->
-        (0 <= Z.of_nat sz2)%Z ->
-        (0 <= z1 < 2 ^ (Z.of_nat sz1))%Z ->
-        (0 <= z2 < 2 ^ (Z.of_nat sz2))%Z ->
-        Word.combine (ZNWord sz1 z1) (ZNWord sz2 z2) =
-        ZNWord (sz1 + sz2) (Z.lor z1 (Z.shiftl z2 (Z.of_nat sz1))).
-    Proof using Type.
-      cbv [ZNWord]; intros.
-      rewrite !Word.NToWord_nat.
-      match goal with |- ?a = _ => rewrite <- (Word.natToWord_wordToNat a) end.
-      rewrite WordUtil.wordToNat_combine.
-      rewrite !Word.wordToNat_natToWord_idempotent by (rewrite Nnat.N2Nat.id; auto using ZToN_NPow2_lt).
-      f_equal.
-      rewrite Z.lor_shiftl by auto.
-      rewrite !Z_N_nat.
-      rewrite Znat.Z2Nat.inj_add by (try apply Z.shiftl_nonneg; omega).
-      f_equal.
-      rewrite Z.shiftl_mul_pow2 by auto.
-      rewrite Znat.Z2Nat.inj_mul by omega.
-      rewrite <-Z.pow_Z2N_Zpow by omega.
-      rewrite Nat.mul_comm.
-      f_equal.
-    Qed.
-  End ZN.
-
-End N.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
deleted file mode 100644
index 932f48fee..000000000
--- a/src/Util/WordUtil.v
+++ /dev/null
@@ -1,1362 +0,0 @@
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.NArith.NArith.
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Program.Program.
-Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
-Require Import Coq.micromega.Psatz.
-Require Import Coq.Bool.Bool.
-
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.Util.Sigma.
-
-Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
-Require Import Crypto.Util.ZUtil.N2Z.
-Require Import Crypto.Util.ZUtil.Definitions.
-
-Require Import bbv.WordScope.
-Require Import bbv.Nomega.
-
-Require Import Crypto.Util.FixCoqMistakes.
-
-Local Open Scope nat_scope.
-
-Create HintDb pull_wordToN discriminated.
-Create HintDb push_wordToN discriminated.
-Create HintDb pull_ZToWord discriminated.
-Create HintDb push_ZToWord discriminated.
-
-Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN.
-Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN.
-Hint Extern 1 => autorewrite with pull_ZToWord in * : pull_ZToWord.
-Hint Extern 1 => autorewrite with push_ZToWord in * : push_ZToWord.
-
-Module Word.
-  Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool :=
-    match x, y with
-    | WO, WO => true
-    | WO, _ => false
-    | WS b _ x', WS b' _ y'
-      => eqb b b' && @weqb_hetero _ _ x' y'
-    | WS _ _ _, _
-      => false
-    end%bool.
-  Global Arguments weqb_hetero {_ _} _ _.
-  Theorem weqb_hetero_true_iff : forall sz1 x sz2 y,
-      @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y.
-  Proof.
-    induction x; intros sz2 y; (split; [ destruct y | ]);
-      repeat first [ progress simpl
-                   | intro
-                   | congruence
-                   | exists eq_refl
-                   | progress destruct_head ex
-                   | progress destruct_head bool
-                   | progress subst
-                   | progress split_andb
-                   | match goal with
-                     | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ]
-                       => apply IHx in H
-                     | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
-                       => apply IHx
-                     end ].
-  Defined.
-  (* oh, the hoops I jump through to make this transparent... *)
-  Theorem weqb_hetero_homo_true_iff : forall sz x y,
-      @weqb_hetero sz sz x y = true <-> x = y.
-  Proof.
-    intros sz x y; etransitivity; [ apply weqb_hetero_true_iff | ].
-    split; [ intros [pf H] | intro ]; try (subst y; exists eq_refl; reflexivity).
-    revert y H; induction x as [|b n x IHx]; intros y H.
-    { subst y;
-        refine match pf in (_ = z)
-                     return match z return 0 = z -> Prop with
-                            | 0 => fun pf => WO = eq_rect 0 word WO 0 pf
-                            | _ => fun pf => True
-                            end pf
-               with
-               | eq_refl => eq_refl
-               end. }
-    { revert x y H IHx.
-      refine (match pf in _ = Sn
-                    return match Sn return S n = Sn -> Prop with
-                           | 0 => fun _ => True
-                           | S n' => fun pf =>
-                                       forall (pfn : n = n')
-                                              (x : word n)
-                                              (y : word (S n'))
-                                              (H : eq_rect (S n) word (WS b x) (S n') pf = y)
-                                              (IHx : forall (pf : n = n') (y : word n'), eq_rect n word x n' pf = y -> eq_rect n word x n' pfn = y),
-                                         WS b (eq_rect n word x n' pfn) = y
-                           end pf
-              with
-              | eq_refl
-                => fun pfn x y H IHx
-                   => eq_trans
-                        (f_equal2 (fun b => @WS b _)
-                                  (f_equal (@whd _) H)
-                                  (IHx eq_refl (wtl y) (f_equal (@wtl _) H)))
-                        _
-              end eq_refl).
-      refine match y in word Sn return match Sn return word Sn -> Prop with
-                                       | 0 => fun _ => True
-                                       | S n => fun y => WS (whd y) (wtl y) = y
-                                       end y
-             with
-             | WS _ _ _ => eq_refl
-             | _ => I
-             end. }
-  Defined.
-End Word.
-
-(* Utility Tactics *)
-
-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.
-
-Ltac shatter a :=
-  let H := fresh in
-  pose proof (shatter_word a) as H; simpl in H;
-    try rewrite H in *; clear H.
-
-Section Natural.
-  Definition Nge_dec (x y: N): {N.ge x y} + {N.lt x y}.
-    refine (
-      let c := (x ?= y)%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;
-        repeat match goal with
-        | [ H: (_ ?= _)%N = _ |- _] =>
-          rewrite H; intuition; try inversion H
-        | [ H: Eq = _ |- _] => inversion H
-        | [ H: Gt = _ |- _] => inversion H
-        | [ H: Lt = _ |- _] => inversion H
-        end).
-  Defined.
-
-  Lemma N_ge_0: forall x: N, (0 <= x)%N.
-  Proof.
-    intro x0; unfold N.le.
-    pose proof (N.compare_0_r x0) as H.
-    rewrite N.compare_antisym in H.
-    induction x0; simpl in *;
-      intro V; inversion V.
-  Qed.
-
-  Lemma of_nat_lt: forall x b, (x < b)%nat <-> (N.of_nat x < N.of_nat b)%N.
-  Proof.
-    intros x b; split; intro H.
-
-    - unfold N.lt; rewrite N2Nat.inj_compare.
-      repeat rewrite Nat2N.id.
-      apply nat_compare_lt in H.
-      intuition.
-
-    - unfold N.lt in H; rewrite N2Nat.inj_compare in H.
-      repeat rewrite Nat2N.id in H.
-      apply nat_compare_lt in H.
-      intuition.
-  Qed.
-End Natural.
-
-Section Pow2.
-  Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)).
-  Proof.
-    induction n as [|n IHn]; intros; auto.
-    simpl pow2.
-    rewrite Nat2Z.inj_succ.
-    rewrite Z.pow_succ_r by apply Zle_0_nat.
-    rewrite untimes2.
-    rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
-    rewrite <- IHn.
-    auto.
-  Qed.
-
-  Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N.
-  Proof.
-    intros x; induction x as [|x IHx].
-
-    - 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_ge1 : forall x, (1 <= Npow2 x)%N.
-  Proof.
-    intro x.
-    pose proof (Npow2_gt0 x) as Z.
-    apply N.lt_pred_le; simpl.
-    assumption.
-  Qed.
-
-  Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N.
-  Proof.
-    induction n as [|n IHn].
-
-    - simpl; intuition.
-
-    - rewrite Nat2N.inj_succ.
-      rewrite N.pow_succ_r; [|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 x n H.
-    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 Npow2_ordered: forall n m, (n <= m)%nat -> (Npow2 n <= Npow2 m)%N.
-  Proof.
-    induction n as [|n IHn]; intros m H; try rewrite Npow2_succ.
-
-    - simpl; apply Npow2_ge1.
-
-    - induction m; try rewrite Npow2_succ.
-
-      + inversion H.
-
-      + assert (n <= m)%nat as H0 by omega.
-        apply IHn in H0.
-        apply N.mul_le_mono_l.
-        assumption.
-  Qed.
-End Pow2.
-
-Section WordToN.
-  Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
-    wordToN (NToWord sz n) = n.
-  Proof.
-    intros.
-    rewrite wordToN_nat, NToWord_nat.
-    rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
-  Qed.
-
-  Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
-  Proof.
-    intros.
-    rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
-    apply natToWord_wordToNat.
-  Qed.
-
-  Lemma wordToN_zero: forall w, wordToN (wzero w) = 0%N.
-  Proof.
-    intros.
-    unfold wzero; rewrite wordToN_nat.
-    rewrite wordToNat_natToWord_idempotent; simpl; intuition.
-    apply Npow2_gt0.
-  Qed.
-
-  Fixpoint wbit {n} (x: word n) (k: nat): bool :=
-    match n as n' return word n' -> bool with
-    | O => fun _ => false
-    | S m => fun x' =>
-      match k with
-      | O => (whd x')
-      | S k' => wbit (wtl x') k'
-      end
-    end x.
-
-  Lemma wbit_large {n} (x: word n) (k: nat)
-    : n <= k -> wbit x k = false.
-  Proof.
-    revert k; induction x as [|b n x IHx], k; intro H; simpl; try reflexivity; try omega.
-    apply IHx; omega.
-  Qed.
-
-  Lemma wbit_inj_iff {n} (x y : word n)
-    : (forall k, wbit x k = wbit y k) <-> x = y.
-  Proof.
-    split; intro H; subst; try reflexivity.
-    induction x.
-    { revert dependent y.
-      let G := match goal with |- forall y, @?G y => G end in
-      intro y;
-        refine (match y in word n return match n with
-                                         | 0 => G
-                                         | _ => fun _ => True
-                                         end y
-                with
-                | WO => fun _ => eq_refl
-                | _ => I
-                end). }
-    { move y at top; revert dependent n.
-      let G := match goal with |- forall n y, @?G n y => G end in
-      intros n y;
-        refine (match y in word n return match n with
-                                         | 0 => fun _ => True
-                                         | S n' => G n'
-                                         end y
-                with
-                | WO => I
-                | _ => _
-                end).
-      intros x H IH.
-      pose proof (H 0) as H0; simpl in H0; subst; f_equal.
-      apply IH; intro k; specialize (H (S k)); apply H. }
-  Qed.
-
-  Lemma wbit_inj_iff_lt {n} (x y : word n)
-    : (forall k, k < n -> wbit x k = wbit y k) <-> x = y.
-  Proof.
-    rewrite <- wbit_inj_iff.
-    split; intros H k; specialize (H k);
-      destruct (le_lt_dec n k);
-      rewrite ?wbit_large by assumption;
-      auto.
-  Qed.
-
-  Lemma wordToN_testbit: forall {n} (x: word n) k,
-    N.testbit (wordToN x) k = wbit x (N.to_nat k).
-  Proof.
-    assert (forall x: N, match x with
-            | 0%N => 0%N
-            | N.pos q => N.pos (q~0)%positive
-            end = N.double x) as kill_match by (
-      induction x; simpl; intuition).
-
-    induction n as [|n IHn]; intros x k.
-
-    - shatter x; simpl; intuition.
-
-    - revert IHn; rewrite <- (N2Nat.id k).
-      generalize (N.to_nat k) as k'; intros k' IHn; clear k.
-      rewrite Nat2N.id in *.
-
-      induction k' as [|k' IHk'].
-
-      + clear IHn; induction x as [|b ? x IHx]; simpl; intuition.
-        destruct (wordToN x), b; simpl; intuition.
-
-      + clear IHk'.
-        shatter x; simpl.
-
-        rewrite kill_match.
-        replace (N.pos (Pos.of_succ_nat k'))
-           with (N.succ (N.of_nat k'))
-             by (rewrite <- Nat2N.inj_succ;
-                 simpl; intuition).
-
-        rewrite N.double_spec.
-        replace (N.succ (2 * wordToN (wtl x)))
-           with (2 * wordToN (wtl x) + 1)%N
-             by nomega.
-
-        destruct (whd x);
-          try rewrite N.testbit_odd_succ;
-          try rewrite N.testbit_even_succ;
-          let k' := k' in
-          try abstract (
-            unfold N.le; simpl;
-            induction (N.of_nat k'); intuition;
-            match goal with H : _ |- _ => solve [ inversion H ] end);
-          rewrite IHn;
-          rewrite Nat2N.id;
-          reflexivity.
-  Qed.
-
-  Lemma wbit_NToWord {sz} k v
-    : wbit (NToWord sz v) k = if Nat.ltb k sz
-                              then N.testbit v (N.of_nat k)
-                              else false.
-  Proof.
-    revert k v; induction sz as [|sz IHsz], k; intros v **; try reflexivity.
-    { destruct v as [|p]; simpl; try reflexivity.
-      destruct p; simpl; reflexivity. }
-    { pose proof (fun v k => IHsz k (Npos v)) as IHszp.
-      pose proof (fun k => IHsz k 0%N) as IHsz0.
-      destruct v as [|p]; simpl in *.
-      { rewrite IHsz0; break_match; reflexivity. }
-      { destruct p; simpl in *; try (rewrite IHsz0; break_match; reflexivity);
-          rewrite IHszp, N.pos_pred_spec;
-          change (N.pos (Pos.of_succ_nat k)) with (N.of_nat (S k));
-          rewrite <- Nat2N.inj_pred; simpl;
-            reflexivity. } }
-  Qed.
-
-  Lemma NToWord_wordToN_NToWord_small : forall sz1 sz2 w,
-      (wordToN (NToWord sz2 w) < 2^N.of_nat sz1)%N
-      -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w.
-  Proof.
-    intros sz1 sz2 w H.
-    apply wbit_inj_iff_lt; intros k Hlt.
-    rewrite !wbit_NToWord, wordToN_testbit, wbit_NToWord, Nat2N.id.
-    destruct (N.eq_dec (wordToN (NToWord sz2 w)) 0) as [H'|H'];
-      [ apply N.bits_inj_iff in H'; specialize (H' (N.of_nat k));
-        rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'; simpl in *
-      | assert (H'' : sz1 <= k -> N.testbit (wordToN (NToWord sz2 w)) (N.of_nat k) = false);
-        [ intro;
-          apply N.log2_lt_pow2 in H; [ | lia.. ]
-        | rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'' ] ];
-    break_match; try reflexivity;
-      repeat match goal with
-             | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
-             | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
-             | _ => omega
-             | _ => congruence
-             | _ => rewrite N.bits_above_log2 by lia
-             | _ => solve [ symmetry; auto ]
-             end.
-  Qed.
-
-  Lemma NToWord_wordToN_NToWord : forall sz1 sz2 w,
-      sz2 <= sz1 -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w.
-  Proof.
-    intros.
-    apply wbit_inj_iff_lt; intros k Hlt.
-    rewrite !wbit_NToWord, wordToN_testbit, wbit_NToWord, Nat2N.id.
-    break_match; try reflexivity;
-      repeat match goal with
-             | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
-             | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
-             | _ => omega
-             end.
-  Qed.
-
-  Lemma wordToN_NToWord_wordToN : forall sz1 sz2 w, (sz1 <= sz2)%nat -> wordToN (NToWord sz2 (@wordToN sz1 w)) = wordToN w.
-  Proof.
-    intros sz1 sz2 w H.
-    apply N.bits_inj; intro k.
-    rewrite !wordToN_testbit, !wbit_NToWord, wordToN_testbit, N2Nat.id.
-    destruct (N.to_nat k <? sz2) eqn:H'; try reflexivity.
-    apply Nat.ltb_ge in H'.
-    rewrite wbit_large by omega.
-    reflexivity.
-  Qed.
-
-  Lemma wordToN_NToWord_mod : forall sz w, wordToN (NToWord sz w) = N.modulo w (2^N.of_nat sz).
-  Proof.
-    intros.
-    apply N.bits_inj; intro k.
-    repeat match goal with
-           | _ => reflexivity
-           | _ => progress rewrite ?wordToN_testbit, ?wbit_NToWord, ?N2Nat.id
-           | _ => rewrite N.mod_pow2_bits_low by lia
-           | _ => rewrite N.mod_pow2_bits_high by lia
-           | _ => progress break_match
-           | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
-           | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
-           | _ => omega
-           end.
-  Qed.
-
-  Lemma wordToN_split1: forall {n m} x,
-    wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)).
-  Proof.
-    intros n m x.
-
-    pose proof (Word.combine_split _ _ x) as C; revert C.
-    generalize (split1 n m x) as a, (split2 n m x) as b.
-    intros a b C; rewrite <- C; clear C x.
-
-    apply N.bits_inj_iff; unfold N.eqf; intro x.
-    rewrite N.land_spec.
-    repeat rewrite wordToN_testbit.
-    revert x a b.
-
-    induction n as [|n IHn], m; intros;
-      shatter a; shatter b;
-      induction (N.to_nat x) as [|n0];
-      try rewrite <- (Nat2N.id n0);
-      try rewrite andb_false_r;
-      try rewrite andb_true_r;
-      simpl; intuition.
-  Qed.
-
-  Lemma wordToN_split2: forall {n m} x,
-    wordToN (@split2 n m x) = N.shiftr (wordToN x) (N.of_nat n).
-  Proof.
-    intros n m x.
-
-    pose proof (Word.combine_split _ _ x) as C; revert C.
-    generalize (split1 n m x) as a, (split2 n m x) as b.
-    intros a b C.
-    rewrite <- C; clear C x.
-
-    apply N.bits_inj_iff; unfold N.eqf; intro x;
-      rewrite N.shiftr_spec;
-      repeat rewrite wordToN_testbit;
-      try apply N_ge_0.
-
-    revert x a b.
-    induction n as [|n IHn], m; intros;
-      shatter a;
-      try apply N_ge_0.
-
-    - simpl; intuition.
-
-    - replace (x + N.of_nat 0)%N with x by nomega.
-      simpl; intuition.
-
-    - rewrite (IHn x (wtl a) b).
-      rewrite <- (N2Nat.id x).
-      repeat rewrite <- Nat2N.inj_add.
-      repeat rewrite Nat2N.id; simpl.
-      replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega.
-      reflexivity.
-
-    - rewrite (IHn x (wtl a) b).
-      rewrite <- (N2Nat.id x).
-      repeat rewrite <- Nat2N.inj_add.
-      repeat rewrite Nat2N.id; simpl.
-      replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega.
-      reflexivity.
-  Qed.
-
-  Lemma wordToN_wones: forall x, wordToN (wones x) = N.ones (N.of_nat x).
-  Proof.
-    induction x as [|x IHx].
-
-    - simpl; intuition.
-
-    - rewrite Nat2N.inj_succ.
-      replace (wordToN (wones (S x))) with (2 * wordToN (wones x) + N.b2n true)%N
-        by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
-      replace (N.ones (N.succ _))
-         with (2 * N.ones (N.of_nat x) + N.b2n true)%N.
-
-      + rewrite IHx; nomega.
-
-      + replace (N.succ (N.of_nat x)) with (1 + (N.of_nat x))%N by (
-          rewrite N.add_comm; nomega).
-        rewrite N.ones_add.
-        replace (N.ones 1) with 1%N by (
-          unfold N.ones; simpl; intuition).
-        simpl.
-        reflexivity.
-  Qed.
-
-  Tactic Notation "replaceAt1" constr(x) "with" constr(y) "by" tactic(tac) :=
-    let tmp := fresh in
-    set (tmp := x) at 1;
-    replace tmp with y by (unfold tmp; tac);
-    clear tmp.
-
-  Lemma wordToN_combine: forall {n m} a b,
-    wordToN (@Word.combine n a m b)
-      = N.lxor (N.shiftl (wordToN b) (N.of_nat n)) (wordToN a).
-  Proof.
-    intros n m a b; symmetry.
-
-    replaceAt1 a with (Word.split1 _ _ (Word.combine a b))
-      by (apply Word.split1_combine).
-
-    replaceAt1 b with (Word.split2 _ _ (Word.combine a b))
-      by (apply Word.split2_combine).
-
-    generalize (Word.combine a b); intro x; clear a b.
-
-    rewrite wordToN_split1, wordToN_split2, wordToN_wones.
-    generalize (wordToN x); clear x; intro x.
-    apply N.bits_inj_iff; unfold N.eqf; intro k.
-    rewrite N.lxor_spec.
-
-    destruct (Nge_dec k (N.of_nat n)).
-
-    - rewrite N.shiftl_spec_high; try apply N_ge_0;
-        [|apply N.ge_le; assumption].
-      rewrite N.shiftr_spec; try apply N_ge_0.
-      replace (k - N.of_nat n + N.of_nat n)%N with k by nomega.
-      rewrite N.land_spec, N.ones_spec_high; [|apply N.ge_le; assumption].
-      induction (N.testbit x k); cbv; reflexivity.
-
-    - rewrite N.shiftl_spec_low; try assumption; try apply N_ge_0.
-      rewrite N.land_spec, N.ones_spec_low; [|nomega].
-      induction (N.testbit x k); cbv; reflexivity.
-  Qed.
-
-  Lemma NToWord_equal: forall n (x y: word n),
-      wordToN x = wordToN y -> x = y.
-  Proof.
-    intros n x y H.
-    rewrite <- (NToWord_wordToN _ x).
-    rewrite <- (NToWord_wordToN _ y).
-    rewrite H; reflexivity.
-  Qed.
-
-  Lemma Npow2_ignore: forall {n} (x: word n),
-    x = NToWord _ (wordToN x + Npow2 n).
-  Proof.
-    intros n x.
-    rewrite <- (NToWord_wordToN n x) at 1.
-    repeat rewrite NToWord_nat.
-    rewrite N2Nat.inj_add.
-    rewrite Npow2_nat.
-    replace (N.to_nat (wordToN x))
-       with ((N.to_nat (wordToN x) + pow2 n) - 1 * pow2 n)
-         by omega.
-    rewrite drop_sub; f_equal; nomega.
-  Qed.
-End WordToN.
-
-Section WordBounds.
-  Lemma word_size_bound : forall {n} (w: word n), (wordToN w < Npow2 n)%N.
-  Proof.
-    intros n w; 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 wordize_plus: forall {n} (x y: word n),
-       (wordToN x + wordToN y < Npow2 n)%N
-    -> (wordToN x + wordToN y)%N = wordToN (x ^+ y).
-  Proof.
-    intros n x y H.
-    pose proof (word_size_bound x) as Hbx.
-    pose proof (word_size_bound y) as Hby.
-
-    unfold wplus, wordBin.
-    rewrite wordToN_NToWord_idempotent; intuition.
-  Qed.
-
-  Lemma wordize_minus: forall {n} (x y: word n),
-       (wordToN x >= wordToN y)%N
-    -> (wordToN x - wordToN y)%N = wordToN (x ^- y).
-  Proof.
-    intros n x y H.
-
-    destruct (Nge_dec 0%N (wordToN y)). {
-      unfold wminus, wneg.
-      replace (wordToN y) with 0%N in * by nomega.
-      replace (Npow2 n - 0)%N with (wordToN (wzero n) + Npow2 n)%N
-        by (rewrite wordToN_zero; nomega).
-      rewrite <- Npow2_ignore.
-      rewrite wplus_comm.
-      rewrite wplus_unit.
-      nomega.
-    }
-
-    assert (wordToN x - wordToN y < Npow2 n)%N. {
-      transitivity (wordToN x);
-        try apply word_size_bound;
-        apply N.sub_lt;
-        [apply N.ge_le|]; assumption.
-    }
-
-    assert (wordToN x - wordToN y + wordToN y < Npow2 n)%N. {
-      replace (wordToN x - wordToN y + wordToN y)%N
-        with (wordToN x) by nomega;
-        apply word_size_bound.
-    }
-
-    assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. {
-      apply NToWord_equal.
-      rewrite <- wordize_plus; rewrite wordToN_NToWord_idempotent; try assumption.
-      nomega.
-    }
-
-    symmetry.
-    rewrite Hv at 1.
-    unfold wminus.
-    repeat rewrite <- wplus_assoc.
-    rewrite wminus_inv.
-    rewrite wplus_comm.
-    rewrite wplus_unit.
-    rewrite wordToN_NToWord_idempotent; try assumption.
-    reflexivity.
-  Qed.
-
-  Lemma wordize_mult: forall {n} (x y: word n),
-      (wordToN x * wordToN y < Npow2 n)%N
-    -> (wordToN x * wordToN y)%N = wordToN (x ^* y).
-  Proof.
-    intros n x y H.
-    pose proof (word_size_bound x) as Hbx.
-    pose proof (word_size_bound y) as Hby.
-
-    unfold wmult, wordBin.
-    rewrite wordToN_NToWord_idempotent; intuition.
-  Qed.
-
-  Lemma wordize_and: forall {n} (x y: word n),
-    wordToN (wand x y) = N.land (wordToN x) (wordToN y).
-  Proof.
-    intros n x y.
-    apply N.bits_inj_iff; unfold N.eqf; intro k.
-    rewrite N.land_spec.
-    repeat rewrite wordToN_testbit.
-    revert x y.
-    generalize (N.to_nat k) as k'.
-    induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|].
-    induction k'; [reflexivity|].
-    fold wand.
-    rewrite IHn.
-    reflexivity.
-  Qed.
-
-  Lemma wordize_or: forall {n} (x y: word n),
-    wordToN (wor x y) = N.lor (wordToN x) (wordToN y).
-  Proof.
-    intros n x y.
-    apply N.bits_inj_iff; unfold N.eqf; intro k.
-    rewrite N.lor_spec.
-    repeat rewrite wordToN_testbit.
-    revert x y.
-    generalize (N.to_nat k) as k'; clear k.
-    induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|].
-    induction k'; [reflexivity|].
-    rewrite IHn.
-    reflexivity.
-  Qed.
-End WordBounds.
-
-Hint Rewrite NToWord_wordToN : pull_wordToN.
-
-Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
-Proof.
-  intros x n bound_nat.
-  rewrite <- Nnat.N2Nat.id, Npow2_nat.
-  replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
-  apply (Nat2N_inj_lt _ (pow2 n)).
-  assumption.
-Qed.
-
-Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y.
-Proof.
-  intros sz x y; split; intros.
-  + intro eq_xy; apply weqb_true_iff in eq_xy; congruence.
-  + case_eq (weqb x y); intros weqb_xy; auto.
-    apply weqb_true_iff in weqb_xy.
-    congruence.
-Qed.
-
-Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
-  refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
-                            | eq_refl => w
-                            end)); abstract omega. Defined.
-
-Lemma combine_eq_iff {a b} (A:word a) (B:word b) C :
-  combine A B = C <-> A = split1 a b C /\ B = split2 a b C.
-Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed.
-
-Class wordsize_eq (x y : nat) := wordsize_eq_to_eq : x = y.
-Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
-Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
-Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
-
-Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
-  := match x, y with
-     | O, O => fun _ => eq_refl
-     | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf))
-     | _, _ => fun x => x
-     end.
-
-Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
-Proof.
-  induction n as [|n IHn]; [ reflexivity | simpl ].
-  rewrite IHn; reflexivity.
-Qed.
-
-Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m :=
-  match correct_wordsize_eq n m pf in _ = y return word n -> word y with
-  | eq_refl => fun w => w
-  end.
-
-Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed.
-
-Lemma wordToNat_cast_word {n} (w:word n) m pf :
-  wordToNat (@cast_word n m pf w) = wordToNat w.
-Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
-
-Lemma wordToN_cast_word {n} (w:word n) m pf :
-  wordToN (@cast_word n m pf w) = wordToN w.
-Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
-Hint Rewrite @wordToN_cast_word : push_wordToN.
-
-Import NPeano Nat.
-Local Infix "++" := combine.
-
-Definition zext_ge n {m} {pf:m <= n} (w:word m) : word n :=
-  cast_word (w ++ wzero (n - m)).
-
-Definition keeplow {b} n (w:word b) : word b :=
-  wand (cast_word( wones (min b n) ++ wzero (b-n) )) w.
-
-Definition clearlow {b} n (w:word b) : word b :=
-  wand (cast_word( wzero (min b n) ++ wones (b-n) )) w.
-
-Definition setbit {b} n {H:n < b} (w:word b) : word b :=
-  wor (cast_word( wzero n ++ wones 1 ++ wzero (b-n-1) )) w.
-
-Definition clearbit {b} n {H:n < b} (w:word b) : word b :=
-  wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w.
-
-Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b),
-  wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
-Proof.
-  induction wa as [|??? IHwa]; intros; simpl; rewrite ?IHwa; break_match; nia.
-Qed.
-
-Lemma wordToNat_zext_ge {n m pf} (w:word m) : wordToNat (@zext_ge n m pf w) = wordToNat w.
-Proof.
-  unfold zext_ge.
-  rewrite wordToNat_cast_word, wordToNat_combine, wordToNat_wzero; nia.
-Qed.
-
-Lemma bitwp_combine {a b} f (x x' : word a) (y y' : word b)
-  : bitwp f x x' ++ bitwp f y y' = bitwp f (x ++ y) (x' ++ y').
-Proof.
-  revert x' y y'.
-  induction x as [|b' n x IHx]; simpl.
-  { intro x'; intros.
-    refine match x' with
-           | WO => _
-           | _ => I
-           end.
-    reflexivity. }
-  { intros x' y y'; rewrite IHx; clear IHx; revert x.
-    refine match x' in word Sn return match Sn return word Sn -> _ with
-                                      | 0 => fun _ => True
-                                      | S _ => fun x' => forall x, WS (f b' (whd x')) (bitwp f (x ++ y) (wtl x' ++ y')) = WS (f b' (whd (x' ++ y'))) (bitwp f (x ++ y) (wtl (x' ++ y')))
-                                      end x'
-           with
-           | WO => I
-           | WS _ _ _ => fun _ => Logic.eq_refl
-           end. }
-Qed.
-
-Lemma wand_combine {a b} (x : word a) (y : word b) (z : word (a + b))
-  : (x ++ y) ^& z = ((x ^& split1 _ _ z) ++ (y ^& split2 _ _ z)).
-Proof.
-  rewrite <- (combine_split _ _ z) at 1.
-  unfold wand.
-  rewrite bitwp_combine.
-  reflexivity.
-Qed.
-
-Lemma wordToNat_clearlow {b} (c : nat) (x : Word.word b) :
-  wordToNat (clearlow c x) = wordToNat x - (wordToNat x) mod (2^c).
-Proof.
-  assert (2^c <> 0) by auto with arith.
-  unfold clearlow.
-  match goal with
-  | [ |- context[@cast_word _ _ ?pf ?w] ]
-    => generalize pf
-  end.
-  intro H'; revert x; destruct H'; intro x; rewrite cast_word_refl.
-  rewrite <- (combine_split _ _ x) at 2 3.
-  rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero.
-  repeat match goal with H := _ |- _ => subst H end. (* only needed in 8.4 *)
-  let min := match type of x with word (?min _ _ + _) => min end in
-  repeat match goal with
-         | [ |- context[?min' b c] ]
-           => progress change min' with min
-         end.
-  generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl.
-  apply Min.min_case_strong; intros Hbc x0 x1;
-    pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1).
-  { assert (b - c = 0) by omega.
-    assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
-    generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega; [].
-    simpl; rewrite mul_0_r, add_0_r.
-    rewrite mod_small by omega.
-    omega. }
-  { rewrite !(mul_comm (2^c)), mod_add, mod_small by omega.
-    lia. }
-Qed.
-
-Lemma wordToNat_keeplow {b} (c : nat) (x : Word.word b) :
-  wordToNat (keeplow c x) = (wordToNat x) mod (2^c).
-Proof.
-  assert (2^c <> 0) by auto with arith.
-  unfold keeplow.
-  match goal with
-  | [ |- context[@cast_word _ _ ?pf ?w] ]
-    => generalize pf
-  end.
-  intro H'; revert x; destruct H'; intro x; rewrite cast_word_refl.
-  repeat match goal with H := _ |- _ => subst H end. (* only needed in 8.4 *)
-  let min := match type of x with word (?min _ _ + _) => min end in
-  repeat match goal with
-         | [ |- context[?min' b c] ]
-           => progress change min' with min
-         end.
-  rewrite <- (combine_split _ _ x) at 2 3.
-  rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero.
-  generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl.
-  apply Min.min_case_strong; intros Hbc x0 x1;
-    pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1).
-  { assert (b - c = 0) by omega.
-    assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
-    generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega.
-    simpl; rewrite mul_0_r, add_0_r.
-    rewrite mod_small by omega.
-    omega. }
-  { rewrite !(mul_comm (2^c)), mod_add, mod_small by omega.
-    lia. }
-Qed.
-
-Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
-Proof.
-  intro a; induction a as [|a IHa].
-  { reflexivity. }
-  { simpl; intros b w; rewrite IHa; clear IHa.
-    rewrite (shatter_word w); simpl.
-    change (2^a + (2^a + 0)) with (2 * 2^a).
-    rewrite (mul_comm 2 (2^a)).
-    assert (2^a <> 0) by auto with arith.
-    destruct (whd w); try rewrite S_mod; try rewrite mul_mod_distr_r; omega. }
-Qed.
-
-Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
-Proof.
-  unfold wfirstn.
-  intros; rewrite wordToNat_split1.
-  match goal with |- context[match ?x with _ => _ end] => generalize x end.
-  intro H'; destruct H'.
-  reflexivity.
-Qed.
-
-Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y.
-Proof.
-  match goal with |- ?LHS = ?RHS => destruct LHS eqn:HL, RHS eqn:HR end;
-    repeat match goal with
-           | _ => reflexivity
-           | _ => progress unfold not in *
-           | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H
-           | [ |- Z.eqb _ _ = true ] => apply Z.eqb_eq
-           | [ H : context[Z.of_N _ = Z.of_N _] |- _ ] => rewrite N2Z.inj_iff in H
-           | [ H : wordToN _ = wordToN _ |- _ ] => apply wordToN_inj in H
-           | [ H : x = y :> word _ |- _ ] => apply weqb_true_iff in H
-           | [ H : ?x = false |- _ ] => progress rewrite <- H; clear H
-           | _ => congruence
-           | [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst
-           end.
-Qed.
-
-Section Bounds.
-  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.
-    intros sz x y H H0.
-    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.
-
-  Lemma wordToN_wminus : bounds_2statement (@wminus _) Z.sub.
-  Proof.
-    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.
-
-  Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul.
-  Proof.
-    intros sz x y H H0.
-    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.
-
-  Lemma wordToN_wand : bounds_2statement (@wand _) Z.land.
-  Proof.
-    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.
-
-  Lemma wordToN_wor : bounds_2statement (@wor _) Z.lor.
-  Proof.
-    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.
-End Bounds.
-
-Hint Rewrite @wordToN_wplus using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wplus using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wminus using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wminus using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wand using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wand using word_util_arith : pull_wordToN.
-
-Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN.
-Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN.
-
-Section Updates.
-  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 (instantiate; 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_idempotent; [|apply Npow2_Zlog2]; rewrite N2Z.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_idempotent; [|apply Npow2_Zlog2]; rewrite N2Z.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.
-End Updates.
-
-Definition winit {sz} (x: word (sz + 1)): word sz :=
-  split1 sz 1 x.
-
-Definition wlast {sz} (x: word (sz + 1)): bool :=
-  whd (split2 sz 1 x).
-
-Arguments winit {_} _.
-Arguments wlast {_} _.
-
-Lemma combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
-    @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
-Proof.
-  intros sz a b c; split; unfold winit, wlast; intro H.
-
-  - rewrite <- H.
-    rewrite split1_combine, split2_combine.
-    split; [reflexivity|].
-    shatter b; simpl; f_equal.
-    generalize (wtl b) as b'; intro;
-      shatter b'; reflexivity.
-
-  - destruct H as [H0 H1]; rewrite H0.
-    replace b with (split2 sz 1 c); [apply combine_split|].
-    rewrite H1.
-    generalize (split2 sz 1 c) as b'; intro b'.
-    shatter b'.
-    generalize (wtl b') as b''; intro;
-      shatter b''; reflexivity.
-Qed.
-
-Lemma winit_combine : forall sz a b, @winit sz (combine a b) = a.
-Proof.
-  intros; unfold winit; rewrite split1_combine; reflexivity.
-Qed.
-
-Lemma wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
-Proof.
-  intros; unfold wlast; rewrite split2_combine; cbv; reflexivity.
-Qed.
-
-(* TODO : automate *)
-Lemma WordNZ_split1 : forall {n m} w,
-    Z.of_N (Word.wordToN (Word.split1 n m w)) = Z.pow2_mod (Z.of_N (Word.wordToN w)) (Z.of_nat n).
-Proof.
-  intros n m w; unfold Z.pow2_mod.
-  rewrite wordToN_split1.
-  apply Z.bits_inj_iff'; intros k Hpos.
-  rewrite Z.land_spec.
-  repeat (rewrite Z2N.inj_testbit; [|assumption]).
-  rewrite N.land_spec; f_equal.
-  rewrite wordToN_wones.
-
-  destruct (Nge_dec (Z.to_N k) (N.of_nat n)).
-
-  - rewrite Z.ones_spec_high, N.ones_spec_high;
-      [reflexivity|apply N.ge_le; assumption|split; [omega|]].
-    apply Z2N.inj_le; [apply Nat2Z.is_nonneg|assumption|].
-    etransitivity; [|apply N.ge_le; eassumption].
-    apply N.eq_le_incl.
-    induction n as [|n IHn]; simpl; reflexivity.
-
-  - rewrite Z.ones_spec_low, N.ones_spec_low;
-      [reflexivity|assumption|split; [omega|]].
-    apply Z2N.inj_lt; [assumption|apply Nat2Z.is_nonneg|].
-    eapply N.lt_le_trans; [eassumption|].
-    apply N.eq_le_incl.
-    induction n as [|n IHn]; simpl; reflexivity.
-Qed.
-
-(* TODO : automate *)
-Lemma WordNZ_split2 : forall {n m} w,
-    Z.of_N (Word.wordToN (Word.split2 n m w)) = Z.shiftr (Z.of_N (Word.wordToN w)) (Z.of_nat n).
-Proof.
-  intros n m w; unfold Z.pow2_mod.
-  rewrite wordToN_split2.
-  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 Z2N.inj_testbit; [f_equal|omega].
-  rewrite Z2N.inj_add; [f_equal|assumption|apply Nat2Z.is_nonneg].
-  induction n as [|n IHn]; simpl; reflexivity.
-Qed.
-
-Lemma WordNZ_range : forall {n} B w,
-  (2 ^ Z.of_nat n <= B)%Z ->
-  (0 <= Z.of_N (@Word.wordToN n w) < B)%Z.
-Proof.
-  intros n B w H.
-  split; [apply N2Z.is_nonneg|].
-  eapply Z.lt_le_trans; [apply N2Z.inj_lt; apply word_size_bound|].
-  rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
-  assumption.
-Qed.
-
-Lemma WordNZ_range_mono : forall {n} m w,
-  (Z.of_nat n <= m)%Z ->
-  (0 <= Z.of_N (@Word.wordToN n w) < 2 ^ m)%Z.
-Proof.
-  intros n m w H.
-  split; [apply N2Z.is_nonneg|].
-  eapply Z.lt_le_trans; [apply N2Z.inj_lt; apply word_size_bound|].
-  rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
-  apply Z.pow_le_mono; [|assumption].
-  split; simpl; omega.
-Qed.