Add lemmas about shift bounds to ZUtil

After     | File Name                                                    | Before    || Change
-------------------------------------------------------------------------------------------------
13m38.70s | Total                                                        | 14m34.38s || -0m55.68s
-------------------------------------------------------------------------------------------------
1m05.36s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast             | 1m14.01s  || -0m08.65s
0m49.32s  | Compilers/Z/ArithmeticSimplifierWf                           | 0m56.11s  || -0m06.78s
3m50.24s  | Specific/IntegrationTestLadderstep                           | 3m55.59s  || -0m05.34s
1m30.01s  | Spec/Test/X25519                                             | 1m34.98s  || -0m04.96s
0m11.63s  | Specific/IntegrationTestSub                                  | 0m15.00s  || -0m03.36s
1m30.00s  | Specific/IntegrationTestLadderstep130                        | 1m32.52s  || -0m02.52s
0m37.04s  | Spec/Ed25519                                                 | 0m39.69s  || -0m02.64s
0m17.82s  | Primitives/EdDSARepChange                                    | 0m20.25s  || -0m02.42s
0m14.41s  | Specific/IntegrationTestMul                                  | 0m16.55s  || -0m02.14s
0m16.54s  | Util/ZUtil                                                   | 0m15.06s  || +0m01.47s
0m11.14s  | Compilers/Z/ArithmeticSimplifierInterp                       | 0m12.19s  || -0m01.04s
0m09.43s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy          | 0m10.63s  || -0m01.20s
0m08.62s  | LegacyArithmetic/ArchitectureToZLikeProofs                   | 0m10.12s  || -0m01.50s
0m08.03s  | LegacyArithmetic/Double/Proofs/Multiply                      | 0m09.28s  || -0m01.25s
0m07.89s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m09.62s  || -0m01.72s
0m06.92s  | Arithmetic/Core                                              | 0m08.11s  || -0m01.18s
0m04.98s  | Specific/ArithmeticSynthesisTest130                          | 0m06.04s  || -0m01.05s
0m02.57s  | LegacyArithmetic/Double/Proofs/ShiftRight                    | 0m04.08s  || -0m01.51s
0m20.49s  | Compilers/Named/MapCastWf                                    | 0m20.67s  || -0m00.18s
0m09.86s  | Compilers/Named/MapCastInterp                                | 0m09.93s  || -0m00.07s
0m09.00s  | Arithmetic/MontgomeryReduction/Proofs                        | 0m09.90s  || -0m00.90s
0m07.49s  | Specific/ArithmeticSynthesisTest                             | 0m08.48s  || -0m00.99s
0m06.82s  | Util/FixedWordSizesEquality                                  | 0m06.86s  || -0m00.04s
0m06.79s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate           | 0m06.82s  || -0m00.03s
0m05.36s  | LegacyArithmetic/Pow2BaseProofs                              | 0m05.65s  || -0m00.29s
0m05.33s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub             | 0m05.49s  || -0m00.16s
0m03.92s  | Arithmetic/BarrettReduction/HAC                              | 0m03.84s  || +0m00.08s
0m03.46s  | Arithmetic/Saturated                                         | 0m03.90s  || -0m00.43s
0m03.34s  | LegacyArithmetic/InterfaceProofs                             | 0m03.67s  || -0m00.33s
0m03.14s  | Specific/FancyMachine256/Montgomery                          | 0m03.69s  || -0m00.54s
0m03.06s  | LegacyArithmetic/ZBoundedZ                                   | 0m03.31s  || -0m00.25s
0m02.98s  | Arithmetic/BarrettReduction/Generalized                      | 0m02.93s  || +0m00.04s
0m02.94s  | Arithmetic/ModularArithmeticTheorems                         | 0m02.95s  || -0m00.01s
0m02.89s  | Specific/FancyMachine256/Barrett                             | 0m03.36s  || -0m00.46s
0m02.64s  | LegacyArithmetic/Double/Proofs/ShiftLeft                     | 0m03.19s  || -0m00.54s
0m02.45s  | LegacyArithmetic/Double/Proofs/Decode                        | 0m02.54s  || -0m00.08s
0m02.34s  | Compilers/Z/Bounds/Relax                                     | 0m02.46s  || -0m00.12s
0m02.10s  | Util/WordUtil                                                | 0m02.15s  || -0m00.04s
0m02.09s  | LegacyArithmetic/BarretReduction                             | 0m02.51s  || -0m00.41s
0m01.93s  | Specific/FancyMachine256/Core                                | 0m02.18s  || -0m00.25s
0m01.54s  | LegacyArithmetic/MontgomeryReduction                         | 0m01.76s  || -0m00.21s
0m01.52s  | Arithmetic/PrimeFieldTheorems                                | 0m01.50s  || +0m00.02s
0m01.48s  | Arithmetic/BarrettReduction/Wikipedia                        | 0m01.52s  || -0m00.04s
0m01.22s  | Compilers/Z/Syntax/Equality                                  | 0m01.32s  || -0m00.10s
0m01.09s  | Compilers/Z/Bounds/Pipeline/Definition                       | 0m01.14s  || -0m00.04s
0m01.08s  | Util/NumTheoryUtil                                           | 0m01.07s  || +0m00.01s
0m00.96s  | Arithmetic/Karatsuba                                         | 0m00.88s  || +0m00.07s
0m00.90s  | LegacyArithmetic/Double/Proofs/BitwiseOr                     | 0m01.17s  || -0m00.26s
0m00.83s  | LegacyArithmetic/BaseSystemProofs                            | 0m00.80s  || +0m00.02s
0m00.82s  | LegacyArithmetic/Double/Proofs/LoadImmediate                 | 0m00.97s  || -0m00.15s
0m00.76s  | Compilers/MapCastByDeBruijnInterp                            | 0m00.83s  || -0m00.06s
0m00.68s  | Util/IterAssocOp                                             | 0m00.68s  || +0m00.00s
0m00.67s  | Compilers/Z/Syntax/Util                                      | 0m00.63s  || +0m00.04s
0m00.66s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                | 0m00.71s  || -0m00.04s
0m00.66s  | LegacyArithmetic/Double/Proofs/SelectConditional             | 0m00.87s  || -0m00.20s
0m00.66s  | Compilers/MapCastByDeBruijnWf                                | 0m00.72s  || -0m00.05s
0m00.61s  | LegacyArithmetic/Interface                                   | 0m00.63s  || -0m00.02s
0m00.52s  | Spec/EdDSA                                                   | 0m00.48s  || +0m00.04s
0m00.49s  | Compilers/Z/Bounds/Pipeline                                  | 0m00.56s  || -0m00.07s
0m00.48s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics              | 0m00.44s  || +0m00.03s
0m00.48s  | Util/NUtil                                                   | 0m00.64s  || -0m00.16s
0m00.47s  | LegacyArithmetic/Double/Core                                 | 0m00.46s  || +0m00.00s
0m00.46s  | Arithmetic/ModularArithmeticPre                              | 0m00.52s  || -0m00.06s
0m00.46s  | Compilers/Z/MapCastByDeBruijnWf                              | 0m00.43s  || +0m00.03s
0m00.45s  | LegacyArithmetic/Pow2Base                                    | 0m00.46s  || -0m00.01s
0m00.45s  | LegacyArithmetic/ZBounded                                    | 0m00.47s  || -0m00.01s
0m00.45s  | Compilers/Z/Bounds/Pipeline/Glue                             | 0m00.49s  || -0m00.03s
0m00.44s  | LegacyArithmetic/ArchitectureToZLike                         | 0m00.54s  || -0m00.10s
0m00.44s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                   | 0m00.46s  || -0m00.02s
0m00.44s  | Compilers/Z/Reify                                            | 0m00.54s  || -0m00.10s
0m00.43s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic          | 0m00.44s  || -0m00.01s
0m00.42s  | Compilers/Z/MapCastByDeBruijnInterp                          | 0m00.40s  || +0m00.01s
0m00.41s  | LegacyArithmetic/BaseSystem                                  | 0m00.43s  || -0m00.02s
0m00.40s  | Compilers/Z/Bounds/MapCastByDeBruijn                         | 0m00.37s  || +0m00.03s
0m00.39s  | Spec/ModularArithmetic                                       | 0m00.38s  || +0m00.01s
0m00.36s  | Arithmetic/MontgomeryReduction/Definition                    | 0m00.39s  || -0m00.03s
0m00.36s  | Compilers/Z/InlineWf                                         | 0m00.35s  || +0m00.01s
0m00.36s  | Compilers/Z/FoldTypes                                        | 0m00.40s  || -0m00.04s
0m00.36s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                       | 0m00.50s  || -0m00.14s
0m00.34s  | Compilers/Z/Inline                                           | 0m00.36s  || -0m00.01s
0m00.33s  | Compilers/Z/InlineInterp                                     | 0m00.37s  || -0m00.03s

1 files changed, 149 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index e8d963b1b..13fea5c45 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -22,8 +22,9 @@ Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
 Hint Extern 1 => nia : nia.
 Hint Extern 1 => omega : omega.
-Hint Resolve Z.log2_nonneg Z.log2_up_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 Z.log2_nonneg Z.log2_up_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 Z.div_le_compat_l Z.div_le_mono : 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.opp_le_mono n m)) : 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.
 
@@ -2639,6 +2640,153 @@ Module Z.
     try (apply f_equal2; [ | reflexivity ]);
     try zutil_arith.
 
+  Ltac clean_neg :=
+    repeat match goal with
+           | [ H : (-?x) < 0 |- _ ] => assert (0 < x) by omega; clear H
+           | [ H : 0 > (-?x) |- _ ] => assert (0 < x) by omega; clear H
+           | [ H : -?x <= -?y |- _ ] => apply Z.opp_le_mono in H
+           | [ |- -?x <= -?y ] => apply Z.opp_le_mono
+           | _ => progress rewrite <- Z.opp_le_mono in *
+           | [ H : 0 <= ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x < ?y |- _ ] => clear H''
+           | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
+           end.
+  Ltac replace_with_neg x :=
+    assert (x = -(-x)) by omega; generalize dependent (-x);
+    let x' := fresh in
+    rename x into x'; intro x; intros; subst x';
+    clean_neg.
+  Ltac replace_all_neg_with_pos :=
+    repeat match goal with
+           | [ H : ?x < 0 |- _ ] => replace_with_neg x
+           | [ H : 0 > ?x |- _ ] => replace_with_neg x
+           end.
+
+  Lemma shiftl_le_Proper2 y
+    : Proper (Z.le ==> Z.le) (fun x => Z.shiftl x y).
+  Proof.
+    unfold Basics.flip in *.
+    pose proof (Zle_cases 0 y) as Hx.
+    intros x x' H.
+    pose proof (Zle_cases 0 x) as Hy.
+    pose proof (Zle_cases 0 x') as Hy'.
+    destruct (0 <=? y), (0 <=? x), (0 <=? x');
+      autorewrite with Zshift_to_pow;
+      replace_all_neg_with_pos;
+      autorewrite with pull_Zopp;
+      rewrite ?Z.div_opp_l_complete;
+      repeat destruct (Z_zerop _);
+      autorewrite with zsimplify_const pull_Zopp;
+      auto with zarith;
+      repeat match goal with
+             | [ |- context[-?x - ?y] ]
+               => replace (-x - y) with (-(x + y)) by omega
+             | _ => rewrite <- Z.opp_le_mono
+             | _ => rewrite <- Z.add_le_mono_r
+             | _ => solve [ auto with zarith ]
+             | [ |- ?x <= ?y + 1 ]
+               => cut (x <= y); [ omega | solve [ auto with zarith ] ]
+             | [ |- -_ <= _ ]
+               => solve [ transitivity (-0); auto with zarith ]
+             end.
+    { repeat match goal with H : context[_ mod _] |- _ => revert H end;
+        Z.div_mod_to_quot_rem; nia. }
+  Qed.
+
+  Lemma shiftl_le_Proper1 x
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+    : Proper (R (0 <=? x) ==> Z.le) (Z.shiftl x).
+  Proof.
+    unfold Basics.flip in *.
+    pose proof (Zle_cases 0 x) as Hx.
+    intros y y' H.
+    pose proof (Zle_cases 0 y) as Hy.
+    pose proof (Zle_cases 0 y') as Hy'.
+    destruct (0 <=? x), (0 <=? y), (0 <=? y'); subst R; cbv beta iota in *;
+      autorewrite with Zshift_to_pow;
+      replace_all_neg_with_pos;
+      autorewrite with pull_Zopp;
+      rewrite ?Z.div_opp_l_complete;
+      repeat destruct (Z_zerop _);
+      autorewrite with zsimplify_const pull_Zopp;
+      auto with zarith;
+      repeat match goal with
+             | [ |- context[-?x - ?y] ]
+               => replace (-x - y) with (-(x + y)) by omega
+             | _ => rewrite <- Z.opp_le_mono
+             | _ => rewrite <- Z.add_le_mono_r
+             | _ => solve [ auto with zarith ]
+             | [ |- ?x <= ?y + 1 ]
+               => cut (x <= y); [ omega | solve [ auto with zarith ] ]
+             | [ |- context[2^?x] ]
+               => lazymatch goal with
+                  | [ H : 1 < 2^x |- _ ] => fail
+                  | [ H : 0 < 2^x |- _ ] => fail
+                  | [ H : 0 <= 2^x |- _ ] => fail
+                  | _ => first [ assert (1 < 2^x) by auto with zarith
+                               | assert (0 < 2^x) by auto with zarith
+                               | assert (0 <= 2^x) by auto with zarith ]
+                  end
+             | [ H : ?x <= ?y |- _ ]
+               => is_var x; is_var y;
+                    lazymatch goal with
+                    | [ H : 2^x <= 2^y |- _ ] => fail
+                    | [ H : 2^x < 2^y |- _ ] => fail
+                    | _ => assert (2^x <= 2^y) by auto with zarith
+                    end
+             | [ H : ?x <= ?y, H' : ?f ?x = ?k, H'' : ?f ?y <> ?k |- _ ]
+               => let Hn := fresh in
+                  assert (Hn : x <> y) by congruence;
+                    assert (x < y) by omega; clear H Hn
+             | [ H : ?x <= ?y, H' : ?f ?x <> ?k, H'' : ?f ?y = ?k |- _ ]
+               => let Hn := fresh in
+                  assert (Hn : x <> y) by congruence;
+                    assert (x < y) by omega; clear H Hn
+             | _ => solve [ repeat match goal with H : context[_ mod _] |- _ => revert H end;
+                            Z.div_mod_to_quot_rem; subst;
+                            lazymatch goal with
+                            | [ |- _ <= (?a * ?q + ?r) * ?q' ]
+                              => transitivity (q * (a * q') + r * q');
+                                 [ assert (0 < a * q') by nia; nia
+                                 | nia ]
+                            end ]
+             end.
+    { replace y' with (y + (y' - y)) by omega.
+      rewrite Z.pow_add_r, <- Zdiv_Zdiv by auto with zarith.
+      assert (y < y') by (assert (y <> y') by congruence; omega).
+      assert (1 < 2^(y'-y)) by auto with zarith.
+      assert (0 < x / 2^y)
+        by (repeat match goal with H : context[_ mod _] |- _ => revert H end;
+            Z.div_mod_to_quot_rem; nia).
+      assert (2^y <= x)
+        by (repeat match goal with H : context[_ / _] |- _ => revert H end;
+            Z.div_mod_to_quot_rem; nia).
+      match goal with
+      | [ |- ?x + 1 <= ?y ] => cut (x < y); [ omega | ]
+      end.
+      auto with zarith. }
+  Qed.
+
+  Lemma shiftr_le_Proper2 y
+    : Proper (Z.le ==> Z.le) (fun x => Z.shiftr x y).
+  Proof. apply shiftl_le_Proper2. Qed.
+
+  Lemma shiftr_le_Proper1 x
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+    : Proper (R (x <? 0) ==> Z.le) (Z.shiftr x).
+  Proof.
+    subst R; intros y y' H'; unfold Z.shiftr; apply shiftl_le_Proper1.
+    unfold Basics.flip in *.
+    pose proof (Zle_cases 0 x).
+    pose proof (Zlt_cases x 0).
+    destruct (0 <=? x), (x <? 0); try omega.
+  Qed.
+
+
   (* Naming Convention: [X] for thing being divided by, [p] for plus,
      [m] for minus, [d] for div, and [_] to separate parentheses and
      multiplication. *)