More zsimplify lemmas, stronger Ztestbit

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
5m47.85s | Total                                           | 5m48.53s || -0m00.67s
----------------------------------------------------------------------------------
1m34.28s | Test/Curve25519SpecTestVectors                  | 1m35.44s || -0m01.15s
0m35.79s | ModularArithmetic/Conversion                    | 0m36.48s || -0m00.68s
0m27.42s | ModularArithmetic/ModularBaseSystemProofs       | 0m28.32s || -0m00.89s
0m22.15s | BoundedArithmetic/DoubleBoundedProofs           | 0m21.67s || +0m00.47s
0m21.62s | ModularArithmetic/Pow2BaseProofs                | 0m21.38s || +0m00.24s
0m19.60s | EdDSARepChange                                  | 0m19.98s || -0m00.37s
0m14.52s | Specific/GF25519                                | 0m14.89s || -0m00.37s
0m12.99s | Util/ZUtil                                      | 0m12.60s || +0m00.39s
0m09.80s | Testbit                                         | 0m09.45s || +0m00.35s
0m08.85s | ModularArithmetic/Montgomery/ZProofs            | 0m08.11s || +0m00.74s
0m08.21s | BoundedArithmetic/ArchitectureToZLikeProofs     | 0m08.57s || -0m00.35s
0m07.85s | Encoding/PointEncoding                          | 0m08.24s || -0m00.39s
0m07.71s | Specific/GF1305                                 | 0m07.87s || -0m00.16s
0m03.94s | BaseSystemProofs                                | 0m03.85s || +0m00.08s
0m03.93s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m03.64s || +0m00.29s
0m03.52s | ModularArithmetic/Tutorial                      | 0m03.35s || +0m00.16s
0m03.48s | ModularArithmetic/ModularBaseSystemListProofs   | 0m03.58s || -0m00.10s
0m03.36s | BoundedArithmetic/InterfaceProofs               | 0m03.18s || +0m00.17s
0m03.16s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.89s || +0m00.27s
0m02.80s | Encoding/PointEncodingPre                       | 0m02.87s || -0m00.07s
0m02.65s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.59s || +0m00.06s
0m02.48s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.32s || +0m00.16s
0m02.36s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.35s || +0m00.00s
0m02.24s | Specific/FancyMachine256/Montgomery             | 0m02.01s || +0m00.23s
0m02.14s | Specific/FancyMachine256/Barrett                | 0m02.11s || +0m00.03s
0m01.89s | Specific/FancyMachine256/Core                   | 0m01.68s || +0m00.20s
0m01.86s | ModularArithmetic/Montgomery/ZBounded           | 0m01.83s || +0m00.03s
0m01.55s | ModularArithmetic/BarrettReduction/Z            | 0m01.50s || +0m00.05s
0m01.27s | ModularArithmetic/PrimeFieldTheorems            | 0m01.36s || -0m00.09s
0m01.26s | BaseSystem                                      | 0m01.35s || -0m00.09s
0m01.12s | ModularArithmetic/ExtendedBaseVector            | 0m01.17s || -0m00.04s
0m00.92s | Util/NumTheoryUtil                              | 0m00.87s || +0m00.05s
0m00.89s | Experiments/EncodingLemmas                      | 0m00.84s || +0m00.05s
0m00.67s | Encoding/ModularWordEncodingTheorems            | 0m00.64s || +0m00.03s
0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.74s || -0m00.07s
0m00.64s | Spec/EdDSA                                      | 0m00.58s || +0m00.06s
0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.63s || -0m00.03s
0m00.60s | Encoding/ModularWordEncodingPre                 | 0m00.60s || +0m00.00s
0m00.60s | ModularArithmetic/ModularBaseSystem             | 0m00.61s || -0m00.01s
0m00.59s | BoundedArithmetic/Interface                     | 0m00.62s || -0m00.03s
0m00.58s | ModularArithmetic/ModularBaseSystemList         | 0m00.60s || -0m00.02s
0m00.56s | Spec/Ed25519                                    | 0m00.55s || +0m00.01s
0m00.55s | Spec/ModularWordEncoding                        | 0m00.59s || -0m00.03s
0m00.54s | BoundedArithmetic/StripCF                       | 0m00.44s || +0m00.10s
0m00.52s | ModularArithmetic/ZBounded                      | 0m00.44s || +0m00.08s
0m00.49s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.37s || +0m00.12s
0m00.48s | BoundedArithmetic/DoubleBounded                 | 0m00.53s || -0m00.05s
0m00.47s | ModularArithmetic/Pre                           | 0m00.47s || +0m00.00s
0m00.46s | BoundedArithmetic/ArchitectureToZLike           | 0m00.50s || -0m00.03s
0m00.43s | ModularArithmetic/Pow2Base                      | 0m00.44s || -0m00.01s
0m00.42s | Spec/ModularArithmetic                          | 0m00.38s || +0m00.03s
0m00.38s | ModularArithmetic/Montgomery/Z                  | 0m00.46s || -0m00.08s

1 files changed, 117 insertions, 4 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index b5c2e63a7..657ba8468 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -19,7 +19,7 @@ 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.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 : zarith.
+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.
 
 Ltac zutil_arith := solve [ omega | lia | auto with nocore ].
@@ -39,13 +39,13 @@ Create HintDb zsimplify_const discriminated.
 (** We create separate databases for two directions of transformations
       involving [Z.log2]; combining them leads to loops. *)
 (* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *)
-Create HintDb hyp_log2.
+Create HintDb hyp_log2 discriminated.
 (* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *)
-Create HintDb concl_log2.
+Create HintDb concl_log2 discriminated.
 Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2.
 Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2.
 Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l : zsimplify_fast.
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus : zsimplify.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag : zsimplify.
 Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l using zutil_arith : zsimplify.
 Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify.
 Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify.
@@ -806,6 +806,17 @@ Module Z.
   Qed.
   Hint Rewrite <- Z.lor_shiftl using zutil_arith : convert_to_Ztestbit.
 
+  Lemma shiftl_spec_full a n m
+    : Z.testbit (a << n) m = if Z_lt_dec m n
+                             then false
+                             else if Z_le_dec 0 m
+                                  then Z.testbit a (m - n)
+                                  else false.
+  Proof.
+    repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega.
+  Qed.
+  Hint Rewrite shiftl_spec_full : Ztestbit.
+
   (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
   Ltac zero_bounds' :=
     repeat match goal with
@@ -1935,6 +1946,19 @@ Module Z.
       omega.
   Qed.
 
+  Lemma shiftr_nonneg_le : forall a n, 0 <= a -> 0 <= n -> a >> n <= a.
+  Proof.
+    intros.
+    repeat match goal with
+           | [ H : _ <= _ |- _ ]
+             => rewrite Z.lt_eq_cases in H
+           | [ H : _ \/ _ |- _ ] => destruct H
+           | _ => progress subst
+           | _ => progress autorewrite with zsimplify Zshift_to_pow
+           | _ => solve [ auto with zarith omega ]
+           end.
+  Qed.
+  Hint Resolve shiftr_nonneg_le : zarith.
 
   Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y.
   Proof. lia. Qed.
@@ -2490,11 +2514,21 @@ def to_def(name):
 
 names = []
 names += ['%sX%s%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp']
+names += ['%sX%s_X%s' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp']
 names += ['X%s%s_X%s' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp']
+names += ['%sX%s_%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp']
+names += ['X%s%s_%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp']
 names += ['m2XpX', 'm2XpXpX']
 
+print(r'''  (* Python code to generate these hints:
+<<''')
+print(open(__file__).read())
+print(r'''
+>> *)''')
 for name in names:
     print(to_def(name))
+
+
 >> *)
   Lemma simplify_mXmmX a b X : a - X - b - X = - 2 * X + a - b.
   Proof. lia. Qed.
@@ -2520,6 +2554,30 @@ for name in names:
   Lemma simplify_pXppX a b X : a + X + b + X = 2 * X + a + b.
   Proof. lia. Qed.
   Hint Rewrite simplify_pXppX : zsimplify.
+  Lemma simplify_mXm_Xm a b X : a - X - (X - b) = - 2 * X + a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXm_Xm : zsimplify.
+  Lemma simplify_mXm_Xp a b X : a - X - (X + b) = - 2 * X + a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXm_Xp : zsimplify.
+  Lemma simplify_mXp_Xm a b X : a - X + (X - b) = a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXp_Xm : zsimplify.
+  Lemma simplify_mXp_Xp a b X : a - X + (X + b) = a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXp_Xp : zsimplify.
+  Lemma simplify_pXm_Xm a b X : a + X - (X - b) = a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXm_Xm : zsimplify.
+  Lemma simplify_pXm_Xp a b X : a + X - (X + b) = a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXm_Xp : zsimplify.
+  Lemma simplify_pXp_Xm a b X : a + X + (X - b) = 2 * X + a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXp_Xm : zsimplify.
+  Lemma simplify_pXp_Xp a b X : a + X + (X + b) = 2 * X + a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXp_Xp : zsimplify.
   Lemma simplify_Xmm_Xm a b X : X - a - (X - b) = - a + b.
   Proof. lia. Qed.
   Hint Rewrite simplify_Xmm_Xm : zsimplify.
@@ -2544,6 +2602,54 @@ for name in names:
   Lemma simplify_Xpp_Xp a b X : X + a + (X + b) = 2 * X + a + b.
   Proof. lia. Qed.
   Hint Rewrite simplify_Xpp_Xp : zsimplify.
+  Lemma simplify_mXm_mX a b X : a - X - (b - X) = a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXm_mX : zsimplify.
+  Lemma simplify_mXm_pX a b X : a - X - (b + X) = - 2 * X + a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXm_pX : zsimplify.
+  Lemma simplify_mXp_mX a b X : a - X + (b - X) = - 2 * X + a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXp_mX : zsimplify.
+  Lemma simplify_mXp_pX a b X : a - X + (b + X) = a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_mXp_pX : zsimplify.
+  Lemma simplify_pXm_mX a b X : a + X - (b - X) = 2 * X + a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXm_mX : zsimplify.
+  Lemma simplify_pXm_pX a b X : a + X - (b + X) = a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXm_pX : zsimplify.
+  Lemma simplify_pXp_mX a b X : a + X + (b - X) = a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXp_mX : zsimplify.
+  Lemma simplify_pXp_pX a b X : a + X + (b + X) = 2 * X + a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_pXp_pX : zsimplify.
+  Lemma simplify_Xmm_mX a b X : X - a - (b - X) = 2 * X - a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xmm_mX : zsimplify.
+  Lemma simplify_Xmm_pX a b X : X - a - (b + X) = - a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xmm_pX : zsimplify.
+  Lemma simplify_Xmp_mX a b X : X - a + (b - X) = - a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xmp_mX : zsimplify.
+  Lemma simplify_Xmp_pX a b X : X - a + (b + X) = 2 * X - a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xmp_pX : zsimplify.
+  Lemma simplify_Xpm_mX a b X : X + a - (b - X) = 2 * X + a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xpm_mX : zsimplify.
+  Lemma simplify_Xpm_pX a b X : X + a - (b + X) = a - b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xpm_pX : zsimplify.
+  Lemma simplify_Xpp_mX a b X : X + a + (b - X) = a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xpp_mX : zsimplify.
+  Lemma simplify_Xpp_pX a b X : X + a + (b + X) = 2 * X + a + b.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_Xpp_pX : zsimplify.
   Lemma simplify_m2XpX a X : a - 2 * X + X = - X + a.
   Proof. lia. Qed.
   Hint Rewrite simplify_m2XpX : zsimplify.
@@ -2694,3 +2800,10 @@ Ltac pull_Zmod :=
            => rewrite (Zmod_mod x z)
          | _ => progress autorewrite with pull_Zmod
          end.
+
+Ltac Ztestbit :=
+  repeat match goal with
+         | _ => progress autorewrite with Ztestbit
+         | [ |- context[Z.testbit ?x ?y] ]
+           => rewrite (Z.testbit_neg_r x y) by zutil_arith
+         end.