Stronger Ztestbit, convert_to_ztestbit

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
5m51.78s | Total                                           | 5m58.93s || -0m07.15s
----------------------------------------------------------------------------------
0m35.42s | ModularArithmetic/Conversion                    | 0m37.08s || -0m01.65s
0m22.17s | BoundedArithmetic/DoubleBoundedProofs           | 0m23.61s || -0m01.43s
1m35.32s | Test/Curve25519SpecTestVectors                  | 1m36.20s || -0m00.88s
0m28.51s | ModularArithmetic/ModularBaseSystemProofs       | 0m27.76s || +0m00.75s
0m22.26s | ModularArithmetic/Pow2BaseProofs                | 0m22.74s || -0m00.47s
0m20.29s | EdDSARepChange                                  | 0m19.76s || +0m00.52s
0m14.57s | Specific/GF25519                                | 0m14.40s || +0m00.16s
0m13.05s | Util/ZUtil                                      | 0m13.37s || -0m00.31s
0m09.95s | Testbit                                         | 0m10.68s || -0m00.73s
0m08.56s | ModularArithmetic/Montgomery/ZProofs            | 0m09.22s || -0m00.66s
0m08.34s | BoundedArithmetic/ArchitectureToZLikeProofs     | 0m08.38s || -0m00.04s
0m07.98s | Encoding/PointEncoding                          | 0m08.40s || -0m00.41s
0m07.75s | Specific/GF1305                                 | 0m08.07s || -0m00.32s
0m03.84s | ModularArithmetic/Tutorial                      | 0m03.43s || +0m00.40s
0m03.83s | BaseSystemProofs                                | 0m04.14s || -0m00.30s
0m03.79s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m04.31s || -0m00.51s
0m03.58s | ModularArithmetic/ModularBaseSystemListProofs   | 0m03.57s || +0m00.01s
0m03.35s | BoundedArithmetic/InterfaceProofs               | 0m03.53s || -0m00.17s
0m03.13s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.12s || +0m00.00s
0m02.84s | Encoding/PointEncodingPre                       | 0m02.83s || +0m00.00s
0m02.77s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.95s || -0m00.18s
0m02.42s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.20s || +0m00.21s
0m02.36s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.35s || +0m00.00s
0m02.22s | Specific/FancyMachine256/Montgomery             | 0m02.10s || +0m00.12s
0m02.12s | Specific/FancyMachine256/Barrett                | 0m02.39s || -0m00.27s
0m01.88s | ModularArithmetic/Montgomery/ZBounded           | 0m01.97s || -0m00.09s
0m01.74s | Specific/FancyMachine256/Core                   | 0m01.76s || -0m00.02s
0m01.47s | ModularArithmetic/BarrettReduction/Z            | 0m01.49s || -0m00.02s
0m01.35s | ModularArithmetic/PrimeFieldTheorems            | 0m01.48s || -0m00.12s
0m01.31s | BaseSystem                                      | 0m01.36s || -0m00.05s
0m01.28s | ModularArithmetic/ExtendedBaseVector            | 0m01.50s || -0m00.21s
0m00.98s | Util/NumTheoryUtil                              | 0m01.12s || -0m00.14s
0m00.97s | Experiments/EncodingLemmas                      | 0m00.97s || +0m00.00s
0m00.69s | Encoding/ModularWordEncodingPre                 | 0m00.74s || -0m00.05s
0m00.67s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.80s || -0m00.13s
0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.70s || -0m00.02s
0m00.66s | ModularArithmetic/ModularBaseSystem             | 0m00.60s || +0m00.06s
0m00.66s | Encoding/ModularWordEncodingTheorems            | 0m00.66s || +0m00.00s
0m00.64s | BoundedArithmetic/Interface                     | 0m00.58s || +0m00.06s
0m00.64s | ModularArithmetic/ModularBaseSystemList         | 0m00.57s || +0m00.07s
0m00.61s | Spec/EdDSA                                      | 0m00.66s || -0m00.05s
0m00.59s | Spec/Ed25519                                    | 0m00.57s || +0m00.02s
0m00.58s | Spec/ModularWordEncoding                        | 0m00.53s || +0m00.04s
0m00.53s | ModularArithmetic/Pre                           | 0m00.54s || -0m00.01s
0m00.51s | BoundedArithmetic/DoubleBounded                 | 0m00.50s || +0m00.01s
0m00.49s | BoundedArithmetic/ArchitectureToZLike           | 0m00.43s || +0m00.06s
0m00.47s | ModularArithmetic/ZBounded                      | 0m00.47s || +0m00.00s
0m00.45s | BoundedArithmetic/StripCF                       | 0m00.46s || -0m00.01s
0m00.40s | ModularArithmetic/Pow2Base                      | 0m00.66s || -0m00.26s
0m00.40s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.42s || -0m00.01s
0m00.37s | ModularArithmetic/Montgomery/Z                  | 0m00.40s || -0m00.03s
0m00.35s | Spec/ModularArithmetic                          | 0m00.41s || -0m00.06s

1 files changed, 11 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 657ba8468..8d482d1ee 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -806,6 +806,13 @@ Module Z.
   Qed.
   Hint Rewrite <- Z.lor_shiftl using zutil_arith : convert_to_Ztestbit.
 
+  Lemma lor_shiftl' : forall a b n, 0 <= n -> 0 <= a < 2 ^ n ->
+    Z.lor (Z.shiftl b n) a = (Z.shiftl b n) + a.
+  Proof.
+    intros; rewrite Z.lor_comm, Z.add_comm; apply lor_shiftl; assumption.
+  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
@@ -2806,4 +2813,8 @@ Ltac Ztestbit :=
          | _ => progress autorewrite with Ztestbit
          | [ |- context[Z.testbit ?x ?y] ]
            => rewrite (Z.testbit_neg_r x y) by zutil_arith
+         | [ |- context[Z.testbit ?x ?y] ]
+           => 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
          end.