remove old pipeline

3 files changed, 0 insertions, 603 deletions

diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
deleted file mode 100644
index b23e0ff1b..000000000
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ /dev/null
@@ -1,214 +0,0 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Psatz.
-Require Import Crypto.Compilers.Z.Syntax.
-Require Import Crypto.Compilers.Z.Syntax.Util.
-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.Stabilization.
-Require Import Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Modulo.
-Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
-Require Import Crypto.Util.ZUtil.Morphisms.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.FixedWordSizesEquality.
-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.
-
-Local Arguments Bounds.is_bounded_by' !_ _ _ / .
-
-Lemma is_bounded_by_truncation_bounds' Tout bs v
-      (H : Bounds.is_bounded_by (T:=Tbase TZ) bs v)
-  : Bounds.is_bounded_by (T:=Tbase Tout)
-                         (Bounds.truncation_bounds' (Bounds.bit_width_of_base_type Tout) bs)
-                         (ZToInterp v).
-Proof.
-  destruct bs as [l u]; cbv [Bounds.truncation_bounds' Bounds.is_bounded_by Bounds.is_bounded_by' Bounds.bit_width_of_base_type Bounds.log_bit_width_of_base_type option_map ZRange.is_bounded_by'] in *; simpl in *.
-  repeat first [ break_t_step
-               | fin_t
-               | progress simpl in *
-               | Zarith_t_step
-               | rewriter_t
-               | word_arith_t ].
-Qed.
-
-Lemma is_bounded_by_compose T1 T2 f_v bs v f_bs fv
-      (H : Bounds.is_bounded_by (T:=Tbase T1) bs v)
-      (Hf : forall bs v, Bounds.is_bounded_by (T:=Tbase T1) bs v -> Bounds.is_bounded_by (T:=Tbase T2) (f_bs bs) (f_v v))
-      (Hfv : f_v v = fv)
-  : Bounds.is_bounded_by (T:=Tbase T2) (f_bs bs) fv.
-Proof.
-  subst; eauto.
-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).
-Proof.
-  unfold Bounds.upper_lor_and_bounds.
-  apply stabilizes_bounded; auto with zarith.
-  rewrite <- !Z.max_mono by exact _.
-  apply land_stabilizes; apply stabilization_time_weaker.
-Qed.
-
-Lemma lor_upper_lor_land_bounds a b
-  : Z.abs (Z.lor a b) <= Bounds.upper_lor_and_bounds (Z.abs a) (Z.abs b).
-Proof.
-  unfold Bounds.upper_lor_and_bounds.
-  apply stabilizes_bounded; auto with zarith.
-  rewrite <- !Z.max_mono by exact _.
-  apply lor_stabilizes; apply stabilization_time_weaker.
-Qed.
-
-Lemma upper_lor_and_bounds_Proper
-  : Proper (Z.le ==> Z.le ==> Z.le) Bounds.upper_lor_and_bounds.
-Proof.
-  intros ??? ???.
-  unfold Bounds.upper_lor_and_bounds.
-  auto with zarith.
-Qed.
-
-Local Arguments Z.pow !_ !_.
-Local Arguments Z.log2_up !_.
-Local Arguments Z.add !_ !_.
-Lemma land_bounds_extreme xb yb x y
-      (Hx : ZRange.is_bounded_by' None xb x)
-      (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 ZRange.monotonify2; auto;
-    unfold Bounds.extreme_lor_land_bounds;
-    [ apply land_upper_lor_land_bounds
-    | apply upper_lor_and_bounds_Proper ].
-Qed.
-Lemma lor_bounds_extreme xb yb x y
-      (Hx : ZRange.is_bounded_by' None xb x)
-      (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 ZRange.monotonify2; auto;
-    unfold Bounds.extreme_lor_land_bounds;
-    [ apply lor_upper_lor_land_bounds
-    | apply upper_lor_and_bounds_Proper ].
-Qed.
-
-Local Arguments N.ldiff : simpl never.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.add !_ !_.
-Local Existing Instances Z.add_le_Proper Z.sub_le_flip_le_Proper Z.log2_up_le_Proper Z.pow_Zpos_le_Proper Z.sub_le_eq_Proper Z.add_with_carry_le_Proper.
-Local Hint Extern 1 => progress cbv beta iota : typeclass_instances.
-Local Ltac ibbio_prefin :=
-  [ > | intros | simpl; reflexivity ].
-Local Ltac apply_is_bounded_by_truncation_bounds :=
-  cbv [id
-         Bounds.interp_op interp_op Bounds.is_bounded_by Relations.interp_flat_type_rel_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop SmartVarfMap smart_interp_flat_map lift_op SmartFlatTypeMapUnInterp cast_const Zinterp_op SmartFlatTypeMapInterp2
-         Z.add_with_get_carry Bounds.add_with_get_carry Bounds.sub_with_get_borrow Bounds.get_carry Bounds.get_borrow Z.get_carry Bounds.mul_split];
-  cbn [interpToZ fst snd];
-  repeat match goal with
-         | [ |- _ /\ _ ] => split
-         end;
-  lazymatch goal with
-  | [ |- Bounds.is_bounded_by' (Bounds.truncation_bounds _ _) (ZToInterp _) ]
-    => apply is_bounded_by_truncation_bounds'
-  end.
-Local Ltac handle_mul :=
-  apply (ZRange.monotone_four_corners_genb Z.mul); try (split; auto);
-  unfold Basics.flip;
-  let x := fresh "x" in
-  intro x;
-  exists (0 <=? x);
-  break_match; Z.ltb_to_lt;
-  intros ???; nia.
-Lemma is_bounded_by_interp_op t tR (opc : op t tR)
-      (bs : interp_flat_type Bounds.interp_base_type _)
-      (v : interp_flat_type interp_base_type _)
-      (H : Bounds.is_bounded_by bs v)
-      (H_side : to_prop (interped_op_side_conditions opc v))
-  : Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v).
-Proof.
-  destruct opc; apply_is_bounded_by_truncation_bounds;
-    [ ..
-    | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _);
-      [ .. | cbn -[Z.mul_split_at_bitwidth]; rewrite Z.mul_split_at_bitwidth_mod ];
-      ibbio_prefin
-    | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v / _))   (v:=ZToInterp _);
-        [ .. | cbn -[Z.mul_split_at_bitwidth]; rewrite Z.mul_split_at_bitwidth_div ];
-        ibbio_prefin
-    |
-    | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _);
-        ibbio_prefin
-    | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v / _))   (v:=ZToInterp _);
-        ibbio_prefin
-    |
-    | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _);
-        ibbio_prefin
-    | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (-(v / _)))   (v:=ZToInterp _);
-      ibbio_prefin ];
-    repeat first [ progress simpl in *
-                 | progress cbv [Bounds.interp_base_type Bounds.is_bounded_by' ZRange.is_bounded_by'] in *
-                 | progress destruct_head'_prod
-                 | progress destruct_head'_and
-                 | omega
-                 | match goal with
-                   | [ |- context[interpToZ ?x] ]
-                     => generalize dependent (interpToZ x); clear x; intros
-                   | [ |- _ /\ True ] => split; [ | tauto ]
-                   end ].
-  { apply (@ZRange.monotone_four_corners true true Z.add _); split; auto. }
-  { apply (@ZRange.monotone_four_corners true false Z.sub _); split; auto. }
-  { handle_mul. }
-  { apply (ZRange.monotone_four_corners_genb Z.shiftl); try (split; auto);
-      [ eexists; apply Z.shiftl_le_Proper1
-      | exists true; apply Z.shiftl_le_Proper2 ]. }
-  { apply (ZRange.monotone_four_corners_genb Z.shiftr); 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;
-      [ apply land_bounds_extreme; split; auto | .. ];
-      repeat first [ progress simpl in *
-                   | Zarith_t_step
-                   | rewriter_t
-                   | progress saturate_land_lor_facts
-                   | split_min_max; omega ]. }
-  { cbv [Bounds.lor Bounds.extremization_bounds]; break_innermost_match;
-      [ apply lor_bounds_extreme; split; auto | .. ];
-      repeat first [ progress simpl in *
-                   | Zarith_t_step
-                   | rewriter_t
-                   | progress Zarith_land_lor_t_step
-                   | solve [ split_min_max; try omega; try Zarith_land_lor_t_step ] ]. }
-  { repeat first [ progress destruct_head Bounds.t
-                 | progress simpl in *
-                 | progress split_min_max
-                 | omega ]. }
-  { cbv [Bounds.id_with_alt];
-      break_innermost_match; simpl in *; Z.ltb_to_lt; subst;
-        split; assumption. }
-  { destruct_head Bounds.t; cbv [Bounds.zselect' Z.zselect].
-    break_innermost_match; split_min_max; omega. }
-  { handle_mul. }
-  { apply Z.mod_bound_min_max; auto. }
-  { handle_mul. }
-  { auto with zarith. }
-  { apply (@ZRange.monotone_eight_corners true true true Z.add_with_carry _ _); split; auto. }
-  { apply (@ZRange.monotone_eight_corners true true true Z.add_with_carry _ _); split; auto. }
-  { apply Z.mod_bound_min_max; auto. }
-  { apply (@ZRange.monotone_eight_corners true true true Z.add_with_carry _ _); split; auto. }
-  { auto with zarith. }
-  { apply (@ZRange.monotone_eight_corners false true false Z.sub_with_borrow _ _); split; auto. }
-  { apply (@ZRange.monotone_eight_corners false true false Z.sub_with_borrow _ _); split; auto. }
-  { apply Z.mod_bound_min_max; auto. }
-  { apply (@ZRange.monotone_eight_corners false true false Z.sub_with_borrow _ _); split; auto. }
-  { auto with zarith. }
-Qed.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
deleted file mode 100644
index 7ffe0beb1..000000000
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
+++ /dev/null
@@ -1,192 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Psatz.
-Require Import Crypto.Compilers.Z.Syntax.
-Require Import Crypto.Compilers.Z.Syntax.Util.
-Require Import Crypto.Compilers.Z.Syntax.Equality.
-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.ZUtil.Morphisms.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Pow2.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.FixedWordSizesEquality.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.UniquePose.
-
-Local Open Scope Z_scope.
-
-Local Arguments lift_op : simpl never.
-Local Arguments cast_back_flat_const : simpl never.
-Local Arguments unzify_op : simpl never.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.add !_ !_.
-Local Existing Instances Z.pow_Zpos_le_Proper Z.log2_up_le_Proper.
-
-Section with_round_up.
-  Context (is_bounded_by_interp_op
-           : forall t tR (opc : op t tR)
-                    (bs : interp_flat_type Bounds.interp_base_type _)
-                    (v : interp_flat_type interp_base_type _)
-                    (H : Bounds.is_bounded_by bs v)
-                    (Hside : to_prop (interped_op_side_conditions opc v)),
-              Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v)).
-  Context {round_up : nat -> option nat}.
-
-  Local Notation pick_typeb := (@Bounds.bounds_to_base_type round_up) (only parsing).
-  Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
-
-  Local Ltac t_small :=
-    repeat first [ progress cbv [Bounds.bounds_to_base_type Bounds.smallest_logsz Bounds.actual_logsz] in *
-                 | progress simpl in *
-                 | progress autorewrite with push_Zof_nat zsimplify_const
-                 | solve [ trivial ]
-                 | progress change (@interpToZ) with (fun t1 => cast_const (t1:=t1) (t2:=TZ)) in *
-                 | progress change (@cast_const TZ TZ) with (fun x : Z => x) in *
-                 | progress Z.ltb_to_lt
-                 | rewrite Z2Nat.id in * by auto with zarith
-                 | rewrite <- Z.log2_up_le_pow2_full in * by auto with zarith
-                 | break_innermost_match_step
-                 | apply conj
-                 | omega
-                 | rewrite <- Z.log2_up_le_full
-                 | match goal with
-                   | [ |- ?x < ?y ] => cut (x + 1 <= y); [ omega | ]
-                   | [ H : (_ <=? _)%nat = true |- _ ] => apply Nat.leb_le in H
-                   | [ H : (_ <= _)%nat |- _ ] => apply inj_le in H
-                   end ].
-
-  Local Arguments cast_const : simpl never.
-  Lemma interpToZ_cast_const_small T0 (bs : Bounds.interp_base_type T0)
-        (v : interp_base_type (@Bounds.bounds_to_base_type round_up T0 bs))
-        (H : match Bounds.bit_width_of_base_type T0 with
-             | Some sz => 0 <= ZRange.lower bs /\ ZRange.upper bs < 2 ^ sz
-             | None => True
-             end)
-        (Hv : ZRange.lower bs <= interpToZ (cast_const (t2:=T0) v) <= ZRange.upper bs)
-    : interpToZ (cast_const (t2:=T0) v) = interpToZ v.
-  Proof.
-    destruct_head base_type; simpl in *; try reflexivity.
-    unfold Bounds.smallest_logsz, Bounds.interp_base_type, cast_const in *.
-    break_innermost_match_hyps; Z.ltb_to_lt; simpl in *;
-      [ pose proof (wordToZ_range v) | omega ].
-    rewrite wordToZ_ZToWord_mod_full.
-    rewrite wordToZ_ZToWord_mod_full in Hv.
-    revert Hv; apply Z.max_case_strong; Z.rewrite_mod_small; intros; try omega; [].
-    rewrite Z.mod_small; [ reflexivity | split; auto with zarith ].
-    autorewrite with push_Zof_nat zsimplify_const in *.
-    rewrite Z2Nat.id in * by auto with zarith.
-    destruct_head' and.
-    eapply Z.lt_le_trans; [ eassumption | ].
-    repeat first [ progress Z.peel_le
-                 | rewrite <- Z.log2_up_pow2 by auto with zarith; progress Z.peel_le
-                 | omega ].
-  Qed.
-
-  Local Existing Instances Z.pow_Zpos_le_Proper Z.pow_Zpos_le_Proper_flip Z.lt_le_flip_Proper_flip_impl.
-  Lemma ZToInterp_cast_const_small T (bs : Bounds.interp_base_type T)
-        v
-        (H : match Bounds.bit_width_of_base_type T with
-             | Some sz => 0 <= ZRange.lower bs /\ ZRange.upper bs < 2 ^ sz
-             | None => True
-             end)
-        (Hb : ZRange.lower bs <= interpToZ (@ZToInterp T v) <= ZRange.upper bs)
-    : @cast_const (@Bounds.bounds_to_base_type round_up T bs) T (ZToInterp v) = ZToInterp v.
-  Proof.
-    apply ZToInterp_eq_inj.
-    rewrite ?interpToZ_ZToInterp_mod.
-    rewrite interpToZ_ZToInterp_mod in Hb.
-    destruct T; simpl in *.
-    { unfold Bounds.actual_logsz.
-      break_innermost_match; Z.ltb_to_lt; try reflexivity; [].
-      t_small.
-      apply Z.max_case_strong; intros; Z.rewrite_mod_small; omega. }
-    { unfold Bounds.smallest_logsz.
-      break_innermost_match_step; Z.ltb_to_lt; try omega; [].
-      revert Hb; apply (Z.max_case_strong 0 v); intros; Z.rewrite_mod_small; try reflexivity.
-      rewrite Z.max_r by auto with zarith.
-      autorewrite with push_Zof_nat zsimplify_const in *.
-      rewrite Z2Nat.id by auto with zarith.
-      rewrite Z.mod_mod_small; try apply conj; auto with zarith;
-        repeat first [ rewrite <- Z.log2_up_le_pow2_full in * by auto with zarith
-                     | rewrite <- Z.log2_up_le_full
-                     | omega
-                     | apply conj
-                     | progress Z.peel_le
-                     | rewrite <- Z.log2_up_pow2 by auto with zarith; progress Z.peel_le
-                     | match goal with
-                       | [ |- 2^?x mod 2^?y = 0 ]
-                         => destruct (Z.pow2_lt_or_divides x y);
-                            [ solve [ auto with zarith ]
-                            | exfalso; assert (2^y <= 2^x)
-                            | assumption ]
-                       end ]. }
-  Qed.
-
-  Lemma pull_cast_genericize_op
-        t tR (opc : op t tR)
-        (bs : interp_flat_type Bounds.interp_base_type t)
-        (v : interp_flat_type interp_base_type (pick_type bs))
-        (H : Bounds.is_bounded_by bs
-                                  (SmartFlatTypeMapUnInterp
-                                     (fun (t1 : base_type) (b0 : Bounds.interp_base_type t1) => cast_const) v))
-        (Hside : to_prop (interped_op_side_conditions opc (cast_back_flat_const v)))
-    : interp_op t tR opc (cast_back_flat_const v)
-      = cast_back_flat_const (interp_op (pick_type bs) (pick_type (Bounds.interp_op opc bs)) (genericize_op opc) v).
-  Proof.
-    pose proof (is_bounded_by_interp_op t tR opc bs).
-    unfold interp_op in *.
-    rewrite Zinterp_op_genericize_op.
-    generalize dependent (Zinterp_op t tR opc).
-    generalize dependent (Bounds.interp_op opc bs); simpl; intros.
-    repeat (destruct_one_head flat_type; try solve [ inversion opc ]);
-      repeat first [ progress simpl in *
-                   | progress destruct_head unit
-                   | progress destruct_head True
-                   | progress cbv [unzify_op cast_back_flat_const lift_op Bounds.is_bounded_by' ZRange.is_bounded_by'] in *
-                   | progress change (@interpToZ TZ) with (fun x : Z => x) in *
-                   | progress specialize_by auto
-                   | progress specialize_by constructor
-                   | match goal with
-                     | [ H : forall v, _ <= ?f v <= _ /\ _ -> _ |- context[?f ?v'] ]
-                       => specialize (H v')
-                     | _ => progress specialize_by_assumption
-                     | _ => progress specialize_by auto
-                     | [ H : forall v : unit, _ |- _ ] => specialize (H tt)
-                     | [ H : forall v : _ * _, _ /\ _ -> _ |- _ ]
-                       => specialize (fun v1 v2 p1 p2 => H (v1, v2) (conj p1 p2));
-                          cbn [fst snd] in H;
-                          specialize (fun v1 p1 v2 p2 => H v1 v2 p1 p2)
-                     end
-                   | progress destruct_head'_and ];
-      [
-      | rewrite cast_const_idempotent_small by t_small; reflexivity
-      | .. ];
-      repeat match goal with
-             | _ => progress change (@cast_const TZ) with @ZToInterp in *
-             | [ |- context[@cast_const ?x TZ] ]
-               => progress change (@cast_const x TZ) with (@interpToZ x) in *
-             | [ H : context[@cast_const ?x TZ] |- _ ]
-               => progress change (@cast_const x TZ) with (@interpToZ x) in *
-             end;
-      repeat match goal with
-             | _ => reflexivity
-             | _ => progress rewrite ?interpToZ_cast_const_small, ?ZToInterp_cast_const_small by auto
-             | [ H : context[ZToInterp (?f (interpToZ (cast_const ?v)))] |- _ ]
-               => rewrite (@interpToZ_cast_const_small _ _ v) in H by auto
-             | [ H : context[(interpToZ (cast_const ?v), _)] |- _ ]
-               => rewrite (@interpToZ_cast_const_small _ _ v) in H by auto
-             | [ H : context[(_, interpToZ (cast_const ?v))] |- _ ]
-               => rewrite (@interpToZ_cast_const_small _ _ v) in H by auto
-             end.
-  Qed.
-End with_round_up.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
deleted file mode 100644
index 6486b2e00..000000000
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
+++ /dev/null
@@ -1,197 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Psatz.
-Require Import Crypto.Compilers.Z.Bounds.Interpretation.
-Require Import Crypto.Util.ZUtil.Hints.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.ZSimplify.Core.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Shift.
-Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Notations.
-Require Import Crypto.Util.ZRange.Operations.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.FixedWordSizesEquality.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.Tactics.BreakMatch.
-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.
-
-Ltac break_t_step :=
-  first [ progress destruct_head'_and
-        | progress destruct_head'_or
-        | progress destruct_head'_prod
-        | progress split_andb
-        | break_innermost_match_step ].
-
-Ltac fin_t :=
-  first [ reflexivity
-        | assumption
-        | match goal with
-          | [ |- and _ _ ]
-            => first [ split; [ | solve [ fin_t ] ]
-                     | split; [ solve [ fin_t ] | ] ];
-               try solve [ fin_t ]
-          end
-        | omega ].
-
-Ltac specializer_t_step :=
-  first [ progress specialize_by_assumption
-        | progress specialize_by fin_t ].
-
-Ltac Zarith_t_step :=
-  first [ match goal with
-          | [ H : (?x <= ?y)%Z, H' : (?y <= ?x)%Z |- _ ]
-            => assert (x = y) by omega; clear H H'
-          end
-        | progress Z.ltb_to_lt_in_context ].
-Ltac Zarith_land_lor_t_step :=
-  match goal with
-  | [ |- _ <= Z.lor _ _ <= _ ]
-    => split; etransitivity; [ | apply Z.lor_bounds; omega | apply Z.lor_bounds; omega | ]
-  | [ |- 2^Z.log2_up (?x + 1) - 1 <= 2^Z.log2_up (?y + 1) - 1 ]
-    => let H := fresh in assert (H : x <= y) by omega; rewrite H; reflexivity
-  end.
-Ltac word_arith_t :=
-  match goal with
-  | [ |- (0 <= FixedWordSizes.wordToZ ?w <= 2^2^Z.of_nat ?logsz - 1)%Z ]
-    => clear; pose proof (@wordToZ_range logsz w); autorewrite with push_Zof_nat zsimplify_const in *; try omega
-  end.
-
-Ltac case_Zvar_nonneg_on x :=
-  is_var x;
-  lazymatch type of x with
-  | Z => lazymatch goal with
-         | [ H : (0 <= x)%Z |- _ ] => fail
-         | [ H : (x < 0)%Z |- _ ] => fail
-         | _ => destruct (Z_lt_le_dec x 0); try omega
-         end
-  end.
-Ltac case_Zvar_nonneg_step :=
-  match goal with
-  | [ |- context[?x] ]
-    => case_Zvar_nonneg_on x
-  end.
-Ltac case_Zvar_nonneg := repeat case_Zvar_nonneg_step.
-
-Ltac remove_binary_operation_le_hyps_step :=
-  match goal with
-  | [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ]
-    => assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia);
-       clear H
-  | [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ]
-    => assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia);
-       clear H
-  | [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ]
-    => assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia);
-       clear H
-  | [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ]
-    => assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia);
-       clear H
-  | [ H : ?T, H' : ?T |- _ ] => clear H'
-  | [ H : ?A \/ (~?A /\ ?B), H' : ?A \/ (~?A /\ ?C) |- _ ]
-    => assert (A \/ (~A /\ (B /\ C))) by (clear -H H'; tauto); clear H H'
-  | _ => progress destruct_head' or; destruct_head' and; subst; try omega
-  | [ |- (_ <= _ <= _)%Z ] => split
-  | _ => case_Zvar_nonneg_step
-  end.
-
-Ltac saturate_with_shift_facts :=
-  repeat match goal with
-         | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x << ?x'] ]
-           => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
-         | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y << ?y'] ]
-           => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
-          | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x >> ?y'] ]
-            => unique assert (x >> y' <= y >> x') by (Z.shiftr_le_mono; omega)
-         | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?x'] ]
-           => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega)
-         end.
-Ltac saturate_with_all_shift_facts :=
-  repeat match goal with
-         | _ => progress saturate_with_shift_facts
-         | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftl _ _] ]
-           => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
-         | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftr _ _] ]
-           => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega)
-         end.
-Ltac preprocess_shift_min_max :=
-  repeat first [ rewrite (Z.min_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
-               | rewrite (Z.min_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
-               | rewrite (Z.max_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
-               | rewrite (Z.max_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
-               | rewrite (Z.min_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
-               | rewrite (Z.min_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
-               | rewrite (Z.max_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
-               | rewrite (Z.max_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) ].
-Ltac saturate_land_lor_facts :=
-  repeat match goal with
-         | [ |- context[Z.land ?x ?y] ]
-           => let H := fresh in
-              let H' := fresh in
-              assert (H : 0 <= x) by omega;
-              assert (H' : 0 <= y) by omega;
-              unique pose proof (Z.land_upper_bound_r x y H H');
-              unique pose proof (Z.land_upper_bound_l x y H H')
-         | [ |- context[Z.land ?x ?y] ]
-           => unique assert (0 <= Z.land x y) by (apply Z.land_nonneg; omega)
-         | [ |- context[Z.land ?x ?y] ]
-           => case_Zvar_nonneg_on x; case_Zvar_nonneg_on y
-         | [ |- context[Z.lor ?x ?y] ]
-           => let H := fresh in
-              let H' := fresh in
-              assert (H : 0 <= x) by omega;
-              assert (H' : 0 <= y) by omega;
-              unique pose proof (proj1 (Z.lor_bounds x y H H'));
-              unique pose proof (proj2 (Z.lor_bounds x y H H'))
-         | [ |- context[Z.lor ?x ?y] ]
-           => unique assert (0 <= Z.lor x y) by (apply Z.lor_nonneg; omega)
-         | [ |- context[Z.lor ?x ?y] ]
-           => case_Zvar_nonneg_on x; case_Zvar_nonneg_on y
-         end.
-Ltac handle_shift_neg :=
-  repeat first [ rewrite !Z.shiftr_opp_r
-               | rewrite !Z.shiftl_opp_r
-               | rewrite !Z.shiftr_opp_l
-               | rewrite !Z.shiftl_opp_l ].
-
-Ltac handle_four_corners_step_fast :=
-  first [ progress destruct_head Bounds.t
-        | progress cbv [ZRange.four_corners] in *
-        | progress subst
-        | Zarith_t_step
-        | progress split_min_max
-        | omega
-        | nia ].
-Ltac handle_four_corners_step :=
-  first [ handle_four_corners_step_fast
-        | remove_binary_operation_le_hyps_step ].
-Ltac handle_four_corners :=
-  lazymatch goal with
-  | [ |- (ZRange.lower (ZRange.four_corners _ _ _) <= _ <= _)%Z ]
-    => idtac
-  end;
-  repeat handle_four_corners_step.
-
-Ltac rewriter_t :=
-  first [ rewrite !Bool.andb_true_iff
-        | rewrite !Bool.andb_false_iff
-        | rewrite !Bool.orb_true_iff
-        | rewrite !Bool.orb_false_iff
-        | rewrite !Z.abs_opp
-        | rewrite !Z.max_log2_up
-        | rewrite !Z.add_max_distr_r
-        | rewrite !Z.add_max_distr_l
-        | rewrite wordToZ_ZToWord by (autorewrite with push_Zof_nat zsimplify_const; omega)
-        | match goal with
-          | [ H : _ |- _ ]
-            => first [ rewrite !Bool.andb_true_iff in H
-                     | rewrite !Bool.andb_false_iff in H
-                     | rewrite !Bool.orb_true_iff in H
-                     | rewrite !Bool.orb_false_iff in H ]
-          end ].