diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-22 17:17:02 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-23 21:12:36 -0700 |
| commit | 5cab97ed8f17e294f4e7e66010147a518c45f3a6 (patch) | |
| tree | 0746d590811eb94045aa37b01965563a13ec1f4c /src/Util/ZUtil | |
| parent | a24640e12177576b4c7fcc299f19df09e6b36d81 (diff) | |
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%
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Definitions.v | 5 | ||||
| -rw-r--r-- | src/Util/ZUtil/DistrIf.v | 51 | ||||
| -rw-r--r-- | src/Util/ZUtil/Div.v | 164 | ||||
| -rw-r--r-- | src/Util/ZUtil/Divide.v | 36 | ||||
| -rw-r--r-- | src/Util/ZUtil/Hints/ZArith.v | 2 | ||||
| -rw-r--r-- | src/Util/ZUtil/Land.v | 15 | ||||
| -rw-r--r-- | src/Util/ZUtil/LandLorBounds.v | 132 | ||||
| -rw-r--r-- | src/Util/ZUtil/LandLorShiftBounds.v | 340 | ||||
| -rw-r--r-- | src/Util/ZUtil/Le.v | 49 | ||||
| -rw-r--r-- | src/Util/ZUtil/Lnot.v | 16 | ||||
| -rw-r--r-- | src/Util/ZUtil/Log2.v | 90 | ||||
| -rw-r--r-- | src/Util/ZUtil/Modulo.v | 82 | ||||
| -rw-r--r-- | src/Util/ZUtil/Morphisms.v | 10 | ||||
| -rw-r--r-- | src/Util/ZUtil/Mul.v | 8 | ||||
| -rw-r--r-- | src/Util/ZUtil/N2Z.v | 53 | ||||
| -rw-r--r-- | src/Util/ZUtil/Odd.v | 32 | ||||
| -rw-r--r-- | src/Util/ZUtil/Ones.v | 177 | ||||
| -rw-r--r-- | src/Util/ZUtil/Opp.v | 11 | ||||
| -rw-r--r-- | src/Util/ZUtil/Pow.v | 44 | ||||
| -rw-r--r-- | src/Util/ZUtil/Pow2.v | 26 | ||||
| -rw-r--r-- | src/Util/ZUtil/Pow2Mod.v | 11 | ||||
| -rw-r--r-- | src/Util/ZUtil/Shift.v | 393 | ||||
| -rw-r--r-- | src/Util/ZUtil/Stabilization.v | 5 | ||||
| -rw-r--r-- | src/Util/ZUtil/Tactics/PullPush/Modulo.v | 161 | ||||
| -rw-r--r-- | src/Util/ZUtil/Testbit.v | 40 | ||||
| -rw-r--r-- | src/Util/ZUtil/Z2Nat.v | 38 |
26 files changed, 1910 insertions, 81 deletions
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index af2d8239e..4ef6b5403 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -84,4 +84,9 @@ Module Z. := if s =? 2^Z.log2 s then mul_split_at_bitwidth (Z.log2 s) x y else ((x * y) mod s, (x * y) / s). + + Definition round_lor_land_bound (x : Z) : Z + := if (0 <=? x)%Z + then 2^(Z.log2_up (x+1))-1 + else -2^(Z.log2_up (-x)). End Z. diff --git a/src/Util/ZUtil/DistrIf.v b/src/Util/ZUtil/DistrIf.v new file mode 100644 index 000000000..0d20fc1f4 --- /dev/null +++ b/src/Util/ZUtil/DistrIf.v @@ -0,0 +1,51 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Definition opp_distr_if (b : bool) x y : -(if b then x else y) = if b then -x else -y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite opp_distr_if : push_Zopp. + Hint Rewrite <- opp_distr_if : pull_Zopp. + + Lemma mul_r_distr_if (b : bool) x y z : z * (if b then x else y) = if b then z * x else z * y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite mul_r_distr_if : push_Zmul. + Hint Rewrite <- mul_r_distr_if : pull_Zmul. + + Lemma mul_l_distr_if (b : bool) x y z : (if b then x else y) * z = if b then x * z else y * z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite mul_l_distr_if : push_Zmul. + Hint Rewrite <- mul_l_distr_if : pull_Zmul. + + Lemma add_r_distr_if (b : bool) x y z : z + (if b then x else y) = if b then z + x else z + y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite add_r_distr_if : push_Zadd. + Hint Rewrite <- add_r_distr_if : pull_Zadd. + + Lemma add_l_distr_if (b : bool) x y z : (if b then x else y) + z = if b then x + z else y + z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite add_l_distr_if : push_Zadd. + Hint Rewrite <- add_l_distr_if : pull_Zadd. + + Lemma sub_r_distr_if (b : bool) x y z : z - (if b then x else y) = if b then z - x else z - y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite sub_r_distr_if : push_Zsub. + Hint Rewrite <- sub_r_distr_if : pull_Zsub. + + Lemma sub_l_distr_if (b : bool) x y z : (if b then x else y) - z = if b then x - z else y - z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite sub_l_distr_if : push_Zsub. + Hint Rewrite <- sub_l_distr_if : pull_Zsub. + + Lemma div_r_distr_if (b : bool) x y z : z / (if b then x else y) = if b then z / x else z / y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite div_r_distr_if : push_Zdiv. + Hint Rewrite <- div_r_distr_if : pull_Zdiv. + + Lemma div_l_distr_if (b : bool) x y z : (if b then x else y) / z = if b then x / z else y / z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite div_l_distr_if : push_Zdiv. + Hint Rewrite <- div_l_distr_if : pull_Zdiv. +End Z. diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 5ae17ad1a..7012f83c0 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -2,11 +2,14 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. Require Import Coq.ZArith.Znumtheory. Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Le. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.ZArith. Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.ZUtil.Hints. Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. Module Z. @@ -262,4 +265,165 @@ Module Z. Lemma div_opp_r a b : a / (-b) = ((-a) / b). Proof. Z.div_mod_to_quot_rem; nia. Qed. Hint Resolve div_opp_r : zarith. + + Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. + Proof. + intros. + apply Z.lt_succ_r. + apply Z.div_lt_upper_bound; try omega. + Qed. + + Lemma mul_div_le x y z + (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) + (Hyz : y <= z) + : x * y / z <= x. + Proof. + transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. + apply Z_div_le; nia. + Qed. + Hint Resolve mul_div_le : zarith. + + Lemma div_mul_diff_exact a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b = c * (a / b) + (c * (a mod b)) / b. + Proof. + rewrite (Z_div_mod_eq a b) at 1 by lia. + rewrite Z.mul_add_distr_l. + replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. + rewrite Z.div_add_l by lia. + lia. + Qed. + + Lemma div_mul_diff_exact' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * (a / b) = c * a / b - (c * (a mod b)) / b. + Proof. + rewrite div_mul_diff_exact by assumption; lia. + Qed. + + Lemma div_mul_diff_exact'' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : a * c / b = (a / b) * c + (c * (a mod b)) / b. + Proof. + rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. + Qed. + + Lemma div_mul_diff_exact''' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : (a / b) * c = a * c / b - (c * (a mod b)) / b. + Proof. + rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. + Qed. + + Lemma div_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. + Proof. + rewrite div_mul_diff_exact by assumption. + ring_simplify; auto with zarith. + Qed. + + Lemma div_mul_le_le a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. + Proof. + pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. + Qed. + + Lemma div_mul_le_le_offset a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). + Proof. + pose proof (Z.div_mul_le_le a b c); lia. + Qed. + Hint Resolve div_mul_le_le_offset : zarith. + + Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. + reflexivity. + Qed. + Hint Rewrite div_x_y_x using zutil_arith : zsimplify. + + Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). + assert (Hn : -X <= a - b) by lia. + assert (Hp : a - b <= X - 1) by lia. + split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; + instantiate; autorewrite with zsimplify; try reflexivity. + Qed. + + Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) + (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. + + Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound_div a b X H0 H1). + destruct (a <? b) eqn:?; Z.ltb_to_lt. + { cut ((a - b) / X <> 0); [ lia | ]. + autorewrite with zstrip_div; auto with zarith lia. } + { autorewrite with zstrip_div; auto with zarith lia. } + Qed. + + Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0. + Proof. + rewrite !(Z.add_comm (-_)), !Z.add_opp_r. + apply Z.sub_pos_bound_div_eq. + Qed. + + Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using zutil_arith : zstrip_div. + + Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b. + Proof. intros; symmetry; apply Z.div_small; assumption. Qed. + Hint Resolve div_small_sym : zarith. + + Lemma mod_eq_le_div_1 a b : 0 < a <= b -> a mod b = 0 -> a / b = 1. + Proof. intros; Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve mod_eq_le_div_1 : zarith. + Hint Rewrite mod_eq_le_div_1 using zutil_arith : zsimplify. + + Lemma div_small_neg x y : 0 < -x <= y -> x / y = -1. + Proof. intros; Z.div_mod_to_quot_rem; nia. Qed. + Hint Rewrite div_small_neg using zutil_arith : zsimplify. + + Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y <= z -> (x - y) / z = if x <? y then -1 else 0. + Proof. + pose proof (Zlt_cases x y). + (destruct (x <? y) eqn:?); + intros; autorewrite with zsimplify; try lia. + Qed. + Hint Rewrite div_sub_small using zutil_arith : zsimplify. + + Lemma mul_div_lt_by_le x y z b : 0 <= y < z -> 0 <= x < b -> x * y / z < b. + Proof. + intros [? ?] [? ?]; eapply Z.le_lt_trans; [ | eassumption ]. + auto with zarith. + Qed. + Hint Resolve mul_div_lt_by_le : zarith. + + Definition mul_div_le' + := fun x y z w p H0 H1 H2 H3 => @Z.le_trans _ _ w (@Z.mul_div_le x y z H0 H1 H2 H3) p. + Hint Resolve mul_div_le' : zarith. + Lemma mul_div_le'' x y z w : y <= w -> 0 <= x -> 0 <= y -> 0 < z -> x <= z -> x * y / z <= w. + Proof. + rewrite (Z.mul_comm x y); intros; apply mul_div_le'; assumption. + Qed. + Hint Resolve mul_div_le'' : zarith. + + Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n. + Proof. intros; Z.div_mod_to_quot_rem_in_goal; nia. Qed. + Hint Rewrite div_between using zutil_arith : zsimplify. + + Lemma div_between_1 a b : b <> 0 -> b <= a < 2 * b -> a / b = 1. + Proof. intros; rewrite (div_between 1) by lia; reflexivity. Qed. + Hint Rewrite div_between_1 using zutil_arith : zsimplify. + + Lemma div_between_if n a b : 0 <= n -> b <> 0 -> n * b <= a < (2 + n) * b -> (a / b = if (1 + n) * b <=? a then 1 + n else n)%Z. + Proof. + intros. + break_match; Z.ltb_to_lt; + apply div_between; lia. + Qed. + + Lemma div_between_0_if a b : b <> 0 -> 0 <= a < 2 * b -> a / b = if b <=? a then 1 else 0. + Proof. intros; rewrite (div_between_if 0) by lia; autorewrite with zsimplify_const; reflexivity. Qed. End Z. diff --git a/src/Util/ZUtil/Divide.v b/src/Util/ZUtil/Divide.v new file mode 100644 index 000000000..8609db5ad --- /dev/null +++ b/src/Util/ZUtil/Divide.v @@ -0,0 +1,36 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.DivideExistsMul. +Local Open Scope Z_scope. + +Module Z. + Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), + (a | b * (a / c)) -> (c | a) -> (c | b). + Proof. + intros ? ? ? ? ? divide_a divide_c_a; do 2 Z.divide_exists_mul. + rewrite divide_c_a in divide_a. + rewrite Z.div_mul' in divide_a by auto. + replace (b * k) with (k * b) in divide_a by ring. + replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. + rewrite Z.mul_cancel_l in divide_a by (intuition auto with nia; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). + eapply Zdivide_intro; eauto. + Qed. + + Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. + Proof. + intros n; split. { + intro divide2_n. + Z.divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. + rewrite divide2_n. + apply Z.even_mul. + } { + intro n_even. + pose proof (Zmod_even n) as H. + rewrite n_even in H. + apply Zmod_divide; omega || auto. + } + Qed. +End Z. diff --git a/src/Util/ZUtil/Hints/ZArith.v b/src/Util/ZUtil/Hints/ZArith.v index 17e56f9cf..2aa70dc97 100644 --- a/src/Util/ZUtil/Hints/ZArith.v +++ b/src/Util/ZUtil/Hints/ZArith.v @@ -6,3 +6,5 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z Hint Resolve (fun n m => proj1 (Z.opp_le_mono n m)) : zarith. Hint Resolve (fun n m => proj1 (Z.pred_le_mono n m)) : zarith. Hint Resolve (fun a b => proj2 (Z.lor_nonneg a b)) : zarith. + +Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.add_le_mono Z.sub_le_mono : zarith. diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v index f46d541e9..7f27f942d 100644 --- a/src/Util/ZUtil/Land.v +++ b/src/Util/ZUtil/Land.v @@ -1,6 +1,8 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. Require Import Crypto.Util.ZUtil.Notations. -Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Definitions. +Local Open Scope bool_scope. Local Open Scope Z_scope. Module Z. Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. @@ -10,4 +12,15 @@ Module Z. case_eq (Z.testbit b n); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. Qed. + + Lemma land_m1'_l a : Z.land (-1) a = a. + Proof. apply Z.land_m1_l. Qed. + Hint Rewrite Z.land_m1_l land_m1'_l : zsimplify_const zsimplify zsimplify_fast. + + Lemma land_m1'_r a : Z.land a (-1) = a. + Proof. apply Z.land_m1_r. Qed. + Hint Rewrite Z.land_m1_r land_m1'_r : zsimplify_const zsimplify zsimplify_fast. + + Lemma sub_1_lt_le x y : (x - 1 < y) <-> (x <= y). + Proof. lia. Qed. End Z. diff --git a/src/Util/ZUtil/LandLorBounds.v b/src/Util/ZUtil/LandLorBounds.v new file mode 100644 index 000000000..1b10ecf97 --- /dev/null +++ b/src/Util/ZUtil/LandLorBounds.v @@ -0,0 +1,132 @@ +Require Import Coq.micromega.Lia. +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.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Ones. +Require Import Crypto.Util.ZUtil.Lnot. +Require Import Crypto.Util.ZUtil.Land. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Local Open Scope Z_scope. + +Module Z. + Local Ltac saturate := + repeat first [ progress cbv [Z.round_lor_land_bound Proper respectful Basics.flip] in * + | progress cbn in * + | progress intros + | match goal with + | [ |- context[Z.log2_up ?x] ] + => unique pose proof (Z.log2_up_nonneg x) + | [ |- context[2^?x] ] + => unique assert (0 <= 2^x) by (apply Z.pow_nonneg; lia) + | [ H : 0 <= ?x |- context[2^?x] ] + => unique assert (0 < 2^x) by (apply Z.pow_pos_nonneg; lia) + | [ H : Pos.le ?x ?y |- context[Z.pos ?x] ] + => 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[2^Z.log2_up ?x] ] + => unique assert (2^Z.log2_up x <= 2^Z.log2_up y) by (Z.peel_le; lia) + end ]. + Local Ltac do_rewrites_step := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ |- 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 + | [ |- context[Z.land (2^_-1) (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones_ones, !Z.ones_equiv, <- !Z.sub_1_r + | [ |- context[Z.lor (2^_-1) (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.lor_ones_ones, !Z.ones_equiv, <- !Z.sub_1_r + | [ |- context[Z.land (2^?x-1) (-2^?y)] ] + => rewrite (@Z.land_comm (2^x-1) (-2^y)) + | [ |- context[Z.lor (2^?x-1) (-2^?y)] ] + => rewrite (@Z.lor_comm (2^x-1) (-2^y)) + | [ |- context[Z.land (-2^_) (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones, ?Z.ones_equiv, <- ?Z.sub_1_r by lia + | [ |- 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 + | [ 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] ] + => repeat first [ rewrite (Z.mod_small (2^x) (2^y)) by lia + | rewrite !(@Z_mod_nz_opp_full (2^x) (2^y)) ] + | [ H : ?x < ?y, H' : context[?x mod ?y] |- _ ] => rewrite (Z.mod_small x y) in H' by lia + | [ |- context[2^?x mod 2^?y] ] + => let H := fresh in + 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 + end. + Local Ltac do_rewrites := repeat do_rewrites_step. + Local Ltac fin_t := + repeat first [ progress destruct_head'_and + | match goal with + | [ H : orb _ _ = _ |- _ ] + => progress rewrite ?Bool.orb_true_iff, ?Bool.orb_false_iff, ?Z.ltb_lt, ?Z.ltb_ge in * + end + | break_innermost_match_step + | progress destruct_head'_or + | lia + | progress Z.peel_le ]. + Local Ltac t := + saturate; do_rewrites; fin_t. + + 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. + + 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. + + 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. + + 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. + + 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. + + 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. + + 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. + + 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. +End Z. diff --git a/src/Util/ZUtil/LandLorShiftBounds.v b/src/Util/ZUtil/LandLorShiftBounds.v new file mode 100644 index 000000000..e978ab6b0 --- /dev/null +++ b/src/Util/ZUtil/LandLorShiftBounds.v @@ -0,0 +1,340 @@ +Require Import Coq.Classes.Morphisms. +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Pow. +Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Div. +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.NUtil.WithoutReferenceToZ. +Local Open Scope Z_scope. + +Module Z. + Lemma lor_range : forall x y n, 0 <= x < 2 ^ n -> 0 <= y < 2 ^ n -> + 0 <= Z.lor x y < 2 ^ n. + Proof. + intros x y n H H0; assert (0 <= n) by auto with zarith omega. + repeat match goal with + | |- _ => progress intros + | |- _ => rewrite Z.lor_spec + | |- _ => rewrite Z.testbit_eqb by auto with zarith omega + | |- _ => rewrite !Z.div_small by (split; try omega; eapply Z.lt_le_trans; + [ intuition eassumption | apply Z.pow_le_mono_r; omega]) + | |- _ => split + | |- _ => apply Z.testbit_false_bound + | |- _ => solve [auto with zarith] + | |- _ => solve [apply Z.lor_nonneg; intuition auto] + end. + Qed. + Hint Resolve lor_range : zarith. + + Lemma lor_shiftl_bounds : forall x y n m, + (0 <= n)%Z -> (0 <= m)%Z -> + (0 <= x < 2 ^ m)%Z -> + (0 <= y < 2 ^ n)%Z -> + (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z. + Proof. + intros x y n m H H0 H1 H2. + apply Z.lor_range. + { split; try omega. + apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega. + apply Z.pow_le_mono_r; omega. } + { rewrite Z.shiftl_mul_pow2 by omega. + rewrite Z.pow_add_r by omega. + split; Z.zero_bounds. + rewrite Z.mul_comm. + apply Z.mul_lt_mono_pos_l; omega. } + Qed. + + Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= a. + Proof. + intros a b H H0. + destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. + cbv [Z.land]. + rewrite <-N2Z.inj_pos, <-N2Z.inj_le. + auto using N.Pos_land_upper_bound_l. + Qed. + + Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= b. + Proof. + intros. + rewrite Z.land_comm. + auto using Z.land_upper_bound_l. + Qed. + + Section ZInequalities. + 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. + rewrite <- Z.land_0_l with (a := y); f_equal. + rewrite Z.land_comm, Z.land_lnot_diag. + reflexivity. + Qed. + + Lemma lor_lower : forall x y, (0 <= x)%Z -> (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. + Qed. + + Lemma lor_le : forall x y z, + (0 <= x)%Z + -> (x <= y)%Z + -> (y <= z)%Z + -> (Z.lor x y <= (2 ^ Z.log2_up (z+1)) - 1)%Z. + Proof. + intros x y z H H0 H1; apply Z.ldiff_le. + + - apply Z.le_add_le_sub_r. + replace 1%Z with (2 ^ 0)%Z by (cbv; reflexivity). + rewrite Z.add_0_l. + apply Z.pow_le_mono_r; [cbv; reflexivity|]. + apply Z.log2_up_nonneg. + + - destruct (Z_lt_dec 0 z). + + + assert (forall a, a - 1 = Z.pred a)%Z as HP by (intro; omega); + rewrite HP, <- Z.ones_equiv; clear HP. + apply Z.ldiff_ones_r_low; [apply Z.lor_nonneg; split; omega|]. + rewrite Z.log2_up_eqn, Z.log2_lor; try omega. + apply Z.lt_succ_r. + apply Z.max_case_strong; intros; apply Z.log2_le_mono; omega. + + + replace z with 0%Z by omega. + replace y with 0%Z by omega. + replace x with 0%Z by omega. + cbv; reflexivity. + Qed. + + Local Ltac solve_pow2 := + repeat match goal with + | [|- _ /\ _] => split + | [|- (0 < 2 ^ _)%Z] => apply Z.pow2_gt_0 + | [|- (0 <= 2 ^ _)%Z] => apply Z.pow2_ge_0 + | [|- (2 ^ _ <= 2 ^ _)%Z] => apply Z.pow_le_mono_r + | [|- (_ <= _)%Z] => omega + | [|- (_ < _)%Z] => omega + end. + + Lemma pow2_mod_range : forall a n m, + (0 <= n) -> + (n <= m) -> + (0 <= Z.pow2_mod a n < 2 ^ m). + Proof. + intros; unfold Z.pow2_mod. + rewrite Z.land_ones; [|assumption]. + split; [apply Z.mod_pos_bound, Z.pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [apply Z.mod_pos_bound, Z.pow2_gt_0; assumption|]. + apply Z.pow_le_mono; [|assumption]. + split; simpl; omega. + Qed. + + Lemma shiftr_range : forall a n m, + (0 <= n)%Z -> + (0 <= m)%Z -> + (0 <= a < 2 ^ (n + m))%Z -> + (0 <= Z.shiftr a n < 2 ^ m)%Z. + Proof. + intros a n m H0 H1 H2; destruct H2. + split; [apply Z.shiftr_nonneg; assumption|]. + rewrite Z.shiftr_div_pow2; [|assumption]. + apply Z.div_lt_upper_bound; [apply Z.pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl]. + apply Z.pow_add_r; omega. + Qed. + + + Lemma shiftr_le_mono: forall a b c d, + (0 <= a)%Z + -> (0 <= d)%Z + -> (a <= c)%Z + -> (d <= b)%Z + -> (Z.shiftr a b <= Z.shiftr c d)%Z. + Proof. + intros. + repeat rewrite Z.shiftr_div_pow2; [|omega|omega]. + etransitivity; [apply Z.div_le_compat_l | apply Z.div_le_mono]; solve_pow2. + Qed. + + Lemma shiftl_le_mono: forall a b c d, + (0 <= a)%Z + -> (0 <= b)%Z + -> (a <= c)%Z + -> (b <= d)%Z + -> (Z.shiftl a b <= Z.shiftl c d)%Z. + Proof. + intros. + repeat rewrite Z.shiftl_mul_pow2; [|omega|omega]. + etransitivity; [apply Z.mul_le_mono_nonneg_l|apply Z.mul_le_mono_nonneg_r]; solve_pow2. + Qed. + End ZInequalities. + + Lemma lor_bounds x y : 0 <= x -> 0 <= y + -> Z.max x y <= Z.lor x y <= 2^Z.log2_up (Z.max x y + 1) - 1. + Proof. + apply Z.max_case_strong; intros; split; + try solve [ eauto using lor_lower, Z.le_trans, lor_le with omega + | rewrite Z.lor_comm; eauto using lor_lower, Z.le_trans, lor_le with omega ]. + Qed. + Lemma lor_bounds_lower x y : 0 <= x -> 0 <= y + -> Z.max x y <= Z.lor x y. + Proof. intros; apply lor_bounds; assumption. Qed. + Lemma lor_bounds_upper x y : Z.lor x y <= 2^Z.log2_up (Z.max x y + 1) - 1. + Proof. + pose proof (proj2 (Z.lor_neg x y)). + destruct (Z_lt_le_dec x 0), (Z_lt_le_dec y 0); + try solve [ intros; apply lor_bounds; assumption ]; + transitivity (2^0-1); + try apply Z.sub_le_mono_r, Z.pow_le_mono_r, Z.log2_up_nonneg; + simpl; omega. + Qed. + Lemma lor_bounds_gen_lower x y l : 0 <= x -> 0 <= y -> l <= Z.max x y + -> l <= Z.lor x y. + Proof. + intros; etransitivity; + solve [ apply lor_bounds; auto + | eauto ]. + Qed. + Lemma lor_bounds_gen_upper x y u : x <= u -> y <= u + -> Z.lor x y <= 2^Z.log2_up (u + 1) - 1. + Proof. + intros; etransitivity; [ apply lor_bounds_upper | ]. + apply Z.sub_le_mono_r, Z.pow_le_mono_r, Z.log2_up_le_mono, Z.max_case_strong; + omega. + Qed. + Lemma lor_bounds_gen x y l u : 0 <= x -> 0 <= y -> l <= Z.max x y -> x <= u -> y <= u + -> l <= Z.lor x y <= 2^Z.log2_up (u + 1) - 1. + Proof. auto using lor_bounds_gen_lower, lor_bounds_gen_upper. Qed. + + Lemma shiftl_le_Proper2 y + : Proper (Z.le ==> Z.le) (fun x => Z.shiftl x y). + Proof. + unfold Basics.flip in *. + pose proof (Zle_cases 0 y) as Hx. + intros x x' H. + pose proof (Zle_cases 0 x) as Hy. + pose proof (Zle_cases 0 x') as Hy'. + destruct (0 <=? y), (0 <=? x), (0 <=? x'); + autorewrite with Zshift_to_pow; + Z.replace_all_neg_with_pos; + autorewrite with pull_Zopp; + rewrite ?Z.div_opp_l_complete; + repeat destruct (Z_zerop _); + autorewrite with zsimplify_const pull_Zopp; + auto with zarith; + repeat match goal with + | [ |- context[-?x - ?y] ] + => replace (-x - y) with (-(x + y)) by omega + | _ => rewrite <- Z.opp_le_mono + | _ => rewrite <- Z.add_le_mono_r + | _ => solve [ auto with zarith ] + | [ |- ?x <= ?y + 1 ] + => cut (x <= y); [ omega | solve [ auto with zarith ] ] + | [ |- -_ <= _ ] + => solve [ transitivity (-0); auto with zarith ] + end. + { repeat match goal with H : context[_ mod _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; nia. } + Qed. + + Lemma shiftl_le_Proper1 x + (R := fun b : bool => if b then Z.le else Basics.flip Z.le) + : Proper (R (0 <=? x) ==> Z.le) (Z.shiftl x). + Proof. + unfold Basics.flip in *. + pose proof (Zle_cases 0 x) as Hx. + intros y y' H. + pose proof (Zle_cases 0 y) as Hy. + pose proof (Zle_cases 0 y') as Hy'. + destruct (0 <=? x), (0 <=? y), (0 <=? y'); subst R; cbv beta iota in *; + autorewrite with Zshift_to_pow; + Z.replace_all_neg_with_pos; + autorewrite with pull_Zopp; + rewrite ?Z.div_opp_l_complete; + repeat destruct (Z_zerop _); + autorewrite with zsimplify_const pull_Zopp; + auto with zarith; + repeat match goal with + | [ |- context[-?x - ?y] ] + => replace (-x - y) with (-(x + y)) by omega + | _ => rewrite <- Z.opp_le_mono + | _ => rewrite <- Z.add_le_mono_r + | _ => solve [ auto with zarith ] + | [ |- ?x <= ?y + 1 ] + => cut (x <= y); [ omega | solve [ auto with zarith ] ] + | [ |- context[2^?x] ] + => lazymatch goal with + | [ H : 1 < 2^x |- _ ] => fail + | [ H : 0 < 2^x |- _ ] => fail + | [ H : 0 <= 2^x |- _ ] => fail + | _ => first [ assert (1 < 2^x) by auto with zarith + | assert (0 < 2^x) by auto with zarith + | assert (0 <= 2^x) by auto with zarith ] + end + | [ H : ?x <= ?y |- _ ] + => is_var x; is_var y; + lazymatch goal with + | [ H : 2^x <= 2^y |- _ ] => fail + | [ H : 2^x < 2^y |- _ ] => fail + | _ => assert (2^x <= 2^y) by auto with zarith + end + | [ H : ?x <= ?y, H' : ?f ?x = ?k, H'' : ?f ?y <> ?k |- _ ] + => let Hn := fresh in + assert (Hn : x <> y) by congruence; + assert (x < y) by omega; clear H Hn + | [ H : ?x <= ?y, H' : ?f ?x <> ?k, H'' : ?f ?y = ?k |- _ ] + => let Hn := fresh in + assert (Hn : x <> y) by congruence; + assert (x < y) by omega; clear H Hn + | _ => solve [ repeat match goal with H : context[_ mod _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; subst; + lazymatch goal with + | [ |- _ <= (?a * ?q + ?r) * ?q' ] + => transitivity (q * (a * q') + r * q'); + [ assert (0 < a * q') by nia; nia + | nia ] + end ] + end. + { replace y' with (y + (y' - y)) by omega. + rewrite Z.pow_add_r, <- Zdiv_Zdiv by auto with zarith. + assert (y < y') by (assert (y <> y') by congruence; omega). + assert (1 < 2^(y'-y)) by auto with zarith. + assert (0 < x / 2^y) + by (repeat match goal with H : context[_ mod _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; nia). + assert (2^y <= x) + by (repeat match goal with H : context[_ / _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; nia). + match goal with + | [ |- ?x + 1 <= ?y ] => cut (x < y); [ omega | ] + end. + auto with zarith. } + Qed. + + Lemma shiftr_le_Proper2 y + : Proper (Z.le ==> Z.le) (fun x => Z.shiftr x y). + Proof. apply shiftl_le_Proper2. Qed. + + Lemma shiftr_le_Proper1 x + (R := fun b : bool => if b then Z.le else Basics.flip Z.le) + : Proper (R (x <? 0) ==> Z.le) (Z.shiftr x). + Proof. + subst R; intros y y' H'; unfold Z.shiftr; apply shiftl_le_Proper1. + unfold Basics.flip in *. + pose proof (Zle_cases 0 x). + pose proof (Zlt_cases x 0). + destruct (0 <=? x), (x <? 0); try omega. + Qed. +End Z. diff --git a/src/Util/ZUtil/Le.v b/src/Util/ZUtil/Le.v index ab7767de7..ca180c556 100644 --- a/src/Util/ZUtil/Le.v +++ b/src/Util/ZUtil/Le.v @@ -1,9 +1,58 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Local Open Scope Z_scope. Module Z. Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. Proof. intros; omega. Qed. Hint Resolve positive_is_nonzero : zarith. + + Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. + Proof. lia. Qed. + + Lemma le_fold_right_max : forall low l x, (forall y, List.In y l -> low <= y) -> + List.In x l -> x <= List.fold_right Z.max low l. + Proof. + induction l as [|a l IHl]; intros ? lower_bound In_list; [cbv [List.In] in *; intuition | ]. + simpl. + destruct (List.in_inv In_list); subst. + + apply Z.le_max_l. + + etransitivity. + - apply IHl; auto; intuition auto with datatypes. + - apply Z.le_max_r. + Qed. + + Lemma le_fold_right_max_initial : forall low l, low <= List.fold_right Z.max low l. + Proof. + induction l as [|a l IHl]; intros; try reflexivity. + etransitivity; [ apply IHl | apply Z.le_max_r ]. + Qed. + + Lemma add_compare_mono_r: forall n m p, (n + p ?= m + p) = (n ?= m). + Proof. + intros n m p. + rewrite <-!(Z.add_comm p). + apply Z.add_compare_mono_l. + Qed. + + Lemma leb_add_same x y : (x <=? y + x) = (0 <=? y). + Proof. destruct (x <=? y + x) eqn:?, (0 <=? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite leb_add_same : zsimplify. + + Lemma ltb_add_same x y : (x <? y + x) = (0 <? y). + Proof. destruct (x <? y + x) eqn:?, (0 <? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite ltb_add_same : zsimplify. + + Lemma geb_add_same x y : (x >=? y + x) = (0 >=? y). + Proof. destruct (x >=? y + x) eqn:?, (0 >=? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite geb_add_same : zsimplify. + + Lemma gtb_add_same x y : (x >? y + x) = (0 >? y). + Proof. destruct (x >? y + x) eqn:?, (0 >? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite gtb_add_same : zsimplify. + + Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. + Proof. lia. Qed. End Z. diff --git a/src/Util/ZUtil/Lnot.v b/src/Util/ZUtil/Lnot.v new file mode 100644 index 000000000..c4c747c76 --- /dev/null +++ b/src/Util/ZUtil/Lnot.v @@ -0,0 +1,16 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma lnot_equiv n : Z.lnot n = Z.pred (-n). + Proof. reflexivity. Qed. + + Lemma lnot_sub1 n : Z.lnot (n-1) = -n. + Proof. rewrite lnot_equiv; lia. Qed. + + Lemma lnot_opp x : Z.lnot (- x) = x-1. + Proof. + rewrite <-Z.lnot_involutive, lnot_sub1; reflexivity. + Qed. +End Z. diff --git a/src/Util/ZUtil/Log2.v b/src/Util/ZUtil/Log2.v new file mode 100644 index 000000000..90c43b7fb --- /dev/null +++ b/src/Util/ZUtil/Log2.v @@ -0,0 +1,90 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Pow. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Simple. +Local Open Scope Z_scope. + +Module Z. + Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. + Proof. + intros; transitivity 0; auto with zarith. + Qed. + Hint Resolve log2_nonneg' : zarith. + + Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. + Proof. + destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. + Qed. + + Lemma log2_pred_pow2_full a : Z.log2 (Z.pred (2^a)) = Z.max 0 (Z.pred a). + Proof. + destruct (Z_dec 0 a) as [ [?|?] | ?]. + { rewrite Z.log2_pred_pow2 by assumption; lia. } + { autorewrite with zsimplify; simpl. + apply Z.max_case_strong; try omega. + + } + { subst; compute; reflexivity. } + Qed. + Hint Rewrite log2_pred_pow2_full : zsimplify. + + Lemma log2_up_le_full a : a <= 2^Z.log2_up a. + Proof. + destruct (Z_dec 1 a) as [ [ ? | ? ] | ? ]; + first [ apply Z.log2_up_spec; assumption + | rewrite Z.log2_up_eqn0 by omega; simpl; omega ]. + Qed. + + Lemma log2_up_le_pow2_full : forall a b : Z, (0 <= b)%Z -> (a <= 2 ^ b)%Z <-> (Z.log2_up a <= b)%Z. + Proof. + intros a b H. + destruct (Z_lt_le_dec 0 a); [ apply Z.log2_up_le_pow2; assumption | ]. + split; transitivity 0%Z; try omega; auto with zarith. + rewrite Z.log2_up_eqn0 by omega. + reflexivity. + Qed. + + Lemma log2_lt_pow2_alt a b : 0 < b -> (a < 2^b <-> Z.log2 a < b). + Proof. + destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; []. + rewrite Z.log2_nonpos by omega. + split; auto with zarith; []. + intro; eapply Z.le_lt_trans; [ eassumption | ]. + auto with zarith. + Qed. + + Lemma max_log2_up x y : Z.max (Z.log2_up x) (Z.log2_up y) = Z.log2_up (Z.max x y). + Proof. apply Z.max_monotone; intros ??; apply Z.log2_up_le_mono. Qed. + Hint Rewrite max_log2_up : push_Zmax. + Hint Rewrite <- max_log2_up : pull_Zmax. + + Lemma log2_up_le_full_max a : Z.max a 1 <= 2^Z.log2_up a. + Proof. + apply Z.max_case_strong; auto using Z.log2_up_le_full. + intros; rewrite Z.log2_up_eqn0 by assumption; reflexivity. + Qed. + Lemma log2_up_le_1 a : Z.log2_up a <= 1 <-> a <= 2. + Proof. + pose proof (Z.log2_nonneg (Z.pred a)). + destruct (Z_dec a 2) as [ [ ? | ? ] | ? ]. + { rewrite (proj2 (Z.log2_up_null a)) by omega; split; omega. } + { rewrite Z.log2_up_eqn by omega. + split; try omega; intro. + assert (Z.log2 (Z.pred a) = 0) by omega. + assert (Z.pred a <= 1) by (apply Z.log2_null; omega). + omega. } + { subst; cbv -[Z.le]; split; omega. } + Qed. + Lemma log2_up_1_le a : 1 <= Z.log2_up a <-> 2 <= a. + Proof. + pose proof (Z.log2_nonneg (Z.pred a)). + destruct (Z_dec a 2) as [ [ ? | ? ] | ? ]. + { rewrite (proj2 (Z.log2_up_null a)) by omega; split; omega. } + { rewrite Z.log2_up_eqn by omega; omega. } + { subst; cbv -[Z.le]; split; omega. } + Qed. +End Z. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 84917a454..567d106e3 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -4,6 +4,7 @@ Require Import Crypto.Util.ZUtil.ZSimplify.Core. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Div. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. @@ -287,4 +288,85 @@ Module Z. Lemma mod_opp_r a b : a mod (-b) = -((-a) mod b). Proof. pose proof (Z.div_opp_r a b); Z.div_mod_to_quot_rem; nia. Qed. Hint Resolve mod_opp_r : zarith. + + Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. + Proof. + intros a b c H. + replace b with (b - c + c) by ring. + rewrite Z.pow_add_r by omega. + apply Z_mod_mult. + Qed. + Hint Rewrite mod_same_pow using zutil_arith : zsimplify. + + Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. + Proof. + split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. + Qed. + Hint Rewrite <- mod_opp_l_z_iff using zutil_arith : zsimplify. + + Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. + Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. + Hint Resolve mod_small_sym : zarith. + + Lemma mod_eq_le_to_eq a b : 0 < a <= b -> a mod b = 0 -> a = b. + Proof. pose proof (Z.mod_eq_le_div_1 a b); intros; Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve mod_eq_le_to_eq : zarith. + + Lemma mod_neq_0_le_to_neq a b : a mod b <> 0 -> a <> b. + Proof. repeat intro; subst; autorewrite with zsimplify in *; lia. Qed. + Hint Resolve mod_neq_0_le_to_neq : zarith. + + Lemma div_mod' a b : b <> 0 -> a = (a / b) * b + a mod b. + Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. + Hint Rewrite <- div_mod' using zutil_arith : zsimplify. + + Lemma div_mod'' a b : b <> 0 -> a = a mod b + b * (a / b). + Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. + Hint Rewrite <- div_mod'' using zutil_arith : zsimplify. + + Lemma div_mod''' a b : b <> 0 -> a = a mod b + (a / b) * b. + Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. + Hint Rewrite <- div_mod''' using zutil_arith : zsimplify. + + Lemma sub_mod_mod_0 x d : (x - x mod d) mod d = 0. + Proof. + destruct (Z_zerop d); subst; push_Zmod; autorewrite with zsimplify; reflexivity. + Qed. + Hint Resolve sub_mod_mod_0 : zarith. + Hint Rewrite sub_mod_mod_0 : zsimplify. + + Lemma mod_small_n n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a mod b = a - n * b. + Proof. intros; erewrite Zmod_eq_full, Z.div_between by eassumption. reflexivity. Qed. + Hint Rewrite mod_small_n using zutil_arith : zsimplify. + + Lemma mod_small_1 a b : b <> 0 -> b <= a < 2 * b -> a mod b = a - b. + Proof. intros; rewrite (mod_small_n 1) by lia; lia. Qed. + Hint Rewrite mod_small_1 using zutil_arith : zsimplify. + + Lemma mod_small_n_if n a b : 0 <= n -> b <> 0 -> n * b <= a < (2 + n) * b -> a mod b = a - (if (1 + n) * b <=? a then (1 + n) else n) * b. + Proof. intros; erewrite Zmod_eq_full, Z.div_between_if by eassumption; autorewrite with zsimplify_const. reflexivity. Qed. + + Lemma mod_small_0_if a b : b <> 0 -> 0 <= a < 2 * b -> a mod b = a - if b <=? a then b else 0. + Proof. intros; rewrite (mod_small_n_if 0) by lia; autorewrite with zsimplify_const. break_match; lia. Qed. + + Lemma mul_mod_distr_r_full a b c : (a * c) mod (b * c) = (a mod b * c). + Proof. + destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; + autorewrite with zsimplify; auto using Z.mul_mod_distr_r. + Qed. + + Lemma mul_mod_distr_l_full a b c : (c * a) mod (c * b) = c * (a mod b). + Proof. + destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; + autorewrite with zsimplify; auto using Z.mul_mod_distr_l. + Qed. + + Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b. + Proof. + intros a b H H0. + replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring). + rewrite Z.mod_add_l by auto. + apply Z.mod_small. + omega. + Qed. End Z. diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index 91f3dff3c..15a9fcf1a 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -6,6 +6,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Classes.RelationPairs. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.LandLorBounds. Require Import Crypto.Util.ZUtil.Tactics.PeelLe. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -279,4 +280,13 @@ Module Z. Lemma shiftl_Zneg_Zneg_le_Proper_r x : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftl (Zneg p) (Zneg x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftl_Zneg_Zneg_le_Proper_r : zarith. + + Hint Resolve Z.land_round_Proper_pos_r : zarith. + Hint Resolve Z.land_round_Proper_pos_l : zarith. + Hint Resolve Z.lor_round_Proper_pos_r : zarith. + Hint Resolve Z.lor_round_Proper_pos_l : zarith. + Hint Resolve Z.land_round_Proper_neg_r : zarith. + Hint Resolve Z.land_round_Proper_neg_l : zarith. + Hint Resolve Z.lor_round_Proper_neg_r : zarith. + Hint Resolve Z.lor_round_Proper_neg_l : zarith. End Z. diff --git a/src/Util/ZUtil/Mul.v b/src/Util/ZUtil/Mul.v new file mode 100644 index 000000000..6cf851e4e --- /dev/null +++ b/src/Util/ZUtil/Mul.v @@ -0,0 +1,8 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma mul_comm3 x y z : x * (y * z) = y * (x * z). + Proof. lia. Qed. +End Z. diff --git a/src/Util/ZUtil/N2Z.v b/src/Util/ZUtil/N2Z.v new file mode 100644 index 000000000..928f0b334 --- /dev/null +++ b/src/Util/ZUtil/N2Z.v @@ -0,0 +1,53 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module N2Z. + Lemma inj_land n m : Z.of_N (N.land n m) = Z.land (Z.of_N n) (Z.of_N m). + Proof. destruct n, m; reflexivity. Qed. + Hint Rewrite inj_land : push_Zof_N. + Hint Rewrite <- inj_land : pull_Zof_N. + + Lemma inj_lor n m : Z.of_N (N.lor n m) = Z.lor (Z.of_N n) (Z.of_N m). + Proof. destruct n, m; reflexivity. Qed. + Hint Rewrite inj_lor : push_Zof_N. + Hint Rewrite <- inj_lor : pull_Zof_N. + + Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). + Proof. + intros x y. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftl_spec; [|assumption]. + + assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by ( + unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left]; + intro H; inversion H). + + destruct g as [g|g]; + [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le] + | rewrite N.shiftl_spec_low]; try assumption. + + - rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption]. + + - apply N2Z.inj_lt in g. + rewrite Z2N.id in g; [symmetry|assumption]. + apply Z.testbit_neg_r; omega. + Qed. + Hint Rewrite inj_shiftl : push_Zof_N. + Hint Rewrite <- inj_shiftl : pull_Zof_N. + + Lemma inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y). + Proof. + intros. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. + rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_add; f_equal. + apply Z2N.id; assumption. + Qed. + Hint Rewrite inj_shiftr : push_Zof_N. + Hint Rewrite <- inj_shiftr : pull_Zof_N. +End N2Z. diff --git a/src/Util/ZUtil/Odd.v b/src/Util/ZUtil/Odd.v new file mode 100644 index 000000000..37b8bd443 --- /dev/null +++ b/src/Util/ZUtil/Odd.v @@ -0,0 +1,32 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. + Proof. + intros p prime_p. + apply Decidable.imp_not_l; try apply Z.eq_decidable. + intros p_neq2. + pose proof (Zmod_odd p) as mod_odd. + destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. + rewrite p_not_odd in mod_odd. + apply Zmod_divides in mod_odd; try omega. + destruct mod_odd as [c c_id]. + rewrite Z.mul_comm in c_id. + apply Zdivide_intro in c_id. + apply prime_divisors in c_id; auto. + destruct c_id; [omega | destruct H; [omega | destruct H; auto] ]. + pose proof (prime_ge_2 p prime_p); omega. + Qed. + + Lemma odd_mod : forall a b, (b <> 0)%Z -> + Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. + Proof. + intros a b H. + rewrite Zmod_eq_full by assumption. + rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. + case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. + Qed. +End Z. diff --git a/src/Util/ZUtil/Ones.v b/src/Util/ZUtil/Ones.v new file mode 100644 index 000000000..e856f23a0 --- /dev/null +++ b/src/Util/ZUtil/Ones.v @@ -0,0 +1,177 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Lnot. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.ZSimplify.Simple. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.UniquePose. +Local Open Scope bool_scope. Local Open Scope Z_scope. + +Module Z. + Lemma ones_le x y : x <= y -> Z.ones x <= Z.ones y. + Proof. + rewrite !Z.ones_equiv; auto with zarith. + Qed. + Hint Resolve ones_le : zarith. + + Lemma ones_lt_pow2 x y : 0 <= x <= y -> Z.ones x < 2^y. + Proof. + rewrite Z.ones_equiv, Z.lt_pred_le. + auto with zarith. + Qed. + Hint Resolve ones_lt_pow2 : zarith. + + Lemma log2_ones_full x : Z.log2 (Z.ones x) = Z.max 0 (Z.pred x). + Proof. + rewrite Z.ones_equiv, Z.log2_pred_pow2_full; reflexivity. + Qed. + Hint Rewrite log2_ones_full : zsimplify. + + Lemma log2_ones_lt x y : 0 < x <= y -> Z.log2 (Z.ones x) < y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_lt : zarith. + + Lemma log2_ones_le x y : 0 <= x <= y -> Z.log2 (Z.ones x) <= y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_le : zarith. + + Lemma log2_ones_lt_nonneg x y : 0 < y -> x <= y -> Z.log2 (Z.ones x) < y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_lt_nonneg : zarith. + + Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. + Proof. + induction i as [|p|p]; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. + intros. + unfold Z.ones. + rewrite !Z.shiftl_1_l, Z.shiftr_div_pow2, <-!Z.sub_1_r, Z.pow_1_r, <-!Z.add_opp_r by omega. + replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2). + rewrite Z.div_add_l by omega. + reflexivity. + change 2 with (2 ^ 1) at 2. + rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega). + f_equal. omega. + Qed. + Hint Rewrite <- ones_pred using zutil_arith : push_Zshift. + + Lemma ones_succ : forall x, (0 <= x) -> + Z.ones (Z.succ x) = 2 ^ x + Z.ones x. + Proof. + unfold Z.ones; intros. + rewrite !Z.shiftl_1_l. + rewrite Z.add_pred_r. + apply Z.succ_inj. + rewrite !Z.succ_pred. + rewrite Z.pow_succ_r; omega. + Qed. + + Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. + Proof. + apply natlike_ind. + + unfold Z.ones. simpl; omega. + + intros. + rewrite Z.ones_succ by assumption. + Z.zero_bounds. + Qed. + Hint Resolve ones_nonneg : zarith. + + Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. + Proof. + intros. + unfold Z.ones. + rewrite Z.shiftl_1_l. + apply Z.lt_succ_lt_pred. + apply Z.pow_gt_1; omega. + Qed. + Hint Resolve ones_pos_pos : zarith. + + Lemma lnot_ones_equiv n : Z.lnot (Z.ones n) = -2^n. + Proof. rewrite Z.ones_equiv, Z.lnot_equiv, <- ?Z.sub_1_r; lia. Qed. + + Lemma land_ones_ones n m + : Z.land (Z.ones n) (Z.ones m) + = Z.ones (if ((n <? 0) || (m <? 0)) + then Z.max n m + else Z.min n m). + Proof. + repeat first [ reflexivity + | break_innermost_match_step + | progress rewrite ?Bool.orb_true_iff in * + | progress rewrite ?Bool.orb_false_iff in * + | progress rewrite ?Z.ltb_lt, ?Z.ltb_ge in * + | progress destruct_head'_and + | apply Z.min_case_strong + | apply Z.max_case_strong + | progress intros + | progress destruct_head'_or + | rewrite !Z.pow_r_Zneg + | rewrite !Z.land_m1_l + | rewrite !Z.land_m1_r + | progress change (Z.pred 0) with (-1) + | rewrite Z.mod_small by lia + | match goal with + | [ H : ?x < 0 |- _ ] => is_var x; destruct x; try lia + | [ H : ?x <= Z.neg _ |- _ ] => is_var x; destruct x; try lia + | [ |- context[Z.ones (Z.neg ?x)] ] => rewrite (Z.ones_equiv (Z.neg x)) + | [ H : ?n <= ?m |- Z.land (Z.ones ?m) (Z.ones ?n) = _ ] + => rewrite (Z.land_comm (Z.ones m) (Z.ones n)) + | [ H : ?n <= ?m |- Z.land (Z.ones ?n) (Z.ones ?m) = _ ] + => progress rewrite ?Z.land_ones, ?Z.ones_equiv, <- ?Z.sub_1_r by auto + | [ H : ?n <= ?m |- _ ] + => is_var n; is_var m; unique pose proof (Z.pow_le_mono_r 2 n m ltac:(lia) H) + | [ |- context[2^?x] ] => unique pose proof (Z.pow2_gt_0 x ltac:(lia)) + end ]. + Qed. + Hint Rewrite land_ones_ones : zsimplify. + + Lemma lor_ones_ones n m + : Z.lor (Z.ones n) (Z.ones m) + = Z.ones (if ((n <? 0) || (m <? 0)) + then Z.min n m + else Z.max n m). + Proof. + destruct (Z_zerop n), (Z_zerop m); subst; + repeat first [ reflexivity + | break_innermost_match_step + | progress rewrite ?Bool.orb_true_iff in * + | progress rewrite ?Bool.orb_false_iff in * + | progress rewrite ?Z.ltb_lt, ?Z.ltb_ge in * + | progress destruct_head'_and + | apply Z.min_case_strong + | apply Z.max_case_strong + | progress intros + | progress destruct_head'_or + | rewrite !Z.pow_r_Zneg + | rewrite !Z.lor_m1_l + | rewrite !Z.lor_m1_r + | progress change (Z.pred 0) with (-1) + | rewrite Z.mod_small by lia + | lia + | match goal with + | [ H : ?x < 0 |- _ ] => is_var x; destruct x; try lia + | [ H : ?x <= Z.neg _ |- _ ] => is_var x; destruct x; try lia + | [ |- context[Z.ones (Z.neg ?x)] ] => rewrite (Z.ones_equiv (Z.neg x)) + | [ H : ?n <= ?m |- Z.lor (Z.ones ?m) (Z.ones ?n) = _ ] + => rewrite (Z.lor_comm (Z.ones m) (Z.ones n)) + | [ H : ?n <= ?m |- Z.lor (Z.ones ?n) (Z.ones ?m) = _ ] + => progress rewrite ?Z.lor_ones_low; try apply Z.log2_ones_lt_nonneg; rewrite ?Z.ones_equiv, <- ?Z.sub_1_r + | [ H : ?n <= ?m |- _ ] + => is_var n; is_var m; unique pose proof (Z.pow_le_mono_r 2 n m ltac:(lia) H) + | [ |- context[2^?x] ] => unique pose proof (Z.pow2_gt_0 x ltac:(lia)) + end ]. + Qed. + Hint Rewrite lor_ones_ones : zsimplify. +End Z. diff --git a/src/Util/ZUtil/Opp.v b/src/Util/ZUtil/Opp.v new file mode 100644 index 000000000..3cc18241b --- /dev/null +++ b/src/Util/ZUtil/Opp.v @@ -0,0 +1,11 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. + Proof. omega. Qed. + Hint Rewrite opp_eq_0_iff : zsimplify. +End Z. diff --git a/src/Util/ZUtil/Pow.v b/src/Util/ZUtil/Pow.v new file mode 100644 index 000000000..06ce2187b --- /dev/null +++ b/src/Util/ZUtil/Pow.v @@ -0,0 +1,44 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma base_pow_neg b n : n < 0 -> b^n = 0. + Proof. + destruct n; intro H; try reflexivity; compute in H; congruence. + Qed. + Hint Rewrite base_pow_neg using zutil_arith : zsimplify. + + Lemma nonneg_pow_pos a b : 0 < a -> 0 < a^b -> 0 <= b. + Proof. + destruct (Z_lt_le_dec b 0); intros; auto. + erewrite Z.pow_neg_r in * by eassumption. + omega. + Qed. + Hint Resolve nonneg_pow_pos (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith. + Lemma nonneg_pow_pos_helper a b dummy : 0 < a -> 0 <= dummy < a^b -> 0 <= b. + Proof. eauto with zarith omega. Qed. + Hint Resolve nonneg_pow_pos_helper (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith. + + Lemma div_pow2succ : forall n x, (0 <= x) -> + n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). + Proof. + intros. + rewrite Z.pow_succ_r, Z.mul_comm by auto. + rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). + rewrite Zdiv2_div. + reflexivity. + Qed. + + Definition pow_sub_r' + := fun a b c y H0 H1 => @Logic.eq_trans _ _ _ y (@Z.pow_sub_r a b c H0 H1). + Definition pow_sub_r'_sym + := fun a b c y p H0 H1 => Logic.eq_sym (@Logic.eq_trans _ y _ _ (Logic.eq_sym p) (@Z.pow_sub_r a b c H0 H1)). + Hint Resolve pow_sub_r' pow_sub_r'_sym Z.eq_le_incl : zarith. + Hint Resolve (fun b => f_equal (fun e => b ^ e)) (fun e => f_equal (fun b => b ^ e)) : zarith. + + Lemma two_p_two_eq_four : 2^(2) = 4. + Proof. reflexivity. Qed. + Hint Rewrite <- two_p_two_eq_four : push_Zpow. +End Z. diff --git a/src/Util/ZUtil/Pow2.v b/src/Util/ZUtil/Pow2.v new file mode 100644 index 000000000..bc3b01225 --- /dev/null +++ b/src/Util/ZUtil/Pow2.v @@ -0,0 +1,26 @@ +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Local Open Scope Z_scope. + +Module Z. + Lemma pow2_ge_0: forall a, (0 <= 2 ^ a)%Z. + Proof. + intros; apply Z.pow_nonneg; omega. + Qed. + + Lemma pow2_gt_0: forall a, (0 <= a)%Z -> (0 < 2 ^ a)%Z. + Proof. + intros; apply Z.pow_pos_nonneg; [|assumption]; omega. + Qed. + + Lemma pow2_lt_or_divides : forall a b, 0 <= b -> + 2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0. + Proof. + intros a b H. + destruct (Z_lt_dec a b); [left|right]. + { apply Z.pow_lt_mono_r; auto; omega. } + { replace a with (a - b + b) by ring. + rewrite Z.pow_add_r by omega. + apply Z.mod_mul, Z.pow_nonzero; omega. } + Qed. +End Z. diff --git a/src/Util/ZUtil/Pow2Mod.v b/src/Util/ZUtil/Pow2Mod.v index 237ca19dc..74c22394a 100644 --- a/src/Util/ZUtil/Pow2Mod.v +++ b/src/Util/ZUtil/Pow2Mod.v @@ -3,6 +3,7 @@ Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.Ztestbit. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.ZUtil.Testbit. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. @@ -51,4 +52,14 @@ Module Z. auto with zarith. Qed. Hint Resolve pow2_mod_pos_bound : zarith. + + Lemma pow2_mod_id_iff : forall a n, 0 <= n -> + (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). + Proof. + intros a n H. + rewrite Z.pow2_mod_spec by assumption. + assert (0 < 2 ^ n) by Z.zero_bounds. + rewrite Z.mod_small_iff by omega. + split; intros; intuition omega. + Qed. End Z. diff --git a/src/Util/ZUtil/Shift.v b/src/Util/ZUtil/Shift.v new file mode 100644 index 000000000..b5fb79c13 --- /dev/null +++ b/src/Util/ZUtil/Shift.v @@ -0,0 +1,393 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Ones. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SpecializeBy. +Local Open Scope Z_scope. + +Module Z. + Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> + Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). + Proof. + intros n m a b H H0. + rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega. + replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by + (rewrite <-Z.pow_add_r by omega; f_equal; ring). + rewrite <-Z.div_div, Z.div_add, (Z.div_small a) ; try solve + [assumption || apply Z.pow_nonzero || apply Z.pow_pos_nonneg; omega]. + f_equal; ring. + Qed. + Hint Rewrite Z.shiftr_add_shiftl_high using zutil_arith : pull_Zshift. + Hint Rewrite <- Z.shiftr_add_shiftl_high using zutil_arith : push_Zshift. + + Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> + Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n). + Proof. + intros n m a b H H0. + rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega. + replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by + (rewrite <-Z.pow_add_r by omega; f_equal; ring). + rewrite Z.mul_assoc, Z.div_add by (apply Z.pow_nonzero; omega). + repeat f_equal; ring. + Qed. + Hint Rewrite Z.shiftr_add_shiftl_low using zutil_arith : pull_Zshift. + Hint Rewrite <- Z.shiftr_add_shiftl_low using zutil_arith : push_Zshift. + + Lemma testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) -> + 0 <= a < 2 ^ n -> + Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n). + Proof. + intros i ?. + apply natlike_ind with (x := i); [ intros a b n | intros x H0 H1 a b n | ]; intros; try assumption; + (destruct (Z.eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; + replace a with 0 by omega; f_equal; ring | ]); try omega. + rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. + replace (Z.succ x - n) with (x - (n - 1)) by ring. + rewrite shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega. + rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ]. + rewrite Z.shiftr_div_pow2 by omega. + split; apply Z.div_pos || apply Z.div_lt_upper_bound; + try solve [rewrite ?Z.pow_1_r; omega]. + rewrite <-Z.pow_add_r by omega. + replace (1 + (n - 1)) with n by ring; omega. + Qed. + Hint Rewrite testbit_add_shiftl_high using zutil_arith : Ztestbit. + + Lemma shiftr_succ : forall n x, + Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. + Proof. + intros. + rewrite Z.shiftr_shiftr by omega. + reflexivity. + Qed. + Hint Rewrite Z.shiftr_succ using zutil_arith : push_Zshift. + Hint Rewrite <- Z.shiftr_succ using zutil_arith : pull_Zshift. + + Lemma shiftr_1_r_le : forall a b, a <= b -> + Z.shiftr a 1 <= Z.shiftr b 1. + Proof. + intros. + rewrite !Z.shiftr_div_pow2, Z.pow_1_r by omega. + apply Z.div_le_mono; omega. + Qed. + Hint Resolve shiftr_1_r_le : zarith. + + Lemma shiftr_le : forall a b i : Z, 0 <= i -> a <= b -> a >> i <= b >> i. + Proof. + intros a b i ?; revert a b. apply natlike_ind with (x := i); intros; auto. + rewrite !shiftr_succ, shiftr_1_r_le; eauto. reflexivity. + Qed. + Hint Resolve shiftr_le : zarith. + + Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> + Z.shiftr a i <= Z.ones (n - i) \/ n <= i. + Proof. + intros a n H. + apply natlike_ind. + + unfold Z.ones. + rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. + omega. + + intros x H0 H1. + destruct (Z_lt_le_dec x n); try omega. + intuition auto with zarith lia. + left. + rewrite shiftr_succ. + replace (n - Z.succ x) with (Z.pred (n - x)) by omega. + rewrite Z.ones_pred by omega. + apply Z.shiftr_1_r_le. + assumption. + Qed. + + Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> + Z.shiftr a i <= Z.ones (n - i) . + Proof. + intros a n i G G0 G1. + destruct (Z_le_lt_eq_dec i n G1). + + destruct (Z.shiftr_ones' a n G i G0); omega. + + subst; rewrite Z.sub_diag. + destruct (Z.eq_dec a 0). + - subst; rewrite Z.shiftr_0_l; reflexivity. + - rewrite Z.shiftr_eq_0; try omega; try reflexivity. + apply Z.log2_lt_pow2; omega. + Qed. + Hint Resolve shiftr_ones : zarith. + + Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. + Proof. + intros a ? ? [a_nonneg a_upper_bound]. + apply Z_le_lt_eq_dec in a_upper_bound. + destruct a_upper_bound. + + destruct (Z.eq_dec 0 a). + - subst; rewrite Z.shiftr_0_l; omega. + - rewrite Z.shiftr_eq_0; auto; try omega. + apply Z.log2_lt_pow2; auto; omega. + + subst. + rewrite Z.shiftr_div_pow2 by assumption. + rewrite Z.div_same; try omega. + assert (0 < 2 ^ n) by (apply Z.pow_pos_nonneg; omega). + omega. + Qed. + Hint Resolve shiftr_upper_bound : zarith. + + Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). + Proof. + intros a b n H H0. + apply Z.bits_inj'; intros t ?. + rewrite Z.lor_spec, Z.shiftl_spec by assumption. + destruct (Z_lt_dec t n). + + rewrite Z.testbit_add_shiftl_low by omega. + rewrite Z.testbit_neg_r with (n := t - n) by omega. + apply Bool.orb_false_r. + + rewrite testbit_add_shiftl_high by omega. + replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. + symmetry. + apply Z.testbit_false; try omega. + rewrite Z.div_small; try reflexivity. + split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. + apply Z.pow_le_mono_r; omega. + Qed. + Hint Rewrite <- Z.lor_shiftl using zutil_arith : convert_to_Ztestbit. + + Lemma lor_shiftl' : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Z.lor (Z.shiftl b n) a = (Z.shiftl b n) + a. + Proof. + intros; rewrite Z.lor_comm, Z.add_comm; apply lor_shiftl; assumption. + Qed. + Hint Rewrite <- Z.lor_shiftl' using zutil_arith : convert_to_Ztestbit. + + Lemma shiftl_spec_full a n m + : Z.testbit (a << n) m = if Z_lt_dec m n + then false + else if Z_le_dec 0 m + then Z.testbit a (m - n) + else false. + Proof. + repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega. + Qed. + Hint Rewrite shiftl_spec_full : Ztestbit_full. + + Lemma shiftr_spec_full a n m + : Z.testbit (a >> n) m = if Z_lt_dec m (-n) + then false + else if Z_le_dec 0 m + then Z.testbit a (m + n) + else false. + Proof. + rewrite <- Z.shiftl_opp_r, shiftl_spec_full, Z.sub_opp_r; reflexivity. + Qed. + Hint Rewrite shiftr_spec_full : Ztestbit_full. + + Lemma testbit_add_shiftl_full i (Hi : 0 <= i) a b n (Ha : 0 <= a < 2^n) + : Z.testbit (a + b << n) i + = if (i <? n) then Z.testbit a i else Z.testbit b (i - n). + Proof. + assert (0 < 2^n) by omega. + assert (0 <= n) by eauto 2 with zarith. + pose proof (Zlt_cases i n); break_match; autorewrite with Ztestbit; reflexivity. + Qed. + Hint Rewrite testbit_add_shiftl_full using zutil_arith : Ztestbit. + + Lemma land_add_land : forall n m a b, (m <= n)%nat -> + Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). + Proof. + intros n m a b H. + rewrite !Z.land_ones by apply Nat2Z.is_nonneg. + rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. + replace (b * 2 ^ Z.of_nat n) with + ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by + (rewrite (le_plus_minus m n) at 2; try assumption; + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). + symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). + rewrite (le_plus_minus m n) by assumption. + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. + apply Z.divide_factor_l. + Qed. + + Lemma shiftl_add x y z : 0 <= z -> (x + y) << z = (x << z) + (y << z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftl_add using zutil_arith : push_Zshift. + Hint Rewrite <- shiftl_add using zutil_arith : pull_Zshift. + + Lemma shiftr_add x y z : z <= 0 -> (x + y) >> z = (x >> z) + (y >> z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftr_add using zutil_arith : push_Zshift. + Hint Rewrite <- shiftr_add using zutil_arith : pull_Zshift. + + Lemma shiftl_sub x y z : 0 <= z -> (x - y) << z = (x << z) - (y << z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftl_sub using zutil_arith : push_Zshift. + Hint Rewrite <- shiftl_sub using zutil_arith : pull_Zshift. + + Lemma shiftr_sub x y z : z <= 0 -> (x - y) >> z = (x >> z) - (y >> z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftr_sub using zutil_arith : push_Zshift. + Hint Rewrite <- shiftr_sub using zutil_arith : pull_Zshift. + + Lemma compare_add_shiftl : forall x1 y1 x2 y2 n, 0 <= n -> + Z.pow2_mod x1 n = x1 -> Z.pow2_mod x2 n = x2 -> + x1 + (y1 << n) ?= x2 + (y2 << n) = + if Z.eq_dec y1 y2 + then x1 ?= x2 + else y1 ?= y2. + Proof. + repeat match goal with + | |- _ => progress intros + | |- _ => progress subst y1 + | |- _ => rewrite Z.shiftl_mul_pow2 by omega + | |- _ => rewrite Z.add_compare_mono_r + | |- _ => rewrite <-Z.mul_sub_distr_r + | |- _ => break_innermost_match_step + | H : Z.pow2_mod _ _ = _ |- _ => rewrite Z.pow2_mod_id_iff in H by omega + | H : ?a <> ?b |- _ = (?a ?= ?b) => + case_eq (a ?= b); rewrite ?Z.compare_eq_iff, ?Z.compare_gt_iff, ?Z.compare_lt_iff + | |- _ + (_ * _) > _ + (_ * _) => cbv [Z.gt] + | |- _ + (_ * ?x) < _ + (_ * ?x) => + apply Z.lt_sub_lt_add; apply Z.lt_le_trans with (m := 1 * x); [omega|] + | |- _ => apply Z.mul_le_mono_nonneg_r; omega + | |- _ => reflexivity + | |- _ => congruence + end. + Qed. + + Lemma shiftl_opp_l a n + : Z.shiftl (-a) n = - Z.shiftl a n - (if Z_zerop (a mod 2 ^ (- n)) then 0 else 1). + Proof. + destruct (Z_dec 0 n) as [ [?|?] | ? ]; + subst; + rewrite ?Z.pow_neg_r by omega; + autorewrite with zsimplify_const; + [ | | simpl; omega ]. + { rewrite !Z.shiftl_mul_pow2 by omega. + nia. } + { rewrite !Z.shiftl_div_pow2 by omega. + rewrite Z.div_opp_l_complete by auto with zarith. + reflexivity. } + Qed. + Hint Rewrite shiftl_opp_l : push_Zshift. + Hint Rewrite <- shiftl_opp_l : pull_Zshift. + + Lemma shiftr_opp_l a n + : Z.shiftr (-a) n = - Z.shiftr a n - (if Z_zerop (a mod 2 ^ n) then 0 else 1). + Proof. + unfold Z.shiftr; rewrite shiftl_opp_l at 1; rewrite Z.opp_involutive. + reflexivity. + Qed. + Hint Rewrite shiftr_opp_l : push_Zshift. + Hint Rewrite <- shiftr_opp_l : pull_Zshift. + + Lemma shl_shr_lt x y n m (Hx : 0 <= x < 2^n) (Hy : 0 <= y < 2^n) (Hm : 0 <= m <= n) + : 0 <= (x >> (n - m)) + ((y << m) mod 2^n) < 2^n. + Proof. + cut (0 <= (x >> (n - m)) + ((y << m) mod 2^n) <= 2^n - 1); [ omega | ]. + assert (0 <= x <= 2^n - 1) by omega. + assert (0 <= y <= 2^n - 1) by omega. + assert (0 < 2 ^ (n - m)) by auto with zarith. + assert (0 <= y mod 2 ^ (n - m) < 2^(n-m)) by auto with zarith. + assert (0 <= y mod 2 ^ (n - m) <= 2 ^ (n - m) - 1) by omega. + assert (0 <= (y mod 2 ^ (n - m)) * 2^m <= (2^(n-m) - 1)*2^m) by auto with zarith. + assert (0 <= x / 2^(n-m) < 2^n / 2^(n-m)). + { split; Z.zero_bounds. + apply Z.div_lt_upper_bound; autorewrite with pull_Zpow zsimplify; nia. } + autorewrite with Zshift_to_pow. + split; Z.zero_bounds. + replace (2^n) with (2^(n-m) * 2^m) by (autorewrite with pull_Zpow; f_equal; omega). + rewrite Zmult_mod_distr_r. + autorewrite with pull_Zpow zsimplify push_Zmul in * |- . + nia. + Qed. + + Lemma add_shift_mod x y n m + (Hx : 0 <= x < 2^n) (Hy : 0 <= y) + (Hn : 0 <= n) (Hm : 0 < m) + : (x + y << n) mod (m * 2^n) = x + (y mod m) << n. + Proof. + pose proof (Z.mod_bound_pos y m). + specialize_by omega. + assert (0 < 2^n) by auto with zarith. + autorewrite with Zshift_to_pow. + rewrite Zplus_mod, !Zmult_mod_distr_r. + rewrite Zplus_mod, !Zmod_mod, <- Zplus_mod. + rewrite !(Zmod_eq (_ + _)) by nia. + etransitivity; [ | apply Z.add_0_r ]. + rewrite <- !Z.add_opp_r, <- !Z.add_assoc. + repeat apply f_equal. + ring_simplify. + cut (((x + y mod m * 2 ^ n) / (m * 2 ^ n)) = 0); [ nia | ]. + apply Z.div_small; split; nia. + Qed. + + Lemma add_mul_mod x y n m + (Hx : 0 <= x < 2^n) (Hy : 0 <= y) + (Hn : 0 <= n) (Hm : 0 < m) + : (x + y * 2^n) mod (m * 2^n) = x + (y mod m) * 2^n. + Proof. + generalize (add_shift_mod x y n m). + autorewrite with Zshift_to_pow; auto. + Qed. + + Lemma lt_pow_2_shiftr : forall a n, 0 <= a < 2 ^ n -> a >> n = 0. + Proof. + intros a n H. + destruct (Z_le_dec 0 n). + + rewrite Z.shiftr_div_pow2 by assumption. + auto using Z.div_small. + + assert (2 ^ n = 0) by (apply Z.pow_neg_r; omega). + omega. + Qed. + + Hint Rewrite Z.pow2_bits_eqb using zutil_arith : Ztestbit. + Lemma pow_2_shiftr : forall n, 0 <= n -> (2 ^ n) >> n = 1. + Proof. + intros; apply Z.bits_inj'; intros. + replace 1 with (2 ^ 0) by ring. + repeat match goal with + | |- _ => progress intros + | |- _ => progress rewrite ?Z.eqb_eq, ?Z.eqb_neq in * + | |- _ => progress autorewrite with Ztestbit + | |- context[Z.eqb ?a ?b] => case_eq (Z.eqb a b) + | |- _ => reflexivity || omega + end. + Qed. + + Lemma lt_mul_2_pow_2_shiftr : forall a n, 0 <= a < 2 * 2 ^ n -> + a >> n = if Z_lt_dec a (2 ^ n) then 0 else 1. + Proof. + intros a n H; break_match; [ apply lt_pow_2_shiftr; omega | ]. + destruct (Z_le_dec 0 n). + + replace (2 * 2 ^ n) with (2 ^ (n + 1)) in * + by (rewrite Z.pow_add_r; try omega; ring). + pose proof (Z.shiftr_ones a (n + 1) n H). + pose proof (Z.shiftr_le (2 ^ n) a n). + specialize_by omega. + replace (n + 1 - n) with 1 in * by ring. + replace (Z.ones 1) with 1 in * by reflexivity. + rewrite pow_2_shiftr in * by omega. + omega. + + assert (2 ^ n = 0) by (apply Z.pow_neg_r; omega). + omega. + Qed. + + Lemma shiftr_nonneg_le : forall a n, 0 <= a -> 0 <= n -> a >> n <= a. + Proof. + intros. + repeat match goal with + | [ H : _ <= _ |- _ ] + => rewrite Z.lt_eq_cases in H + | [ H : _ \/ _ |- _ ] => destruct H + | _ => progress subst + | _ => progress autorewrite with zsimplify Zshift_to_pow + | _ => solve [ auto with zarith omega ] + end. + Qed. + Hint Resolve shiftr_nonneg_le : zarith. +End Z. diff --git a/src/Util/ZUtil/Stabilization.v b/src/Util/ZUtil/Stabilization.v index 4df0300da..7e89ea1b4 100644 --- a/src/Util/ZUtil/Stabilization.v +++ b/src/Util/ZUtil/Stabilization.v @@ -1,7 +1,10 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Testbit. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeBy. diff --git a/src/Util/ZUtil/Tactics/PullPush/Modulo.v b/src/Util/ZUtil/Tactics/PullPush/Modulo.v index 55889cbf0..fe0c3224c 100644 --- a/src/Util/ZUtil/Tactics/PullPush/Modulo.v +++ b/src/Util/ZUtil/Tactics/PullPush/Modulo.v @@ -3,89 +3,92 @@ Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo.PullPush. Local Open Scope Z_scope. -Ltac push_Zmod := - repeat match goal with - | _ => progress autorewrite with push_Zmod - | [ |- context[(?x * ?y) mod ?z] ] - => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod - | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod - | rewrite (Z.mul_mod_r_push x y z) by Z.NoZMod ] - | [ |- context[(?x + ?y) mod ?z] ] - => first [ rewrite (Z.add_mod_push x y z) by Z.NoZMod - | rewrite (Z.add_mod_l_push x y z) by Z.NoZMod - | rewrite (Z.add_mod_r_push x y z) by Z.NoZMod ] - | [ |- context[(?x - ?y) mod ?z] ] - => first [ rewrite (Z.sub_mod_push x y z) by Z.NoZMod - | rewrite (Z.sub_mod_l_push x y z) by Z.NoZMod - | rewrite (Z.sub_mod_r_push x y z) by Z.NoZMod ] - | [ |- context[(-?y) mod ?z] ] - => rewrite (Z.opp_mod_mod_push y z) by Z.NoZMod - | [ |- context[(?p^?q) mod ?z] ] - => rewrite (Z.pow_mod_push p q z) by Z.NoZMod - end. +Ltac push_Zmod_step := + match goal with + | _ => progress autorewrite with push_Zmod + | [ |- context[(?x * ?y) mod ?z] ] + => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod + | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod + | rewrite (Z.mul_mod_r_push x y z) by Z.NoZMod ] + | [ |- context[(?x + ?y) mod ?z] ] + => first [ rewrite (Z.add_mod_push x y z) by Z.NoZMod + | rewrite (Z.add_mod_l_push x y z) by Z.NoZMod + | rewrite (Z.add_mod_r_push x y z) by Z.NoZMod ] + | [ |- context[(?x - ?y) mod ?z] ] + => first [ rewrite (Z.sub_mod_push x y z) by Z.NoZMod + | rewrite (Z.sub_mod_l_push x y z) by Z.NoZMod + | rewrite (Z.sub_mod_r_push x y z) by Z.NoZMod ] + | [ |- context[(-?y) mod ?z] ] + => rewrite (Z.opp_mod_mod_push y z) by Z.NoZMod + | [ |- context[(?p^?q) mod ?z] ] + => rewrite (Z.pow_mod_push p q z) by Z.NoZMod + end. +Ltac push_Zmod := repeat push_Zmod_step. -Ltac push_Zmod_hyps := - repeat match goal with - | _ => progress autorewrite with push_Zmod in * |- - | [ H : context[(?x * ?y) mod ?z] |- _ ] - => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod - | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod - | rewrite (Z.mul_mod_r_push x y z) in H by Z.NoZMod ] - | [ H : context[(?x + ?y) mod ?z] |- _ ] - => first [ rewrite (Z.add_mod_push x y z) in H by Z.NoZMod - | rewrite (Z.add_mod_l_push x y z) in H by Z.NoZMod - | rewrite (Z.add_mod_r_push x y z) in H by Z.NoZMod ] - | [ H : context[(?x - ?y) mod ?z] |- _ ] - => first [ rewrite (Z.sub_mod_push x y z) in H by Z.NoZMod - | rewrite (Z.sub_mod_l_push x y z) in H by Z.NoZMod - | rewrite (Z.sub_mod_r_push x y z) in H by Z.NoZMod ] - | [ H : context[(-?y) mod ?z] |- _ ] - => rewrite (Z.opp_mod_mod_push y z) in H by Z.NoZMod - | [ H : context[(?p^?q) mod ?z] |- _ ] - => rewrite (Z.pow_mod_push p q z) in H by Z.NoZMod - end. +Ltac push_Zmod_hyps_step := + match goal with + | _ => progress autorewrite with push_Zmod in * |- + | [ H : context[(?x * ?y) mod ?z] |- _ ] + => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod + | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod + | rewrite (Z.mul_mod_r_push x y z) in H by Z.NoZMod ] + | [ H : context[(?x + ?y) mod ?z] |- _ ] + => first [ rewrite (Z.add_mod_push x y z) in H by Z.NoZMod + | rewrite (Z.add_mod_l_push x y z) in H by Z.NoZMod + | rewrite (Z.add_mod_r_push x y z) in H by Z.NoZMod ] + | [ H : context[(?x - ?y) mod ?z] |- _ ] + => first [ rewrite (Z.sub_mod_push x y z) in H by Z.NoZMod + | rewrite (Z.sub_mod_l_push x y z) in H by Z.NoZMod + | rewrite (Z.sub_mod_r_push x y z) in H by Z.NoZMod ] + | [ H : context[(-?y) mod ?z] |- _ ] + => rewrite (Z.opp_mod_mod_push y z) in H by Z.NoZMod + | [ H : context[(?p^?q) mod ?z] |- _ ] + => rewrite (Z.pow_mod_push p q z) in H by Z.NoZMod + end. +Ltac push_Zmod_hyps := repeat push_Zmod_hyps_step. Ltac has_no_mod x z := lazymatch x with | context[_ mod z] => fail | _ => idtac end. -Ltac pull_Zmod := - repeat match goal with - | [ |- context[((?x mod ?z) * (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.mul_mod_full x y z) - | [ |- context[((?x mod ?z) * ?y) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.mul_mod_l x y z) - | [ |- context[(?x * (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.mul_mod_r x y z) - | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.add_mod_full x y z) - | [ |- context[((?x mod ?z) + ?y) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.add_mod_l x y z) - | [ |- context[(?x + (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.add_mod_r x y z) - | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.sub_mod_full x y z) - | [ |- context[((?x mod ?z) - ?y) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.sub_mod_l x y z) - | [ |- context[(?x - (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.sub_mod_r x y z) - | [ |- context[(((-?y) mod ?z)) mod ?z] ] - => has_no_mod y z; - rewrite <- (Z.opp_mod_mod y z) - | [ |- context[((?x mod ?z)^?y) mod ?z] ] - => has_no_mod x z; - rewrite <- (Z.pow_mod_full x y z) - | [ |- context[(?x mod ?z) mod ?z] ] - => rewrite (Zmod_mod x z) - | _ => progress autorewrite with pull_Zmod - end. +Ltac pull_Zmod_step := + match goal with + | [ |- context[((?x mod ?z) * (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.mul_mod_full x y z) + | [ |- context[((?x mod ?z) * ?y) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.mul_mod_l x y z) + | [ |- context[(?x * (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.mul_mod_r x y z) + | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.add_mod_full x y z) + | [ |- context[((?x mod ?z) + ?y) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.add_mod_l x y z) + | [ |- context[(?x + (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.add_mod_r x y z) + | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.sub_mod_full x y z) + | [ |- context[((?x mod ?z) - ?y) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.sub_mod_l x y z) + | [ |- context[(?x - (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.sub_mod_r x y z) + | [ |- context[(-(?y mod ?z)) mod ?z] ] + => has_no_mod y z; + rewrite <- (Z.opp_mod_mod y z) + | [ |- context[((?x mod ?z)^?y) mod ?z] ] + => has_no_mod x z; + rewrite <- (Z.pow_mod_full x y z) + | [ |- context[(?x mod ?z) mod ?z] ] + => rewrite (Zmod_mod x z) + | _ => progress autorewrite with pull_Zmod + end. +Ltac pull_Zmod := repeat pull_Zmod_step. diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v index 175d07b02..f8ef5465a 100644 --- a/src/Util/ZUtil/Testbit.v +++ b/src/Util/ZUtil/Testbit.v @@ -1,7 +1,12 @@ +Require Import Coq.micromega.Lia. Require Import Coq.ZArith.ZArith. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Hints. Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Lnot. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. @@ -87,4 +92,39 @@ Module Z. auto using Z.mod_pow2_bits_low. Qed. Hint Rewrite testbit_add_shiftl_low using zutil_arith : Ztestbit. + + Lemma testbit_sub_pow2 n i x (i_range:0 <= i < n) (x_range:0 < x < 2 ^ n) : + Z.testbit (2 ^ n - x) i = negb (Z.testbit (x - 1) i). + Proof. + rewrite <-Z.lnot_spec, Z.lnot_sub1 by omega. + rewrite <-(Z.mod_pow2_bits_low (-x) _ _ (proj2 i_range)). + f_equal. + rewrite Z.mod_opp_l_nz; autorewrite with zsimplify; omega. + Qed. + + Lemma testbit_false_bound : forall a x, 0 <= x -> + (forall n, ~ (n < x) -> Z.testbit a n = false) -> + a < 2 ^ x. + Proof. + intros a x H H0. + assert (H1 : a = Z.pow2_mod a x). { + apply Z.bits_inj'; intros. + rewrite Z.testbit_pow2_mod by omega; break_match; auto. + } + rewrite H1. + cbv [Z.pow2_mod]; rewrite Z.land_ones by auto. + try apply Z.mod_pos_bound; Z.zero_bounds. + Qed. + + Lemma testbit_neg_eq_if x n : + 0 <= n -> + - (2 ^ n) <= x < 2 ^ n -> + Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2. + Proof. + intros. break_match; Z.ltb_to_lt. + { autorewrite with zsimplify. reflexivity. } + { autorewrite with zsimplify. + rewrite Z.bits_above_pow2 by omega. + reflexivity. } + Qed. End Z. diff --git a/src/Util/ZUtil/Z2Nat.v b/src/Util/ZUtil/Z2Nat.v index d6dd49a41..75d27dcaf 100644 --- a/src/Util/ZUtil/Z2Nat.v +++ b/src/Util/ZUtil/Z2Nat.v @@ -7,3 +7,41 @@ Module Z2Nat. destruct n; try reflexivity; lia. Qed. End Z2Nat. + +Module Z. + Lemma pos_pow_nat_pos : forall x n, + Z.pos x ^ Z.of_nat n > 0. + Proof. intros; apply Z.lt_gt, Z.pow_pos_nonneg; lia. Qed. + + Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> + ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. + Proof. + intros a n H; induction n as [|n IHn]; try reflexivity. + rewrite Nat2Z.inj_succ. + rewrite Nat.pow_succ_r by apply le_0_n. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite IHn. + rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. + Qed. + + Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. + Proof with auto using Zle_0_nat, Z.pow_nonneg. + intros; apply Z2Nat.inj... + rewrite <- pow_Z2N_Zpow, !Nat2Z.id... + Qed. + Hint Rewrite pow_Zpow : push_Zof_nat. + Hint Rewrite <- pow_Zpow : pull_Zof_nat. + + Lemma Zpow_sub_1_nat_pow a v + : (Z.pos a^Z.of_nat v - 1 = Z.of_nat (Z.to_nat (Z.pos a)^v - 1))%Z. + Proof. + rewrite <- (Z2Nat.id (Z.pos a)) at 1 by lia. + change 2%Z with (Z.of_nat 2); change 1%Z with (Z.of_nat 1); + autorewrite with pull_Zof_nat. + rewrite Nat2Z.inj_sub + by (change 1%nat with (Z.to_nat (Z.pos a)^0)%nat; apply Nat.pow_le_mono_r; simpl; lia). + reflexivity. + Qed. + Hint Rewrite Zpow_sub_1_nat_pow : pull_Zof_nat. + Hint Rewrite <- Zpow_sub_1_nat_pow : push_Zof_nat. +End Z. |