Add testbit_add_shiftl_full

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
5m41.93s | Total                                           | 5m42.43s || -0m00.50s
----------------------------------------------------------------------------------
1m34.78s | Test/Curve25519SpecTestVectors                  | 1m34.04s || +0m00.74s
0m34.74s | ModularArithmetic/Conversion                    | 0m35.23s || -0m00.48s
0m27.39s | ModularArithmetic/ModularBaseSystemProofs       | 0m27.12s || +0m00.26s
0m21.67s | ModularArithmetic/Pow2BaseProofs                | 0m21.30s || +0m00.37s
0m20.51s | BoundedArithmetic/DoubleBoundedProofs           | 0m20.75s || -0m00.23s
0m19.42s | EdDSARepChange                                  | 0m19.76s || -0m00.33s
0m14.36s | Specific/GF25519                                | 0m14.30s || +0m00.05s
0m12.32s | Util/ZUtil                                      | 0m12.23s || +0m00.08s
0m09.36s | Testbit                                         | 0m09.15s || +0m00.20s
0m08.41s | ModularArithmetic/Montgomery/ZProofs            | 0m08.39s || +0m00.01s
0m08.35s | BoundedArithmetic/ArchitectureToZLikeProofs     | 0m08.48s || -0m00.13s
0m08.05s | Encoding/PointEncoding                          | 0m08.02s || +0m00.03s
0m07.51s | Specific/GF1305                                 | 0m07.54s || -0m00.03s
0m03.86s | BaseSystemProofs                                | 0m03.84s || +0m00.02s
0m03.57s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m03.69s || -0m00.12s
0m03.46s | ModularArithmetic/ModularBaseSystemListProofs   | 0m03.47s || -0m00.01s
0m03.44s | ModularArithmetic/Tutorial                      | 0m03.59s || -0m00.14s
0m03.26s | BoundedArithmetic/InterfaceProofs               | 0m03.16s || +0m00.09s
0m02.87s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.87s || +0m00.00s
0m02.80s | Encoding/PointEncodingPre                       | 0m02.94s || -0m00.14s
0m02.53s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.58s || -0m00.05s
0m02.25s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.28s || -0m00.02s
0m02.24s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.29s || -0m00.04s
0m02.07s | Specific/FancyMachine256/Montgomery             | 0m02.22s || -0m00.15s
0m02.02s | Specific/FancyMachine256/Barrett                | 0m02.16s || -0m00.14s
0m01.83s | ModularArithmetic/Montgomery/ZBounded           | 0m01.74s || +0m00.09s
0m01.66s | Specific/FancyMachine256/Core                   | 0m01.73s || -0m00.07s
0m01.48s | ModularArithmetic/BarrettReduction/Z            | 0m01.40s || +0m00.08s
0m01.28s | BaseSystem                                      | 0m01.20s || +0m00.08s
0m01.27s | ModularArithmetic/PrimeFieldTheorems            | 0m01.56s || -0m00.29s
0m01.16s | ModularArithmetic/ExtendedBaseVector            | 0m01.19s || -0m00.03s
0m00.95s | Util/NumTheoryUtil                              | 0m00.91s || +0m00.03s
0m00.87s | Experiments/EncodingLemmas                      | 0m00.96s || -0m00.08s
0m00.70s | ModularArithmetic/ModularBaseSystem             | 0m00.62s || +0m00.07s
0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.66s || +0m00.01s
0m00.65s | BoundedArithmetic/Interface                     | 0m00.64s || +0m00.01s
0m00.64s | Encoding/ModularWordEncodingPre                 | 0m00.62s || +0m00.02s
0m00.64s | Spec/EdDSA                                      | 0m00.70s || -0m00.05s
0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.60s || +0m00.01s
0m00.61s | Encoding/ModularWordEncodingTheorems            | 0m00.63s || -0m00.02s
0m00.56s | Spec/ModularWordEncoding                        | 0m00.56s || +0m00.00s
0m00.56s | ModularArithmetic/ModularBaseSystemList         | 0m00.62s || -0m00.05s
0m00.52s | BoundedArithmetic/DoubleBounded                 | 0m00.43s || +0m00.09s
0m00.52s | ModularArithmetic/ZBounded                      | 0m00.58s || -0m00.05s
0m00.51s | BoundedArithmetic/ArchitectureToZLike           | 0m00.45s || +0m00.06s
0m00.50s | Spec/Ed25519                                    | 0m00.56s || -0m00.06s
0m00.47s | BoundedArithmetic/StripCF                       | 0m00.46s || +0m00.00s
0m00.45s | ModularArithmetic/Pre                           | 0m00.67s || -0m00.22s
0m00.43s | ModularArithmetic/Pow2Base                      | 0m00.44s || -0m00.01s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.36s || +0m00.06s
0m00.39s | ModularArithmetic/Montgomery/Z                  | 0m00.38s || +0m00.01s
0m00.34s | Spec/ModularArithmetic                          | 0m00.36s || -0m00.01s

1 files changed, 20 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 06696f08b..05d16ef46 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -534,6 +534,7 @@ Module Z.
     rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega).
     auto using Z.mod_pow2_bits_low.
   Qed.
+  Hint Rewrite testbit_add_shiftl_low using zutil_arith : Ztestbit.
 
   Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0.
   Proof.
@@ -588,6 +589,25 @@ Module Z.
     rewrite <-Z.pow_add_r by omega.
     replace (1 + (n - 1)) with n by ring; omega.
   Qed.
+  Hint Rewrite testbit_add_shiftl_high using zutil_arith : Ztestbit.
+
+  Lemma nonneg_pow_pos a b : 0 < a -> 0 < a^b -> 0 <= b.
+  Proof.
+    destruct (Z_lt_le_dec b 0); intros; auto.
+    erewrite Z.pow_neg_r in * by eassumption.
+    omega.
+  Qed.
+  Hint Resolve nonneg_pow_pos : zarith.
+
+  Lemma testbit_add_shiftl_full i (Hi : 0 <= i) a b n (Ha : 0 <= a < 2^n)
+    : Z.testbit (a + b << n) i
+      = if (i <? n) then Z.testbit a i else Z.testbit b (i - n).
+  Proof.
+    assert (0 < 2^n) by omega.
+    assert (0 <= n) by eauto 2 with zarith.
+    pose proof (Zlt_cases i n); break_match; autorewrite with Ztestbit; reflexivity.
+  Qed.
+  Hint Rewrite testbit_add_shiftl_full using zutil_arith : Ztestbit.
 
   Lemma land_add_land : forall n m a b, (m <= n)%nat ->
     Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)).