Add a Ztestbit_full database

After    | File Name                                                  | Before   || Change
---------------------------------------------------------------------------------------------
6m00.58s | Total                                                      | 6m23.23s || -0m22.64s
---------------------------------------------------------------------------------------------
0m35.50s | ModularArithmetic/Conversion                               | 0m39.25s || -0m03.75s
1m35.19s | Test/Curve25519SpecTestVectors                             | 1m38.04s || -0m02.84s
0m06.69s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate        | 0m08.83s || -0m02.13s
0m27.51s | ModularArithmetic/ModularBaseSystemProofs                  | 0m28.99s || -0m01.47s
0m08.13s | Encoding/PointEncoding                                     | 0m09.64s || -0m01.50s
0m05.25s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub          | 0m06.96s || -0m01.71s
0m22.82s | ModularArithmetic/Pow2BaseProofs                           | 0m23.37s || -0m00.55s
0m20.17s | EdDSARepChange                                             | 0m20.89s || -0m00.71s
0m14.41s | Specific/GF25519                                           | 0m14.81s || -0m00.40s
0m13.08s | Util/ZUtil                                                 | 0m13.30s || -0m00.22s
0m10.31s | Testbit                                                    | 0m10.50s || -0m00.18s
0m09.57s | ModularArithmetic/Montgomery/ZProofs                       | 0m09.74s || -0m00.16s
0m08.46s | BoundedArithmetic/ArchitectureToZLikeProofs                | 0m08.68s || -0m00.21s
0m08.16s | BoundedArithmetic/Double/Proofs/Multiply                   | 0m09.02s || -0m00.85s
0m07.64s | Specific/GF1305                                            | 0m07.94s || -0m00.30s
0m04.01s | ModularArithmetic/Tutorial                                 | 0m03.61s || +0m00.39s
0m03.91s | BaseSystemProofs                                           | 0m04.01s || -0m00.09s
0m03.86s | ModularArithmetic/BarrettReduction/ZHandbook               | 0m04.40s || -0m00.54s
0m03.46s | ModularArithmetic/ModularBaseSystemListProofs              | 0m03.65s || -0m00.18s
0m03.37s | BoundedArithmetic/InterfaceProofs                          | 0m03.98s || -0m00.60s
0m03.28s | ModularArithmetic/BarrettReduction/ZGeneralized            | 0m03.78s || -0m00.50s
0m02.86s | Encoding/PointEncodingPre                                  | 0m03.22s || -0m00.36s
0m02.78s | BoundedArithmetic/Double/Proofs/Decode                     | 0m03.25s || -0m00.47s
0m02.78s | ModularArithmetic/ModularArithmeticTheorems                | 0m03.42s || -0m00.64s
0m02.31s | ModularArithmetic/ModularBaseSystemOpt                     | 0m02.38s || -0m00.06s
0m02.26s | Specific/FancyMachine256/Barrett                           | 0m02.80s || -0m00.54s
0m02.22s | ModularArithmetic/BarrettReduction/ZBounded                | 0m02.54s || -0m00.31s
0m02.07s | Specific/FancyMachine256/Montgomery                        | 0m02.31s || -0m00.24s
0m01.83s | ModularArithmetic/Montgomery/ZBounded                      | 0m02.12s || -0m00.29s
0m01.78s | Specific/FancyMachine256/Core                              | 0m01.78s || +0m00.00s
0m01.70s | ModularArithmetic/PrimeFieldTheorems                       | 0m01.38s || +0m00.32s
0m01.52s | ModularArithmetic/BarrettReduction/Z                       | 0m01.88s || -0m00.35s
0m01.38s | BaseSystem                                                 | 0m01.40s || -0m00.02s
0m01.24s | BoundedArithmetic/Double/Repeated/Proofs/Decode            | 0m01.16s || +0m00.08s
0m01.10s | ModularArithmetic/ExtendedBaseVector                       | 0m01.20s || -0m00.09s
0m01.05s | Util/NumTheoryUtil                                         | 0m01.01s || +0m00.04s
0m00.88s | Experiments/EncodingLemmas                                 | 0m00.93s || -0m00.05s
0m00.86s | BoundedArithmetic/Double/Proofs/LoadImmediate              | 0m00.92s || -0m00.06s
0m00.84s | BoundedArithmetic/Double/Proofs/BitwiseOr                  | 0m01.19s || -0m00.35s
0m00.80s | Encoding/ModularWordEncodingPre                            | 0m00.61s || +0m00.19s
0m00.78s | ModularArithmetic/PseudoMersenneBaseParamProofs            | 0m00.75s || +0m00.03s
0m00.71s | BoundedArithmetic/X86ToZLike                               | 0m00.89s || -0m00.18s
0m00.67s | Encoding/ModularWordEncodingTheorems                       | 0m00.72s || -0m00.04s
0m00.62s | BoundedArithmetic/Interface                                | 0m00.66s || -0m00.04s
0m00.62s | Spec/EdDSA                                                 | 0m00.59s || +0m00.03s
0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs                     | 0m00.74s || -0m00.13s
0m00.61s | Spec/ModularWordEncoding                                   | 0m00.69s || -0m00.07s
0m00.61s | ModularArithmetic/ModularBaseSystemList                    | 0m00.65s || -0m00.04s
0m00.60s | BoundedArithmetic/Double/Core                              | 0m00.49s || +0m00.10s
0m00.60s | Spec/Ed25519                                               | 0m00.50s || +0m00.09s
0m00.58s | ModularArithmetic/ModularBaseSystem                        | 0m00.62s || -0m00.04s
0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.63s || -0m00.07s
0m00.53s | BoundedArithmetic/Double/Proofs/SelectConditional          | 0m00.62s || -0m00.08s
0m00.51s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.55s || -0m00.04s
0m00.50s | BoundedArithmetic/StripCF                                  | 0m00.51s || -0m00.01s
0m00.50s | BoundedArithmetic/ArchitectureToZLike                      | 0m00.48s || +0m00.02s
0m00.49s | ModularArithmetic/Pre                                      | 0m00.47s || +0m00.02s
0m00.49s | BoundedArithmetic/Double/Repeated/Core                     | 0m00.48s || +0m00.01s
0m00.48s | ModularArithmetic/ZBounded                                 | 0m00.50s || -0m00.02s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr         | 0m00.54s || -0m00.08s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate     | 0m00.54s || -0m00.08s
0m00.44s | ModularArithmetic/Pow2Base                                 | 0m00.49s || -0m00.04s
0m00.40s | ModularArithmetic/PseudoMersenneBaseParams                 | 0m00.44s || -0m00.03s
0m00.38s | ModularArithmetic/Montgomery/Z                             | 0m00.44s || -0m00.06s
0m00.35s | Spec/ModularArithmetic                                     | 0m00.36s || -0m00.01s

1 files changed, 46 insertions, 2 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 8d482d1ee..c98b63554 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -203,8 +203,10 @@ Ltac zify_nat_op ::=
  end.
 
 Create HintDb Ztestbit discriminated.
-Hint Rewrite Z.testbit_0_l : Ztestbit.
-Hint Rewrite Z.land_spec Z.lor_spec Z.shiftl_spec Z.shiftr_spec using zutil_arith : Ztestbit.
+Create HintDb Ztestbit_full discriminated.
+Hint Rewrite Z.testbit_0_l Z.land_spec Z.lor_spec : Ztestbit.
+Hint Rewrite Z.testbit_0_l Z.land_spec Z.lor_spec : Ztestbit_full.
+Hint Rewrite Z.shiftl_spec Z.shiftr_spec using zutil_arith : Ztestbit.
 Hint Rewrite Z.testbit_neg_r using zutil_arith : Ztestbit.
 Hint Rewrite Bool.andb_true_r Bool.andb_false_r Bool.orb_true_r Bool.orb_false_r
              Bool.andb_true_l Bool.andb_false_l Bool.orb_true_l Bool.orb_false_l : Ztestbit.
@@ -247,6 +249,22 @@ Module Z.
   Qed.
   Hint Rewrite ones_spec using zutil_arith : Ztestbit.
 
+  Lemma ones_spec_full : forall n m, Z.testbit (Z.ones n) m
+                                     = if Z_lt_dec m 0
+                                       then false
+                                       else if Z_lt_dec n 0
+                                            then true
+                                            else if Z_lt_dec m n then true else false.
+  Proof.
+    intros.
+    repeat (break_if || autorewrite with Ztestbit); try reflexivity; try omega.
+    unfold Z.ones.
+    rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl.
+    destruct m; simpl in *; try reflexivity.
+    exfalso; auto using Zlt_neg_0.
+  Qed.
+  Hint Rewrite ones_spec_full : Ztestbit_full.
+
   Lemma testbit_pow2_mod : forall a n i, 0 <= n ->
   Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false.
   Proof.
@@ -261,6 +279,20 @@ Module Z.
   Qed.
   Hint Rewrite testbit_pow2_mod using zutil_arith : Ztestbit.
 
+  Lemma testbit_pow2_mod_full : forall a n i,
+      Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec n 0
+                                     then if Z_lt_dec i 0 then false else Z.testbit a i
+                                     else if Z_lt_dec i n then Z.testbit a i else false.
+  Proof.
+    intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ].
+    unfold pow2_mod.
+    autorewrite with Ztestbit_full;
+      repeat break_match;
+      autorewrite with Ztestbit;
+      reflexivity.
+  Qed.
+  Hint Rewrite testbit_pow2_mod_full : Ztestbit_full.
+
   Lemma bits_above_pow2 a n : 0 <= a < 2^n -> Z.testbit a n = false.
   Proof.
     intros.
@@ -824,6 +856,17 @@ Module Z.
   Qed.
   Hint Rewrite shiftl_spec_full : Ztestbit.
 
+  Lemma shiftr_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
@@ -2817,4 +2860,5 @@ Ltac Ztestbit :=
            => rewrite (Z.bits_above_pow2 x y) by zutil_arith
          | [ |- context[Z.testbit ?x ?y] ]
            => rewrite (Z.bits_above_log2 x y) by zutil_arith
+         | _ => progress autorewrite with Ztestbit_full
          end.