Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil

The file src/Util/ZUtil.v no longer exports any lemmas, nor does it
contain any lemmas.  Instead, it pulls in all of the various ZUtil files
so that `Search` will pick up the relevant lemma, and allow users to
`Require Import` the relevant file.

This allows more parallelization in the build.  It also prevents
needlessly rebuilding lots of files whenever we change anything anywhere
in ZUtil.

From this point forward, no file in the development should `Require`
`Crypto.Util.ZUtil` itself.

After     | File Name                                                               | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------------------------------
73m47.61s | Total                                                                   | 73m49.49s || -0m01.87s | -0.04%
-----------------------------------------------------------------------------------------------------------------------
0m14.49s  | Util/ZUtil/LandLorBounds                                                |    N/A    || +0m14.49s | ∞
0m00.42s  | Util/ZUtil                                                              | 0m11.07s  || -0m10.65s | -96.20%
0m03.54s  | Util/ZUtil/LandLorShiftBounds                                           |    N/A    || +0m03.54s | ∞
0m03.49s  | Util/ZUtil/Shift                                                        |    N/A    || +0m03.49s | ∞
4m09.67s  | Experiments/NewPipeline/RewriterRulesGood                               | 4m07.61s  || +0m02.05s | +0.83%
1m22.68s  | Experiments/NewPipeline/RewriterWf2                                     | 1m20.22s  || +0m02.46s | +3.06%
1m21.09s  | Compilers/Named/MapCastInterp                                           | 1m23.14s  || -0m02.04s | -2.46%
0m17.79s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs     | 0m20.61s  || -0m02.82s | -13.68%
0m08.00s  | Arithmetic/MontgomeryReduction/Proofs                                   | 0m10.90s  || -0m02.90s | -26.60%
0m05.46s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate                      | 0m08.07s  || -0m02.61s | -32.34%
8m39.34s  | Experiments/SimplyTypedArithmetic                                       | 8m38.00s  || +0m01.34s | +0.25%
1m30.51s  | Spec/Test/X25519                                                        | 1m28.92s  || +0m01.59s | +1.78%
1m16.98s  | Experiments/NewPipeline/Rewriter                                        | 1m18.02s  || -0m01.03s | -1.33%
0m25.51s  | Experiments/NewPipeline/UnderLetsProofs                                 | 0m27.02s  || -0m01.50s | -5.58%
0m10.75s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs               | 0m12.00s  || -0m01.25s | -10.41%
0m09.28s  | LegacyArithmetic/Double/Proofs/Multiply                                 | 0m10.97s  || -0m01.69s | -15.40%
0m05.70s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub                        | 0m07.01s  || -0m01.30s | -18.68%
0m03.36s  | LegacyArithmetic/InterfaceProofs                                        | 0m04.67s  || -0m01.31s | -28.05%
0m01.43s  | Util/ZUtil/Ones                                                         |    N/A    || +0m01.42s | ∞
0m01.37s  | Arithmetic/BarrettReduction/Wikipedia                                   | 0m02.38s  || -0m01.00s | -42.43%
6m02.75s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                      | 6m03.58s  || -0m00.82s | -0.22%
4m45.52s  | Experiments/NewPipeline/Toplevel1                                       | 4m45.02s  || +0m00.50s | +0.17%
3m46.16s  | Curves/Montgomery/XZProofs                                              | 3m45.20s  || +0m00.96s | +0.42%
2m11.24s  | Specific/X25519/C64/ladderstep                                          | 2m11.78s  || -0m00.53s | -0.40%
1m52.27s  | Specific/NISTP256/AMD64/femul                                           | 1m52.36s  || -0m00.08s | -0.08%
1m43.21s  | Experiments/NewPipeline/Toplevel2                                       | 1m43.70s  || -0m00.48s | -0.47%
1m30.09s  | Experiments/NewPipeline/Arithmetic                                      | 1m29.59s  || +0m00.50s | +0.55%
1m18.58s  | Specific/X2448/Karatsuba/C64/femul                                      | 1m19.45s  || -0m00.87s | -1.09%
0m59.72s  | Specific/X25519/C32/femul                                               | 1m00.00s  || -0m00.28s | -0.46%
0m52.94s  | Demo                                                                    | 0m52.24s  || +0m00.69s | +1.33%
0m48.98s  | Compilers/Z/Named/RewriteAddToAdcInterp                                 | 0m49.12s  || -0m00.14s | -0.28%
0m47.34s  | Compilers/Z/ArithmeticSimplifierInterp                                  | 0m47.24s  || +0m00.10s | +0.21%
0m43.02s  | Specific/X25519/C32/fesquare                                            | 0m43.06s  || -0m00.03s | -0.09%
0m42.02s  | Arithmetic/Karatsuba                                                    | 0m42.08s  || -0m00.05s | -0.14%
0m41.76s  | Experiments/NewPipeline/AbstractInterpretationWf                        | 0m42.33s  || -0m00.57s | -1.34%
0m38.51s  | p521_32.c                                                               | 0m38.75s  || -0m00.24s | -0.61%
0m37.14s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery         | 0m37.22s  || -0m00.07s | -0.21%
0m36.10s  | Spec/Ed25519                                                            | 0m36.23s  || -0m00.12s | -0.35%
0m35.83s  | Experiments/NewPipeline/LanguageInversion                               | 0m35.71s  || +0m00.11s | +0.33%
0m34.38s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery       | 0m34.91s  || -0m00.52s | -1.51%
0m33.32s  | Specific/X25519/C32/freeze                                              | 0m33.32s  || +0m00.00s | +0.00%
0m31.92s  | p521_64.c                                                               | 0m32.20s  || -0m00.28s | -0.86%
0m31.32s  | Compilers/Z/ArithmeticSimplifierWf                                      | 0m30.82s  || +0m00.50s | +1.62%
0m28.96s  | Compilers/CommonSubexpressionEliminationWf                              | 0m29.19s  || -0m00.23s | -0.78%
0m27.73s  | Specific/NISTP256/AMD128/femul                                          | 0m27.70s  || +0m00.03s | +0.10%
0m26.79s  | Primitives/EdDSARepChange                                               | 0m26.90s  || -0m00.10s | -0.40%
0m25.27s  | Specific/X25519/C32/fecarry                                             | 0m25.34s  || -0m00.07s | -0.27%
0m24.87s  | Experiments/NewPipeline/AbstractInterpretationZRangeProofs              | 0m25.26s  || -0m00.39s | -1.54%
0m23.71s  | p384_32.c                                                               | 0m23.60s  || +0m00.10s | +0.46%
0m22.37s  | Experiments/NewPipeline/LanguageWf                                      | 0m22.49s  || -0m00.11s | -0.53%
0m21.43s  | Arithmetic/Core                                                         | 0m21.60s  || -0m00.17s | -0.78%
0m21.41s  | Specific/X25519/C32/fesub                                               | 0m21.28s  || +0m00.12s | +0.61%
0m20.86s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas           | 0m20.26s  || +0m00.59s | +2.96%
0m20.86s  | Specific/NISTP256/AMD64/fesub                                           | 0m21.69s  || -0m00.83s | -3.82%
0m20.53s  | Specific/X25519/C64/femul                                               | 0m20.54s  || -0m00.00s | -0.04%
0m19.67s  | Specific/X25519/C32/Synthesis                                           | 0m19.54s  || +0m00.13s | +0.66%
0m19.44s  | Curves/Edwards/XYZT/Basic                                               | 0m19.05s  || +0m00.39s | +2.04%
0m19.30s  | Specific/NISTP256/AMD64/feadd                                           | 0m19.35s  || -0m00.05s | -0.25%
0m19.23s  | Specific/X25519/C32/feadd                                               | 0m19.20s  || +0m00.03s | +0.15%
0m18.84s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas             | 0m18.60s  || +0m00.23s | +1.29%
0m18.07s  | Compilers/Named/MapCastWf                                               | 0m17.87s  || +0m00.19s | +1.11%
0m18.01s  | Compilers/Z/CNotations                                                  | 0m18.15s  || -0m00.13s | -0.77%
0m17.50s  | Specific/X25519/C64/freeze                                              | 0m17.52s  || -0m00.01s | -0.11%
0m17.03s  | Specific/X25519/C64/fesquare                                            | 0m17.14s  || -0m00.10s | -0.64%
0m16.10s  | Curves/Edwards/AffineProofs                                             | 0m15.80s  || +0m00.30s | +1.89%
0m15.71s  | Specific/NISTP256/AMD64/feopp                                           | 0m15.97s  || -0m00.25s | -1.62%
0m15.62s  | Compilers/Named/ContextProperties/SmartMap                              | 0m15.57s  || +0m00.04s | +0.32%
0m15.35s  | Compilers/Named/ContextProperties/NameUtil                              | 0m15.30s  || +0m00.04s | +0.32%
0m15.04s  | Specific/NISTP256/AMD128/fesub                                          | 0m15.16s  || -0m00.12s | -0.79%
0m14.88s  | Specific/NISTP256/AMD128/feadd                                          | 0m14.83s  || +0m00.05s | +0.33%
0m14.20s  | Specific/NISTP256/AMD64/fenz                                            | 0m14.56s  || -0m00.36s | -2.47%
0m14.16s  | Specific/X25519/C64/fecarry                                             | 0m14.13s  || +0m00.02s | +0.21%
0m13.78s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas             | 0m13.54s  || +0m00.24s | +1.77%
0m13.69s  | Arithmetic/Saturated/AddSub                                             | 0m13.66s  || +0m00.02s | +0.21%
0m13.67s  | Specific/NISTP256/AMD128/fenz                                           | 0m13.69s  || -0m00.01s | -0.14%
0m13.16s  | Experiments/NewPipeline/CStringification                                | 0m13.08s  || +0m00.08s | +0.61%
0m13.10s  | Specific/X25519/C64/fesub                                               | 0m13.16s  || -0m00.06s | -0.45%
0m12.34s  | Experiments/NewPipeline/AbstractInterpretationProofs                    | 0m12.47s  || -0m00.13s | -1.04%
0m12.29s  | Specific/NISTP256/AMD128/feopp                                          | 0m12.34s  || -0m00.05s | -0.40%
0m12.26s  | Compilers/Z/Syntax/Equality                                             | 0m12.69s  || -0m00.42s | -3.38%
0m11.94s  | Specific/X25519/C64/feadd                                               | 0m11.90s  || +0m00.03s | +0.33%
0m11.87s  | Primitives/MxDHRepChange                                                | 0m11.76s  || +0m00.10s | +0.93%
0m11.85s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs          | 0m11.66s  || +0m00.18s | +1.62%
0m11.42s  | Arithmetic/Saturated/MontgomeryAPI                                      | 0m11.45s  || -0m00.02s | -0.26%
0m10.69s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas               | 0m10.30s  || +0m00.38s | +3.78%
0m10.61s  | Arithmetic/Saturated/Core                                               | 0m10.66s  || -0m00.05s | -0.46%
0m09.89s  | Specific/X2448/Karatsuba/C64/Synthesis                                  | 0m09.79s  || +0m00.10s | +1.02%
0m09.35s  | Util/ZRange/CornersMonotoneBounds                                       | 0m09.90s  || -0m00.55s | -5.55%
0m08.79s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml      | 0m08.60s  || +0m00.18s | +2.20%
0m08.64s  | p384_64.c                                                               | 0m08.50s  || +0m00.14s | +1.64%
0m08.63s  | LegacyArithmetic/ArchitectureToZLikeProofs                              | 0m08.61s  || +0m00.02s | +0.23%
0m08.49s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate            | 0m08.38s  || +0m00.10s | +1.31%
0m08.19s  | Compilers/Named/CompileInterpSideConditions                             | 0m07.78s  || +0m00.40s | +5.26%
0m08.15s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes                | 0m08.20s  || -0m00.04s | -0.60%
0m07.98s  | Compilers/Named/RegisterAssignInterp                                    | 0m08.11s  || -0m00.12s | -1.60%
0m07.81s  | Arithmetic/BarrettReduction/RidiculousFish                              | 0m08.20s  || -0m00.38s | -4.75%
0m07.45s  | Compilers/InlineConstAndOpWf                                            | 0m07.40s  || +0m00.04s | +0.67%
0m07.01s  | Specific/NISTP256/AMD64/Synthesis                                       | 0m06.98s  || +0m00.02s | +0.42%
0m06.55s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast                        | 0m06.44s  || +0m00.10s | +1.70%
0m06.51s  | Arithmetic/Saturated/MulSplit                                           | 0m06.45s  || +0m00.05s | +0.93%
0m06.40s  | Util/FixedWordSizesEquality                                             | 0m06.46s  || -0m00.05s | -0.92%
0m06.28s  | Arithmetic/BarrettReduction/Generalized                                 | 0m06.64s  || -0m00.35s | -5.42%
0m06.08s  | Util/ZUtil/Modulo                                                       | 0m05.58s  || +0m00.50s | +8.96%
0m06.07s  | Compilers/InlineWf                                                      | 0m06.20s  || -0m00.12s | -2.09%
0m06.04s  | Util/ZUtil/Morphisms                                                    | 0m06.09s  || -0m00.04s | -0.82%
0m05.94s  | Specific/X25519/C64/Synthesis                                           | 0m05.95s  || -0m00.00s | -0.16%
0m05.66s  | Compilers/LinearizeWf                                                   | 0m05.73s  || -0m00.07s | -1.22%
0m05.64s  | LegacyArithmetic/Pow2BaseProofs                                         | 0m06.27s  || -0m00.62s | -10.04%
0m05.60s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs    | 0m05.45s  || +0m00.14s | +2.75%
0m05.45s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml          | 0m05.54s  || -0m00.08s | -1.62%
0m05.29s  | Compilers/Z/HexNotationConstants                                        | 0m05.44s  || -0m00.15s | -2.75%
0m05.02s  | Compilers/WfProofs                                                      | 0m04.98s  || +0m00.03s | +0.80%
0m04.76s  | Experiments/NewPipeline/RewriterWf1                                     | 0m04.74s  || +0m00.01s | +0.42%
0m04.69s  | Specific/Framework/ArithmeticSynthesis/Montgomery                       | 0m04.71s  || -0m00.01s | -0.42%
0m04.63s  | Arithmetic/BarrettReduction/HAC                                         | 0m05.14s  || -0m00.50s | -9.92%
0m04.48s  | Compilers/Z/Bounds/Pipeline/Definition                                  | 0m04.68s  || -0m00.19s | -4.27%
0m04.34s  | Compilers/Z/BinaryNotationConstants                                     | 0m04.39s  || -0m00.04s | -1.13%
0m04.14s  | Compilers/Named/CompileWf                                               | 0m04.19s  || -0m00.05s | -1.19%
0m04.02s  | Experiments/NewPipeline/MiscCompilerPassesProofs                        | 0m03.98s  || +0m00.03s | +1.00%
0m03.99s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs        | 0m03.87s  || +0m00.12s | +3.10%
0m03.90s  | secp256k1_32.c                                                          | 0m03.91s  || -0m00.01s | -0.25%
0m03.87s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml            | 0m03.98s  || -0m00.10s | -2.76%
0m03.83s  | Arithmetic/MontgomeryReduction/WordByWord/Proofs                        | 0m03.72s  || +0m00.10s | +2.95%
0m03.76s  | p256_32.c                                                               | 0m03.81s  || -0m00.05s | -1.31%
0m03.67s  | LegacyArithmetic/Double/Proofs/ShiftRight                               | 0m03.59s  || +0m00.08s | +2.22%
0m03.58s  | Compilers/Z/ArithmeticSimplifier                                        | 0m03.60s  || -0m00.02s | -0.55%
0m03.48s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy                     | 0m03.46s  || +0m00.02s | +0.57%
0m03.41s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs          | 0m03.32s  || +0m00.09s | +2.71%
0m03.28s  | Specific/NISTP256/AMD128/Synthesis                                      | 0m03.30s  || -0m00.02s | -0.60%
0m03.24s  | Util/ZUtil/Div                                                          | 0m02.78s  || +0m00.46s | +16.54%
0m03.12s  | LegacyArithmetic/Double/Proofs/ShiftLeft                                | 0m03.13s  || -0m00.00s | -0.31%
0m03.05s  | Compilers/InlineInterp                                                  | 0m02.91s  || +0m00.13s | +4.81%
0m03.04s  | LegacyArithmetic/Double/Proofs/Decode                                   | 0m03.48s  || -0m00.43s | -12.64%
0m02.98s  | Compilers/Named/ContextProperties                                       | 0m03.00s  || -0m00.02s | -0.66%
0m02.90s  | Compilers/TestCase                                                      | 0m02.89s  || +0m00.00s | +0.34%
0m02.88s  | LegacyArithmetic/ZBoundedZ                                              | 0m03.85s  || -0m00.97s | -25.19%
0m02.88s  | Util/WordUtil                                                           | 0m02.90s  || -0m00.02s | -0.68%
0m02.72s  | Compilers/Named/CompileInterp                                           | 0m02.74s  || -0m00.02s | -0.72%
0m02.58s  | Arithmetic/Saturated/Freeze                                             | 0m02.56s  || +0m00.02s | +0.78%
0m02.58s  | LegacyArithmetic/BarretReduction                                        | 0m02.72s  || -0m00.14s | -5.14%
0m02.54s  | Compilers/Named/ContextProperties/Proper                                | 0m02.61s  || -0m00.06s | -2.68%
0m02.40s  | Arithmetic/ModularArithmeticTheorems                                    | 0m03.33s  || -0m00.93s | -27.92%
0m02.38s  | Specific/NISTP256/FancyMachine256/Montgomery                            | 0m02.33s  || +0m00.04s | +2.14%
0m02.30s  | Specific/NISTP256/FancyMachine256/Core                                  | 0m02.28s  || +0m00.02s | +0.87%
0m02.27s  | Compilers/CommonSubexpressionEliminationProperties                      | 0m02.20s  || +0m00.06s | +3.18%
0m02.22s  | Compilers/Z/Bounds/Relax                                                | 0m02.21s  || +0m00.01s | +0.45%
0m02.22s  | Specific/NISTP256/FancyMachine256/Barrett                               | 0m02.27s  || -0m00.04s | -2.20%
0m02.16s  | Util/ZUtil/Quot                                                         | 0m02.08s  || +0m00.08s | +3.84%
0m02.10s  | Compilers/Named/NameUtilProperties                                      | 0m02.04s  || +0m00.06s | +2.94%
0m02.10s  | Compilers/Z/RewriteAddToAdcInterp                                       | 0m02.14s  || -0m00.04s | -1.86%
0m02.10s  | p224_32.c                                                               | 0m02.11s  || -0m00.00s | -0.47%
0m02.09s  | Specific/Framework/ArithmeticSynthesis/Defaults                         | 0m02.11s  || -0m00.02s | -0.94%
0m02.07s  | Util/ZRange/SplitBounds                                                 | 0m02.01s  || +0m00.06s | +2.98%
0m02.01s  | curve25519_32.c                                                         | 0m02.02s  || -0m00.01s | -0.49%
0m01.90s  | Compilers/Z/JavaNotations                                               | 0m01.96s  || -0m00.06s | -3.06%
0m01.84s  | LegacyArithmetic/MontgomeryReduction                                    | 0m01.82s  || +0m00.02s | +1.09%
0m01.84s  | Util/ZUtil/AddGetCarry                                                  | 0m01.87s  || -0m00.03s | -1.60%
0m01.73s  | Util/ZUtil/Pow2Mod                                                      | 0m01.48s  || +0m00.25s | +16.89%
0m01.68s  | Compilers/Named/WfFromUnit                                              | 0m01.70s  || -0m00.02s | -1.17%
0m01.67s  | Util/Tuple                                                              | 0m01.63s  || +0m00.04s | +2.45%
0m01.66s  | Arithmetic/CoreUnfolder                                                 | 0m01.66s  || +0m00.00s | +0.00%
0m01.64s  | secp256k1_64.c                                                          | 0m01.50s  || +0m00.13s | +9.33%
0m01.63s  | p256_64.c                                                               | 0m01.53s  || +0m00.09s | +6.53%
0m01.56s  | Specific/Framework/ReificationTypes                                     | 0m01.71s  || -0m00.14s | -8.77%
0m01.53s  | p224_64.c                                                               | 0m01.52s  || +0m00.01s | +0.65%
0m01.52s  | Specific/Framework/ArithmeticSynthesis/Base                             | 0m01.49s  || +0m00.03s | +2.01%
0m01.50s  | Compilers/Relations                                                     | 0m01.48s  || +0m00.02s | +1.35%
0m01.47s  | Specific/Framework/OutputType                                           | 0m01.48s  || -0m00.01s | -0.67%
0m01.45s  | Compilers/Named/InterpretToPHOASWf                                      | 0m01.48s  || -0m00.03s | -2.02%
0m01.45s  | Experiments/NewPipeline/CLI                                             | 0m01.41s  || +0m00.04s | +2.83%
0m01.40s  | LegacyArithmetic/Double/Proofs/BitwiseOr                                | 0m01.28s  || +0m00.11s | +9.37%
0m01.39s  | curve25519_64.c                                                         | 0m01.38s  || +0m00.01s | +0.72%
0m01.37s  | Arithmetic/PrimeFieldTheorems                                           | 0m01.30s  || +0m00.07s | +5.38%
0m01.32s  | Curves/Edwards/XYZT/Precomputed                                         | 0m01.28s  || +0m00.04s | +3.12%
0m01.30s  | Specific/Framework/ArithmeticSynthesis/Karatsuba                        | 0m01.34s  || -0m00.04s | -2.98%
0m01.28s  | Util/QUtil                                                              | 0m01.52s  || -0m00.24s | -15.78%
0m01.25s  | Util/ZUtil/Testbit                                                      | 0m01.06s  || +0m00.18s | +17.92%
0m01.23s  | Experiments/NewPipeline/StandaloneOCamlMain                             | 0m01.23s  || +0m00.00s | +0.00%
0m01.22s  | Arithmetic/Saturated/CoreUnfolder                                       | 0m01.12s  || +0m00.09s | +8.92%
0m01.20s  | Experiments/NewPipeline/Language                                        | 0m01.22s  || -0m00.02s | -1.63%
0m01.20s  | Experiments/NewPipeline/StandaloneHaskellMain                           | 0m01.30s  || -0m00.10s | -7.69%
0m01.19s  | LegacyArithmetic/Double/Proofs/LoadImmediate                            | 0m01.40s  || -0m00.20s | -15.00%
0m01.18s  | LegacyArithmetic/BaseSystemProofs                                       | 0m01.24s  || -0m00.06s | -4.83%
0m01.18s  | Util/ZRange/BasicLemmas                                                 | 0m01.18s  || +0m00.00s | +0.00%
0m01.17s  | Compilers/LinearizeInterp                                               | 0m01.19s  || -0m00.02s | -1.68%
0m01.17s  | Experiments/NewPipeline/CompilersTestCases                              | 0m01.07s  || +0m00.09s | +9.34%
0m01.14s  | Compilers/Z/Syntax/Util                                                 | 0m00.84s  || +0m00.29s | +35.71%
0m01.11s  | Compilers/MultiSizeTest                                                 | 0m01.13s  || -0m00.01s | -1.76%
0m01.08s  | Compilers/Z/RewriteAddToAdcWf                                           | 0m01.08s  || +0m00.00s | +0.00%
0m01.06s  | Experiments/NewPipeline/AbstractInterpretation                          | 0m01.07s  || -0m00.01s | -0.93%
0m01.00s  | Experiments/NewPipeline/RewriterProofs                                  | 0m00.90s  || +0m00.09s | +11.11%
0m01.00s  | Specific/X25519/C32/CurveParameters                                     | 0m00.95s  || +0m00.05s | +5.26%
0m00.96s  | Arithmetic/Saturated/WrappersUnfolder                                   | 0m01.08s  || -0m00.12s | -11.11%
0m00.96s  | Compilers/Named/InterpretToPHOASInterp                                  | 0m01.02s  || -0m00.06s | -5.88%
0m00.96s  | Specific/Framework/SynthesisFramework                                   | 0m01.10s  || -0m00.14s | -12.72%
0m00.95s  | Util/ZUtil/Stabilization                                                | 0m01.02s  || -0m00.07s | -6.86%
0m00.92s  | Specific/Framework/IntegrationTestDisplayCommon                         | 0m00.98s  || -0m00.05s | -6.12%
0m00.90s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                           | 0m00.88s  || +0m00.02s | +2.27%
0m00.89s  | Compilers/Z/CommonSubexpressionElimination                              | 0m00.98s  || -0m00.08s | -9.18%
0m00.89s  | Util/NumTheoryUtil                                                      | 0m01.21s  || -0m00.31s | -26.44%
0m00.86s  | Arithmetic/Saturated/FreezeUnfolder                                     | 0m00.80s  || +0m00.05s | +7.49%
0m00.86s  | Compilers/Named/FMapContext                                             | 0m00.82s  || +0m00.04s | +4.87%
0m00.85s  | Arithmetic/Saturated/UniformWeight                                      | 0m00.93s  || -0m00.08s | -8.60%
0m00.84s  | Specific/Framework/ArithmeticSynthesis/Freeze                           | 0m00.89s  || -0m00.05s | -5.61%
0m00.82s  | Compilers/Named/CompileProperties                                       | 0m00.84s  || -0m00.02s | -2.38%
0m00.82s  | Compilers/Named/InterpSideConditionsInterp                              | 0m00.80s  || +0m00.01s | +2.49%
0m00.82s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage                | 0m00.83s  || -0m00.01s | -1.20%
0m00.82s  | Util/CPSUtil                                                            | 0m00.72s  || +0m00.09s | +13.88%
0m00.81s  | Compilers/InlineConstAndOpInterp                                        | 0m00.79s  || +0m00.02s | +2.53%
0m00.81s  | Util/ZUtil/CC                                                           | 0m00.74s  || +0m00.07s | +9.45%
0m00.80s  | Compilers/InterpByIsoProofs                                             | 0m00.84s  || -0m00.03s | -4.76%
0m00.80s  | Util/ZUtil/Log2                                                         |    N/A    || +0m00.80s | ∞
0m00.79s  | Specific/Framework/IntegrationTestTemporaryMiscCommon                   | 0m00.76s  || +0m00.03s | +3.94%
0m00.78s  | Arithmetic/Saturated/MulSplitUnfolder                                   | 0m00.91s  || -0m00.13s | -14.28%
0m00.76s  | Compilers/Named/AListContext                                            | 0m01.10s  || -0m00.34s | -30.90%
0m00.76s  | Util/ZUtil/Divide                                                       |    N/A    || +0m00.76s | ∞
0m00.75s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul                    | 0m00.71s  || +0m00.04s | +5.63%
0m00.75s  | Util/ZUtil/EquivModulo                                                  | 0m00.68s  || +0m00.06s | +10.29%
0m00.74s  | Compilers/MapCastByDeBruijnInterp                                       | 0m00.86s  || -0m00.12s | -13.95%
0m00.74s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage                | 0m00.72s  || +0m00.02s | +2.77%
0m00.74s  | Specific/Framework/MontgomeryReificationTypesPackage                    | 0m00.71s  || +0m00.03s | +4.22%
0m00.73s  | Arithmetic/MontgomeryReduction/WordByWord/Definition                    | 0m00.77s  || -0m00.04s | -5.19%
0m00.73s  | Util/ZUtil/Tactics/RewriteModSmall                                      | 0m00.80s  || -0m00.07s | -8.75%
0m00.72s  | Specific/Framework/ReificationTypesPackage                              | 0m00.75s  || -0m00.03s | -4.00%
0m00.72s  | Util/ZUtil/Le                                                           | 0m00.30s  || +0m00.42s | +140.00%
0m00.72s  | Util/ZUtil/Rshi                                                         | 0m00.74s  || -0m00.02s | -2.70%
0m00.72s  | Util/ZUtil/Z2Nat                                                        | 0m00.31s  || +0m00.41s | +132.25%
0m00.71s  | Compilers/Z/Bounds/Pipeline                                             | 0m00.66s  || +0m00.04s | +7.57%
0m00.70s  | Experiments/NewPipeline/MiscCompilerPasses                              | 0m00.70s  || +0m00.00s | +0.00%
0m00.70s  | Specific/Framework/MontgomeryReificationTypes                           | 0m00.75s  || -0m00.05s | -6.66%
0m00.69s  | Compilers/CommonSubexpressionEliminationInterp                          | 0m00.66s  || +0m00.02s | +4.54%
0m00.69s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage                  | 0m00.74s  || -0m00.05s | -6.75%
0m00.69s  | Specific/Framework/ArithmeticSynthesis/HelperTactics                    | 0m00.69s  || +0m00.00s | +0.00%
0m00.69s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage                 | 0m00.68s  || +0m00.00s | +1.47%
0m00.68s  | Arithmetic/Saturated/Wrappers                                           | 0m00.70s  || -0m00.01s | -2.85%
0m00.68s  | Specific/Framework/ArithmeticSynthesis/BasePackage                      | 0m00.72s  || -0m00.03s | -5.55%
0m00.68s  | Specific/Framework/ArithmeticSynthesis/FreezePackage                    | 0m00.72s  || -0m00.03s | -5.55%
0m00.68s  | Specific/Framework/ArithmeticSynthesis/Ladderstep                       | 0m00.72s  || -0m00.03s | -5.55%
0m00.67s  | Arithmetic/Saturated/UniformWeightInstances                             | 0m00.68s  || -0m00.01s | -1.47%
0m00.67s  | Compilers/SmartMap                                                      | 0m00.70s  || -0m00.02s | -4.28%
0m00.67s  | LegacyArithmetic/Double/Proofs/SelectConditional                        | 0m00.69s  || -0m00.01s | -2.89%
0m00.65s  | Compilers/CommonSubexpressionElimination                                | 0m00.65s  || +0m00.00s | +0.00%
0m00.63s  | Compilers/MapCastByDeBruijnWf                                           | 0m00.63s  || +0m00.00s | +0.00%
0m00.62s  | LegacyArithmetic/Interface                                              | 0m00.74s  || -0m00.12s | -16.21%
0m00.61s  | Compilers/Named/WfInterp                                                | 0m00.58s  || +0m00.03s | +5.17%
0m00.60s  | Compilers/InputSyntax                                                   | 0m00.50s  || +0m00.09s | +19.99%
0m00.60s  | Compilers/MapBaseTypeWf                                                 | 0m00.58s  || +0m00.02s | +3.44%
0m00.60s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                                  | 0m00.53s  || +0m00.06s | +13.20%
0m00.60s  | Compilers/Z/Bounds/Pipeline/Glue                                        | 0m00.61s  || -0m00.01s | -1.63%
0m00.60s  | Util/NUtil                                                              | 0m00.69s  || -0m00.08s | -13.04%
0m00.60s  | Util/ZUtil/Lnot                                                         |    N/A    || +0m00.60s | ∞
0m00.60s  | Util/ZUtil/Mul                                                          |    N/A    || +0m00.60s | ∞
0m00.59s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                              | 0m00.59s  || +0m00.00s | +0.00%
0m00.58s  | Compilers/InterpWfRel                                                   | 0m00.52s  || +0m00.05s | +11.53%
0m00.58s  | Compilers/Z/Bounds/RoundUpLemmas                                        | 0m00.52s  || +0m00.05s | +11.53%
0m00.58s  | Compilers/Z/Reify                                                       | 0m00.60s  || -0m00.02s | -3.33%
0m00.58s  | LegacyArithmetic/Double/Core                                            | 0m00.58s  || +0m00.00s | +0.00%
0m00.58s  | Spec/EdDSA                                                              | 0m00.60s  || -0m00.02s | -3.33%
0m00.57s  | Arithmetic/ModularArithmeticPre                                         | 0m00.60s  || -0m00.03s | -5.00%
0m00.57s  | Compilers/Z/Named/RewriteAddToAdc                                       | 0m00.69s  || -0m00.12s | -17.39%
0m00.56s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics                         | 0m00.60s  || -0m00.03s | -6.66%
0m00.56s  | Util/HList                                                              | 0m00.50s  || +0m00.06s | +12.00%
0m00.55s  | Compilers/Z/FoldTypes                                                   | 0m00.48s  || +0m00.07s | +14.58%
0m00.52s  | Compilers/Z/MapCastByDeBruijnInterp                                     | 0m00.55s  || -0m00.03s | -5.45%
0m00.52s  | Compilers/Z/Syntax                                                      | 0m00.52s  || +0m00.00s | +0.00%
0m00.52s  | Util/Decidable/Decidable2Bool                                           | 0m00.53s  || -0m00.01s | -1.88%
0m00.52s  | Util/ZBounded                                                           | 0m00.46s  || +0m00.06s | +13.04%
0m00.51s  | Compilers/Z/Bounds/Interpretation                                       | 0m00.50s  || +0m00.01s | +2.00%
0m00.50s  | Compilers/GeneralizeVarInterp                                           | 0m00.48s  || +0m00.02s | +4.16%
0m00.50s  | Compilers/Z/CommonSubexpressionEliminationWf                            | 0m00.56s  || -0m00.06s | -10.71%
0m00.50s  | Compilers/Z/RewriteAddToAdc                                             | 0m00.65s  || -0m00.15s | -23.07%
0m00.50s  | LegacyArithmetic/ArchitectureToZLike                                    | 0m00.51s  || -0m00.01s | -1.96%
0m00.49s  | Compilers/GeneralizeVarWf                                               | 0m00.49s  || +0m00.00s | +0.00%
0m00.49s  | Compilers/InlineConstAndOpByRewriteWf                                   | 0m00.51s  || -0m00.02s | -3.92%
0m00.49s  | Compilers/Z/ArithmeticSimplifierUtil                                    | 0m00.50s  || -0m00.01s | -2.00%
0m00.49s  | Compilers/Z/InlineInterp                                                | 0m00.54s  || -0m00.05s | -9.25%
0m00.49s  | Compilers/Z/InlineWf                                                    | 0m00.49s  || +0m00.00s | +0.00%
0m00.48s  | Compilers/Reify                                                         | 0m00.46s  || +0m00.01s | +4.34%
0m00.48s  | Compilers/Z/Bounds/MapCastByDeBruijn                                    | 0m00.53s  || -0m00.05s | -9.43%
0m00.48s  | Compilers/Z/GeneralizeVarInterp                                         | 0m00.46s  || +0m00.01s | +4.34%
0m00.48s  | Compilers/Z/InlineConstAndOpByRewrite                                   | 0m00.51s  || -0m00.03s | -5.88%
0m00.48s  | Compilers/Z/InlineConstAndOpByRewriteInterp                             | 0m00.46s  || +0m00.01s | +4.34%
0m00.48s  | Compilers/Z/InlineConstAndOpInterp                                      | 0m00.50s  || -0m00.02s | -4.00%
0m00.48s  | Experiments/NewPipeline/UnderLets                                       | 0m00.46s  || +0m00.01s | +4.34%
0m00.47s  | Compilers/InterpWf                                                      | 0m00.49s  || -0m00.02s | -4.08%
0m00.47s  | Compilers/Named/PositiveContext/DefaultsProperties                      | 0m00.45s  || +0m00.01s | +4.44%
0m00.47s  | Compilers/Z/InterpSideConditions                                        | 0m00.51s  || -0m00.04s | -7.84%
0m00.46s  | Compilers/InterpProofs                                                  | 0m00.44s  || +0m00.02s | +4.54%
0m00.46s  | Compilers/Named/DeadCodeEliminationInterp                               | 0m00.50s  || -0m00.03s | -7.99%
0m00.46s  | Compilers/Z/CommonSubexpressionEliminationInterp                        | 0m00.56s  || -0m00.10s | -17.85%
0m00.46s  | Compilers/Z/InlineConstAndOp                                            | 0m00.50s  || -0m00.03s | -7.99%
0m00.46s  | Compilers/Z/MapCastByDeBruijn                                           | 0m00.43s  || +0m00.03s | +6.97%
0m00.46s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic                     | 0m00.58s  || -0m00.11s | -20.68%
0m00.46s  | Specific/Framework/CurveParameters                                      | 0m00.45s  || +0m00.01s | +2.22%
0m00.45s  | Compilers/Z/Inline                                                      | 0m00.55s  || -0m00.10s | -18.18%
0m00.45s  | Specific/X25519/C64/CurveParameters                                     | 0m00.44s  || +0m00.01s | +2.27%
0m00.44s  | Compilers/InlineConstAndOpByRewriteInterp                               | 0m00.48s  || -0m00.03s | -8.33%
0m00.44s  | Compilers/Z/MapCastByDeBruijnWf                                         | 0m00.57s  || -0m00.12s | -22.80%
0m00.44s  | Compilers/ZExtended/Syntax                                              | 0m00.42s  || +0m00.02s | +4.76%
0m00.44s  | LegacyArithmetic/BaseSystem                                             | 0m00.60s  || -0m00.15s | -26.66%
0m00.44s  | Util/ZRange                                                             | 0m00.44s  || +0m00.00s | +0.00%
0m00.43s  | Compilers/Named/WeakListContext                                         | 0m00.44s  || -0m00.01s | -2.27%
0m00.43s  | Compilers/ZExtended/MapBaseType                                         | 0m00.44s  || -0m00.01s | -2.27%
0m00.43s  | Specific/Framework/IntegrationTestDisplayCommonTactics                  | 0m00.49s  || -0m00.06s | -12.24%
0m00.43s  | Util/NUtil/WithoutReferenceToZ                                          |    N/A    || +0m00.43s | ∞
0m00.43s  | Util/ZUtil/CPS                                                          | 0m00.44s  || -0m00.01s | -2.27%
0m00.42s  | Compilers/Named/InterpSideConditions                                    | 0m00.32s  || +0m00.09s | +31.24%
0m00.42s  | Compilers/Z/GeneralizeVar                                               | 0m00.39s  || +0m00.02s | +7.69%
0m00.42s  | Compilers/Z/GeneralizeVarWf                                             | 0m00.46s  || -0m00.04s | -8.69%
0m00.42s  | Compilers/Z/InlineConstAndOpWf                                          | 0m00.54s  || -0m00.12s | -22.22%
0m00.42s  | Compilers/Z/Named/DeadCodeEliminationInterp                             | 0m00.46s  || -0m00.04s | -8.69%
0m00.42s  | LegacyArithmetic/ZBounded                                               | 0m00.59s  || -0m00.17s | -28.81%
0m00.42s  | Specific/Framework/RawCurveParameters                                   | 0m00.41s  || +0m00.01s | +2.43%
0m00.42s  | Util/ZRange/Operations                                                  | 0m00.52s  || -0m00.10s | -19.23%
0m00.41s  | Compilers/Z/TypeInversion                                               | 0m00.36s  || +0m00.04s | +13.88%
0m00.40s  | Compilers/GeneralizeVar                                                 | 0m00.35s  || +0m00.05s | +14.28%
0m00.40s  | Compilers/InlineConstAndOp                                              | 0m00.39s  || +0m00.01s | +2.56%
0m00.40s  | Compilers/Z/InlineConstAndOpByRewriteWf                                 | 0m00.49s  || -0m00.08s | -18.36%
0m00.39s  | Compilers/Named/RegisterAssign                                          | 0m00.36s  || +0m00.03s | +8.33%
0m00.38s  | Compilers/Inline                                                        | 0m00.39s  || -0m00.01s | -2.56%
0m00.38s  | Compilers/Named/Wf                                                      | 0m00.37s  || +0m00.01s | +2.70%
0m00.38s  | Compilers/StripExpr                                                     | 0m00.33s  || +0m00.04s | +15.15%
0m00.38s  | Compilers/Z/Named/DeadCodeElimination                                   | 0m00.35s  || +0m00.03s | +8.57%
0m00.38s  | Specific/Framework/CurveParametersPackage                               | 0m00.34s  || +0m00.03s | +11.76%
0m00.38s  | Specific/NISTP256/AMD128/CurveParameters                                | 0m00.36s  || +0m00.02s | +5.55%
0m00.38s  | Specific/NISTP256/AMD64/CurveParameters                                 | 0m00.40s  || -0m00.02s | -5.00%
0m00.38s  | Specific/X2448/Karatsuba/C64/CurveParameters                            | 0m00.36s  || +0m00.02s | +5.55%
0m00.38s  | Util/ZUtil/Definitions                                                  | 0m00.29s  || +0m00.09s | +31.03%
0m00.37s  | Compilers/Z/Bounds/Pipeline/OutputType                                  | 0m00.35s  || +0m00.02s | +5.71%
0m00.36s  | Compilers/Named/Compile                                                 | 0m00.34s  || +0m00.01s | +5.88%
0m00.36s  | Compilers/Named/ContextProperties/Tactics                               | 0m00.38s  || -0m00.02s | -5.26%
0m00.36s  | Compilers/Named/DeadCodeElimination                                     | 0m00.36s  || +0m00.00s | +0.00%
0m00.36s  | Compilers/Named/EstablishLiveness                                       | 0m00.36s  || +0m00.00s | +0.00%
0m00.36s  | Compilers/Named/GetNames                                                | 0m00.35s  || +0m00.01s | +2.85%
0m00.36s  | Compilers/Named/MapCast                                                 | 0m00.36s  || +0m00.00s | +0.00%
0m00.36s  | Util/ZUtil/Tactics/SimplifyFractionsLe                                  | 0m00.31s  || +0m00.04s | +16.12%
0m00.36s  | Util/ZUtil/Tactics/ZeroBounds                                           | 0m00.35s  || +0m00.01s | +2.85%
0m00.35s  | Compilers/Named/ContextOn                                               | 0m00.33s  || +0m00.01s | +6.06%
0m00.35s  | Compilers/Named/PositiveContext/Defaults                                | 0m00.42s  || -0m00.07s | -16.66%
0m00.35s  | Compilers/ZExtended/InlineConstAndOpInterp                              | 0m00.35s  || +0m00.00s | +0.00%
0m00.35s  | Compilers/ZExtended/Syntax/Util                                         | 0m00.37s  || -0m00.02s | -5.40%
0m00.35s  | LegacyArithmetic/Pow2Base                                               | 0m00.46s  || -0m00.11s | -23.91%
0m00.35s  | Util/ZUtil/Odd                                                          |    N/A    || +0m00.35s | ∞
0m00.35s  | Util/ZUtil/Pow                                                          |    N/A    || +0m00.35s | ∞
0m00.35s  | Util/ZUtil/Pow2                                                         |    N/A    || +0m00.35s | ∞
0m00.34s  | Compilers/InlineConstAndOpByRewrite                                     | 0m00.35s  || -0m00.00s | -2.85%
0m00.34s  | Compilers/Named/CountLets                                               | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Compilers/Named/MapType                                                 | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Compilers/Named/PositiveContext                                         | 0m00.38s  || -0m00.03s | -10.52%
0m00.34s  | Compilers/Named/Syntax                                                  | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Compilers/Tuple                                                         | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Compilers/ZExtended/InlineConstAndOpByRewriteInterp                     | 0m00.35s  || -0m00.00s | -2.85%
0m00.34s  | Compilers/ZExtended/InlineConstAndOpWf                                  | 0m00.34s  || +0m00.00s | +0.00%
0m00.34s  | Util/ZUtil/Land                                                         | 0m00.29s  || +0m00.05s | +17.24%
0m00.34s  | Util/ZUtil/N2Z                                                          |    N/A    || +0m00.34s | ∞
0m00.34s  | Util/ZUtil/Tactics/PullPush/Modulo                                      | 0m00.33s  || +0m00.01s | +3.03%
0m00.34s  | Util/ZUtil/Tactics/Ztestbit                                             | 0m00.36s  || -0m00.01s | -5.55%
0m00.33s  | Arithmetic/MontgomeryReduction/Definition                               | 0m00.52s  || -0m00.19s | -36.53%
0m00.33s  | Compilers/CountLets                                                     | 0m00.30s  || +0m00.03s | +10.00%
0m00.33s  | Compilers/FoldTypes                                                     | 0m00.31s  || +0m00.02s | +6.45%
0m00.33s  | Compilers/InterpByIso                                                   | 0m00.35s  || -0m00.01s | -5.71%
0m00.33s  | Compilers/MapCastByDeBruijn                                             | 0m00.60s  || -0m00.26s | -44.99%
0m00.33s  | Compilers/Named/ContextDefinitions                                      | 0m00.36s  || -0m00.02s | -8.33%
0m00.33s  | Compilers/Named/SmartMap                                                | 0m00.32s  || +0m00.01s | +3.12%
0m00.33s  | Util/BoundedWord                                                        | 0m00.43s  || -0m00.09s | -23.25%
0m00.33s  | Util/ZUtil/Hints                                                        | 0m00.33s  || +0m00.00s | +0.00%
0m00.33s  | Util/ZUtil/Hints/ZArith                                                 | 0m00.33s  || +0m00.00s | +0.00%
0m00.32s  | Compilers/FilterLive                                                    | 0m00.35s  || -0m00.02s | -8.57%
0m00.32s  | Compilers/MapBaseType                                                   | 0m00.32s  || +0m00.00s | +0.00%
0m00.32s  | Compilers/Named/ExprInversion                                           | 0m00.34s  || -0m00.02s | -5.88%
0m00.32s  | Compilers/Named/IdContext                                               | 0m00.31s  || +0m00.01s | +3.22%
0m00.32s  | Compilers/Named/InterpretToPHOAS                                        | 0m00.35s  || -0m00.02s | -8.57%
0m00.32s  | Compilers/ZExtended/InlineConstAndOp                                    | 0m00.34s  || -0m00.02s | -5.88%
0m00.32s  | Util/IdfunWithAlt                                                       | 0m00.32s  || +0m00.00s | +0.00%
0m00.32s  | Util/ZRange/Show                                                        | 0m00.32s  || +0m00.00s | +0.00%
0m00.32s  | Util/ZUtil/DistrIf                                                      |    N/A    || +0m00.32s | ∞
0m00.32s  | Util/ZUtil/Opp                                                          |    N/A    || +0m00.32s | ∞
0m00.31s  | Compilers/CommonSubexpressionEliminationDenote                          | 0m00.38s  || -0m00.07s | -18.42%
0m00.31s  | Compilers/Linearize                                                     | 0m00.34s  || -0m00.03s | -8.82%
0m00.31s  | Compilers/Named/Context                                                 | 0m00.34s  || -0m00.03s | -8.82%
0m00.31s  | Spec/ModularArithmetic                                                  | 0m00.41s  || -0m00.09s | -24.39%
0m00.31s  | Util/ZUtil/Tactics                                                      | 0m00.29s  || +0m00.02s | +6.89%
0m00.30s  | Compilers/Z/OpInversion                                                 | 0m00.35s  || -0m00.04s | -14.28%
0m00.30s  | Compilers/ZExtended/InlineConstAndOpByRewrite                           | 0m00.34s  || -0m00.04s | -11.76%
0m00.30s  | Compilers/ZExtended/InlineConstAndOpByRewriteWf                         | 0m00.33s  || -0m00.03s | -9.09%
0m00.30s  | Util/ZUtil/MulSplit                                                     | 0m00.37s  || -0m00.07s | -18.91%
0m00.28s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition           | 0m00.26s  || +0m00.02s | +7.69%
0m00.27s  | Util/ZUtil/AddModulo                                                    | 0m00.25s  || +0m00.02s | +8.00%
0m00.27s  | Util/ZUtil/Tactics/PullPush                                             | 0m00.26s  || +0m00.01s | +3.84%
0m00.25s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition | 0m00.24s  || +0m00.01s | +4.16%
0m00.24s  | Util/ZUtil/Zselect                                                      | 0m00.25s  || -0m00.01s | -4.00%

4 files changed, 51 insertions, 124 deletions

diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index 410cb8dfe..56a7051af 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -21,8 +21,15 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sum.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Opp.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Le.
 Require Import Crypto.Util.ZUtil.Hints.PullPush.
 Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
@@ -37,7 +44,7 @@ Require Import Crypto.Util.ZUtil.Sorting.
 Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
 Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
 Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
 Require Import Crypto.Util.ZUtil.Hints.PullPush.
 Require Import Crypto.Util.ZUtil.EquivModulo.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 869abea8e..01018c3e2 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -30,10 +30,17 @@ Require Import Crypto.Util.ZUtil.Rshi.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Log2.
 Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.AddModulo.
 Require Import Crypto.Util.ZUtil.CC.
+Require Import Crypto.Util.ZUtil.EquivModulo.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
 Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs.
 Require Import Crypto.Util.ZUtil.ModInv.
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v
index e35e14616..ffb6b0215 100644
--- a/src/Experiments/NewPipeline/Toplevel2.v
+++ b/src/Experiments/NewPipeline/Toplevel2.v
@@ -16,6 +16,7 @@ Require Import Crypto.Util.LetIn.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Tactics.SubstEvars.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -29,10 +30,14 @@ Require Import Crypto.Util.ZUtil.Rshi.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.AddModulo.
 Require Import Crypto.Util.ZUtil.CC.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Notations.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.EquivModulo.
 Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
 Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs.
 Require Import Crypto.Util.ErrorT.
@@ -2087,24 +2092,13 @@ Module ProdEquiv.
       let new_ctx := fun n => if reg_eqb n rd then result mod wordmax else ctx n in interp256 cont new_cc new_ctx.
   Proof. reflexivity. Qed.
 
-  (* TODO : move *)
-  Lemma tuple_map_ext {A B} (f g : A -> B) n (t : tuple A n) :
-    (forall x : A, f x = g x) ->
-    Tuple.map f t = Tuple.map g t.
-  Proof.
-    destruct n; [reflexivity|]; cbn in *.
-    induction n; cbn in *; intro H; auto; [ ].
-    rewrite IHn by assumption.
-    rewrite H; reflexivity.
-  Qed.
-
   Lemma interp_state_equiv e :
     forall cc ctx cc' ctx',
     cc = cc' -> (forall r, ctx r = ctx' r) ->
     interp256 e cc ctx = interp256 e cc' ctx'.
   Proof.
     induction e; intros; subst; cbn; [solve[auto]|].
-    apply IHe; rewrite tuple_map_ext with (g:=ctx') by auto;
+    apply IHe; rewrite Tuple.map_ext with (g:=ctx') by auto;
       [reflexivity|].
     intros; break_match; auto.
   Qed.
@@ -2116,17 +2110,6 @@ Module ProdEquiv.
     reflexivity.
   Qed.
 
-  Lemma tuple_map_ext_In {A B} (f g : A -> B) n (t : tuple A n) :
-    (forall x, In x (to_list n t) -> f x = g x) ->
-    Tuple.map f t = Tuple.map g t.
-  Proof.
-    destruct n; [reflexivity|]; cbn in *.
-    induction n; cbn in *; intro H; auto; [ ].
-    destruct t.
-    rewrite IHn by auto using in_cons.
-    rewrite H; auto using in_eq.
-  Qed.
-
   Definition value_unused r e : Prop :=
     forall x cc ctx, interp256 e cc ctx = interp256 e cc (fun r' => if reg_eqb r' r then x else ctx r').
 
@@ -2141,7 +2124,7 @@ Module ProdEquiv.
     match goal with |- ?lhs = ?rhs =>
                     match lhs with context [Tuple.map ?f ?t] =>
                                    match rhs with context [Tuple.map ?g ?t] =>
-                                                  rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
+                                                  rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
                                    end end end.
     apply interp_state_equiv; [ congruence | ].
     { intros; cbv [reg_eqb] in *; break_match; congruence. }
@@ -2155,7 +2138,7 @@ Module ProdEquiv.
     match goal with |- ?lhs = ?rhs =>
                     match lhs with context [Tuple.map ?f ?t] =>
                                    match rhs with context [Tuple.map ?g ?t] =>
-                                                  rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
+                                                  rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
                                    end end end.
     apply interp_state_equiv; [ congruence | ].
     { intros; cbv [reg_eqb] in *; break_match; congruence. }
@@ -2649,19 +2632,6 @@ Module Barrett256.
       => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result]
     end.
 
-  (* TODO: move this lemma to ZUtil *)
-  Lemma testbit_neg_eq_if x n :
-    0 <= n ->
-    - (2 ^ n) <= x  < 2 ^ n ->
-    Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2.
-  Proof.
-    intros. break_match; Z.ltb_to_lt.
-    { autorewrite with zsimplify. reflexivity. }
-    { autorewrite with zsimplify.
-      rewrite Z.bits_above_pow2 by omega.
-      reflexivity. }
-  Qed.
-
   Lemma prod_barrett_red256_correct :
     forall (cc_start_state : Fancy.CC.state) (* starting carry flags *)
            (start_context : register -> Z)   (* starting register values *)
@@ -2755,7 +2725,7 @@ Module Barrett256.
     { reflexivity. }
     { autorewrite with zsimplify_fast.
       match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-      rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega).
+      rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega).
       reflexivity. }
     step start_context.
     { reflexivity. }
@@ -2763,7 +2733,7 @@ Module Barrett256.
       rewrite Z.mod_small with (a:=(if (if _ <? 0 then true else _) then _ else _)) (b:=2) by (break_innermost_match; omega).
       match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end.
       match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-      rewrite <-testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega).
+      rewrite <-Z.testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega).
       reflexivity. }
     step start_context.
     { rewrite Z.bit0_eqb.
@@ -2782,7 +2752,7 @@ Module Barrett256.
     { reflexivity. }
     { autorewrite with zsimplify_fast.
       repeat match goal with |- context [?x mod ?m] => unique pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-      rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega).
+      rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega).
       reflexivity. }
     step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ].
     reflexivity.
@@ -3169,19 +3139,6 @@ Module Montgomery256.
       => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result]
     end.
 
-  (* TODO: move this lemma to ZUtil *)
-  Lemma testbit_neg_eq_if x y n :
-    0 <= n ->
-    0 <= x < 2 ^ n ->
-    0 <= y < 2 ^ n ->
-    Z.b2z (if (x - y) <? 0 then true else Z.testbit (x - y) n) = - ((x - y) / 2 ^ n) mod 2.
-  Proof.
-    intros. rewrite Z.sub_pos_bound_div_eq by omega.
-    break_innermost_match; Z.ltb_to_lt; try lia; try reflexivity; [ ].
-    rewrite Z.testbit_eqb, Z.div_between_0_if by omega.
-    break_innermost_match; Z.ltb_to_lt; try lia; reflexivity.
-  Qed.
-
   Local Ltac break_ifs :=
     repeat (break_innermost_match_step; Z.ltb_to_lt; try (exfalso; omega); []).
 
@@ -3228,7 +3185,7 @@ Module Montgomery256.
     {
       let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity.
       rewrite !Z.shiftl_0_r, !Z.mod_mod by omega.
-      apply testbit_neg_eq_if;
+      apply Z.testbit_neg_eq_if;
         let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity;
         auto using Z.mod_pos_bound with omega. }
     step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ].
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 3745e59ff..c0c8dbdeb 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -23,13 +23,21 @@ Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Hints.PullPush.
 Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Le.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Notations.
+Require Import Crypto.Util.ZUtil.Shift.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Testbit.
+Require Import Crypto.Util.ZUtil.Notations.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Tactics.SubstEvars.
@@ -41,7 +49,7 @@ Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
 Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
 Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
 Require Import Crypto.Util.ZUtil.Hints.PullPush.
 Require Import Crypto.Util.ZUtil.EquivModulo.
@@ -1245,13 +1253,6 @@ Module Rows.
         rewrite Columns.length_from_associational in *; auto.
       Qed.
 
-      (* TODO : move *)
-      Lemma max_0_iff a b : Nat.max a b = 0%nat <-> (a = 0%nat /\ b = 0%nat).
-      Proof.
-        destruct a, b; try tauto.
-        rewrite <-Nat.succ_max_distr.
-        split; [ | destruct 1]; congruence.
-      Qed.
       Lemma max_column_size_zero_iff x :
         max_column_size x = 0%nat <-> (forall c, In c x -> c = nil).
       Proof.
@@ -10402,24 +10403,13 @@ Module ProdEquiv.
       let new_ctx := fun n => if reg_eqb n rd then result mod wordmax else ctx n in interp256 cont new_cc new_ctx.
   Proof. reflexivity. Qed.
 
-  (* TODO : move *)
-  Lemma tuple_map_ext {A B} (f g : A -> B) n (t : tuple A n) :
-    (forall x : A, f x = g x) ->
-    Tuple.map f t = Tuple.map g t.
-  Proof.
-    destruct n; [reflexivity|]; cbn in *.
-    induction n; cbn in *; intro H; auto; [ ].
-    rewrite IHn by assumption.
-    rewrite H; reflexivity.
-  Qed.
-
   Lemma interp_state_equiv e :
     forall cc ctx cc' ctx',
     cc = cc' -> (forall r, ctx r = ctx' r) ->
     interp256 e cc ctx = interp256 e cc' ctx'.
   Proof.
     induction e; intros; subst; cbn; [solve[auto]|].
-    apply IHe; rewrite tuple_map_ext with (g:=ctx') by auto;
+    apply IHe; rewrite Tuple.map_ext with (g:=ctx') by auto;
       [reflexivity|].
     intros; break_match; auto.
   Qed.
@@ -10431,17 +10421,6 @@ Module ProdEquiv.
     reflexivity.
   Qed.
 
-  Lemma tuple_map_ext_In {A B} (f g : A -> B) n (t : tuple A n) :
-    (forall x, In x (to_list n t) -> f x = g x) ->
-    Tuple.map f t = Tuple.map g t.
-  Proof.
-    destruct n; [reflexivity|]; cbn in *.
-    induction n; cbn in *; intro H; auto; [ ].
-    destruct t.
-    rewrite IHn by auto using in_cons.
-    rewrite H; auto using in_eq.
-  Qed.
-
   Definition value_unused r e : Prop :=
     forall x cc ctx, interp256 e cc ctx = interp256 e cc (fun r' => if reg_eqb r' r then x else ctx r').
 
@@ -10456,7 +10435,7 @@ Module ProdEquiv.
     match goal with |- ?lhs = ?rhs =>
                     match lhs with context [Tuple.map ?f ?t] =>
                                    match rhs with context [Tuple.map ?g ?t] =>
-                                                  rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
+                                                  rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
                                    end end end.
     apply interp_state_equiv; [ congruence | ].
     { intros; cbv [reg_eqb] in *; break_match; congruence. }
@@ -10470,7 +10449,7 @@ Module ProdEquiv.
     match goal with |- ?lhs = ?rhs =>
                     match lhs with context [Tuple.map ?f ?t] =>
                                    match rhs with context [Tuple.map ?g ?t] =>
-                                                  rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
+                                                  rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence)
                                    end end end.
     apply interp_state_equiv; [ congruence | ].
     { intros; cbv [reg_eqb] in *; break_match; congruence. }
@@ -11525,19 +11504,6 @@ Module Barrett256.
     | _ => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result]
     end.
 
-  (* TODO: move this lemma to ZUtil *)
-  Lemma testbit_neg_eq_if x n :
-    0 <= n ->
-    - (2 ^ n) <= x  < 2 ^ n ->
-    Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2.
-  Proof.
-    intros. break_match; Z.ltb_to_lt.
-    { autorewrite with zsimplify. reflexivity. }
-    { autorewrite with zsimplify.
-      rewrite Z.bits_above_pow2 by omega.
-      reflexivity. }
-  Qed.
-
   Lemma prod_barrett_red256_correct :
     forall (cc_start_state : Fancy.CC.state) (* starting carry flags *)
            (start_context : register -> Z)   (* starting register values *)
@@ -11631,7 +11597,7 @@ Module Barrett256.
     { reflexivity. }
     { autorewrite with zsimplify_fast.
       match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-      rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega).
+      rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega).
       reflexivity. }
     step start_context.
     { reflexivity. }
@@ -11639,7 +11605,7 @@ Module Barrett256.
       rewrite Z.mod_small with (a:=(if (if _ <? 0 then true else _) then _ else _)) (b:=2) by (break_innermost_match; omega).
       match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end.
       match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-      rewrite <-testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega).
+      rewrite <-Z.testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega).
       reflexivity. }
     step start_context.
     { rewrite Z.bit0_eqb.
@@ -11658,7 +11624,7 @@ Module Barrett256.
     { reflexivity. }
     { autorewrite with zsimplify_fast.
       repeat match goal with |- context [?x mod ?m] => unique pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-      rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega).
+      rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega).
       reflexivity. }
     step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ].
     reflexivity.
@@ -12567,19 +12533,6 @@ Module Montgomery256.
     | _ => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result]
     end.
 
-  (* TODO: move this lemma to ZUtil *)
-  Lemma testbit_neg_eq_if x y n :
-    0 <= n ->
-    0 <= x < 2 ^ n ->
-    0 <= y < 2 ^ n ->
-    Z.b2z (if (x - y) <? 0 then true else Z.testbit (x - y) n) = - ((x - y) / 2 ^ n) mod 2.
-  Proof.
-    intros. rewrite Z.sub_pos_bound_div_eq by omega.
-    break_innermost_match; Z.ltb_to_lt; try lia; try reflexivity; [ ].
-    rewrite Z.testbit_eqb, Z.div_between_0_if by omega.
-    break_innermost_match; Z.ltb_to_lt; try lia; reflexivity.
-  Qed.
-
   Lemma prod_montred256_correct :
     forall (cc_start_state : Fancy.CC.state) (* starting carry flags can be anything *)
            (start_context : register -> Z)   (* starting register values *)
@@ -12622,9 +12575,12 @@ Module Montgomery256.
     {
       let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity.
       rewrite !Z.shiftl_0_r, !Z.mod_mod by omega.
-      apply testbit_neg_eq_if;
+      repeat match goal with
+             | |- context [?a mod ?b] => unique pose proof (Z.mod_pos_bound a b ltac:(omega))
+             end.
+      apply Z.testbit_neg_eq_if;
         let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity;
-        auto using Z.mod_pos_bound with omega. }
+                               omega. }
     step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ].
     reflexivity.
   Qed.