Minor improvements to various ZUtil things; bounds

We improve the linear_substitute tactic to handle Z.opp.

Also, the ZRange Z.land and Z.lor bounds are now done.

After     | File Name                                                               | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------------------------------
68m36.35s | Total                                                                   | 68m21.13s || +0m15.22s | +0.37%
-----------------------------------------------------------------------------------------------------------------------
0m12.24s  | Util/ZRange/LandLorBounds                                               |    N/A    || +0m12.24s | ∞
0m06.17s  | Util/ZUtil/LandLorBounds                                                | 0m14.63s  || -0m08.46s | -57.82%
8m48.80s  | Experiments/SimplyTypedArithmetic                                       | 8m45.78s  || +0m03.01s | +0.57%
4m40.18s  | Experiments/NewPipeline/Toplevel1                                       | 4m38.02s  || +0m02.16s | +0.77%
3m45.94s  | Curves/Montgomery/XZProofs                                              | 3m44.89s  || +0m01.05s | +0.46%
0m32.78s  | Compilers/Z/ArithmeticSimplifierWf                                      | 0m31.13s  || +0m01.65s | +5.30%
6m03.08s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                      | 6m02.74s  || +0m00.33s | +0.09%
4m10.59s  | Experiments/NewPipeline/RewriterRulesGood                               | 4m10.73s  || -0m00.13s | -0.05%
2m10.48s  | Specific/X25519/C64/ladderstep                                          | 2m11.19s  || -0m00.71s | -0.54%
1m51.84s  | Specific/NISTP256/AMD64/femul                                           | 1m51.84s  || +0m00.00s | +0.00%
1m43.72s  | Experiments/NewPipeline/Toplevel2                                       | 1m43.20s  || +0m00.51s | +0.50%
1m31.20s  | Experiments/NewPipeline/Arithmetic                                      | 1m30.61s  || +0m00.59s | +0.65%
1m29.07s  | Spec/Test/X25519                                                        | 1m29.18s  || -0m00.11s | -0.12%
1m24.10s  | Experiments/NewPipeline/RewriterWf2                                     | 1m23.42s  || +0m00.67s | +0.81%
1m18.68s  | Specific/X2448/Karatsuba/C64/femul                                      | 1m18.59s  || +0m00.09s | +0.11%
1m17.29s  | Experiments/NewPipeline/Rewriter                                        | 1m17.46s  || -0m00.17s | -0.21%
0m59.90s  | Specific/X25519/C32/femul                                               | 0m59.59s  || +0m00.30s | +0.52%
0m51.72s  | Demo                                                                    | 0m51.78s  || -0m00.06s | -0.11%
0m50.38s  | Compilers/Z/ArithmeticSimplifierInterp                                  | 0m50.01s  || +0m00.37s | +0.73%
0m49.23s  | Compilers/Z/Named/RewriteAddToAdcInterp                                 | 0m48.92s  || +0m00.30s | +0.63%
0m43.78s  | Specific/X25519/C32/fesquare                                            | 0m43.51s  || +0m00.27s | +0.62%
0m43.02s  | Arithmetic/Karatsuba                                                    | 0m42.29s  || +0m00.73s | +1.72%
0m42.02s  | Experiments/NewPipeline/AbstractInterpretationWf                        | 0m42.36s  || -0m00.33s | -0.80%
0m38.40s  | p521_32.c                                                               | 0m38.57s  || -0m00.17s | -0.44%
0m37.34s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery         | 0m37.02s  || +0m00.32s | +0.86%
0m36.09s  | Spec/Ed25519                                                            | 0m36.03s  || +0m00.06s | +0.16%
0m35.63s  | Experiments/NewPipeline/LanguageInversion                               | 0m35.62s  || +0m00.01s | +0.02%
0m34.48s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery       | 0m34.53s  || -0m00.05s | -0.14%
0m33.82s  | Specific/X25519/C32/freeze                                              | 0m34.09s  || -0m00.27s | -0.79%
0m32.01s  | p521_64.c                                                               | 0m32.30s  || -0m00.28s | -0.89%
0m27.47s  | Specific/NISTP256/AMD128/femul                                          | 0m27.77s  || -0m00.30s | -1.08%
0m26.65s  | Primitives/EdDSARepChange                                               | 0m26.80s  || -0m00.15s | -0.55%
0m25.91s  | Experiments/NewPipeline/UnderLetsProofs                                 | 0m25.65s  || +0m00.26s | +1.01%
0m25.41s  | Specific/X25519/C32/fecarry                                             | 0m25.35s  || +0m00.05s | +0.23%
0m25.40s  | Experiments/NewPipeline/AbstractInterpretationZRangeProofs              | 0m24.94s  || +0m00.45s | +1.84%
0m23.63s  | p384_32.c                                                               | 0m23.59s  || +0m00.03s | +0.16%
0m22.51s  | Experiments/NewPipeline/LanguageWf                                      | 0m22.62s  || -0m00.10s | -0.48%
0m21.78s  | Arithmetic/Core                                                         | 0m21.55s  || +0m00.23s | +1.06%
0m21.47s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas           | 0m20.96s  || +0m00.50s | +2.43%
0m21.43s  | Specific/X25519/C32/fesub                                               | 0m21.62s  || -0m00.19s | -0.87%
0m20.97s  | Specific/NISTP256/AMD64/fesub                                           | 0m20.87s  || +0m00.09s | +0.47%
0m20.68s  | Specific/X25519/C64/femul                                               | 0m20.39s  || +0m00.28s | +1.42%
0m19.56s  | Specific/X25519/C32/Synthesis                                           | 0m19.55s  || +0m00.00s | +0.05%
0m19.18s  | Specific/X25519/C32/feadd                                               | 0m19.13s  || +0m00.05s | +0.26%
0m19.06s  | Specific/NISTP256/AMD64/feadd                                           | 0m19.12s  || -0m00.06s | -0.31%
0m18.85s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas             | 0m19.00s  || -0m00.14s | -0.78%
0m18.04s  | Compilers/Z/CNotations                                                  | 0m17.97s  || +0m00.07s | +0.38%
0m17.68s  | Specific/X25519/C64/freeze                                              | 0m17.66s  || +0m00.01s | +0.11%
0m17.44s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs     | 0m17.56s  || -0m00.11s | -0.68%
0m17.01s  | Specific/X25519/C64/fesquare                                            | 0m16.94s  || +0m00.07s | +0.41%
0m15.88s  | Specific/NISTP256/AMD64/feopp                                           | 0m16.01s  || -0m00.13s | -0.81%
0m14.93s  | Specific/NISTP256/AMD128/fesub                                          | 0m14.82s  || +0m00.10s | +0.74%
0m14.89s  | Specific/NISTP256/AMD128/feadd                                          | 0m15.02s  || -0m00.12s | -0.86%
0m14.33s  | Specific/NISTP256/AMD64/fenz                                            | 0m14.34s  || -0m00.00s | -0.06%
0m14.12s  | Specific/X25519/C64/fecarry                                             | 0m14.02s  || +0m00.09s | +0.71%
0m14.00s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas             | 0m13.77s  || +0m00.23s | +1.67%
0m13.66s  | Arithmetic/Saturated/AddSub                                             | 0m13.84s  || -0m00.17s | -1.30%
0m13.53s  | Specific/NISTP256/AMD128/fenz                                           | 0m13.56s  || -0m00.03s | -0.22%
0m13.18s  | Specific/X25519/C64/fesub                                               | 0m12.97s  || +0m00.20s | +1.61%
0m13.10s  | Experiments/NewPipeline/CStringification                                | 0m13.06s  || +0m00.03s | +0.30%
0m12.48s  | Experiments/NewPipeline/AbstractInterpretationProofs                    | 0m12.53s  || -0m00.04s | -0.39%
0m12.42s  | Compilers/Z/Syntax/Equality                                             | 0m12.57s  || -0m00.15s | -1.19%
0m12.08s  | Specific/NISTP256/AMD128/feopp                                          | 0m12.18s  || -0m00.09s | -0.82%
0m12.00s  | Specific/X25519/C64/feadd                                               | 0m11.94s  || +0m00.06s | +0.50%
0m11.80s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs          | 0m11.72s  || +0m00.08s | +0.68%
0m11.46s  | Arithmetic/Saturated/MontgomeryAPI                                      | 0m11.59s  || -0m00.12s | -1.12%
0m10.69s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas               | 0m10.49s  || +0m00.19s | +1.90%
0m10.66s  | Arithmetic/Saturated/Core                                               | 0m10.78s  || -0m00.11s | -1.11%
0m10.64s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs               | 0m10.62s  || +0m00.02s | +0.18%
0m09.82s  | Specific/X2448/Karatsuba/C64/Synthesis                                  | 0m09.83s  || -0m00.00s | -0.10%
0m09.44s  | Util/ZRange/CornersMonotoneBounds                                       | 0m09.37s  || +0m00.07s | +0.74%
0m09.33s  | LegacyArithmetic/Double/Proofs/Multiply                                 | 0m09.28s  || +0m00.05s | +0.53%
0m08.92s  | LegacyArithmetic/ArchitectureToZLikeProofs                              | 0m08.73s  || +0m00.18s | +2.17%
0m08.74s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml      | 0m08.56s  || +0m00.17s | +2.10%
0m08.50s  | p384_64.c                                                               | 0m08.60s  || -0m00.09s | -1.16%
0m08.32s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate            | 0m08.25s  || +0m00.07s | +0.84%
0m08.12s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes                | 0m08.20s  || -0m00.08s | -0.97%
0m07.89s  | Arithmetic/MontgomeryReduction/Proofs                                   | 0m08.08s  || -0m00.19s | -2.35%
0m06.98s  | Specific/NISTP256/AMD64/Synthesis                                       | 0m07.00s  || -0m00.01s | -0.28%
0m06.62s  | Arithmetic/Saturated/MulSplit                                           | 0m06.62s  || +0m00.00s | +0.00%
0m06.42s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast                        | 0m06.44s  || -0m00.02s | -0.31%
0m06.41s  | Util/FixedWordSizesEquality                                             | 0m06.51s  || -0m00.09s | -1.53%
0m06.33s  | Util/ZUtil/Modulo                                                       | 0m06.10s  || +0m00.23s | +3.77%
0m06.20s  | Util/ZUtil/Morphisms                                                    | 0m06.25s  || -0m00.04s | -0.79%
0m06.18s  | Arithmetic/BarrettReduction/Generalized                                 | 0m06.20s  || -0m00.02s | -0.32%
0m05.92s  | Specific/X25519/C64/Synthesis                                           | 0m05.90s  || +0m00.01s | +0.33%
0m05.70s  | LegacyArithmetic/Pow2BaseProofs                                         | 0m05.73s  || -0m00.03s | -0.52%
0m05.66s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub                        | 0m05.62s  || +0m00.04s | +0.71%
0m05.59s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs    | 0m05.60s  || -0m00.00s | -0.17%
0m05.54s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml          | 0m05.36s  || +0m00.17s | +3.35%
0m05.45s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate                      | 0m05.37s  || +0m00.08s | +1.48%
0m05.41s  | Compilers/Z/HexNotationConstants                                        | 0m05.40s  || +0m00.00s | +0.18%
0m04.77s  | Experiments/NewPipeline/RewriterWf1                                     | 0m04.78s  || -0m00.01s | -0.20%
0m04.69s  | Specific/Framework/ArithmeticSynthesis/Montgomery                       | 0m04.58s  || +0m00.11s | +2.40%
0m04.64s  | Arithmetic/BarrettReduction/HAC                                         | 0m04.53s  || +0m00.10s | +2.42%
0m04.50s  | Compilers/Z/Bounds/Pipeline/Definition                                  | 0m04.61s  || -0m00.11s | -2.38%
0m04.36s  | Compilers/Z/BinaryNotationConstants                                     | 0m04.34s  || +0m00.02s | +0.46%
0m04.06s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs        | 0m04.06s  || +0m00.00s | +0.00%
0m03.94s  | Experiments/NewPipeline/MiscCompilerPassesProofs                        | 0m03.94s  || +0m00.00s | +0.00%
0m03.90s  | Arithmetic/MontgomeryReduction/WordByWord/Proofs                        | 0m03.78s  || +0m00.12s | +3.17%
0m03.90s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml            | 0m03.88s  || +0m00.02s | +0.51%
0m03.76s  | p256_32.c                                                               | 0m03.81s  || -0m00.05s | -1.31%
0m03.76s  | secp256k1_32.c                                                          | 0m03.86s  || -0m00.10s | -2.59%
0m03.68s  | LegacyArithmetic/Double/Proofs/ShiftRight                               | 0m03.60s  || +0m00.08s | +2.22%
0m03.67s  | Util/ZUtil/LandLorShiftBounds                                           | 0m03.60s  || +0m00.06s | +1.94%
0m03.57s  | Util/ZUtil/Shift                                                        | 0m03.53s  || +0m00.04s | +1.13%
0m03.50s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy                     | 0m03.45s  || +0m00.04s | +1.44%
0m03.49s  | Compilers/Z/ArithmeticSimplifier                                        | 0m03.48s  || +0m00.01s | +0.28%
0m03.32s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs          | 0m03.30s  || +0m00.02s | +0.60%
0m03.31s  | LegacyArithmetic/InterfaceProofs                                        | 0m03.28s  || +0m00.03s | +0.91%
0m03.27s  | Specific/NISTP256/AMD128/Synthesis                                      | 0m03.30s  || -0m00.02s | -0.90%
0m03.18s  | Util/ZUtil/Div                                                          | 0m03.19s  || -0m00.00s | -0.31%
0m03.06s  | LegacyArithmetic/Double/Proofs/Decode                                   | 0m03.11s  || -0m00.04s | -1.60%
0m03.06s  | LegacyArithmetic/Double/Proofs/ShiftLeft                                | 0m03.04s  || +0m00.02s | +0.65%
0m02.96s  | Util/WordUtil                                                           | 0m02.98s  || -0m00.02s | -0.67%
0m02.86s  | LegacyArithmetic/ZBoundedZ                                              | 0m02.86s  || +0m00.00s | +0.00%
0m02.60s  | LegacyArithmetic/BarretReduction                                        | 0m02.66s  || -0m00.06s | -2.25%
0m02.54s  | Arithmetic/Saturated/Freeze                                             | 0m02.60s  || -0m00.06s | -2.30%
0m02.50s  | Arithmetic/ModularArithmeticTheorems                                    | 0m02.48s  || +0m00.02s | +0.80%
0m02.34s  | Specific/NISTP256/FancyMachine256/Montgomery                            | 0m02.34s  || +0m00.00s | +0.00%
0m02.33s  | Specific/NISTP256/FancyMachine256/Core                                  | 0m02.33s  || +0m00.00s | +0.00%
0m02.26s  | Specific/NISTP256/FancyMachine256/Barrett                               | 0m02.29s  || -0m00.03s | -1.31%
0m02.25s  | Compilers/Z/RewriteAddToAdcInterp                                       | 0m02.09s  || +0m00.16s | +7.65%
0m02.19s  | Compilers/Z/Bounds/Relax                                                | 0m02.20s  || -0m00.01s | -0.45%
0m02.17s  | curve25519_32.c                                                         | 0m02.16s  || +0m00.00s | +0.46%
0m02.13s  | Util/ZUtil/Quot                                                         | 0m02.13s  || +0m00.00s | +0.00%
0m02.12s  | Specific/Framework/ArithmeticSynthesis/Defaults                         | 0m02.19s  || -0m00.06s | -3.19%
0m02.12s  | Util/ZRange/SplitBounds                                                 | 0m02.06s  || +0m00.06s | +2.91%
0m02.11s  | p224_32.c                                                               | 0m02.10s  || +0m00.00s | +0.47%
0m01.90s  | Compilers/Z/JavaNotations                                               | 0m01.90s  || +0m00.00s | +0.00%
0m01.89s  | Util/ZUtil/AddGetCarry                                                  | 0m01.90s  || -0m00.01s | -0.52%
0m01.78s  | Specific/Framework/ReificationTypes                                     | 0m01.70s  || +0m00.08s | +4.70%
0m01.76s  | LegacyArithmetic/MontgomeryReduction                                    | 0m01.76s  || +0m00.00s | +0.00%
0m01.73s  | Util/ZUtil/Pow2Mod                                                      | 0m01.68s  || +0m00.05s | +2.97%
0m01.65s  | Arithmetic/CoreUnfolder                                                 | 0m01.67s  || -0m00.02s | -1.19%
0m01.55s  | p224_64.c                                                               | 0m01.69s  || -0m00.13s | -8.28%
0m01.54s  | Specific/Framework/OutputType                                           | 0m01.48s  || +0m00.06s | +4.05%
0m01.54s  | Util/ZUtil/Ones                                                         | 0m01.42s  || +0m00.12s | +8.45%
0m01.52s  | p256_64.c                                                               | 0m01.64s  || -0m00.11s | -7.31%
0m01.50s  | secp256k1_64.c                                                          | 0m01.63s  || -0m00.12s | -7.97%
0m01.48s  | Specific/Framework/ArithmeticSynthesis/Base                             | 0m01.53s  || -0m00.05s | -3.26%
0m01.44s  | Arithmetic/BarrettReduction/Wikipedia                                   | 0m01.39s  || +0m00.05s | +3.59%
0m01.43s  | Experiments/NewPipeline/CLI                                             | 0m01.42s  || +0m00.01s | +0.70%
0m01.43s  | LegacyArithmetic/Double/Proofs/BitwiseOr                                | 0m01.39s  || +0m00.04s | +2.87%
0m01.37s  | curve25519_64.c                                                         | 0m01.38s  || -0m00.00s | -0.72%
0m01.36s  | Util/QUtil                                                              | 0m01.36s  || +0m00.00s | +0.00%
0m01.34s  | Arithmetic/PrimeFieldTheorems                                           | 0m01.24s  || +0m00.10s | +8.06%
0m01.34s  | Specific/Framework/ArithmeticSynthesis/Karatsuba                        | 0m01.37s  || -0m00.03s | -2.18%
0m01.31s  | Util/ZUtil/Testbit                                                      | 0m01.24s  || +0m00.07s | +5.64%
0m01.30s  | Util/ZRange/BasicLemmas                                                 | 0m01.23s  || +0m00.07s | +5.69%
0m01.26s  | Experiments/NewPipeline/StandaloneOCamlMain                             | 0m01.26s  || +0m00.00s | +0.00%
0m01.25s  | Compilers/Z/Syntax/Util                                                 | 0m01.17s  || +0m00.08s | +6.83%
0m01.23s  | Experiments/NewPipeline/StandaloneHaskellMain                           | 0m01.23s  || +0m00.00s | +0.00%
0m01.19s  | Experiments/NewPipeline/Language                                        | 0m01.14s  || +0m00.05s | +4.38%
0m01.18s  | LegacyArithmetic/Double/Proofs/LoadImmediate                            | 0m01.12s  || +0m00.05s | +5.35%
0m01.14s  | Arithmetic/Saturated/CoreUnfolder                                       | 0m01.16s  || -0m00.02s | -1.72%
0m01.08s  | Compilers/Z/RewriteAddToAdcWf                                           | 0m01.09s  || -0m00.01s | -0.91%
0m01.07s  | Experiments/NewPipeline/CompilersTestCases                              | 0m01.02s  || +0m00.05s | +4.90%
0m01.05s  | Experiments/NewPipeline/AbstractInterpretation                          | 0m01.05s  || +0m00.00s | +0.00%
0m01.01s  | Util/ZUtil/Stabilization                                                | 0m00.94s  || +0m00.07s | +7.44%
0m00.99s  | Experiments/NewPipeline/RewriterProofs                                  | 0m00.89s  || +0m00.09s | +11.23%
0m00.98s  | Util/ZUtil/Modulo/PullPush                                              | 0m00.95s  || +0m00.03s | +3.15%
0m00.97s  | Arithmetic/Saturated/WrappersUnfolder                                   | 0m01.01s  || -0m00.04s | -3.96%
0m00.94s  | Compilers/Z/CommonSubexpressionElimination                              | 0m00.95s  || -0m00.01s | -1.05%
0m00.94s  | Specific/Framework/SynthesisFramework                                   | 0m01.07s  || -0m00.13s | -12.14%
0m00.90s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                           | 0m00.93s  || -0m00.03s | -3.22%
0m00.88s  | Arithmetic/Saturated/UniformWeight                                      | 0m01.02s  || -0m00.14s | -13.72%
0m00.88s  | Specific/Framework/ArithmeticSynthesis/Freeze                           | 0m00.84s  || +0m00.04s | +4.76%
0m00.87s  | Specific/Framework/MontgomeryReificationTypesPackage                    | 0m00.79s  || +0m00.07s | +10.12%
0m00.85s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage                | 0m00.72s  || +0m00.13s | +18.05%
0m00.84s  | Specific/Framework/IntegrationTestDisplayCommon                         | 0m01.00s  || -0m00.16s | -16.00%
0m00.84s  | Util/NumTheoryUtil                                                      | 0m00.87s  || -0m00.03s | -3.44%
0m00.80s  | Arithmetic/MontgomeryReduction/WordByWord/Definition                    | 0m00.74s  || +0m00.06s | +8.10%
0m00.80s  | Arithmetic/Saturated/MulSplitUnfolder                                   | 0m00.94s  || -0m00.13s | -14.89%
0m00.78s  | Specific/Framework/MontgomeryReificationTypes                           | 0m00.72s  || +0m00.06s | +8.33%
0m00.78s  | Util/ZUtil/Log2                                                         | 0m00.80s  || -0m00.02s | -2.50%
0m00.77s  | Util/ZUtil/Divide                                                       | 0m00.76s  || +0m00.01s | +1.31%
0m00.77s  | Util/ZUtil/ZSimplify/Simple                                             | 0m00.80s  || -0m00.03s | -3.75%
0m00.76s  | Specific/Framework/ArithmeticSynthesis/HelperTactics                    | 0m00.72s  || +0m00.04s | +5.55%
0m00.76s  | Util/ZUtil/EquivModulo                                                  | 0m00.77s  || -0m00.01s | -1.29%
0m00.74s  | Experiments/NewPipeline/MiscCompilerPasses                              | 0m00.74s  || +0m00.00s | +0.00%
0m00.74s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage                  | 0m00.71s  || +0m00.03s | +4.22%
0m00.74s  | Specific/Framework/ArithmeticSynthesis/FreezePackage                    | 0m00.72s  || +0m00.02s | +2.77%
0m00.74s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage                 | 0m00.68s  || +0m00.05s | +8.82%
0m00.74s  | Util/ZUtil/CC                                                           | 0m00.78s  || -0m00.04s | -5.12%
0m00.73s  | Arithmetic/Saturated/FreezeUnfolder                                     | 0m00.77s  || -0m00.04s | -5.19%
0m00.72s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage                | 0m00.66s  || +0m00.05s | +9.09%
0m00.71s  | Arithmetic/Saturated/Wrappers                                           | 0m00.75s  || -0m00.04s | -5.33%
0m00.70s  | Specific/Framework/ArithmeticSynthesis/BasePackage                      | 0m00.76s  || -0m00.06s | -7.89%
0m00.70s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul                    | 0m00.73s  || -0m00.03s | -4.10%
0m00.68s  | Util/ZUtil/Rshi                                                         | 0m00.72s  || -0m00.03s | -5.55%
0m00.67s  | Specific/Framework/ReificationTypesPackage                              | 0m00.72s  || -0m00.04s | -6.94%
0m00.65s  | Arithmetic/Saturated/UniformWeightInstances                             | 0m00.69s  || -0m00.03s | -5.79%
0m00.65s  | LegacyArithmetic/Double/Proofs/SelectConditional                        | 0m00.65s  || +0m00.00s | +0.00%
0m00.64s  | Specific/Framework/ArithmeticSynthesis/Ladderstep                       | 0m00.75s  || -0m00.10s | -14.66%
0m00.63s  | Compilers/Z/Named/RewriteAddToAdc                                       | 0m00.60s  || +0m00.03s | +5.00%
0m00.61s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                              | 0m00.58s  || +0m00.03s | +5.17%
0m00.61s  | Compilers/Z/Bounds/Pipeline                                             | 0m00.68s  || -0m00.07s | -10.29%
0m00.60s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics                         | 0m00.92s  || -0m00.32s | -34.78%
0m00.57s  | Compilers/Z/ArithmeticSimplifierUtil                                    | 0m00.46s  || +0m00.10s | +23.91%
0m00.57s  | Compilers/Z/Reify                                                       | 0m00.59s  || -0m00.02s | -3.38%
0m00.56s  | Compilers/Z/CommonSubexpressionEliminationWf                            | 0m00.52s  || +0m00.04s | +7.69%
0m00.56s  | Compilers/Z/MapCastByDeBruijnInterp                                     | 0m00.53s  || +0m00.03s | +5.66%
0m00.54s  | Compilers/Z/Bounds/Pipeline/Glue                                        | 0m00.59s  || -0m00.04s | -8.47%
0m00.54s  | Compilers/Z/Bounds/RoundUpLemmas                                        | 0m00.55s  || -0m00.01s | -1.81%
0m00.54s  | Compilers/Z/InlineConstAndOpInterp                                      | 0m00.54s  || +0m00.00s | +0.00%
0m00.54s  | LegacyArithmetic/Double/Core                                            | 0m00.60s  || -0m00.05s | -9.99%
0m00.53s  | Util/NUtil                                                              | 0m00.52s  || +0m00.01s | +1.92%
0m00.52s  | Arithmetic/ModularArithmeticPre                                         | 0m00.52s  || +0m00.00s | +0.00%
0m00.52s  | Compilers/Z/CommonSubexpressionEliminationInterp                        | 0m00.52s  || +0m00.00s | +0.00%
0m00.52s  | Compilers/Z/MapCastByDeBruijn                                           | 0m00.46s  || +0m00.06s | +13.04%
0m00.52s  | Compilers/Z/RewriteAddToAdc                                             | 0m00.50s  || +0m00.02s | +4.00%
0m00.51s  | LegacyArithmetic/ArchitectureToZLike                                    | 0m00.54s  || -0m00.03s | -5.55%
0m00.50s  | Compilers/Z/Bounds/Interpretation                                       | 0m00.50s  || +0m00.00s | +0.00%
0m00.50s  | Compilers/Z/Bounds/MapCastByDeBruijn                                    | 0m00.49s  || +0m00.01s | +2.04%
0m00.50s  | Compilers/ZExtended/MapBaseType                                         | 0m00.48s  || +0m00.02s | +4.16%
0m00.49s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                                  | 0m00.50s  || -0m00.01s | -2.00%
0m00.49s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic                     | 0m00.49s  || +0m00.00s | +0.00%
0m00.49s  | Specific/Framework/IntegrationTestDisplayCommonTactics                  | 0m00.46s  || +0m00.02s | +6.52%
0m00.48s  | Compilers/Z/InlineConstAndOpByRewriteInterp                             | 0m00.48s  || +0m00.00s | +0.00%
0m00.48s  | Spec/EdDSA                                                              | 0m00.70s  || -0m00.21s | -31.42%
0m00.47s  | Compilers/Z/GeneralizeVarWf                                             | 0m00.48s  || -0m00.01s | -2.08%
0m00.47s  | Compilers/Z/Inline                                                      | 0m00.44s  || +0m00.02s | +6.81%
0m00.47s  | Compilers/Z/InlineConstAndOpByRewriteWf                                 | 0m00.43s  || +0m00.03s | +9.30%
0m00.47s  | Compilers/Z/InlineConstAndOpWf                                          | 0m00.48s  || -0m00.01s | -2.08%
0m00.47s  | Compilers/Z/InlineInterp                                                | 0m00.45s  || +0m00.01s | +4.44%
0m00.47s  | Compilers/Z/Syntax                                                      | 0m00.54s  || -0m00.07s | -12.96%
0m00.45s  | Compilers/Z/InlineConstAndOpByRewrite                                   | 0m00.42s  || +0m00.03s | +7.14%
0m00.45s  | Compilers/Z/InlineWf                                                    | 0m00.42s  || +0m00.03s | +7.14%
0m00.45s  | Compilers/Z/InterpSideConditions                                        | 0m00.46s  || -0m00.01s | -2.17%
0m00.45s  | Compilers/Z/Named/DeadCodeEliminationInterp                             | 0m00.49s  || -0m00.03s | -8.16%
0m00.45s  | Compilers/ZExtended/Syntax                                              | 0m00.41s  || +0m00.04s | +9.75%
0m00.45s  | Util/ZUtil                                                              | 0m00.42s  || +0m00.03s | +7.14%
0m00.44s  | Compilers/Z/InlineConstAndOp                                            | 0m00.44s  || +0m00.00s | +0.00%
0m00.44s  | Compilers/Z/MapCastByDeBruijnWf                                         | 0m00.46s  || -0m00.02s | -4.34%
0m00.43s  | Compilers/Z/FoldTypes                                                   | 0m00.46s  || -0m00.03s | -6.52%
0m00.42s  | Compilers/Z/GeneralizeVarInterp                                         | 0m00.44s  || -0m00.02s | -4.54%
0m00.41s  | Experiments/NewPipeline/UnderLets                                       | 0m00.51s  || -0m00.10s | -19.60%
0m00.40s  | Util/ZRange/Operations                                                  | 0m00.44s  || -0m00.03s | -9.09%
0m00.40s  | Util/ZUtil/CPS                                                          | 0m00.42s  || -0m00.01s | -4.76%
0m00.39s  | Compilers/ZExtended/Syntax/Util                                         | 0m00.36s  || +0m00.03s | +8.33%
0m00.38s  | Compilers/Z/Bounds/Pipeline/OutputType                                  | 0m00.40s  || -0m00.02s | -5.00%
0m00.38s  | Compilers/Z/GeneralizeVar                                               | 0m00.35s  || +0m00.03s | +8.57%
0m00.38s  | Compilers/Z/Named/DeadCodeElimination                                   | 0m00.44s  || -0m00.06s | -13.63%
0m00.38s  | Compilers/ZExtended/InlineConstAndOpInterp                              | 0m00.32s  || +0m00.06s | +18.75%
0m00.36s  | Util/ZUtil/MulSplit                                                     | 0m00.30s  || +0m00.06s | +20.00%
0m00.36s  | Util/ZUtil/ZSimplify/Core                                               | 0m00.35s  || +0m00.01s | +2.85%
0m00.35s  | Compilers/ZExtended/InlineConstAndOpByRewriteInterp                     | 0m00.32s  || +0m00.02s | +9.37%
0m00.35s  | Compilers/ZExtended/InlineConstAndOpByRewriteWf                         | 0m00.34s  || +0m00.00s | +2.94%
0m00.34s  | Arithmetic/MontgomeryReduction/Definition                               | 0m00.38s  || -0m00.03s | -10.52%
0m00.34s  | Compilers/ZExtended/InlineConstAndOpWf                                  | 0m00.33s  || +0m00.01s | +3.03%
0m00.34s  | Util/ZUtil/Tactics/Ztestbit                                             | 0m00.41s  || -0m00.06s | -17.07%
0m00.33s  | Compilers/ZExtended/InlineConstAndOpByRewrite                           | 0m00.33s  || +0m00.00s | +0.00%
0m00.33s  | Spec/ModularArithmetic                                                  | 0m00.35s  || -0m00.01s | -5.71%
0m00.32s  | Compilers/Z/OpInversion                                                 | 0m00.34s  || -0m00.02s | -5.88%
0m00.32s  | Compilers/Z/TypeInversion                                               | 0m00.34s  || -0m00.02s | -5.88%
0m00.32s  | Compilers/ZExtended/InlineConstAndOp                                    | 0m00.33s  || -0m00.01s | -3.03%
0m00.32s  | Util/ZUtil/Tactics                                                      | 0m00.29s  || +0m00.03s | +10.34%
0m00.32s  | Util/ZUtil/Tactics/SimplifyFractionsLe                                  | 0m00.34s  || -0m00.02s | -5.88%
0m00.32s  | Util/ZUtil/Tactics/ZeroBounds                                           | 0m00.33s  || -0m00.01s | -3.03%
0m00.31s  | Util/ZUtil/Hints                                                        | 0m00.32s  || -0m00.01s | -3.12%
0m00.31s  | Util/ZUtil/Tactics/PullPush/Modulo                                      | 0m00.32s  || -0m00.01s | -3.12%
0m00.30s  | Util/ZUtil/ZSimplify                                                    | 0m00.28s  || +0m00.01s | +7.14%
0m00.30s  | Util/ZUtil/Zselect                                                      | 0m00.27s  || +0m00.02s | +11.11%
0m00.29s  | Util/ZUtil/Land                                                         | 0m00.30s  || -0m00.01s | -3.33%
0m00.29s  | Util/ZUtil/Tactics/PullPush                                             | 0m00.28s  || +0m00.00s | +3.57%
0m00.28s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition           | 0m00.24s  || +0m00.04s | +16.66%
0m00.28s  | Util/ZUtil/Definitions                                                  | 0m00.30s  || -0m00.01s | -6.66%
0m00.28s  | Util/ZUtil/Tactics/LinearSubstitute                                     | 0m00.34s  || -0m00.06s | -17.64%
0m00.27s  | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition | 0m00.28s  || -0m00.01s | -3.57%
0m00.27s  | Util/ZUtil/AddModulo                                                    | 0m00.26s  || +0m00.01s | +3.84%
0m00.27s  | Util/ZUtil/Opp                                                          | 0m00.32s  || -0m00.04s | -15.62%

11 files changed, 469 insertions, 57 deletions

diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index 6cfdaaff8..4bdcb19ef 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -71,6 +71,9 @@ Module ZRange.
           | progress specialize_by omega
           | progress destruct_head'_or ].
 
+  Lemma is_tighter_than_bool_extend_land_lor_bounds r : is_tighter_than_bool r (extend_land_lor_bounds r) = true.
+  Proof. repeat t2_step. Qed.
+
   Lemma is_bounded_by_iff_is_tighter_than r1 r2
     : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true)
       <-> (is_tighter_than_bool r1 r2 = true \/ goodb r1 = false).
@@ -92,6 +95,10 @@ Module ZRange.
     rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; etransitivity; destruct_head'_and; eassumption.
   Qed.
 
+  Lemma is_bounded_by_of_is_tighter_than r1 r2 (H : is_tighter_than_bool r1 r2 = true)
+    : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true).
+  Proof. apply is_bounded_by_iff_is_tighter_than; auto. Qed.
+
   Lemma is_bounded_by_bool_Proper_if_sumbool_union_dep {A B} (b : sumbool A B) x y rx ry
     : (A -> is_bounded_by_bool x rx = true)
       -> (B -> is_bounded_by_bool y ry = true)
diff --git a/src/Util/ZRange/LandLorBounds.v b/src/Util/ZRange/LandLorBounds.v
new file mode 100644
index 000000000..dd538d967
--- /dev/null
+++ b/src/Util/ZRange/LandLorBounds.v
@@ -0,0 +1,159 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.LandLorBounds.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.ZRange.BasicLemmas.
+Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+Local Open Scope bool_scope.
+Local Open Scope Z_scope.
+
+Module ZRange.
+  Import Operations.ZRange.
+  Import CornersMonotoneBounds.ZRange.
+
+  Lemma is_bounded_by_bool_lor_land_bound_helper
+        f (Hf : f = Z.lor \/ f = Z.land)
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+    : is_tighter_than_bool
+        (constant (f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y)))
+        (four_corners_and_zero (fun x y => f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y)) x_bs y_bs)
+      = true.
+  Proof.
+    apply monotoneb_four_corners_and_zero_gen with (x:=x) (y:=y);
+      destruct_head'_or; subst f; eauto with typeclass_instances zarith core.
+  Qed.
+
+  Local Existing Instances Z.land_round_Proper_pos_r
+        Z.land_round_Proper_pos_l
+        Z.lor_round_Proper_pos_r
+        Z.lor_round_Proper_pos_l
+        Z.land_round_Proper_neg_r
+        Z.land_round_Proper_neg_l
+        Z.lor_round_Proper_neg_r
+        Z.lor_round_Proper_neg_l.
+
+  Lemma is_bounded_by_bool_land_lor_bounds_helper
+        f (Hf : f = Z.lor \/ f = Z.land)
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+    : is_bounded_by_bool (f x y) (land_lor_bounds f x_bs y_bs) = true.
+  Proof.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs)) as H.
+    pose proof (fun pf1 pf2 => is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs) pf2 pf1) as H0x.
+    pose proof (fun pf1 pf2 => is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs) pf2 pf1) as Hm1x.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as H0y.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as Hm1y.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as H00.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as Hm10.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as H0m1.
+    pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as Hm1m1.
+    specialize_by (eapply ZRange.is_bounded_by_of_is_tighter_than; try eapply ZRange.is_tighter_than_bool_extend_land_lor_bounds; eassumption || reflexivity).
+    revert H H0x Hm1x H0y Hm1y H00 Hm1m1 H0m1 Hm10.
+    cbv [land_lor_bounds constant is_tighter_than_bool is_bounded_by_bool is_true] in *; cbn [lower upper] in *.
+    rewrite !Bool.andb_true_iff, !Z.leb_le in *.
+    cbv [extend_land_lor_bounds].
+    cbn [lower upper] in *.
+    destruct (Z.round_lor_land_bound_bounds x) as [Hx|Hx], (Z.round_lor_land_bound_bounds y) as [Hy|Hy].
+    all: repeat apply Z.min_case_strong; repeat apply Z.max_case_strong.
+    all: try (intros; exfalso; clear dependent f; lia).
+    all: destruct x as [|x|x], y as [|y|y]; try (intros; exfalso; clear dependent f; lia).
+    all: change (Z.round_lor_land_bound 0) with 0 in *.
+    all: change (Z.round_lor_land_bound (-1)) with (-1) in *.
+    all: intros.
+    all: repeat match goal with
+                | _ => assumption
+                | [ H : ?T, H' : ?T |- _ ] => clear H'
+                | [ H : 0 <= 0 <= 0 |- _ ] => clear H
+                | [ H : 0 <= -1 <= _ -> _ |- _ ] => clear H
+                | [ H : 0 <= -1 -> _ |- _ ] => clear H
+                | [ H : ?x <= ?x <= _ -> _ |- _ ] => specialize (fun pf => H (conj (@Z.le_refl x) pf))
+                | [ H : _ <= ?x <= ?x -> _ |- _ ] => specialize (fun pf => H (conj pf (@Z.le_refl x)))
+                | [ H : ?T, H' : ?T /\ _ -> _ |- _ ] => specialize (fun pf => H' (conj H pf))
+                | [ H : ?T, H' : _ /\ ?T -> _ |- _ ] => specialize (fun pf => H' (conj pf H))
+                | _ => progress specialize_by_assumption
+                | _ => progress specialize_by (destruct_head'_and; assumption)
+                | [ H : _ <= Z.pos _ <= ?x |- _ ] => unique assert (0 <= x) by (clear -H; lia)
+                | [ H : ?x <= Z.neg _ <= _ |- _ ] => unique assert (x <= -1) by (clear -H; lia)
+                | [ H : ?a <= _ <= ?c, H' : ?c <= ?d, H'' : ?a <= ?d -> _ |- _ ]
+                  => unique assert (a <= d) by (clear -H H'; lia)
+                | [ H : ?a <= ?b -> ?c <= ?d <= ?e -> _ |- _ ] => specialize (fun pf1 pf2 => H pf2 pf1)
+                end.
+    all: destruct Hf; subst f.
+    all: split.
+    all: destruct_head'_and.
+    all: split_and.
+    all: repeat lazymatch goal with
+                | [ |- Z.land _ (Z.pos ?x) <= _ ]
+                  => is_var x; etransitivity; [ apply Z.land_round_bound_pos_r' | ]
+                | [ |- Z.land (Z.pos ?x) _ <= _ ]
+                  => is_var x; etransitivity; [ apply Z.land_round_bound_pos_l' | ]
+                | [ |- _ <= Z.land _ (Z.pos ?x) ]
+                  => is_var x; etransitivity; [ | apply Z.land_round_bound_pos_r ]
+                | [ |- _ <= Z.land (Z.pos ?x) _ ]
+                  => is_var x; etransitivity; [ | apply Z.land_round_bound_pos_l ]
+                | [ |- Z.land _ (Z.neg ?x) <= _ ]
+                  => is_var x; etransitivity; [ apply Z.land_round_bound_neg_r | ]
+                | [ |- Z.land (Z.neg ?x) _ <= _ ]
+                  => is_var x; etransitivity; [ apply Z.land_round_bound_neg_l | ]
+                | [ |- _ <= Z.land _ (Z.neg ?x) ]
+                  => is_var x; etransitivity; [ | apply Z.land_round_bound_neg_r' ]
+                | [ |- _ <= Z.land (Z.neg ?x) _ ]
+                  => is_var x; etransitivity; [ | apply Z.land_round_bound_neg_l' ]
+                | [ |- Z.lor _ (Z.pos ?x) <= _ ]
+                  => is_var x; etransitivity; [ apply Z.lor_round_bound_pos_r' | ]
+                | [ |- Z.lor (Z.pos ?x) _ <= _ ]
+                  => is_var x; etransitivity; [ apply Z.lor_round_bound_pos_l' | ]
+                | [ |- _ <= Z.lor _ (Z.pos ?x) ]
+                  => is_var x; etransitivity; [ | apply Z.lor_round_bound_pos_r ]
+                | [ |- _ <= Z.lor (Z.pos ?x) _ ]
+                  => is_var x; etransitivity; [ | apply Z.lor_round_bound_pos_l ]
+                | [ |- Z.lor _ (Z.neg ?x) <= _ ]
+                  => is_var x; etransitivity; [ apply Z.lor_round_bound_neg_r | ]
+                | [ |- Z.lor (Z.neg ?x) _ <= _ ]
+                  => is_var x; etransitivity; [ apply Z.lor_round_bound_neg_l | ]
+                | [ |- _ <= Z.lor _ (Z.neg ?x) ]
+                  => is_var x; etransitivity; [ | apply Z.lor_round_bound_neg_r' ]
+                | [ |- _ <= Z.lor (Z.neg ?x) _ ]
+                  => is_var x; etransitivity; [ | apply Z.lor_round_bound_neg_l' ]
+                | [ |- Z.pos ?x <= _ ]
+                  => is_var x; etransitivity; [ eassumption | ]
+                | [ |- _ <= Z.neg ?x ]
+                  => is_var x; etransitivity; [ | eassumption ]
+                | [ |- _ <= Z.pos ?x ]
+                  => is_var x; transitivity 0; [ assumption | lia ]
+                | [ |- Z.neg ?x <= _ ]
+                  => is_var x; transitivity (-1); [ lia | assumption ]
+                | _ => idtac
+                end.
+    all: try assumption.
+    all: try (rewrite ?Z.lor_0_l, ?Z.lor_0_r, ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_m1_l, ?Z.lor_m1_r, ?Z.land_m1_l, ?Z.land_m1_r in *; reflexivity || assumption).
+  Qed.
+
+  Lemma is_bounded_by_bool_land_bounds
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+    : is_bounded_by_bool (Z.land x y) (ZRange.land_bounds x_bs y_bs) = true.
+  Proof. apply is_bounded_by_bool_land_lor_bounds_helper; auto. Qed.
+
+  Lemma is_bounded_by_bool_lor_bounds
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+    : is_bounded_by_bool (Z.lor x y) (ZRange.lor_bounds x_bs y_bs) = true.
+  Proof. apply is_bounded_by_bool_land_lor_bounds_helper; auto. Qed.
+End ZRange.
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 130fdc0c4..c6f209e16 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -145,13 +145,13 @@ Module ZRange.
     rewrite Z.max_comm; reflexivity.
   Qed.
 
-  (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *)
-  Definition round_lor_land_bound (x : BinInt.Z) : BinInt.Z
-    := if (0 <=? x)%Z
-       then 2^(Z.log2_up (x+1))-1
-       else -2^(Z.log2_up (-x)).
+  Definition extend_land_lor_bounds (v : zrange) : zrange
+    := let (l, u) := eta v in
+       r[ Z.min 0 l ~> Z.max (-1) u ].
+
   Definition land_lor_bounds (f : BinInt.Z -> BinInt.Z -> BinInt.Z) (x y : zrange) : zrange
-    := four_corners_and_zero (fun x y => f (round_lor_land_bound x) (round_lor_land_bound y)) x y.
+    := four_corners_and_zero (fun x y => f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y))
+                             (extend_land_lor_bounds x) (extend_land_lor_bounds y).
   Definition land_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.land.
   Definition lor_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.lor.
 
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 4ef6b5403..8fe5772f5 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -85,6 +85,7 @@ Module Z.
        then mul_split_at_bitwidth (Z.log2 s) x y
        else ((x * y) mod s, (x * y) / s).
 
+  (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *)
   Definition round_lor_land_bound (x : Z) : Z
     := if (0 <=? x)%Z
        then 2^(Z.log2_up (x+1))-1
diff --git a/src/Util/ZUtil/LandLorBounds.v b/src/Util/ZUtil/LandLorBounds.v
index 1b10ecf97..78866ec7f 100644
--- a/src/Util/ZUtil/LandLorBounds.v
+++ b/src/Util/ZUtil/LandLorBounds.v
@@ -3,8 +3,17 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Pow2.
+Require Import Crypto.Util.ZUtil.Log2.
 Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
 Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Util.ZUtil.Ones.
 Require Import Crypto.Util.ZUtil.Lnot.
 Require Import Crypto.Util.ZUtil.Land.
@@ -14,10 +23,34 @@ Require Import Crypto.Util.Tactics.BreakMatch.
 Local Open Scope Z_scope.
 
 Module Z.
+  Lemma round_lor_land_bound_bounds x
+  : (0 <= x <= Z.round_lor_land_bound x) \/ (Z.round_lor_land_bound x <= x <= -1).
+  Proof.
+    cbv [Z.round_lor_land_bound]; break_innermost_match; Z.ltb_to_lt.
+    all: constructor; split; try lia; [].
+    all: Z.replace_all_neg_with_pos.
+    all: match goal with |- context[2^Z.log2_up ?x] => pose proof (Z.log2_up_le_full x) end.
+    all: lia.
+  Qed.
+  Hint Resolve round_lor_land_bound_bounds : zarith.
+
+  Lemma round_lor_land_bound_bounds_pos x
+  : (0 <= Z.pos x <= Z.round_lor_land_bound (Z.pos x)).
+  Proof. generalize (round_lor_land_bound_bounds (Z.pos x)); lia. Qed.
+  Hint Resolve round_lor_land_bound_bounds_pos : zarith.
+
+  Lemma round_lor_land_bound_bounds_neg x
+  : Z.round_lor_land_bound (Z.neg x) <= Z.neg x <= -1.
+  Proof. generalize (round_lor_land_bound_bounds (Z.neg x)); lia. Qed.
+  Hint Resolve round_lor_land_bound_bounds_neg : zarith.
+
   Local Ltac saturate :=
     repeat first [ progress cbv [Z.round_lor_land_bound Proper respectful Basics.flip] in *
-                 | progress cbn in *
+                 | progress Z.ltb_to_lt
                  | progress intros
+                 | break_innermost_match_step
+                 | lia
+                 | rewrite !Pos2Z.opp_neg
                  | match goal with
                    | [ |- context[Z.log2_up ?x] ]
                      => unique pose proof (Z.log2_up_nonneg x)
@@ -29,13 +62,18 @@ Module Z.
                      => unique assert (Z.pos x <= Z.pos y) by lia
                    | [ H : Pos.le ?x ?y |- context[Z.pos (?x+1)] ]
                      => unique assert (Z.pos (x+1) <= Z.pos (y+1)) by lia
+                   | [ H : Z.le ?x ?y |- context[?x+1] ]
+                     => unique assert (x+1 <= y+1) by lia
                    | [ H : Z.le ?x ?y |- context[2^Z.log2_up ?x] ]
                      => unique assert (2^Z.log2_up x <= 2^Z.log2_up y) by (Z.peel_le; lia)
+                   | [ H : ?a^?b <= ?a^?c |- _ ]
+                     => unique assert (a^(c-b) = a^c/a^b) by auto with zarith;
+                       unique assert (a^c mod a^b = 0) by auto with zarith
                    end ].
   Local Ltac do_rewrites_step :=
     match goal with
     | [ |- ?R ?x ?x ] => reflexivity
-    | [ |- context[Z.land (-2^_) (-2^_)] ]
+    (*| [ |- context[Z.land (-2^_) (-2^_)] ]
       => rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_lor, !Z.lor_ones_ones, !Z.lnot_ones_equiv
     | [ |- context[Z.lor (-2^_) (-2^_)] ]
       => rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_land, !Z.land_ones_ones, !Z.lnot_ones_equiv
@@ -52,8 +90,45 @@ Module Z.
     | [ |- context[Z.lor (-2^?x) (2^?y-1)] ]
       => rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive (2^y-1)), <- !Z.lnot_land, ?Z.lnot_ones_equiv, (Z.lnot_sub1 (2^y)), !Z.ones_equiv, ?Z.lnot_equiv, <- !Z.sub_1_r
     | [ |- context[-?x mod ?y] ]
-      => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod
-    | [ H : ?x <= ?x |- _ ] => clear H
+      => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod*)
+    | [ |- context[Z.land (2^?y-1) ?x] ]
+      => is_var x; rewrite (Z.land_comm (2^y-1) x)
+    | [ |- context[Z.lor (2^?y-1) ?x] ]
+      => is_var x; rewrite (Z.lor_comm (2^y-1) x)
+    | [ |- context[Z.land (-2^?y) ?x] ]
+      => is_var x; rewrite (Z.land_comm (-2^y) x)
+    | [ |- context[Z.lor (-2^?y) ?x] ]
+      => is_var x; rewrite (Z.lor_comm (-2^y) x)
+    | [ |- context[Z.land _ (2^_-1)] ]
+      => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones by auto with zarith
+    | [ |- context[Z.land ?x (-2^?y)] ]
+      => is_var x;
+        rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive x), <- !Z.lnot_lor, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r;
+        let x' := fresh in
+        remember (-x-1) as x' eqn:?; Z.linear_substitute x;
+        rename x' into x
+    | [ |- context[Z.lor ?x (-2^?y)] ]
+      => is_var x;
+        rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive x), <- !Z.lnot_land, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r;
+        let x' := fresh in
+        remember (-x-1) as x' eqn:?; Z.linear_substitute x;
+        rename x' into x
+    | [ |- Z.lor ?x (?y-1) <= Z.lor ?x (?y'-1) ]
+      => rewrite (Z.div_mod'' (Z.lor x (y-1)) y), (Z.div_mod'' (Z.lor x (y'-1)) y') by auto with zarith
+    | [ |- Z.lor ?x (?y-1) = _ ]
+      => rewrite (Z.div_mod'' (Z.lor x (y-1)) y) by auto with zarith
+    | [ |- context[?m1 - 1 + (?x - ?x mod ?m1)] ]
+      => replace (m1 - 1 + (x - x mod m1)) with ((m1 - x mod m1) + (x - 1)) by lia
+    | _ => progress rewrite ?Z.lor_pow2_div_pow2_r, ?Z.lor_pow2_div_pow2_l, ?Z.lor_pow2_mod_pow2_r, ?Z.lor_pow2_mod_pow2_l by auto with zarith
+    | _ => rewrite !Z.mul_div_eq by lia
+    | _ => progress rewrite ?(Z.add_comm 1) in *
+    | [ |- context[?x mod 2^(Z.log2_up (?x + 1))] ]
+      => rewrite (Z.mod_small x (2^Z.log2_up (x+1))) by (rewrite <- Z.le_succ_l, <- Z.add_1_r, Z.log2_up_le_pow2 by lia; lia)
+    | [ H : ?a^?b <= ?a^?c |- context[?x mod ?a^?b] ]
+      => rewrite (@Z.mod_pow_r_split x a b c) by auto with zarith;
+        (Z.div_mod_to_quot_rem; nia)
+    | _ => progress Z.peel_le
+    (*| [ H : ?x <= ?x |- _ ] => clear H
     | [ H : ?x < ?y, H' : ?y <= ?z |- _ ] => unique assert (x < z) by lia
     | [ H : ?x < ?y, H' : ?a <= ?x |- _ ] => unique assert (a < y) by lia
     | [ H : 2^?x < 2^?y |- context[2^?x mod 2^?y] ]
@@ -65,8 +140,15 @@ Module Z.
          destruct (@Z.pow2_lt_or_divides x y ltac:(lia)) as [H|H];
          [ repeat first [ rewrite (Z.mod_small (2^x) (2^y)) by lia
                         | rewrite !(@Z_mod_nz_opp_full (2^x) (2^y)) ]
-         | rewrite H ]
-    | _ => progress autorewrite with zsimplify_const
+         | rewrite H ]*)
+    | _ => progress autorewrite with zsimplify_fast in *
+    | [ |- context[-(-?x-1)] ] => replace (-(-x-1)) with (1+x) by lia
+    | [ H : 0 > -(1+?x) |- _ ] => assert (0 <= x) by (clear -H; lia); clear H
+    | [ H : 0 > -(?x+1) |- _ ] => assert (0 <= x) by (clear -H; lia); clear H
+    | [ |- ?a - ?b = ?a' - ?b' ] => apply f_equal2; try reflexivity; []
+    | [ |- -?a = -?a' ] => apply f_equal
+    | _ => rewrite <- !Z.sub_1_r
+    | _ => lia
     end.
   Local Ltac do_rewrites := repeat do_rewrites_step.
   Local Ltac fin_t :=
@@ -80,53 +162,129 @@ Module Z.
                  | lia
                  | progress Z.peel_le ].
   Local Ltac t :=
-    saturate; do_rewrites; fin_t.
+    saturate; do_rewrites.
 
   Local Instance land_round_Proper_pos_r x
-    : Proper (Pos.le ==> Z.le)
-             (fun y =>
-                Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))).
-  Proof. destruct x; t. Qed.
+    : Proper (Pos.le ==> Z.le) (fun y => Z.land x (Z.round_lor_land_bound (Z.pos y))).
+  Proof. t. Qed.
 
   Local Instance land_round_Proper_pos_l y
-    : Proper (Pos.le ==> Z.le)
-             (fun x =>
-                Z.land (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)).
-  Proof. destruct y; t. Qed.
+    : Proper (Pos.le ==> Z.le) (fun x => Z.land (Z.round_lor_land_bound (Z.pos x)) y).
+  Proof. t. Qed.
 
   Local Instance lor_round_Proper_pos_r x
-    : Proper (Pos.le ==> Z.le)
-             (fun y =>
-                Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))).
-  Proof. destruct x; t. Qed.
+    : Proper (Pos.le ==> Z.le) (fun y => Z.lor x (Z.round_lor_land_bound (Z.pos y))).
+  Proof. t. Qed.
 
   Local Instance lor_round_Proper_pos_l y
-    : Proper (Pos.le ==> Z.le)
-             (fun x =>
-                Z.lor (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)).
-  Proof. destruct y; t. Qed.
+    : Proper (Pos.le ==> Z.le) (fun x => Z.lor (Z.round_lor_land_bound (Z.pos x)) y).
+  Proof. t. Qed.
 
   Local Instance land_round_Proper_neg_r x
-    : Proper (Basics.flip Pos.le ==> Z.le)
-             (fun y =>
-                Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))).
-  Proof. destruct x; t. Qed.
+    : Proper (Basics.flip Pos.le ==> Z.le) (fun y => Z.land x (Z.round_lor_land_bound (Z.neg y))).
+  Proof. t. Qed.
 
   Local Instance land_round_Proper_neg_l y
-    : Proper (Basics.flip Pos.le ==> Z.le)
-             (fun x =>
-                Z.land (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)).
-  Proof. destruct y; t. Qed.
+    : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.land (Z.round_lor_land_bound (Z.neg x)) y).
+  Proof. t. Qed.
 
   Local Instance lor_round_Proper_neg_r x
-    : Proper (Basics.flip Pos.le ==> Z.le)
-             (fun y =>
-                Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))).
-  Proof. destruct x; t. Qed.
+    : Proper (Basics.flip Pos.le ==> Z.le) (fun y => Z.lor x (Z.round_lor_land_bound (Z.neg y))).
+  Proof. t. Qed.
 
   Local Instance lor_round_Proper_neg_l y
-    : Proper (Basics.flip Pos.le ==> Z.le)
-             (fun x =>
-                Z.lor (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)).
-  Proof. destruct y; t. Qed.
+    : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.lor (Z.round_lor_land_bound (Z.neg x)) y).
+  Proof. t. Qed.
+
+  Lemma land_round_lor_land_bound_r x
+    : Z.land x (Z.round_lor_land_bound x) = if (0 <=? x) then x else Z.round_lor_land_bound x.
+  Proof. t. Qed.
+  Hint Rewrite land_round_lor_land_bound_r : zsimplify_fast zsimplify.
+  Lemma land_round_lor_land_bound_l x
+    : Z.land (Z.round_lor_land_bound x) x = if (0 <=? x) then x else Z.round_lor_land_bound x.
+  Proof. rewrite Z.land_comm, land_round_lor_land_bound_r; reflexivity. Qed.
+  Hint Rewrite land_round_lor_land_bound_l : zsimplify_fast zsimplify.
+
+  Lemma lor_round_lor_land_bound_r x
+    : Z.lor x (Z.round_lor_land_bound x) = if (0 <=? x) then Z.round_lor_land_bound x else x.
+  Proof. t. Qed.
+  Hint Rewrite lor_round_lor_land_bound_r : zsimplify_fast zsimplify.
+  Lemma lor_round_lor_land_bound_l x
+    : Z.lor (Z.round_lor_land_bound x) x = if (0 <=? x) then Z.round_lor_land_bound x else x.
+  Proof. rewrite Z.lor_comm, lor_round_lor_land_bound_r; reflexivity. Qed.
+  Hint Rewrite lor_round_lor_land_bound_l : zsimplify_fast zsimplify.
+
+  Lemma land_round_bound_pos_r v x
+    : 0 <= Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)).
+  Proof.
+    rewrite Z.land_nonneg; split; [ lia | ].
+    replace (Z.pos x) with (Z.land (Z.pos x) (Z.round_lor_land_bound (Z.pos x))) at 1
+      by now rewrite land_round_lor_land_bound_r.
+    rewrite (Z.land_comm (Z.pos x)), Z.land_assoc.
+    apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
+  Qed.
+  Hint Resolve land_round_bound_pos_r (fun v x => proj1 (land_round_bound_pos_r v x)) (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith.
+  Lemma land_round_bound_pos_l v x
+    : 0 <= Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v.
+  Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_pos_r. Qed.
+  Hint Resolve land_round_bound_pos_l (fun v x => proj1 (land_round_bound_pos_l v x)) (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith.
+
+  Lemma land_round_bound_neg_r v x
+    : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x) <= v.
+  Proof.
+    assert (0 < 2 ^ Z.log2_up (Z.pos x)) by auto with zarith.
+    split; [ | apply Z.land_le; lia ].
+    replace (Z.round_lor_land_bound (Z.neg x)) with (Z.land (Z.neg x) (Z.round_lor_land_bound (Z.neg x)))
+      by now rewrite land_round_lor_land_bound_r.
+    rewrite !Z.land_assoc.
+    etransitivity; [ apply Z.land_le; cbn; lia | ]; lia.
+  Qed.
+  Hint Resolve land_round_bound_neg_r (fun v x => proj1 (land_round_bound_neg_r v x)) (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith.
+  Lemma land_round_bound_neg_l v x
+    : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v <= v.
+  Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_neg_r. Qed.
+  Hint Resolve land_round_bound_neg_l (fun v x => proj1 (land_round_bound_neg_l v x)) (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith.
+
+  Lemma lor_round_bound_neg_r v x
+    : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x) <= -1.
+  Proof.
+    change (-1) with (Z.pred 0); rewrite <- Z.lt_le_pred.
+    rewrite Z.lor_neg; split; [ | lia ].
+    replace (Z.neg x) with (Z.lor (Z.neg x) (Z.round_lor_land_bound (Z.neg x))) at 2
+      by now rewrite lor_round_lor_land_bound_r.
+    rewrite (Z.lor_comm (Z.neg x)), Z.lor_assoc.
+    cbn; rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive v), <- (Z.lnot_involutive (Z.neg x)), <- !Z.lnot_land, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r, !Pos2Z.opp_neg.
+    Z.peel_le.
+    apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
+  Qed.
+  Hint Resolve lor_round_bound_neg_r (fun v x => proj1 (lor_round_bound_neg_r v x)) (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith.
+  Lemma lor_round_bound_neg_l v x
+    : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v <= -1.
+  Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_neg_r. Qed.
+  Hint Resolve lor_round_bound_neg_l (fun v x => proj1 (lor_round_bound_neg_l v x)) (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith.
+
+  Lemma lor_round_bound_pos_r v x
+    : v <= Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)).
+  Proof.
+    assert (0 < 2 ^ Z.log2_up (Z.pos (x + 1))) by auto with zarith.
+    split; [ apply Z.lor_lower; lia | ].
+    replace (Z.round_lor_land_bound (Z.pos x)) with (Z.lor (Z.pos x) (Z.round_lor_land_bound (Z.pos x)))
+      by now rewrite lor_round_lor_land_bound_r.
+    rewrite !Z.lor_assoc.
+    etransitivity; [ | apply Z.lor_lower; rewrite ?Z.lor_nonneg; cbn; lia ]; lia.
+  Qed.
+  Hint Resolve lor_round_bound_pos_r (fun v x => proj1 (lor_round_bound_pos_r v x)) (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith.
+  Lemma lor_round_bound_pos_l v x
+    : v <= Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v.
+  Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_pos_r. Qed.
+  Hint Resolve lor_round_bound_pos_l (fun v x => proj1 (lor_round_bound_pos_l v x)) (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith.
+
+  Lemma land_round_bound_pos_r' v x : Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed.
+  Lemma land_round_bound_pos_l' v x : Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed.
+  Lemma land_round_bound_neg_r' v x : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x). Proof. auto with zarith. Qed.
+  Lemma land_round_bound_neg_l' v x : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v. Proof. auto with zarith. Qed.
+  Lemma lor_round_bound_neg_r' v x : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x). Proof. auto with zarith. Qed.
+  Lemma lor_round_bound_neg_l' v x : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v. Proof. auto with zarith. Qed.
+  Lemma lor_round_bound_pos_r' v x : Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed.
+  Lemma lor_round_bound_pos_l' v x : Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed.
 End Z.
diff --git a/src/Util/ZUtil/LandLorShiftBounds.v b/src/Util/ZUtil/LandLorShiftBounds.v
index e978ab6b0..a8e0b2051 100644
--- a/src/Util/ZUtil/LandLorShiftBounds.v
+++ b/src/Util/ZUtil/LandLorShiftBounds.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.Testbit.
 Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
 Require Import Crypto.Util.NUtil.WithoutReferenceToZ.
 Local Open Scope Z_scope.
 
@@ -70,7 +71,7 @@ Module Z.
   Qed.
 
   Section ZInequalities.
-    Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z.
+    Lemma land_le' : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z.
     Proof.
       intros x y H; apply Z.ldiff_le; [assumption|].
       rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc.
@@ -79,14 +80,38 @@ Module Z.
       reflexivity.
     Qed.
 
-    Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z.
+    Lemma lor_lower : forall x y, (0 <= x -> 0 <= y)%Z -> (x <= Z.lor x y)%Z.
     Proof.
-      intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
-      rewrite Z.ldiff_land.
-      apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
-      rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec;
-        [|apply Z.ge_le; assumption].
-      induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity.
+      intros x y H.
+      destruct (Z_lt_le_dec x 0).
+      { Z.replace_all_neg_with_pos.
+        replace (-x) with (Z.lnot (x - 1)) by (cbv [Z.pred Z.lnot]; lia).
+        rewrite <- (Z.lnot_involutive y).
+        rewrite <- Z.lnot_land.
+        cbv [Z.lnot].
+        rewrite <- !Z.sub_1_r.
+        Z.peel_le.
+        apply land_le'; lia. }
+      { apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
+        rewrite Z.ldiff_land.
+        apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
+        rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec;
+          [|apply Z.ge_le; assumption].
+        induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity. }
+    Qed.
+
+    Lemma land_le : forall x y, (0 <= y -> 0 <= x)%Z -> (Z.land x y <= x)%Z.
+    Proof.
+      intros x y H.
+      destruct (Z_lt_le_dec y 0), (Z_lt_le_dec x 0); auto using land_le' with lia.
+      Z.replace_all_neg_with_pos.
+      replace (-x) with (Z.lnot (x - 1)) by (cbv [Z.pred Z.lnot]; lia).
+      replace (-y) with (Z.lnot (y - 1)) by (cbv [Z.pred Z.lnot]; lia).
+      rewrite <- Z.lnot_lor.
+      cbv [Z.lnot].
+      rewrite <- !Z.sub_1_r.
+      Z.peel_le.
+      apply lor_lower; lia.
     Qed.
 
     Lemma lor_le : forall x y z,
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 567d106e3..9944c8124 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -297,6 +297,7 @@ Module Z.
     apply Z_mod_mult.
   Qed.
   Hint Rewrite mod_same_pow using zutil_arith : zsimplify.
+  Hint Resolve mod_same_pow : zarith.
 
   Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0.
   Proof.
@@ -369,4 +370,14 @@ Module Z.
     apply Z.mod_small.
     omega.
   Qed.
+
+  Lemma mod_pow_r_split x b e1 e2 : 0 <= b -> 0 <= e1 <= e2 -> x mod b^e2 = (x mod b^e1) + (b^e1) * ((x / b^e1) mod b^(e2-e1)).
+  Proof.
+    destruct (Z_zerop b).
+    { destruct (Z_zerop e1), (Z_zerop e2), (Z.eq_dec e1 e2); subst; intros; cbn; autorewrite with zsimplify_fast; lia. }
+    intros.
+    replace (b^e2) with (b^e1 * b^(e2 - e1)) by (autorewrite with pull_Zpow; f_equal; lia).
+    rewrite Z.rem_mul_r by auto with zarith.
+    reflexivity.
+  Qed.
 End Z.
diff --git a/src/Util/ZUtil/Ones.v b/src/Util/ZUtil/Ones.v
index e856f23a0..37a0d184e 100644
--- a/src/Util/ZUtil/Ones.v
+++ b/src/Util/ZUtil/Ones.v
@@ -174,4 +174,42 @@ Module Z.
                      end ].
   Qed.
   Hint Rewrite lor_ones_ones : zsimplify.
+
+  Lemma lor_pow2_mod_pow2_r x e (He : 0 <= e) : Z.lor x (2^e-1) mod (2^e) = 2^e-1.
+  Proof.
+    destruct (Z_zerop e).
+    { subst; autorewrite with zsimplify_const; reflexivity. }
+    assert (0 <= x mod 2^e < 2^e) by auto with zarith.
+    assert (0 <= x mod 2^e <= 2^e-1) by lia.
+    assert (Z.log2 (x mod 2^e) <= Z.log2 (2^e-1)) by (apply Z.log2_le_mono; lia).
+    assert (Z.log2 (x mod 2^e) < e) by (rewrite Z.sub_1_r, Z.log2_pred_pow2 in * by lia; lia).
+    rewrite <- Z.land_ones, Z.land_lor_distr_l by assumption.
+    rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones_ones, Z.min_id, Z.max_id, Bool.if_const.
+    rewrite Z.land_ones by assumption.
+    rewrite Z.lor_ones_low; auto with zarith.
+  Qed.
+  Hint Rewrite lor_pow2_mod_pow2_r using zutil_arith : zsimplify.
+  Hint Rewrite lor_pow2_mod_pow2_r using assumption : zsimplify_fast.
+
+  Lemma lor_pow2_mod_pow2_l x e (He : 0 <= e) : Z.lor (2^e-1) x mod (2^e) = 2^e-1.
+  Proof. rewrite Z.lor_comm; apply lor_pow2_mod_pow2_r; assumption. Qed.
+  Hint Rewrite lor_pow2_mod_pow2_l using zutil_arith : zsimplify.
+  Hint Rewrite lor_pow2_mod_pow2_l using assumption : zsimplify_fast.
+  
+  Lemma lor_pow2_div_pow2_r x e (He : 0 <= e) : (Z.lor x (2^e-1)) / (2^e) = x / 2^e.
+  Proof.
+    destruct (Z_zerop e).
+    { subst; autorewrite with zsimplify_const; reflexivity. }
+    assert (0 < 2^e) by auto with zarith.
+    rewrite <- Z.shiftr_div_pow2, Z.shiftr_lor, !Z.shiftr_div_pow2 by lia.
+    rewrite (Z.div_small (_-1) _), Z.lor_0_r by lia.
+    reflexivity.
+  Qed.
+  Hint Rewrite lor_pow2_div_pow2_r using zutil_arith : zsimplify.
+  Hint Rewrite lor_pow2_div_pow2_r using assumption : zsimplify_fast.
+
+  Lemma lor_pow2_div_pow2_l x e (He : 0 <= e) : (Z.lor (2^e-1) x) / (2^e) = x / 2^e.
+  Proof. rewrite Z.lor_comm; apply lor_pow2_div_pow2_r; assumption. Qed.
+  Hint Rewrite lor_pow2_div_pow2_l using zutil_arith : zsimplify.
+  Hint Rewrite lor_pow2_div_pow2_l using assumption : zsimplify_fast.
 End Z.
diff --git a/src/Util/ZUtil/Tactics/LinearSubstitute.v b/src/Util/ZUtil/Tactics/LinearSubstitute.v
index d03c9d196..960c06ce9 100644
--- a/src/Util/ZUtil/Tactics/LinearSubstitute.v
+++ b/src/Util/ZUtil/Tactics/LinearSubstitute.v
@@ -12,6 +12,8 @@ Module Z.
   Proof. omega. Qed.
   Lemma move_R_Xm x y z : y - x = z -> x = y - z.
   Proof. omega. Qed.
+  Lemma move_R_nX x y : -x = y -> x = -y.
+  Proof. omega. Qed.
   Lemma move_L_pX x y z : z = x + y -> z - y = x.
   Proof. omega. Qed.
   Lemma move_L_mX x y z : z = x - y -> z + y = x.
@@ -20,6 +22,8 @@ Module Z.
   Proof. omega. Qed.
   Lemma move_L_Xm x y z : z = y - x -> y - z = x.
   Proof. omega. Qed.
+  Lemma move_L_nX x y : y = -x -> -y = x.
+  Proof. omega. Qed.
 
   (** [linear_substitute x] attempts to maipulate equations using only
       addition and subtraction to put [x] on the left, and then
@@ -36,6 +40,8 @@ Module Z.
             | ?a - ?b
               => first [ contains for_var b; apply move_L_mX in H
                        | contains for_var a; apply move_L_Xm in H ]
+            | -?a
+              => contains for_var a; apply move_L_nX in H
             | for_var
               => progress symmetry in H
             end
@@ -46,6 +52,8 @@ Module Z.
             | ?a - ?b
               => first [ not contains for_var b; apply move_R_mX in H
                        | not contains for_var a; apply move_R_Xm in H ]
+            | -?a
+              => contains for_var a; apply move_R_nX in H
             end ].
   Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H.
   Ltac linear_solve_for for_var :=
diff --git a/src/Util/ZUtil/ZSimplify/Core.v b/src/Util/ZUtil/ZSimplify/Core.v
index c850ddef6..06bc648ff 100644
--- a/src/Util/ZUtil/ZSimplify/Core.v
+++ b/src/Util/ZUtil/ZSimplify/Core.v
@@ -1,14 +1,16 @@
 Require Import Coq.ZArith.ZArith.
 Require Export Crypto.Util.ZUtil.Hints.Core.
 
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_fast.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r : zsimplify_fast.
+Hint Rewrite Z.pow_0_l Z.pow_0_l' using assumption : zsimplify_fast.
 
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify.
-Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l using zutil_arith : zsimplify.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r : zsimplify.
+Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l Z.pow_0_l using zutil_arith : zsimplify.
 Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify.
 Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify.
 Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify.
-Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l : zsimplify_const.
+Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l Z.sub_diag : zsimplify_const.
+Hint Rewrite Z.pow_0_l Z.pow_0_l' using assumption : zsimplify_const.
 
 Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const.
 
diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v
index 94fa05e1a..b176c0b21 100644
--- a/src/Util/ZUtil/ZSimplify/Simple.v
+++ b/src/Util/ZUtil/ZSimplify/Simple.v
@@ -13,6 +13,9 @@ Module Z.
   Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1.
   Proof. apply Z.pow_1_l; lia. Qed.
   Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify.
+  Lemma pow_0_l_Zpos a : 0^Zpos a = 0.
+  Proof. apply Z.pow_0_l; lia. Qed.
+  Hint Rewrite pow_0_l_Zpos : zsimplify_fast zsimplify_const zsimplify.
 
   Lemma sub_same_minus (x y : Z) : x - (x - y) = y.
   Proof. lia. Qed.