Split off ZRange lemmas

8 files changed, 377 insertions, 307 deletions

diff --git a/_CoqProject b/_CoqProject
index fa0dcff31..41790980e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6543,6 +6543,8 @@ src/Util/Tactics/UnfoldArg.v
 src/Util/Tactics/UnifyAbstractReflexivity.v
 src/Util/Tactics/UniquePose.v
 src/Util/Tactics/VM.v
+src/Util/ZRange/BasicLemmas.v
+src/Util/ZRange/CornersMonotoneBounds.v
 src/Util/ZRange/Operations.v
 src/Util/ZUtil/AddGetCarry.v
 src/Util/ZUtil/CPS.v
@@ -6583,6 +6585,7 @@ src/Util/ZUtil/Tactics/PullPush.v
 src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
 src/Util/ZUtil/Tactics/RewriteModSmall.v
 src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
+src/Util/ZUtil/Tactics/SplitMinMax.v
 src/Util/ZUtil/Tactics/ZeroBounds.v
 src/Util/ZUtil/Tactics/Ztestbit.v
 src/Util/ZUtil/Tactics/PullPush/Modulo.v
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index 11539d014..e37b64a09 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -6,6 +6,7 @@ Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.Tactics.DestructHead.
 Export Compilers.Syntax.Notations.
@@ -26,31 +27,12 @@ Module Import Bounds.
 
   Section ops.
     (** Generic helper definitions *)
-    Definition two_corners (f : Z -> Z) : t -> t
-      := fun x
-         => let (lx, ux) := x in
-            {| lower := Z.min (f lx) (f ux);
-               upper := Z.max (f lx) (f ux) |}.
-    Definition four_corners (f : Z -> Z -> Z) : t -> t -> t
-      := fun x y
-         => let (lx, ux) := x in
-            let (lfl, ufl) := two_corners (f lx) y in
-            let (lfu, ufu) := two_corners (f ux) y in
-            {| lower := Z.min lfl lfu;
-               upper := Z.max ufl ufu |}.
-    Definition eight_corners (f : Z -> Z -> Z -> Z) : t -> t -> t -> t
-      := fun x y z
-         => let (lx, ux) := x in
-            let (lfl, ufl) := four_corners (f lx) y z in
-            let (lfu, ufu) := four_corners (f ux) y z in
-            {| lower := Z.min lfl lfu;
-               upper := Z.max ufl ufu |}.
     Definition t_map1 (f : Z -> Z) : t -> t
-      := fun x => two_corners f x.
+      := fun x => ZRange.two_corners f x.
     Definition t_map2 (f : Z -> Z -> Z) : t -> t -> t
-      := fun x y => four_corners f x y.
+      := fun x y => ZRange.four_corners f x y.
     Definition t_map3 (f : Z -> Z -> Z -> Z) : t -> t -> t -> t
-      := fun x y z => eight_corners f x y z.
+      := fun x y z => ZRange.eight_corners f x y z.
     (** Definitions of the actual bounds propogation *)
     (** Rules for adding new operations:
 
@@ -64,7 +46,7 @@ Module Import Bounds.
     Definition shl : t -> t -> t := t_map2 Z.shiftl.
     Definition shr : t -> t -> t := t_map2 Z.shiftr.
     Definition max_abs_bound (x : t) : Z
-      := Z.max (Z.abs (lower x)) (Z.abs (upper x)).
+      := upper (ZRange.abs x).
     Definition upper_lor_and_bounds (x y : Z) : Z
       := 2^(1 + Z.log2_up (Z.max x y)).
     Definition extreme_lor_land_bounds (x y : t) : t
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index 0c709abe9..ba0582827 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -7,6 +7,7 @@ Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
 Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Stabilization.
 Require Import Crypto.Util.ZUtil.MulSplit.
@@ -17,6 +18,7 @@ Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
 
 Local Open Scope Z_scope.
 
@@ -46,230 +48,6 @@ Proof.
   subst; eauto.
 Qed.
 
-Lemma monotone_two_corners_genb
-      (f : Z -> Z)
-      (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-      (Hmonotone : exists b, Proper (R b ==> Z.le) f)
-      x_bs x
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-  : ZRange.is_bounded_by' None (Bounds.two_corners f x_bs) (f x).
-Proof.
-  unfold ZRange.is_bounded_by' in *; split; trivial.
-  destruct x_bs as [lx ux]; simpl in *.
-  destruct Hboundedx as [Hboundedx _].
-  destruct_head'_ex.
-  repeat match goal with
-         | [ H : Proper (R ?b ==> Z.le) f |- _ ]
-           => unique assert (R b (if b then lx else x) (if b then x else lx)
-                             /\ R b (if b then x else ux) (if b then ux else x))
-             by (unfold R, Basics.flip; destruct b; omega)
-         end.
-  destruct_head' and.
-  repeat match goal with
-         | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
-           => unique pose proof (H _ _ H')
-         end.
-  destruct_head bool; split_min_max; omega.
-Qed.
-
-Lemma monotone_two_corners_gen
-      (f : Z -> Z)
-      (Hmonotone : Proper (Z.le ==> Z.le) f \/ Proper (Basics.flip Z.le ==> Z.le) f)
-      x_bs x
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-  : ZRange.is_bounded_by' None (Bounds.two_corners f x_bs) (f x).
-Proof.
-  eapply monotone_two_corners_genb; auto.
-  destruct Hmonotone; [ exists true | exists false ]; assumption.
-Qed.
-Lemma monotone_two_corners
-      (b : bool)
-      (f : Z -> Z)
-      (R := if b then Z.le else Basics.flip Z.le)
-      (Hmonotone : Proper (R ==> Z.le) f)
-      x_bs x
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-  : ZRange.is_bounded_by' None (Bounds.two_corners f x_bs) (f x).
-Proof.
-  apply monotone_two_corners_genb; auto; subst R;
-    exists b.
-  intros ???; apply Hmonotone; auto.
-Qed.
-
-Lemma monotone_four_corners_genb
-      (f : Z -> Z -> Z)
-      (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-      (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (f x))
-      (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y))
-      x_bs y_bs x y
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-      (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-  : ZRange.is_bounded_by' None (Bounds.four_corners f x_bs y_bs) (f x y).
-Proof.
-  destruct x_bs as [lx ux], y_bs as [ly uy].
-  unfold Bounds.four_corners.
-  pose proof (monotone_two_corners_genb (f lx) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fl.
-  pose proof (monotone_two_corners_genb (f ux) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fu.
-  repeat match goal with
-         | [ |- context[Bounds.two_corners ?x ?y] ]
-           => let l := fresh "lf" in
-              let u := fresh "uf" in
-              generalize dependent (Bounds.two_corners x y); intros [l u]; intros
-         end.
-  unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial.
-  destruct_head'_and; destruct_head' True.
-  pose proof (Hmonotone2 y).
-  destruct_head'_ex.
-  repeat match goal with
-         | [ H : Proper (R ?b ==> Z.le) (f _) |- _ ]
-           => unique assert (R b (if b then ly else y) (if b then y else ly)
-                             /\ R b (if b then y else uy) (if b then uy else y))
-             by (unfold R, Basics.flip; destruct b; omega)
-         | [ H : Proper (R ?b ==> Z.le) (fun x => f x _) |- _ ]
-           => unique assert (R b (if b then lx else x) (if b then x else lx)
-                             /\ R b (if b then x else ux) (if b then ux else x))
-             by (unfold R, Basics.flip; destruct b; omega)
-         end.
-  destruct_head' and.
-  repeat match goal with
-         | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
-           => unique pose proof (H _ _ H')
-         end; cbv beta in *.
-  destruct_head bool; split_min_max; omega.
-Qed.
-
-Lemma monotone_four_corners_gen
-      (f : Z -> Z -> Z)
-      (Hmonotone1 : forall x, Proper (Z.le ==> Z.le) (f x) \/ Proper (Basics.flip Z.le ==> Z.le) (f x))
-      (Hmonotone2 : forall y, Proper (Z.le ==> Z.le) (fun x => f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y))
-      x_bs y_bs x y
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-      (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-  : ZRange.is_bounded_by' None (Bounds.four_corners f x_bs y_bs) (f x y).
-Proof.
-  eapply monotone_four_corners_genb; auto.
-  { intro x'; destruct (Hmonotone1 x'); [ exists true | exists false ]; assumption. }
-  { intro x'; destruct (Hmonotone2 x'); [ exists true | exists false ]; assumption. }
-Qed.
-Lemma monotone_four_corners
-      (b1 b2 : bool)
-      (f : Z -> Z -> Z)
-      (R1 := if b1 then Z.le else Basics.flip Z.le) (R2 := if b2 then Z.le else Basics.flip Z.le)
-      (Hmonotone : Proper (R1 ==> R2 ==> Z.le) f)
-      x_bs y_bs x y
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-      (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-  : ZRange.is_bounded_by' None (Bounds.four_corners f x_bs y_bs) (f x y).
-Proof.
-  apply monotone_four_corners_genb; auto; intro x'; subst R1 R2;
-    [ exists b2 | exists b1 ];
-    [ eapply (Hmonotone x' x'); destruct b1; reflexivity
-    | intros ???; apply Hmonotone; auto; destruct b2; reflexivity ].
-Qed.
-
-Lemma monotone_eight_corners_genb
-      (f : Z -> Z -> Z -> Z)
-      (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-      (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (f x y))
-      (Hmonotone2 : forall x z, exists b, Proper (R b ==> Z.le) (fun y => f x y z))
-      (Hmonotone3 : forall y z, exists b, Proper (R b ==> Z.le) (fun x => f x y z))
-      x_bs y_bs z_bs x y z
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-      (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-      (Hboundedz : ZRange.is_bounded_by' None z_bs z)
-  : ZRange.is_bounded_by' None (Bounds.eight_corners f x_bs y_bs z_bs) (f x y z).
-Proof.
-  destruct x_bs as [lx ux], y_bs as [ly uy], z_bs as [lz uz].
-  unfold Bounds.eight_corners.
-  pose proof (monotone_four_corners_genb (f lx) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fl.
-  pose proof (monotone_four_corners_genb (f ux) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fu.
-  repeat match goal with
-         | [ |- context[Bounds.four_corners ?x ?y ?z] ]
-           => let l := fresh "lf" in
-              let u := fresh "uf" in
-              generalize dependent (Bounds.four_corners x y z); intros [l u]; intros
-         end.
-  unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial.
-  destruct_head'_and; destruct_head' True.
-  pose proof (Hmonotone3 y z).
-  destruct_head'_ex.
-  repeat match goal with
-         | [ H : Proper (R ?b ==> Z.le) (f _ _) |- _ ]
-           => unique assert (R b (if b then lz else z) (if b then z else lz)
-                             /\ R b (if b then z else uz) (if b then uz else z))
-             by (unfold R, Basics.flip; destruct b; omega)
-         | [ H : Proper (R ?b ==> Z.le) (fun y' => f _ y' _) |- _ ]
-           => unique assert (R b (if b then ly else y) (if b then y else ly)
-                             /\ R b (if b then y else uy) (if b then uy else y))
-             by (unfold R, Basics.flip; destruct b; omega)
-         | [ H : Proper (R ?b ==> Z.le) (fun x' => f x' _ _) |- _ ]
-           => unique assert (R b (if b then lx else x) (if b then x else lx)
-                             /\ R b (if b then x else ux) (if b then ux else x))
-             by (unfold R, Basics.flip; destruct b; omega)
-         end.
-  destruct_head' and.
-  repeat match goal with
-         | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
-           => unique pose proof (H _ _ H')
-         end.
-  destruct_head bool; split_min_max; omega.
-Qed.
-
-Lemma monotone_eight_corners_gen
-      (f : Z -> Z -> Z -> Z)
-      (Hmonotone1 : forall x y, Proper (Z.le ==> Z.le) (f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (f x y))
-      (Hmonotone2 : forall x z, Proper (Z.le ==> Z.le) (fun y => f x y z) \/ Proper (Basics.flip Z.le ==> Z.le) (fun y => f x y z))
-      (Hmonotone3 : forall y z, Proper (Z.le ==> Z.le) (fun x => f x y z) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y z))
-      x_bs y_bs z_bs x y z
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-      (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-      (Hboundedz : ZRange.is_bounded_by' None z_bs z)
-  : ZRange.is_bounded_by' None (Bounds.eight_corners f x_bs y_bs z_bs) (f x y z).
-Proof.
-  eapply monotone_eight_corners_genb; auto.
-  { intros x' y'; destruct (Hmonotone1 x' y'); [ exists true | exists false ]; assumption. }
-  { intros x' y'; destruct (Hmonotone2 x' y'); [ exists true | exists false ]; assumption. }
-  { intros x' y'; destruct (Hmonotone3 x' y'); [ exists true | exists false ]; assumption. }
-Qed.
-Lemma monotone_eight_corners
-      (b1 b2 b3 : bool)
-      (f : Z -> Z -> Z -> Z)
-      (R1 := if b1 then Z.le else Basics.flip Z.le)
-      (R2 := if b2 then Z.le else Basics.flip Z.le)
-      (R3 := if b3 then Z.le else Basics.flip Z.le)
-      (Hmonotone : Proper (R1 ==> R2 ==> R3 ==> Z.le) f)
-      x_bs y_bs z_bs x y z
-      (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-      (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-      (Hboundedz : ZRange.is_bounded_by' None z_bs z)
-  : ZRange.is_bounded_by' None (Bounds.eight_corners f x_bs y_bs z_bs) (f x y z).
-Proof.
-  apply monotone_eight_corners_genb; auto; intro x'; subst R1 R2 R3;
-    [ exists b3 | exists b2 | exists b1 ];
-    intros ???; apply Hmonotone; break_innermost_match; try reflexivity; trivial.
-Qed.
-
-Lemma monotonify2 (f : Z -> Z -> Z) (upper : Z -> Z -> Z)
-      (Hbounded : forall a b, Z.abs (f a b) <= upper (Z.abs a) (Z.abs b))
-      (Hupper_monotone : Proper (Z.le ==> Z.le ==> Z.le) upper)
-      {xb yb x y}
-      (Hboundedx : ZRange.is_bounded_by' None xb x)
-      (Hboundedy : ZRange.is_bounded_by' None yb y)
-  : ZRange.is_bounded_by'
-      None
-      {| ZRange.lower := -upper (Bounds.max_abs_bound xb) (Bounds.max_abs_bound yb);
-         ZRange.upper := upper (Bounds.max_abs_bound xb) (Bounds.max_abs_bound yb) |}
-      (f x y).
-Proof.
-  split; [ | exact I ]; simpl.
-  apply Z.abs_le.
-  destruct Hboundedx as [Hx _], Hboundedy as [Hy _].
-  etransitivity; [ apply Hbounded | ].
-  apply Hupper_monotone;
-    unfold Bounds.max_abs_bound;
-    repeat (apply Z.max_case_strong || apply Zabs_ind); omega.
-Qed.
-
 Local Existing Instances Z.log2_up_le_Proper Z.add_le_Proper Z.sub_with_borrow_le_Proper.
 Lemma land_upper_lor_land_bounds a b
   : Z.abs (Z.land a b) <= Bounds.upper_lor_and_bounds (Z.abs a) (Z.abs b).
@@ -305,7 +83,7 @@ Lemma land_bounds_extreme xb yb x y
       (Hy : ZRange.is_bounded_by' None yb y)
   : ZRange.is_bounded_by' None (Bounds.extreme_lor_land_bounds xb yb) (Z.land x y).
 Proof.
-  apply monotonify2; auto;
+  apply ZRange.monotonify2; auto;
     unfold Bounds.extreme_lor_land_bounds;
     [ apply land_upper_lor_land_bounds
     | apply upper_lor_and_bounds_Proper ].
@@ -315,7 +93,7 @@ Lemma lor_bounds_extreme xb yb x y
       (Hy : ZRange.is_bounded_by' None yb y)
   : ZRange.is_bounded_by' None (Bounds.extreme_lor_land_bounds xb yb) (Z.lor x y).
 Proof.
-  apply monotonify2; auto;
+  apply ZRange.monotonify2; auto;
     unfold Bounds.extreme_lor_land_bounds;
     [ apply lor_upper_lor_land_bounds
     | apply upper_lor_and_bounds_Proper ].
@@ -341,7 +119,7 @@ Local Ltac apply_is_bounded_by_truncation_bounds :=
     => apply is_bounded_by_truncation_bounds'
   end.
 Local Ltac handle_mul :=
-  apply monotone_four_corners_genb; try (split; auto);
+  apply ZRange.monotone_four_corners_genb; try (split; auto);
   unfold Basics.flip;
   let x := fresh "x" in
   intro x;
@@ -383,13 +161,13 @@ Proof.
                      => generalize dependent (interpToZ x); clear x; intros
                    | [ |- _ /\ True ] => split; [ | tauto ]
                    end ].
-  { apply (@monotone_four_corners true true _ _); split; auto. }
-  { apply (@monotone_four_corners true false _ _); split; auto. }
+  { apply (@ZRange.monotone_four_corners true true _ _); split; auto. }
+  { apply (@ZRange.monotone_four_corners true false _ _); split; auto. }
   { handle_mul. }
-  { apply monotone_four_corners_genb; try (split; auto);
+  { apply ZRange.monotone_four_corners_genb; try (split; auto);
       [ eexists; apply Z.shiftl_le_Proper1
       | exists true; apply Z.shiftl_le_Proper2 ]. }
-  { apply monotone_four_corners_genb; try (split; auto);
+  { apply ZRange.monotone_four_corners_genb; try (split; auto);
       [ eexists; apply Z.shiftr_le_Proper1
       | exists true; apply Z.shiftr_le_Proper2 ]. }
   { cbv [Bounds.land Bounds.extremization_bounds]; break_innermost_match;
@@ -419,14 +197,14 @@ Proof.
   { apply Z.mod_bound_min_max; auto. }
   { handle_mul. }
   { auto with zarith. }
-  { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
-  { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
+  { apply (@ZRange.monotone_eight_corners true true true _ _ _); split; auto. }
+  { apply (@ZRange.monotone_eight_corners true true true _ _ _); split; auto. }
   { apply Z.mod_bound_min_max; auto. }
-  { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
+  { apply (@ZRange.monotone_eight_corners true true true _ _ _); split; auto. }
   { auto with zarith. }
-  { apply (@monotone_eight_corners false true false _ _ _); split; auto. }
-  { apply (@monotone_eight_corners false true false _ _ _); split; auto. }
+  { apply (@ZRange.monotone_eight_corners false true false _ _ _); split; auto. }
+  { apply (@ZRange.monotone_eight_corners false true false _ _ _); split; auto. }
   { apply Z.mod_bound_min_max; auto. }
-  { apply (@monotone_eight_corners false true false _ _ _); split; auto. }
+  { apply (@ZRange.monotone_eight_corners false true false _ _ _); split; auto. }
   { auto with zarith. }
 Qed.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
index 51c105186..71f4b758b 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Psatz.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
 Require Import Crypto.Util.Option.
@@ -10,6 +11,7 @@ Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
 
 Local Open Scope Z_scope.
 
@@ -54,44 +56,6 @@ Ltac word_arith_t :=
     => clear; pose proof (@wordToZ_range logsz w); autorewrite with push_Zof_nat zsimplify_const in *; try omega
   end.
 
-Ltac revert_min_max :=
-  repeat match goal with
-         | [ H : context[Z.min _ _] |- _ ] => revert H
-         | [ H : context[Z.max _ _] |- _ ] => revert H
-         end.
-Ltac rewrite_min_max_step_fast :=
-  match goal with
-  | [ H : (?a <= ?b)%Z |- context[Z.max ?a ?b] ]
-    => rewrite (Z.max_r a b) by assumption
-  | [ H : (?b <= ?a)%Z |- context[Z.max ?a ?b] ]
-    => rewrite (Z.max_l a b) by assumption
-  | [ H : (?a <= ?b)%Z |- context[Z.min ?a ?b] ]
-    => rewrite (Z.min_l a b) by assumption
-  | [ H : (?b <= ?a)%Z |- context[Z.min ?a ?b] ]
-    => rewrite (Z.min_r a b) by assumption
-  end.
-Ltac rewrite_min_max_step :=
-  match goal with
-  | _ => rewrite_min_max_step_fast
-  | [ |- context[Z.max ?a ?b] ]
-    => first [ rewrite (Z.max_l a b) by omega
-             | rewrite (Z.max_r a b) by omega ]
-  | [ |- context[Z.min ?a ?b] ]
-    => first [ rewrite (Z.min_l a b) by omega
-             | rewrite (Z.min_r a b) by omega ]
-  end.
-Ltac only_split_min_max_step :=
-  match goal with
-  | _ => revert_min_max; progress repeat apply Z.min_case_strong; intros
-  | _ => revert_min_max; progress repeat apply Z.max_case_strong; intros
-  end.
-Ltac split_min_max_step :=
-  match goal with
-  | _ => rewrite_min_max_step
-  | _ => only_split_min_max_step
-  end.
-Ltac split_min_max := repeat split_min_max_step.
-
 Ltac case_Zvar_nonneg_on x :=
   is_var x;
   lazymatch type of x with
@@ -191,7 +155,7 @@ Ltac handle_shift_neg :=
 
 Ltac handle_four_corners_step_fast :=
   first [ progress destruct_head Bounds.t
-        | progress cbv [Bounds.four_corners] in *
+        | progress cbv [ZRange.four_corners] in *
         | progress subst
         | Zarith_t_step
         | progress split_min_max
@@ -202,7 +166,7 @@ Ltac handle_four_corners_step :=
         | remove_binary_operation_le_hyps_step ].
 Ltac handle_four_corners :=
   lazymatch goal with
-  | [ |- (ZRange.lower (Bounds.four_corners _ _ _) <= _ <= _)%Z ]
+  | [ |- (ZRange.lower (ZRange.four_corners _ _ _) <= _ <= _)%Z ]
     => idtac
   end;
   repeat handle_four_corners_step.
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
new file mode 100644
index 000000000..c5dcaa3d4
--- /dev/null
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -0,0 +1,37 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Module ZRange.
+  Import Operations.ZRange.
+  Local Open Scope zrange_scope.
+
+  Local Notation eta v := r[ lower v ~> upper v ].
+
+  Local Ltac t :=
+    repeat first [ reflexivity
+                 | progress destruct_head' zrange
+                 | progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt]
+                 | progress split_min_max
+                 | match goal with
+                   | [ |- _ = _ :> zrange ] => apply f_equal2
+                   end
+                 | omega
+                 | solve [ auto ] ].
+
+
+  Lemma flip_flip v : flip (flip v) = v.
+  Proof. destruct v; reflexivity. Qed.
+
+  Lemma normalize_flip v : normalize (flip v) = normalize v.
+  Proof. t. Qed.
+
+  Lemma normalize_idempotent v : normalize (normalize v) = normalize v.
+  Proof. t. Qed.
+
+  Definition normalize_or v : normalize v = v \/ normalize v = flip v.
+  Proof. t. Qed.
+End ZRange.
diff --git a/src/Util/ZRange/CornersMonotoneBounds.v b/src/Util/ZRange/CornersMonotoneBounds.v
new file mode 100644
index 000000000..f41c712ed
--- /dev/null
+++ b/src/Util/ZRange/CornersMonotoneBounds.v
@@ -0,0 +1,248 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Psatz.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
+Require Import Crypto.Util.ZUtil.Stabilization.
+Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.ZRange.BasicLemmas.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+
+Local Open Scope Z_scope.
+
+Module ZRange.
+  Import Operations.ZRange.
+  Local Arguments is_bounded_by' !_ _ _ / .
+
+  Lemma monotone_two_corners_genb
+        (f : Z -> Z)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotone : exists b, Proper (R b ==> Z.le) f)
+        x_bs x
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+    : ZRange.is_bounded_by' None (two_corners f x_bs) (f x).
+  Proof.
+    split; trivial.
+    destruct x_bs as [lx ux]; simpl in *.
+    destruct Hboundedx as [Hboundedx _].
+    destruct_head'_ex.
+    repeat match goal with
+           | [ H : Proper (R ?b ==> Z.le) f |- _ ]
+             => unique assert (R b (if b then lx else x) (if b then x else lx)
+                               /\ R b (if b then x else ux) (if b then ux else x))
+               by (unfold R, Basics.flip; destruct b; omega)
+           end.
+    destruct_head' and.
+    repeat match goal with
+           | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
+             => unique pose proof (H _ _ H')
+           end.
+    destruct_head bool; split_min_max; omega.
+  Qed.
+
+  Lemma monotone_two_corners_gen
+        (f : Z -> Z)
+        (Hmonotone : Proper (Z.le ==> Z.le) f \/ Proper (Basics.flip Z.le ==> Z.le) f)
+        x_bs x
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+    : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x).
+  Proof.
+    eapply monotone_two_corners_genb; auto.
+    destruct Hmonotone; [ exists true | exists false ]; assumption.
+  Qed.
+  Lemma monotone_two_corners
+        (b : bool)
+        (f : Z -> Z)
+        (R := if b then Z.le else Basics.flip Z.le)
+        (Hmonotone : Proper (R ==> Z.le) f)
+        x_bs x
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+    : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x).
+  Proof.
+    apply monotone_two_corners_genb; auto; subst R;
+      exists b.
+    intros ???; apply Hmonotone; auto.
+  Qed.
+
+  Lemma monotone_four_corners_genb
+        (f : Z -> Z -> Z)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (f x))
+        (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y))
+        x_bs y_bs x y
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+    : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+  Proof.
+    destruct x_bs as [lx ux].
+    cbn [ZRange.four_corners lower upper].
+    pose proof (monotone_two_corners_genb (f lx) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fl.
+    pose proof (monotone_two_corners_genb (f ux) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fu.
+    repeat match goal with
+           | [ |- context[ZRange.two_corners ?x ?y] ]
+             => let l := fresh "lf" in
+                let u := fresh "uf" in
+                generalize dependent (ZRange.two_corners x y); intros [l u]; intros
+           end.
+    unfold ZRange.is_bounded_by', union in *; simpl in *; split; trivial.
+    destruct_head'_and; destruct_head' True.
+    pose proof (Hmonotone2 y).
+    destruct_head'_ex.
+    repeat match goal with
+           | [ H : Proper (R ?b ==> Z.le) (f _) |- _ ]
+             => unique assert (R b (if b then ly else y) (if b then y else ly)
+                               /\ R b (if b then y else uy) (if b then uy else y))
+               by (unfold R, Basics.flip; destruct b; omega)
+           | [ H : Proper (R ?b ==> Z.le) (fun x => f x _) |- _ ]
+             => unique assert (R b (if b then lx else x) (if b then x else lx)
+                               /\ R b (if b then x else ux) (if b then ux else x))
+               by (unfold R, Basics.flip; destruct b; omega)
+           end.
+    destruct_head' and.
+    repeat match goal with
+           | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
+             => unique pose proof (H _ _ H')
+           end; cbv beta in *.
+    destruct_head bool; split_min_max; omega.
+  Qed.
+
+  Lemma monotone_four_corners_gen
+        (f : Z -> Z -> Z)
+        (Hmonotone1 : forall x, Proper (Z.le ==> Z.le) (f x) \/ Proper (Basics.flip Z.le ==> Z.le) (f x))
+        (Hmonotone2 : forall y, Proper (Z.le ==> Z.le) (fun x => f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y))
+        x_bs y_bs x y
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+    : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+  Proof.
+    eapply monotone_four_corners_genb; auto.
+    { intro x'; destruct (Hmonotone1 x'); [ exists true | exists false ]; assumption. }
+    { intro x'; destruct (Hmonotone2 x'); [ exists true | exists false ]; assumption. }
+  Qed.
+  Lemma monotone_four_corners
+        (b1 b2 : bool)
+        (f : Z -> Z -> Z)
+        (R1 := if b1 then Z.le else Basics.flip Z.le) (R2 := if b2 then Z.le else Basics.flip Z.le)
+        (Hmonotone : Proper (R1 ==> R2 ==> Z.le) f)
+        x_bs y_bs x y
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+    : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+  Proof.
+    apply monotone_four_corners_genb; auto; intro x'; subst R1 R2;
+      [ exists b2 | exists b1 ];
+      [ eapply (Hmonotone x' x'); destruct b1; reflexivity
+      | intros ???; apply Hmonotone; auto; destruct b2; reflexivity ].
+  Qed.
+
+  Lemma monotone_eight_corners_genb
+        (f : Z -> Z -> Z -> Z)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (f x y))
+        (Hmonotone2 : forall x z, exists b, Proper (R b ==> Z.le) (fun y => f x y z))
+        (Hmonotone3 : forall y z, exists b, Proper (R b ==> Z.le) (fun x => f x y z))
+        x_bs y_bs z_bs x y z
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+        (Hboundedz : ZRange.is_bounded_by' None z_bs z)
+    : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+  Proof.
+    destruct x_bs as [lx ux].
+    unfold ZRange.eight_corners; cbn [lower upper].
+    pose proof (monotone_four_corners_genb (f lx) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fl.
+    pose proof (monotone_four_corners_genb (f ux) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fu.
+    repeat match goal with
+           | [ |- context[ZRange.four_corners ?x ?y ?z] ]
+             => let l := fresh "lf" in
+                let u := fresh "uf" in
+                generalize dependent (ZRange.four_corners x y z); intros [l u]; intros
+           end.
+    unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial.
+    destruct_head'_and; destruct_head' True.
+    pose proof (Hmonotone3 y z).
+    destruct_head'_ex.
+    repeat match goal with
+           | [ H : Proper (R ?b ==> Z.le) (f _ _) |- _ ]
+             => unique assert (R b (if b then lz else z) (if b then z else lz)
+                               /\ R b (if b then z else uz) (if b then uz else z))
+               by (unfold R, Basics.flip; destruct b; omega)
+           | [ H : Proper (R ?b ==> Z.le) (fun y' => f _ y' _) |- _ ]
+             => unique assert (R b (if b then ly else y) (if b then y else ly)
+                               /\ R b (if b then y else uy) (if b then uy else y))
+               by (unfold R, Basics.flip; destruct b; omega)
+           | [ H : Proper (R ?b ==> Z.le) (fun x' => f x' _ _) |- _ ]
+             => unique assert (R b (if b then lx else x) (if b then x else lx)
+                               /\ R b (if b then x else ux) (if b then ux else x))
+               by (unfold R, Basics.flip; destruct b; omega)
+           end.
+    destruct_head' and.
+    repeat match goal with
+           | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
+             => unique pose proof (H _ _ H')
+           end.
+    destruct_head bool; split_min_max; omega.
+  Qed.
+
+  Lemma monotone_eight_corners_gen
+        (f : Z -> Z -> Z -> Z)
+        (Hmonotone1 : forall x y, Proper (Z.le ==> Z.le) (f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (f x y))
+        (Hmonotone2 : forall x z, Proper (Z.le ==> Z.le) (fun y => f x y z) \/ Proper (Basics.flip Z.le ==> Z.le) (fun y => f x y z))
+        (Hmonotone3 : forall y z, Proper (Z.le ==> Z.le) (fun x => f x y z) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y z))
+        x_bs y_bs z_bs x y z
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+        (Hboundedz : ZRange.is_bounded_by' None z_bs z)
+    : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+  Proof.
+    eapply monotone_eight_corners_genb; auto.
+    { intros x' y'; destruct (Hmonotone1 x' y'); [ exists true | exists false ]; assumption. }
+    { intros x' y'; destruct (Hmonotone2 x' y'); [ exists true | exists false ]; assumption. }
+    { intros x' y'; destruct (Hmonotone3 x' y'); [ exists true | exists false ]; assumption. }
+  Qed.
+  Lemma monotone_eight_corners
+        (b1 b2 b3 : bool)
+        (f : Z -> Z -> Z -> Z)
+        (R1 := if b1 then Z.le else Basics.flip Z.le)
+        (R2 := if b2 then Z.le else Basics.flip Z.le)
+        (R3 := if b3 then Z.le else Basics.flip Z.le)
+        (Hmonotone : Proper (R1 ==> R2 ==> R3 ==> Z.le) f)
+        x_bs y_bs z_bs x y z
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+        (Hboundedz : ZRange.is_bounded_by' None z_bs z)
+    : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+  Proof.
+    apply monotone_eight_corners_genb; auto; intro x'; subst R1 R2 R3;
+      [ exists b3 | exists b2 | exists b1 ];
+      intros ???; apply Hmonotone; break_innermost_match; try reflexivity; trivial.
+  Qed.
+
+  Lemma monotonify2 (f : Z -> Z -> Z) (upper : Z -> Z -> Z)
+        (Hbounded : forall a b, Z.abs (f a b) <= upper (Z.abs a) (Z.abs b))
+        (Hupper_monotone : Proper (Z.le ==> Z.le ==> Z.le) upper)
+        {xb yb x y}
+        (Hboundedx : ZRange.is_bounded_by' None xb x)
+        (Hboundedy : ZRange.is_bounded_by' None yb y)
+        (abs_x := ZRange.upper (ZRange.abs xb))
+        (abs_y := ZRange.upper (ZRange.abs yb))
+    : ZRange.is_bounded_by'
+        None
+        {| ZRange.lower := -upper abs_x abs_y;
+           ZRange.upper := upper abs_x abs_y |}
+        (f x y).
+  Proof.
+    split; [ | exact I ]; subst abs_x abs_y; simpl.
+    apply Z.abs_le.
+    destruct Hboundedx as [Hx _], Hboundedy as [Hy _].
+    etransitivity; [ apply Hbounded | ].
+    apply Hupper_monotone;
+      unfold ZRange.abs;
+      repeat (apply Z.max_case_strong || apply Zabs_ind); omega.
+  Qed.
+End ZRange.
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 7d9b24c40..c73b991e8 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -7,21 +7,38 @@ Module ZRange.
 
   Local Notation eta v := r[ lower v ~> upper v ].
 
+  Definition flip (v : zrange) : zrange
+    := r[ upper v ~> lower v ].
+
+  Definition union (x y : zrange) : zrange
+    := let (lx, ux) := eta x in
+       let (ly, uy) := eta y in
+       r[ Z.min lx ly ~> Z.max ux uy ].
+
   Definition normalize (v : zrange) : zrange
-    := r[ Z.min (lower v) (upper v) ~> Z.max (lower v) (upper v) ].
+    := r[ Z.min (lower v) (upper v) ~> Z.max (upper v) (lower v) ].
+
+  Definition normalize' (v : zrange) : zrange
+    := union v (flip v).
+
+  Lemma normalize'_eq : normalize = normalize'. Proof. reflexivity. Defined.
 
   Definition abs (v : zrange) : zrange
     := let (l, u) := eta v in
        r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ].
 
+  Definition map (f : Z -> Z) (v : zrange) : zrange
+    := let (l, u) := eta v in
+       r[ f l ~> f u ].
+
   Definition two_corners (f : Z -> Z) (v : zrange) : zrange
     := let (l, u) := eta v in
-       r[ Z.min (f l) (f u) ~> Z.max (f l) (f u) ].
+       r[ Z.min (f l) (f u) ~> Z.max (f u) (f l) ].
 
-  Definition union (x y : zrange) : zrange
-    := let (lx, ux) := eta x in
-       let (ly, uy) := eta y in
-       r[ Z.min lx ly ~> Z.max ux uy ].
+  Definition two_corners' (f : Z -> Z) (v : zrange) : zrange
+    := normalize' (map f v).
+
+  Lemma two_corners'_eq : two_corners = two_corners'. Proof. reflexivity. Defined.
 
   Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange
     := let (lx, ux) := eta x in
@@ -32,5 +49,4 @@ Module ZRange.
     := let (lx, ux) := eta x in
        union (four_corners (f lx) y z)
              (four_corners (f ux) y z).
-
 End ZRange.
diff --git a/src/Util/ZUtil/Tactics/SplitMinMax.v b/src/Util/ZUtil/Tactics/SplitMinMax.v
new file mode 100644
index 000000000..901cfde88
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/SplitMinMax.v
@@ -0,0 +1,42 @@
+Require Import Coq.omega.Omega.
+Require Import Coq.ZArith.BinInt.
+
+Ltac rewrite_min_max_side_condition_t := omega.
+
+Ltac revert_min_max :=
+  repeat match goal with
+         | [ H : context[Z.min _ _] |- _ ] => revert H
+         | [ H : context[Z.max _ _] |- _ ] => revert H
+         end.
+Ltac rewrite_min_max_step_fast :=
+  match goal with
+  | [ H : (?a <= ?b)%Z |- context[Z.max ?a ?b] ]
+    => rewrite (Z.max_r a b) by assumption
+  | [ H : (?b <= ?a)%Z |- context[Z.max ?a ?b] ]
+    => rewrite (Z.max_l a b) by assumption
+  | [ H : (?a <= ?b)%Z |- context[Z.min ?a ?b] ]
+    => rewrite (Z.min_l a b) by assumption
+  | [ H : (?b <= ?a)%Z |- context[Z.min ?a ?b] ]
+    => rewrite (Z.min_r a b) by assumption
+  end.
+Ltac rewrite_min_max_step :=
+  match goal with
+  | _ => rewrite_min_max_step_fast
+  | [ |- context[Z.max ?a ?b] ]
+    => first [ rewrite (Z.max_l a b) by rewrite_min_max_side_condition_t
+             | rewrite (Z.max_r a b) by rewrite_min_max_side_condition_t ]
+  | [ |- context[Z.min ?a ?b] ]
+    => first [ rewrite (Z.min_l a b) by rewrite_min_max_side_condition_t
+             | rewrite (Z.min_r a b) by rewrite_min_max_side_condition_t ]
+  end.
+Ltac only_split_min_max_step :=
+  match goal with
+  | _ => revert_min_max; progress repeat apply Z.min_case_strong; intros
+  | _ => revert_min_max; progress repeat apply Z.max_case_strong; intros
+  end.
+Ltac split_min_max_step :=
+  match goal with
+  | _ => rewrite_min_max_step
+  | _ => only_split_min_max_step
+  end.
+Ltac split_min_max := repeat split_min_max_step.