Not quite done with WordUtil lemmas.

11 files changed, 884 insertions, 1 deletions

diff --git a/src/Util/Bool.v b/src/Util/Bool.v
index 7b94c503e..a59cf53f0 100644
--- a/src/Util/Bool.v
+++ b/src/Util/Bool.v
@@ -51,3 +51,9 @@ Definition pull_bool_if_dep {A B} (f : forall b : bool, A b -> B b) (b : bool) (
 Definition pull_bool_if {A B} (f : A -> B) (b : bool) (x : A) (y : A)
   : (if b then f x else f y) = f (if b then x else y)
   := @pull_bool_if_dep (fun _ => A) (fun _ => B) (fun _ => f) b x y.
+
+Definition reflect_iff_gen {P b} : reflect P b -> forall b' : bool, (if b' then P else ~P) <-> b = b'.
+Proof.
+  intros H; apply reflect_iff in H; intro b'; destruct b, b';
+    intuition congruence.
+Qed.
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index a6954663b..b01fe3627 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -111,6 +111,11 @@ Global Instance dec_le_Z : DecidableRel BinInt.Z.le := ZArith_dec.Z_le_dec.
 Global Instance dec_gt_Z : DecidableRel BinInt.Z.gt := ZArith_dec.Z_gt_dec.
 Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec.
 
+Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B}
+       {HD : Decidable (P (fst x) (snd x))}
+  : Decidable (let '(a, b) := x in P a b) | 1.
+Proof. destruct x; assumption. Defined.
+
 Lemma not_not P {d:Decidable P} : not (not P) <-> P.
 Proof. destruct (dec P); intuition. Qed.
 
diff --git a/src/Util/HList.v b/src/Util/HList.v
new file mode 100644
index 000000000..aacefe8f3
--- /dev/null
+++ b/src/Util/HList.v
@@ -0,0 +1,96 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Tuple.
+Require Export Crypto.Util.FixCoqMistakes.
+
+Fixpoint hlist' T n (f : T -> Type) : tuple' T n -> Type :=
+  match n return tuple' _ n -> Type with
+  | 0 => fun T => f T
+  | S n' => fun Ts => (hlist' T n' f (fst Ts) * f (snd Ts))%type
+  end.
+Global Arguments hlist' {T n} f _.
+
+Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type :=
+  match n return tuple _ n -> Type with
+  | 0 => fun _ => unit
+  | S n' => @hlist' T n' f
+  end.
+
+Fixpoint const' {T n F xs} (v : forall x, F x) : @hlist' T n F xs
+  := match n return forall xs, @hlist' T n F xs with
+     | 0 => fun _ => v _
+     | S n' => fun _ => (@const' T n' F _ v, v _)
+     end xs.
+Definition const {T n F xs} (v : forall x, F x) : @hlist T n F xs
+  := match n return forall xs, @hlist T n F xs with
+     | 0 => fun _ => tt
+     | S n' => fun xs => @const' T n' F xs v
+     end xs.
+
+(* tuple map *)
+Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall {ts : tuple' A n}, hlist' F ts -> tuple' B n
+  := match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with
+     | 0 => fun ts v => f _ v
+     | S n' => fun ts v => (@mapt' n' A F B f _ (fst v), f _ (snd v))
+     end.
+Definition mapt {n A F B} (f : forall x : A, F x -> B)
+  : forall {ts : tuple A n}, hlist F ts -> tuple B n
+  := match n return forall ts : tuple A n, hlist F ts -> tuple B n with
+     | 0 => fun ts v => tt
+     | S n' => @mapt' n' A F B f
+     end.
+
+Lemma map'_mapt' {n A F B C} (g : B -> C) (f : forall x : A, F x -> B)
+      {ts : tuple' A n} (ls : hlist' F ts)
+  : Tuple.map (n:=S n) g (mapt' f ls) = mapt' (fun x v => g (f x v)) ls.
+Proof.
+  induction n as [|n IHn]; [ reflexivity | ].
+  { simpl @mapt' in *.
+    rewrite <- IHn.
+    rewrite Tuple.map_S; reflexivity. }
+Qed.
+
+Lemma map_mapt {n A F B C} (g : B -> C) (f : forall x : A, F x -> B)
+      {ts : tuple A n} (ls : hlist F ts)
+  : Tuple.map g (mapt f ls) = mapt (fun x v => g (f x v)) ls.
+Proof.
+  destruct n as [|n]; [ reflexivity | ].
+  apply map'_mapt'.
+Qed.
+
+Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts)
+  : Tuple.map f ts = mapt (fun x _ => f x) ls.
+Proof.
+  destruct n as [|n]; [ reflexivity | ].
+  induction n as [|n IHn]; [ reflexivity | ].
+  { unfold mapt in *; simpl @mapt' in *.
+    rewrite <- IHn; clear IHn.
+    rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. }
+Qed.
+
+Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts)
+  : Tuple.map f ts = mapt' (fun x _ => f x) ls.
+Proof. apply (@map_is_mapt (S n)). Qed.
+
+
+Lemma hlist'_impl {n A F G} (xs:tuple' A n)
+  : (hlist' (fun x => F x -> G x) xs) -> (hlist' F xs -> hlist' G xs).
+Proof.
+  induction n; simpl in *; intuition.
+Defined.
+
+Lemma hlist_impl {n A F G} (xs:tuple A n)
+  : (hlist (fun x => F x -> G x) xs) -> (hlist F xs -> hlist G xs).
+Proof.
+  destruct n; [ constructor | apply hlist'_impl ].
+Defined.
+
+Module Tuple.
+  Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
+  : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
+  Proof.
+  Admitted.
+End Tuple.
diff --git a/src/Util/IffT.v b/src/Util/IffT.v
new file mode 100644
index 000000000..f4eaa9d53
--- /dev/null
+++ b/src/Util/IffT.v
@@ -0,0 +1,10 @@
+Require Import Coq.Classes.RelationClasses.
+Notation iffT A B := (((A -> B) * (B -> A)))%type.
+Notation iffTp := (fun A B => inhabited (iffT A B)).
+
+Global Instance iffTp_Reflexive : Reflexive iffTp | 1.
+Proof. repeat constructor; intro; assumption. Defined.
+Global Instance iffTp_Symmetric : Symmetric iffTp | 1.
+Proof. repeat (intros [?] || intro); constructor; tauto. Defined.
+Global Instance iffTp_Transitive : Transitive iffTp | 1.
+Proof. repeat (intros [?] || intro); constructor; tauto. Defined.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 773fea8fd..d630698e7 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -243,7 +243,7 @@ Proof.
            | _ => solve [ reflexivity | congruence | eauto 99 ]
            | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT))))
            | _ => progress eapply Proper_test_and_op
-           | _ => progress eapply conj
+           | _ => progress split
            | _ => progress (cbv [fst snd pointwise_relation respectful] in * )
            | _ => intro
          end.
diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v
new file mode 100644
index 000000000..ef1567bd8
--- /dev/null
+++ b/src/Util/PartiallyReifiedProp.v
@@ -0,0 +1,165 @@
+(** * Propositions with a distinguished representation of [True], [False], [and], [or], and [impl] *)
+(** This allows for something between [bool] and [Prop], where we can
+    computationally reduce things like [True /\ True], but can still
+    express equality of types. *)
+Require Import Coq.Setoids.Setoid.
+Require Import Coq.Program.Tactics.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.
+
+Delimit Scope reified_prop_scope with reified_prop.
+Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | inject (_ : Prop).
+Bind Scope reified_prop_scope with reified_Prop.
+
+Fixpoint to_prop (x : reified_Prop) : Prop
+  := match x with
+     | rTrue => True
+     | rFalse => False
+     | rAnd x y => to_prop x /\ to_prop y
+     | rOr x y => to_prop x \/ to_prop y
+     | rImpl x y => to_prop x -> to_prop y
+     | @rForall _ f => forall x, to_prop (f x)
+     | @rEq _ x y => x = y
+     | inject x => x
+     end.
+
+Coercion reified_Prop_of_bool (x : bool) : reified_Prop
+  := if x then rTrue else rFalse.
+
+Definition and_reified_Prop (x y : reified_Prop) : reified_Prop
+  := match x, y with
+     | rTrue, y => y
+     | x, rTrue => x
+     | rFalse, y => rFalse
+     | x, rFalse => rFalse
+     | rEq T a b, rEq T' a' b' => rEq (a, a') (b, b')
+     | x', y' => rAnd x' y'
+     end.
+Definition or_reified_Prop (x y : reified_Prop) : reified_Prop
+  := match x, y with
+     | rTrue, y => rTrue
+     | x, rTrue => rTrue
+     | rFalse, y => y
+     | x, rFalse => x
+     | x', y' => rOr x' y'
+     end.
+Definition impl_reified_Prop (x y : reified_Prop) : reified_Prop
+  := match x, y with
+     | rTrue, y => y
+     | x, rTrue => rTrue
+     | rFalse, y => rTrue
+     | rImpl x rFalse, rFalse => x
+     | x', y' => rImpl x' y'
+     end.
+
+Infix "/\" := and_reified_Prop : reified_prop_scope.
+Infix "\/" := or_reified_Prop : reified_prop_scope.
+Infix "->" := impl_reified_Prop : reified_prop_scope.
+Infix "=" := rEq : reified_prop_scope.
+Notation "~ P" := (P -> rFalse)%reified_prop : reified_prop_scope.
+Notation "∀  x .. y , P" := (rForall (fun x => .. (rForall (fun y => P%reified_prop)) .. ))
+                              (at level 200, x binder, y binder, right associativity) : reified_prop_scope.
+
+Definition reified_Prop_eq (x y : reified_Prop)
+  := match x, y with
+     | rTrue, _ => y = rTrue
+     | rFalse, _ => y = rFalse
+     | rAnd x0 x1, rAnd y0 y1
+       => x0 = y0 /\ x1 = y1
+     | rAnd _ _, _ => False
+     | rOr x0 x1, rOr y0 y1
+       => x0 = y0 /\ x1 = y1
+     | rOr _ _, _ => False
+     | rImpl x0 x1, rImpl y0 y1
+       => x0 = y0 /\ x1 = y1
+     | rImpl _ _, _ => False
+     | @rForall Tx fx, @rForall Ty fy
+       => exists pf : Tx = Ty,
+                      forall x, fx x = fy (eq_rect _ (fun t => t) x _ pf)
+     | rForall _ _, _ => False
+     | @rEq Tx x0 x1, @rEq Ty y0 y1
+       => exists pf : Tx = Ty,
+                      eq_rect _ (fun t => t) x0 _ pf = y0
+                      /\ eq_rect _ (fun t => t) x1 _ pf = y1
+     | rEq _ _ _, _ => False
+     | inject x, inject y => x = y
+     | inject _, _ => False
+     end.
+
+Section rel.
+  Local Ltac t :=
+    cbv;
+    repeat (match goal with |- forall x, _ => intro end (* work around broken Ltac [match] in 8.4 that diverges on things under binders *)
+            || break_match
+            || break_match_hyps
+            || intro
+            || (simpl in * )
+            || intuition try congruence
+            || (exists eq_refl)
+            || eauto
+            || (subst * )
+            || apply conj
+            || destruct_head' ex
+            || solve [ apply reflexivity
+                     | apply symmetry; eassumption
+                     | eapply transitivity; eassumption ] ).
+
+  Global Instance Reflexive_reified_Prop_eq : Reflexive reified_Prop_eq.
+  Proof. t. Qed.
+  Global Instance Symmetric_reified_Prop_eq : Symmetric reified_Prop_eq.
+  Proof. t. Qed.
+  Global Instance Transitive_reified_Prop_eq : Transitive reified_Prop_eq.
+  Proof. t. Qed.
+  Global Instance Equivalence_reified_Prop_eq : Equivalence reified_Prop_eq.
+  Proof. split; exact _. Qed.
+End rel.
+
+Definition reified_Prop_leq_to_eq (x y : reified_Prop) : x = y -> reified_Prop_eq x y.
+Proof. intro; subst; simpl; reflexivity. Qed.
+
+Ltac inversion_reified_Prop_step :=
+  let do_on H := apply reified_Prop_leq_to_eq in H; unfold reified_Prop_eq in H in
+  match goal with
+  | [ H : False |- _ ] => solve [ destruct H ]
+  | [ H : (_ = _ :> reified_Prop) /\ (_ = _ :> reified_Prop) |- _ ] => destruct H
+  | [ H : ?x = ?x :> reified_Prop |- _ ] => clear H
+  | [ H : exists pf : _ = _ :> Type, forall x, _ = _ :> reified_Prop |- _ ]
+    => destruct H as [? H]; subst; simpl @eq_rect in H
+  | [ H : ?x = _ :> reified_Prop |- _ ] => is_var x; subst x
+  | [ H : _ = ?y :> reified_Prop |- _ ] => is_var y; subst y
+  | [ H : rTrue = rFalse |- _ ] => solve [ inversion H ]
+  | [ H : rFalse = rTrue |- _ ] => solve [ inversion H ]
+  | [ H : rTrue = _ |- _ ] => do_on H; progress subst
+  | [ H : rFalse = _ |- _ ] => do_on H; progress subst
+  | [ H : rAnd _ _ = _ |- _ ] => do_on H
+  | [ H : rOr _ _ = _ |- _ ] => do_on H
+  | [ H : rImpl _ _ = _ |- _ ] => do_on H
+  | [ H : rForall _ = _ |- _ ] => do_on H
+  | [ H : rEq _ _ = _ |- _ ] => do_on H
+  | [ H : inject _ = _ |- _ ] => do_on H
+  end.
+Ltac inversion_reified_Prop := repeat inversion_reified_Prop_step.
+
+Lemma to_prop_and_reified_Prop x y : to_prop (x /\ y) <-> (to_prop x /\ to_prop y).
+Proof.
+  destruct x, y; simpl; try tauto.
+  { split; intro H; inversion H; subst; repeat split. }
+Qed.
+
+(** Remove all possibly false terms in a reified prop *)
+Fixpoint trueify (p : reified_Prop) : reified_Prop
+  := match p with
+     | rTrue => rTrue
+     | rFalse => rTrue
+     | rAnd x y => rAnd (trueify x) (trueify y)
+     | rOr x y => rOr (trueify x) (trueify y)
+     | rImpl x y => rImpl x (trueify y)
+     | rForall T f => rForall (fun x => trueify (f x))
+     | rEq T x y => rEq x x
+     | inject x => inject True
+     end.
+
+Lemma trueify_true : forall p, to_prop (trueify p).
+Proof.
+  induction p; simpl; auto.
+Qed.
diff --git a/src/Util/Prod.v b/src/Util/Prod.v
index b83aea68f..bcd9404a6 100644
--- a/src/Util/Prod.v
+++ b/src/Util/Prod.v
@@ -5,6 +5,8 @@
     between two such pairs, or when we want such an equality, we have
     a systematic way of reducing such equalities to equalities at
     simpler types. *)
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.IffT.
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.GlobalSettings.
 
@@ -68,6 +70,31 @@ Section prod.
   Definition path_prod_ind {A B u v} (P : u = v :> @prod A B -> Prop) := path_prod_rec P.
 End prod.
 
+Lemma prod_iff_and (A B : Prop) : (A /\ B) <-> (A * B).
+Proof. repeat (intros [? ?] || intro || split); assumption. Defined.
+
+Global Instance iff_prod_Proper
+  : Proper (iff ==> iff ==> iff) (fun A B => prod A B).
+Proof. repeat intro; tauto. Defined.
+Global Instance iff_iffTp_prod_Proper
+  : Proper (iff ==> iffTp ==> iffTp) (fun A B => prod A B) | 1.
+Proof.
+  intros ?? [?] ?? [?]; constructor; tauto.
+Defined.
+Global Instance iffTp_iff_prod_Proper
+  : Proper (iffTp ==> iff ==> iffTp) (fun A B => prod A B) | 1.
+Proof.
+  intros ?? [?] ?? [?]; constructor; tauto.
+Defined.
+Global Instance iffTp_iffTp_prod_Proper
+  : Proper (iffTp ==> iffTp ==> iffTp) (fun A B => prod A B) | 1.
+Proof.
+  intros ?? [?] ?? [?]; constructor; tauto.
+Defined.
+Hint Extern 2 (Proper _ prod) => apply iffTp_iffTp_prod_Proper : typeclass_instances.
+Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffTp_prod_Proper : typeclass_instances.
+Hint Extern 2 (Proper _ (fun A B => prod A B)) => refine iff_prod_Proper : typeclass_instances.
+
 (** ** Useful Tactics *)
 (** *** [inversion_prod] *)
 Ltac simpl_proj_pair_in H :=
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 2f9f6c59f..128fdcfd0 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -109,6 +109,12 @@ Ltac break_match_hyps_when_head_step T :=
                    constr_eq T T').
 Ltac break_match_when_head T := repeat break_match_when_head_step T.
 Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T.
+Ltac break_innermost_match_step :=
+  break_match_step ltac:(fun v => lazymatch v with
+                                  | appcontext[match _ with _ => _ end] => fail
+                                  | _ => idtac
+                                  end).
+Ltac break_innermost_match := repeat break_innermost_match_step.
 
 Ltac free_in x y :=
   idtac;
@@ -481,3 +487,35 @@ Ltac idtac_context :=
        idtac_goal;
        lazymatch goal with |- ?G => idtac "Context:" G end;
        fail).
+
+(** Destruct the convoy pattern ([match e as x return x = e -> _ with _ => _ end eq_refl] *)
+Ltac convoy_destruct_gen T change_in :=
+  let e' := fresh in
+  let H' := fresh in
+  match T with
+  | context G[?f eq_refl]
+    => match f with
+       | match ?e with _ => _ end
+         => pose e as e';
+            match f with
+            | context F[e]
+              => let F' := context F[e'] in
+                 first [ pose (eq_refl : e = e') as H';
+                         let G' := context G[F' H'] in
+                         change_in G';
+                         clearbody H' e'
+                       | pose (eq_refl : e' = e) as H';
+                         let G' := context G[F' H'] in
+                         change_in G';
+                         clearbody H' e' ]
+            end
+       end;
+       destruct e'
+  end.
+
+Ltac convoy_destruct_in H :=
+  let T := type of H in
+  convoy_destruct_gen T ltac:(fun T' => change T' in H).
+Ltac convoy_destruct :=
+  let T := get_goal in
+  convoy_destruct_gen T ltac:(fun T' => change T').
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 2e9f7b0ad..4d97c7857 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1,6 +1,9 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Lists.List.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ListUtil.
 Require Export Crypto.Util.FixCoqMistakes.
@@ -17,6 +20,19 @@ Definition tuple T n : Type :=
   | S n' => tuple' T n'
   end.
 
+Definition tl' {T n} : tuple' T (S n) -> tuple' T n := @fst _ _.
+Definition tl {T n} : tuple T (S n) -> tuple T n :=
+  match n with
+  | O => fun _ => tt
+  | S n' => @tl' T n'
+  end.
+Definition hd' {T n} : tuple' T n -> T :=
+  match n with
+  | O => fun x => x
+  | S n' => @snd _ _
+  end.
+Definition hd {T n} : tuple T (S n) -> T := @hd' _ _.
+
 Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
   match n with
   | 0 => fun x => (x::nil)%list
@@ -136,6 +152,13 @@ Definition on_tuple {A B} (f:list A -> list B)
 Definition map {n A B} (f:A -> B) (xs:tuple A n) : tuple B n
   := on_tuple (List.map f) (fun _ => eq_trans (map_length _ _)) xs.
 
+Lemma map_S {n A B} (f:A -> B) (xs:tuple' A n) (x:A)
+  : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x).
+Proof.
+  unfold map, on_tuple.
+  simpl @List.map.
+Admitted.
+
 Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
            (Hlength : forall la lb, length la = a -> length lb = b -> length (f la lb) = c)
            (ta:tuple A a) (tb:tuple B b) : tuple C c
@@ -145,6 +168,103 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
 Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n
   := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys.
 
+Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n)
+  : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys.
+Proof.
+Admitted.
+
+Lemma map2_fst {n A B C} (f:A -> C) (xs:tuple A n) (ys:tuple B n)
+  : map2 (fun a b => f a) xs ys = map f xs.
+Proof.
+Admitted.
+
+Lemma map2_snd {n A B C} (f:B -> C) (xs:tuple A n) (ys:tuple B n)
+  : map2 (fun a b => f b) xs ys = map f ys.
+Proof.
+Admitted.
+
+Lemma map_id {n A} (xs:tuple A n)
+  : map (fun x => x) xs = xs.
+Proof.
+Admitted.
+
+Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
+  : (forall x, f x = x) -> map f xs = xs.
+Proof.
+Admitted.
+
+Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n)
+  : map g (map f xs) = map (fun x => g (f x)) xs.
+Proof.
+Admitted.
+
+Section monad.
+  Context (M : Type -> Type) (bind : forall X Y, M X -> (X -> M Y) -> M Y) (ret : forall X, X -> M X).
+  Fixpoint lift_monad' {n A} {struct n}
+    : tuple' (M A) n -> M (tuple' A n)
+    := match n return tuple' (M A) n -> M (tuple' A n) with
+       | 0 => fun t => t
+       | S n' => fun xy => bind _ _ (@lift_monad' n' _ (fst xy)) (fun x' => bind _ _ (snd xy) (fun y' => ret _ (x', y')))
+       end.
+  Fixpoint push_monad' {n A} {struct n}
+    : M (tuple' A n) -> tuple' (M A) n
+    := match n return M (tuple' A n) -> tuple' (M A) n with
+       | 0 => fun t => t
+       | S n' => fun xy => (@push_monad' n' _ (bind _ _ xy (fun xy' => ret _ (fst xy'))),
+                            bind _ _ xy (fun xy' => ret _ (snd xy')))
+       end.
+  Definition lift_monad {n A}
+    : tuple (M A) n -> M (tuple A n)
+    := match n return tuple (M A) n -> M (tuple A n) with
+       | 0 => ret _
+       | S n' => @lift_monad' n' A
+       end.
+  Definition push_monad {n A}
+    : M (tuple A n) -> tuple (M A) n
+    := match n return M (tuple A n) -> tuple (M A) n with
+       | 0 => fun _ => tt
+       | S n' => @push_monad' n' A
+       end.
+End monad.
+Local Notation option_bind
+  := (fun A B (x : option A) f => match x with
+                                  | Some x' => f x'
+                                  | None => None
+                                  end).
+Definition lift_option {n A} (xs : tuple (option A) n) : option (tuple A n)
+  := lift_monad option option_bind (@Some) xs.
+Definition push_option {n A} (xs : option (tuple A n)) : tuple (option A) n
+  := push_monad option option_bind (@Some) xs.
+
+Lemma lift_push_option {n A} (xs : option (tuple A (S n))) : lift_option (push_option xs) = xs.
+Proof.
+  simpl in *.
+  induction n; [ reflexivity | ].
+  simpl in *; rewrite IHn; clear IHn.
+  destruct xs as [ [? ?] | ]; reflexivity.
+Qed.
+
+Lemma push_lift_option {n A} {xs : tuple (option A) (S n)} {v}
+  : lift_option xs = Some v <-> xs = push_option (Some v).
+Proof.
+  simpl in *.
+  induction n; [ reflexivity | ].
+  specialize (IHn (fst xs) (fst v)).
+  repeat first [ progress destruct_head_hnf' prod
+               | progress destruct_head_hnf' and
+               | progress destruct_head_hnf' iff
+               | progress destruct_head_hnf' option
+               | progress inversion_option
+               | progress inversion_prod
+               | progress subst
+               | progress break_match
+               | progress simpl in *
+               | progress specialize_by exact eq_refl
+               | reflexivity
+               | split
+               | intro ].
+Qed.
+
 Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop.
   destruct n; simpl @tuple' in *.
   { exact (R a b). }
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 36fd21d28..24160d83e 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -34,6 +34,15 @@ Proof.
   auto.
 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 wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
   wordToN (NToWord sz n) = n.
 Proof.
@@ -364,3 +373,289 @@ Proof.
 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).
+
+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.
+  destruct B0 as [? B0], B1 as [? B1], B0, B1.
+  repeat split; [add_mono| |]; (
+    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.
+  destruct B0 as [? B0], B1 as [? B1], B0, B1.
+  repeat split; [sub_mono| |]; (
+   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.
+  destruct B0 as [? B0], B1 as [? B1], B0, B1.
+  repeat split; [mul_mono| |]; (
+    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.
+  destruct B0 as [? B0], B1 as [? B1], B0, B1.
+  repeat split; [reflexivity| |].
+
+  - rewrite wordToN_wand; [solve_land_ge0|solve_land_ge0|].
+    eapply Z.le_lt_trans; [apply Z.log2_land; land_mono|];
+      eapply Z.le_lt_trans; [| eassumption];
+      repeat match goal with
+      | [|- context[Z.min ?a ?b]] =>
+        destruct (Z.min_dec a b) as [g|g]; rewrite g; clear g
+      end; apply Z.log2_le_mono; try assumption.
+
+    admit. admit.
+
+  - rewrite wordToN_wand; [|solve_land_ge0|].
+    eapply Z.le_lt_trans; [apply Z.log2_land; land_mono|];
+      match goal with
+      | [|- (Z.min ?a ?b < _)%Z] =>
+        destruct (Z.min_dec a b) as [g|g]; rewrite g; clear g
+      end.
+
+  .
+  (*
+[apply N2Z.is_nonneg|];
+      unfold Word64.word64ToZ; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id;
+      rewrite wordize_and.
+
+    destruct (Z_ge_dec upper1 upper0) as [g|g].
+
+    - rewrite Z.min_r; [|abstract (apply Z.log2_le_mono; omega)].
+      abstract (
+        rewrite (land_intro_ones (wordToN value0));
+        rewrite N.land_assoc;
+        etransitivity; [apply N2Z.inj_le; apply N.lt_le_incl; apply land_lt_Npow2|];
+        rewrite N2Z.inj_pow;
+        apply Z.pow_le_mono; [abstract (split; cbn; [omega|reflexivity])|];
+        unfold getBits; rewrite N2Z.inj_succ;
+        apply -> Z.succ_le_mono;
+        rewrite <- (N2Z.id (wordToN value0)), <- log2_conv;
+        apply Z.log2_le_mono;
+        etransitivity; [eassumption|reflexivity]).
+
+    - rewrite Z.min_l; [|abstract (apply Z.log2_le_mono; omega)].
+      abstract (
+        rewrite (land_intro_ones (wordToN value1));
+        rewrite <- N.land_comm, N.land_assoc;
+        etransitivity; [apply N2Z.inj_le; apply N.lt_le_incl; apply land_lt_Npow2|];
+        rewrite N2Z.inj_pow;
+        apply Z.pow_le_mono; [abstract (split; cbn; [omega|reflexivity])|];
+        unfold getBits; rewrite N2Z.inj_succ;
+        apply -> Z.succ_le_mono;
+        rewrite <- (N2Z.id (wordToN value1)), <- log2_conv;
+        apply Z.log2_le_mono;
+        etransitivity; [eassumption|reflexivity]).
+
+*)
+Admitted.
+
+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 (u0+1)) (Z.log2 (u1+1))) - 1)%Z.
+Proof.
+(*      unfold Word64.word64ToZ in *; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id;
+      rewrite wordize_or.
+
+    - transitivity (Z.max (Z.of_N (wordToN value1)) (Z.of_N (wordToN value0)));
+      [ abstract (destruct
+          (Z_ge_dec lower1 lower0) as [l|l],
+          (Z_ge_dec (Z.of_N (& value1)%w) (Z.of_N (& value0)%w)) as [v|v];
+        [ rewrite Z.max_l, Z.max_l | rewrite Z.max_l, Z.max_r
+        | rewrite Z.max_r, Z.max_l | rewrite Z.max_r, Z.max_r ];
+        
+        try (omega || assumption))
+      | ].
+
+      rewrite <- N2Z.inj_max.
+      apply Z2N.inj_le; [apply N2Z.is_nonneg|apply N2Z.is_nonneg|].
+      repeat rewrite N2Z.id.
+
+      abstract (
+        destruct (N.max_dec (wordToN value1) (wordToN value0)) as [v|v];
+        rewrite v;
+        apply N.ldiff_le, N.bits_inj_iff; intros k;
+        rewrite N.ldiff_spec, N.lor_spec;
+        induction (N.testbit (wordToN value1)), (N.testbit (wordToN value0)); simpl;
+        reflexivity).
+
+    - apply Z.lt_le_incl, Z.log2_lt_cancel.
+      rewrite Z.log2_pow2; [| abstract (
+        destruct (Z.max_dec (Z.log2 upper1) (Z.log2 upper0)) as [g|g];
+        rewrite g; apply Z.le_le_succ_r, Z.log2_nonneg)].
+
+      eapply (Z.le_lt_trans _ (Z.log2 (Z.lor _ _)) _).
+
+      + apply Z.log2_le_mono, Z.eq_le_incl.
+        apply Z.bits_inj_iff'; intros k Hpos.
+        rewrite Z2N.inj_testbit, Z.lor_spec, N.lor_spec; [|assumption].
+        repeat (rewrite <- Z2N.inj_testbit; [|assumption]).
+        reflexivity.
+
+      + abstract (
+          rewrite Z.log2_lor; [|trans'|trans'];
+          destruct
+            (Z_ge_dec (Z.of_N (wordToN value1)) (Z.of_N (wordToN value0))) as [g0|g0],
+            (Z_ge_dec upper1 upper0) as [g1|g1];
+            [ rewrite Z.max_l, Z.max_l
+            | rewrite Z.max_l, Z.max_r
+            | rewrite Z.max_r, Z.max_l
+            | rewrite Z.max_r, Z.max_r];
+            try apply Z.log2_le_mono; try omega;
+            apply Z.le_succ_l;
+            apply -> Z.succ_le_mono;
+            apply Z.log2_le_mono;
+            assumption || (etransitivity; [eassumption|]; omega)).
+*)
+Admitted.
+
+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.
+  (*
+    Ltac shr_mono := etransitivity;
+      [apply Z.div_le_compat_l | apply Z.div_le_mono].
+
+    assert (forall x, (0 <= x)%Z -> (0 < 2^x)%Z) as gt0. {
+      intros; rewrite <- (Z2Nat.id x); [|assumption].
+      induction (Z.to_nat x) as [|n]; [cbv; auto|].
+      eapply Z.lt_le_trans; [eassumption|rewrite Nat2Z.inj_succ].
+      apply Z.pow_le_mono_r; [cbv; auto|omega].
+    }
+
+    build_binop Word64.w64shr ZBounds.shr; t_start; abstract (
+      unfold Word64.word64ToZ; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id;
+      rewrite Z.shiftr_div_pow2 in *;
+      repeat match goal with
+      | [|- _ /\ _ ] => split
+      | [|- (0 <= 2 ^ _)%Z ] => apply Z.pow_nonneg
+      | [|- (0 < 2 ^ ?X)%Z ] => apply gt0
+      | [|- (0 <= _ / _)%Z ] => apply Z.div_le_lower_bound; [|rewrite Z.mul_0_r]
+      | [|- (2 ^ _ <= 2 ^ _)%Z ] => apply Z.pow_le_mono_r
+      | [|- context[(?a >> ?b)%Z]] => rewrite Z.shiftr_div_pow2 in *
+      | [|- (_ < Npow2 _)%N] => 
+        apply N2Z.inj_lt, Z.log2_lt_cancel; simpl;
+        eapply Z.le_lt_trans; [|eassumption]; apply Z.log2_le_mono; rewrite Z2N.id
+
+      | _ => progress shr_mono
+      | _ => progress trans'
+      | _ => progress omega
+      end).
+
+*)
+Admitted.
+
+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.
+  (*
+    Ltac shl_mono := etransitivity;
+      [apply Z.mul_le_mono_nonneg_l | apply Z.mul_le_mono_nonneg_r].
+
+    build_binop Word64.w64shl ZBounds.shl; t_start; abstract (
+      unfold Word64.word64ToZ; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id;
+      rewrite Z.shiftl_mul_pow2 in *;
+      repeat match goal with
+      | [|- (0 <= 2 ^ _)%Z ] => apply Z.pow_nonneg
+      | [|- (0 <= _ * _)%Z ] => apply Z.mul_nonneg_nonneg
+      | [|- (2 ^ _ <= 2 ^ _)%Z ] => apply Z.pow_le_mono_r
+      | [|- context[(?a << ?b)%Z]] => rewrite Z.shiftl_mul_pow2
+      | [|- (_ < Npow2 _)%N] => 
+        apply N2Z.inj_lt, Z.log2_lt_cancel; simpl;
+        eapply Z.le_lt_trans; [|eassumption]; apply Z.log2_le_mono; rewrite Z2N.id
+
+      | _ => progress shl_mono
+      | _ => progress trans'
+      | _ => progress omega
+      end).
+
+*)
+Admitted.
+
+
+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)),
+    @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
+Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a.
+Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 5417c3407..d6ffa4a53 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -4,6 +4,7 @@ Require Import Coq.Structures.Equalities.
 Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Notations.
 Require Import Coq.Lists.List.
 Require Export Crypto.Util.FixCoqMistakes.
@@ -21,6 +22,8 @@ Hint Extern 1 => nia : nia.
 Hint Extern 1 => omega : omega.
 Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos Zmult_lt_compat_r Z.pow_le_mono_r Z.pow_le_mono_l Z.div_lt : zarith.
 Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith.
+Hint Resolve (fun n m => proj1 (Z.pred_le_mono n m)) : zarith.
+Hint Resolve (fun a b => proj2 (Z.lor_nonneg a b)) : zarith.
 
 Ltac zutil_arith := solve [ omega | lia | auto with nocore ].
 Ltac zutil_arith_more_inequalities := solve [ zutil_arith | auto with zarith ].
@@ -1083,6 +1086,21 @@ Module Z.
     inversion H; trivial.
   Qed.
 
+  Lemma ones_le x y : x <= y -> Z.ones x <= Z.ones y.
+  Proof.
+    rewrite !Z.ones_equiv; auto with zarith.
+  Qed.
+  Hint Resolve ones_le : zarith.
+
+  Lemma geb_spec0 : forall x y : Z, Bool.reflect (x >= y) (x >=? y).
+  Proof.
+    intros x y; pose proof (Zge_cases x y) as H; destruct (Z.geb x y); constructor; omega.
+  Qed.
+  Lemma gtb_spec0 : forall x y : Z, Bool.reflect (x > y) (x >? y).
+  Proof.
+    intros x y; pose proof (Zgt_cases x y) as H; destruct (Z.gtb x y); constructor; omega.
+  Qed.
+
   Ltac ltb_to_lt_with_hyp H lem :=
     let H' := fresh in
     rename H into H';
@@ -1090,6 +1108,10 @@ Module Z.
     rewrite H' in H;
     clear H'.
 
+  Ltac ltb_to_lt_in_goal b' lem :=
+    refine (proj1 (@reflect_iff_gen _ _ lem b') _);
+    cbv beta iota.
+
   Ltac ltb_to_lt :=
     repeat match goal with
            | [ H : (?x <? ?y) = ?b |- _ ]
@@ -1102,6 +1124,16 @@ Module Z.
              => ltb_to_lt_with_hyp H (Zge_cases x y)
            | [ H : (?x =? ?y) = ?b |- _ ]
              => ltb_to_lt_with_hyp H (eqb_cases x y)
+           | [ |- (?x <? ?y) = ?b ]
+             => ltb_to_lt_in_goal b (Z.ltb_spec0 x y)
+           | [ |- (?x <=? ?y) = ?b ]
+             => ltb_to_lt_in_goal b (Z.leb_spec0 x y)
+           | [ |- (?x >? ?y) = ?b ]
+             => ltb_to_lt_in_goal b (Z.gtb_spec0 x y)
+           | [ |- (?x >=? ?y) = ?b ]
+             => ltb_to_lt_in_goal b (Z.geb_spec0 x y)
+           | [ |- (?x =? ?y) = ?b ]
+             => ltb_to_lt_in_goal b (Z.eqb_spec x y)
            end.
 
   Ltac compare_to_sgn :=
@@ -2054,6 +2086,57 @@ Module Z.
   Qed.
   Hint Resolve shiftr_nonneg_le : zarith.
 
+  Lemma log2_pred_pow2_full a : Z.log2 (Z.pred (2^a)) = Z.max 0 (Z.pred a).
+  Proof.
+    destruct (Z_dec 0 a) as [ [?|?] | ?].
+    { rewrite Z.log2_pred_pow2 by assumption.
+      apply Z.max_case_strong; omega. }
+    { autorewrite with zsimplify; simpl.
+      apply Z.max_case_strong; omega. }
+    { subst; compute; reflexivity. }
+  Qed.
+  Hint Rewrite log2_pred_pow2_full : zsimplify.
+
+  Lemma ones_lt_pow2 x y : 0 <= x <= y -> Z.ones x < 2^y.
+  Proof.
+    rewrite Z.ones_equiv, Z.lt_pred_le.
+    auto with zarith.
+  Qed.
+  Hint Resolve ones_lt_pow2 : zarith.
+
+  Lemma log2_ones_full x : Z.log2 (Z.ones x) = Z.max 0 (Z.pred x).
+  Proof.
+    rewrite Z.ones_equiv, log2_pred_pow2_full; reflexivity.
+  Qed.
+  Hint Rewrite log2_ones_full : zsimplify.
+
+  Lemma log2_ones_lt x y : 0 < x <= y -> Z.log2 (Z.ones x) < y.
+  Proof.
+    rewrite log2_ones_full; apply Z.max_case_strong; omega.
+  Qed.
+  Hint Resolve log2_ones_lt : zarith.
+
+  Lemma log2_ones_le x y : 0 <= x <= y -> Z.log2 (Z.ones x) <= y.
+  Proof.
+    rewrite log2_ones_full; apply Z.max_case_strong; omega.
+  Qed.
+  Hint Resolve log2_ones_le : zarith.
+
+  Lemma log2_ones_lt_nonneg x y : 0 < y -> x <= y -> Z.log2 (Z.ones x) < y.
+  Proof.
+    rewrite log2_ones_full; apply Z.max_case_strong; omega.
+  Qed.
+  Hint Resolve log2_ones_lt_nonneg : zarith.
+
+  Lemma log2_lt_pow2_alt a b : 0 < b -> a < 2^b <-> Z.log2 a < b.
+  Proof.
+    destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; [].
+    rewrite Z.log2_nonpos by omega.
+    split; auto with zarith; [].
+    intro; eapply le_lt_trans; [ eassumption | ].
+    auto with zarith.
+  Qed.
+
   Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y.
   Proof. lia. Qed.
   Hint Rewrite simplify_twice_sub_sub : zsimplify.
@@ -2828,6 +2911,44 @@ for name in names:
   Module RemoveEquivModuloInstances (dummy : Nop).
     Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances.
   End RemoveEquivModuloInstances.
+
+  Module N2Z.
+    Require Import Coq.NArith.NArith.
+
+    Lemma 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 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.
+  End N2Z.
 End Z.
 
 Module Export BoundsTactics.