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%

17 files changed, 94 insertions, 36 deletions

diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v
index 9fa37721a..c2885bc77 100644
--- a/src/Arithmetic/BarrettReduction/Generalized.v
+++ b/src/Arithmetic/BarrettReduction/Generalized.v
@@ -9,7 +9,15 @@
     base ([b]), exponent ([k]), and the [offset] than those given in
     the HAC. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Pow.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.ZSimplify.
+Require Import Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
 
@@ -94,17 +102,17 @@ Section barrett.
       : q * n <= a.
     Proof using a_nonneg a_small base_good k_big_enough m_good n_pos n_reasonable offset_nonneg.
       subst q r m.
-      assert (0 < b^(k-offset)). zero_bounds.
-      assert (0 < b^(k+offset)) by zero_bounds.
-      assert (0 < b^(2 * k)) by zero_bounds.
+      assert (0 < b^(k-offset)). Z.zero_bounds.
+      assert (0 < b^(k+offset)) by Z.zero_bounds.
+      assert (0 < b^(2 * k)) by Z.zero_bounds.
       Z.simplify_fractions_le.
       autorewrite with pull_Zpow pull_Zdiv zsimplify; reflexivity.
     Qed.
 
     Lemma q_nice : { b : bool * bool | q = a / n + (if fst b then -1 else 0) + (if snd b then -1 else 0) }.
     Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg.
-      assert (0 < b^(k+offset)) by zero_bounds.
-      assert (0 < b^(k-offset)) by zero_bounds.
+      assert (0 < b^(k+offset)) by Z.zero_bounds.
+      assert (0 < b^(k-offset)) by Z.zero_bounds.
       assert (a / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia.
       assert (a / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption).
       subst q r m.
diff --git a/src/Arithmetic/BarrettReduction/HAC.v b/src/Arithmetic/BarrettReduction/HAC.v
index 70661ee96..c9fb2f16f 100644
--- a/src/Arithmetic/BarrettReduction/HAC.v
+++ b/src/Arithmetic/BarrettReduction/HAC.v
@@ -9,7 +9,13 @@
     have to carry around extra precision), but requires more stringint
     conditions on the base ([b]), exponent ([k]), and the [offset]. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Hints.
+Require Import Crypto.Util.ZUtil.ZSimplify.
 
 Local Open Scope Z_scope.
 
@@ -72,8 +78,8 @@ Section barrett.
     Let R := x mod m.
     Lemma q3_nice : { b : bool * bool | q3 = Q + (if fst b then -1 else 0) + (if snd b then -1 else 0) }.
     Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg x_nonneg x_small μ_good.
-      assert (0 < b^(k+offset)) by zero_bounds.
-      assert (0 < b^(k-offset)) by zero_bounds.
+      assert (0 < b^(k+offset)) by Z.zero_bounds.
+      assert (0 < b^(k-offset)) by Z.zero_bounds.
       assert (x / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia.
       assert (x / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption).
       subst q1 q2 q3 Q r_mod_3m r_mod_3m_orig r1 r2 R μ.
diff --git a/src/Arithmetic/BarrettReduction/RidiculousFish.v b/src/Arithmetic/BarrettReduction/RidiculousFish.v
index b9697839d..af030dcfe 100644
--- a/src/Arithmetic/BarrettReduction/RidiculousFish.v
+++ b/src/Arithmetic/BarrettReduction/RidiculousFish.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Hints.ZArith.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
diff --git a/src/Arithmetic/BarrettReduction/Wikipedia.v b/src/Arithmetic/BarrettReduction/Wikipedia.v
index 69ce10c4b..46f831281 100644
--- a/src/Arithmetic/BarrettReduction/Wikipedia.v
+++ b/src/Arithmetic/BarrettReduction/Wikipedia.v
@@ -1,7 +1,11 @@
 (*** Barrett Reduction *)
 (** This file implements Barrett Reduction on [Z].  We follow Wikipedia. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
@@ -80,7 +84,7 @@ Section barrett.
       : q * n <= a.
     Proof using a_nonneg k_good m_good n_pos n_reasonable.
       pose proof k_nonnegative; subst q r m.
-      assert (0 <= 2^(k-1)) by zero_bounds.
+      assert (0 <= 2^(k-1)) by Z.zero_bounds.
       Z.simplify_fractions_le.
     Qed.
 
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 98600d9a3..48046d7e3 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -246,8 +246,9 @@ Local Open Scope Z_scope.
 
 Require Import Crypto.Algebra.Nsatz.
 Require Import Crypto.Util.Decidable Crypto.Util.LetIn.
-Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil Crypto.Util.Sigma.
+Require Import Crypto.Util.ListUtil Crypto.Util.Sigma.
 Require Import Crypto.Util.CPSUtil Crypto.Util.Prod.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
 Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Definitions.
@@ -257,6 +258,7 @@ Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.VM.
 Require Import Crypto.Util.IdfunWithAlt.
+Require Import Crypto.Util.Notations.
 
 Require Import Coq.Lists.List. Import ListNotations.
 Require Crypto.Util.Tuple. Local Notation tuple := Tuple.tuple.
diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v
index ad5e25be8..1873e5ef1 100644
--- a/src/Arithmetic/Karatsuba.v
+++ b/src/Arithmetic/Karatsuba.v
@@ -1,10 +1,11 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Require Import Crypto.Algebra.Nsatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.LetIn Crypto.Util.CPSUtil.
+Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil.
 Require Import Crypto.Arithmetic.Core. Import B. Import Positional.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.IdfunWithAlt.
+Require Import Crypto.Util.ZUtil.EquivModulo.
 Local Open Scope Z_scope.
 
 Section Karatsuba.
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 666dd54eb..d1fcd80b9 100644
--- a/src/Arithmetic/ModularArithmeticTheorems.v
+++ b/src/Arithmetic/ModularArithmeticTheorems.v
@@ -8,7 +8,9 @@ Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac.
 
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult.
 Require Crypto.Algebra.Ring Crypto.Algebra.Field.
-Require Import Crypto.Util.Decidable Crypto.Util.ZUtil.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Export Crypto.Util.FixCoqMistakes.
 
 Module F.
diff --git a/src/Arithmetic/MontgomeryReduction/Definition.v b/src/Arithmetic/MontgomeryReduction/Definition.v
index 04c097460..e5cdcc603 100644
--- a/src/Arithmetic/MontgomeryReduction/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/Definition.v
@@ -2,7 +2,7 @@
 (** This file implements Montgomery Form, Montgomery Reduction, and
     Montgomery Multiplication on [Z].  We follow Wikipedia. *)
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.EquivModulo.
 Require Import Crypto.Util.Notations.
 
 Local Open Scope Z_scope.
diff --git a/src/Arithmetic/MontgomeryReduction/Proofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v
index 5f459e52d..e6be440fb 100644
--- a/src/Arithmetic/MontgomeryReduction/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/Proofs.v
@@ -4,7 +4,9 @@
     Wikipedia. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Structures.Equalities.
 Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.EquivModulo.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SimplifyRepeatedIfs.
 Require Import Crypto.Util.Notations.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
index 266fc1f6f..3dd7fc0b3 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
@@ -4,11 +4,19 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition.
 Require Import Crypto.Algebra.Ring.
 Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.EquivModulo.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Tactics.SetEvars.
 Require Import Crypto.Util.Tactics.SubstEvars.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
index 9ca2cf4e9..9eabc5ce4 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
@@ -4,11 +4,19 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Definition.
 Require Import Crypto.Algebra.Ring.
 Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.EquivModulo.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Tactics.SetEvars.
 Require Import Crypto.Util.Tactics.SubstEvars.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index 6d2925d6b..35c9e377b 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -6,7 +6,6 @@ Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Proofs.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v
index a4305a849..47ea89e31 100644
--- a/src/Arithmetic/PrimeFieldTheorems.v
+++ b/src/Arithmetic/PrimeFieldTheorems.v
@@ -8,7 +8,10 @@ Require Import Crypto.Util.NumTheoryUtil.
 Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
 Require Import Coq.Logic.Eqdep_dec.
-Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.NumTheoryUtil.
+Require Import Crypto.Util.ZUtil.Odd.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
@@ -105,7 +108,7 @@ Module F.
       repeat match goal with
              | |- _ => progress subst
              | |- _ => progress rewrite ?F.pow_0_l, <-?F.pow_add_r
-             | |- _ => progress rewrite <-?Z2N.inj_0, <-?Z2N.inj_add by zero_bounds
+             | |- _ => progress rewrite <-?Z2N.inj_0, <-?Z2N.inj_add by Z.zero_bounds
              | |- _ => rewrite <-@euler_criterion by auto
              | |- ?x ^ (?f _) = ?a <-> ?x ^ (?f _) = ?a => do 3 f_equiv; [ ]
              | |- _ => rewrite !Zmod_odd in *; repeat (break_match; break_match_hyps); omega
@@ -114,10 +117,10 @@ Module F.
              | |- (?x ^ Z.to_N ?a = 1) <-> _ =>
                transitivity (x ^ Z.to_N a * x ^ Z.to_N 1 = x);
                  [ rewrite F.pow_1_r, Algebra.Field.mul_cancel_l_iff by auto; reflexivity | ]
-             | |- (_ <> _)%N => rewrite Z2N.inj_iff by zero_bounds
-             | |- (?a <> 0)%Z => assert (0 < a) by zero_bounds; omega
+             | |- (_ <> _)%N => rewrite Z2N.inj_iff by Z.zero_bounds
+             | |- (?a <> 0)%Z => assert (0 < a) by Z.zero_bounds; omega
              | |- (_ = _)%Z => replace 4 with (2 * 2)%Z in * by ring;
-                                 rewrite <-Z.div_div by zero_bounds;
+                                 rewrite <-Z.div_div by Z.zero_bounds;
                                  rewrite Z.add_diag, Z.mul_add_distr_l, Z.mul_div_eq by omega
              end.
     Qed.
@@ -166,8 +169,8 @@ Module F.
       replace (Z.to_N (q / 8 + 1) * (2*2))%N with (Z.to_N (q / 2 + 2))%N.
       Focus 2. { (* this is a boring but gnarly proof :/ *)
         change (2*2)%N with (Z.to_N 4).
-        rewrite <- Z2N.inj_mul by zero_bounds.
-        apply Z2N.inj_iff; try zero_bounds.
+        rewrite <- Z2N.inj_mul by Z.zero_bounds.
+        apply Z2N.inj_iff; try Z.zero_bounds.
         rewrite <- Z.mul_cancel_l with (p := 2) by omega.
         ring_simplify.
         rewrite Z.mul_div_eq by omega.
@@ -179,7 +182,7 @@ Module F.
         ring.
       } Unfocus.
 
-      rewrite Z2N.inj_add, F.pow_add_r by zero_bounds.
+      rewrite Z2N.inj_add, F.pow_add_r by Z.zero_bounds.
       replace (x ^ Z.to_N (q / 2)) with (F.of_Z q 1) by
           (symmetry; apply @euler_criterion; eauto).
       change (Z.to_N 2) with 2%N; ring.
@@ -215,8 +218,8 @@ Module F.
         repeat match goal with
              | |- _ => progress subst
              | |- _ => progress rewrite ?F.pow_0_l
-             | |- (_ <> _)%N => rewrite <-Z2N.inj_0, Z2N.inj_iff by zero_bounds
-             | |- (?a <> 0)%Z => assert (0 < a) by zero_bounds; omega
+             | |- (_ <> _)%N => rewrite <-Z2N.inj_0, Z2N.inj_iff by Z.zero_bounds
+             | |- (?a <> 0)%Z => assert (0 < a) by Z.zero_bounds; omega
              | |- _ => congruence
              end.
         break_match;
diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v
index 189e76113..9c796ad57 100644
--- a/src/Arithmetic/Saturated/Core.v
+++ b/src/Arithmetic/Saturated/Core.v
@@ -9,7 +9,12 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil.
 Require Import Crypto.Util.Tuple Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Decidable Crypto.Util.ZUtil.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Le.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Local Notation "A ^ n" := (tuple A n) : type_scope.
@@ -273,7 +278,7 @@ Module Columns.
         rewrite <-Z.mul_mod_distr_l with (c:=a) by omega.
         rewrite Z.mul_add_distr_l, Z.mul_div_eq, <-Z.add_mod_full by omega.
         f_equal; ring. }
-      { split; [zero_bounds|].
+      { split; [Z.zero_bounds|].
         apply Z.lt_le_trans with (m:=a*(b-1)+a); [|ring_simplify; omega].
         apply Z.add_le_lt_mono; try apply Z.mul_le_mono_nonneg_l; omega. }
     Qed.
diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v
index 78a86bc73..d8e7f4b5e 100644
--- a/src/Arithmetic/Saturated/Freeze.v
+++ b/src/Arithmetic/Saturated/Freeze.v
@@ -7,9 +7,11 @@ Require Import Crypto.Arithmetic.Saturated.Core.
 Require Import Crypto.Arithmetic.Saturated.Wrappers.
 Require Import Crypto.Util.ZUtil.AddGetCarry.
 Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Le.
 Require Import Crypto.Util.ZUtil.CPS.
 Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Decidable Crypto.Util.ZUtil.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Tuple Crypto.Util.LetIn.
 Local Notation "A ^ n" := (tuple A n) : type_scope.
 
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index 6dee1d22b..d08fe7a8b 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -11,12 +11,18 @@ Require Import Crypto.Arithmetic.Saturated.AddSub.
 Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil.
 Require Import Crypto.Util.Tuple Crypto.Util.LetIn.
 Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.CPS.
 Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.AddGetCarry.
 Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Opp.
 Require Import Crypto.Util.Tactics.UniquePose.
 Local Notation "A ^ n" := (tuple A n) : type_scope.
 
diff --git a/src/Arithmetic/Saturated/UniformWeight.v b/src/Arithmetic/Saturated/UniformWeight.v
index bd351b6cd..bf069f2d6 100644
--- a/src/Arithmetic/Saturated/UniformWeight.v
+++ b/src/Arithmetic/Saturated/UniformWeight.v
@@ -4,7 +4,9 @@ Local Open Scope Z_scope.
 
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.Saturated.Core.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Le.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
 Require Import Crypto.Util.LetIn Crypto.Util.Tuple.
 Local Notation "A ^ n" := (tuple A n) : type_scope.
 
@@ -88,4 +90,4 @@ Section UniformWeight.
   Definition small {n} (p : Z^n) : Prop :=
     forall x, In x (to_list _ p) -> 0 <= x < bound.
 
-End UniformWeight.
\ No newline at end of file
+End UniformWeight.