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, 6 insertions, 3 deletions

diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index c49162ef8..5eba3582b 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.ModularArithmetic.Pow2Base Crypto.BaseSystemProofs.
 Require Import Crypto.Util.Notations.
+Require Export Crypto.Util.Bool.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
@@ -295,9 +296,10 @@ Section Pow2BaseProofs.
           apply Z.bits_inj'; intros.
           rewrite Z.testbit_pow2_mod by auto using in_eq.
           break_if. {
-            autorewrite with Ztestbit.
-            rewrite Z.testbit_neg_r with (n := n - w) by omega.
-            autorewrite with Ztestbit. f_equal; ring.
+            autorewrite with Ztestbit; break_match;
+              try rewrite Z.testbit_neg_r with (n := n - w) by omega;
+              autorewrite with bool_congr;
+              f_equal; ring.
           } {
             replace a with (a mod 2 ^ w) by (auto using Z.mod_small).
             apply Z.mod_pow2_bits_high. split; auto using in_eq; omega.
@@ -763,6 +765,7 @@ Section BitwiseDecodeEncode.
         erewrite testbit_decode_digit_select with (i0 := i) by
           (eauto; rewrite sum_firstn_succ_default; omega)
       | |- appcontext[Z.testbit _ (?a - ?b)] => destruct (Z_lt_dec a b)
+      | _ => progress break_if
       end.
   Qed.