From 8a76415f12bb3d45e76e258245310161e102a367 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 24 Aug 2018 21:23:09 -0400 Subject: Minor improvements to various ZUtil things; bounds MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We improve the linear_substitute tactic to handle Z.opp. Also, the ZRange Z.land and Z.lor bounds are now done. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------------------- 68m36.35s | Total | 68m21.13s || +0m15.22s | +0.37% ----------------------------------------------------------------------------------------------------------------------- 0m12.24s | Util/ZRange/LandLorBounds | N/A || +0m12.24s | ∞ 0m06.17s | Util/ZUtil/LandLorBounds | 0m14.63s || -0m08.46s | -57.82% 8m48.80s | Experiments/SimplyTypedArithmetic | 8m45.78s || +0m03.01s | +0.57% 4m40.18s | Experiments/NewPipeline/Toplevel1 | 4m38.02s || +0m02.16s | +0.77% 3m45.94s | Curves/Montgomery/XZProofs | 3m44.89s || +0m01.05s | +0.46% 0m32.78s | Compilers/Z/ArithmeticSimplifierWf | 0m31.13s || +0m01.65s | +5.30% 6m03.08s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m02.74s || +0m00.33s | +0.09% 4m10.59s | Experiments/NewPipeline/RewriterRulesGood | 4m10.73s || -0m00.13s | -0.05% 2m10.48s | Specific/X25519/C64/ladderstep | 2m11.19s || -0m00.71s | -0.54% 1m51.84s | Specific/NISTP256/AMD64/femul | 1m51.84s || +0m00.00s | +0.00% 1m43.72s | Experiments/NewPipeline/Toplevel2 | 1m43.20s || +0m00.51s | +0.50% 1m31.20s | Experiments/NewPipeline/Arithmetic | 1m30.61s || +0m00.59s | +0.65% 1m29.07s | Spec/Test/X25519 | 1m29.18s || -0m00.11s | -0.12% 1m24.10s | Experiments/NewPipeline/RewriterWf2 | 1m23.42s || +0m00.67s | +0.81% 1m18.68s | Specific/X2448/Karatsuba/C64/femul | 1m18.59s || +0m00.09s | +0.11% 1m17.29s | Experiments/NewPipeline/Rewriter | 1m17.46s || -0m00.17s | -0.21% 0m59.90s | Specific/X25519/C32/femul | 0m59.59s || +0m00.30s | +0.52% 0m51.72s | Demo | 0m51.78s || -0m00.06s | -0.11% 0m50.38s | Compilers/Z/ArithmeticSimplifierInterp | 0m50.01s || +0m00.37s | +0.73% 0m49.23s | Compilers/Z/Named/RewriteAddToAdcInterp | 0m48.92s || +0m00.30s | +0.63% 0m43.78s | Specific/X25519/C32/fesquare | 0m43.51s || +0m00.27s | +0.62% 0m43.02s | Arithmetic/Karatsuba | 0m42.29s || +0m00.73s | +1.72% 0m42.02s | Experiments/NewPipeline/AbstractInterpretationWf | 0m42.36s || -0m00.33s | -0.80% 0m38.40s | p521_32.c | 0m38.57s || -0m00.17s | -0.44% 0m37.34s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.02s || +0m00.32s | +0.86% 0m36.09s | Spec/Ed25519 | 0m36.03s || +0m00.06s | +0.16% 0m35.63s | Experiments/NewPipeline/LanguageInversion | 0m35.62s || +0m00.01s | +0.02% 0m34.48s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m34.53s || -0m00.05s | -0.14% 0m33.82s | Specific/X25519/C32/freeze | 0m34.09s || -0m00.27s | -0.79% 0m32.01s | p521_64.c | 0m32.30s || -0m00.28s | -0.89% 0m27.47s | Specific/NISTP256/AMD128/femul | 0m27.77s || -0m00.30s | -1.08% 0m26.65s | Primitives/EdDSARepChange | 0m26.80s || -0m00.15s | -0.55% 0m25.91s | Experiments/NewPipeline/UnderLetsProofs | 0m25.65s || +0m00.26s | +1.01% 0m25.41s | Specific/X25519/C32/fecarry | 0m25.35s || +0m00.05s | +0.23% 0m25.40s | Experiments/NewPipeline/AbstractInterpretationZRangeProofs | 0m24.94s || +0m00.45s | +1.84% 0m23.63s | p384_32.c | 0m23.59s || +0m00.03s | +0.16% 0m22.51s | Experiments/NewPipeline/LanguageWf | 0m22.62s || -0m00.10s | -0.48% 0m21.78s | Arithmetic/Core | 0m21.55s || +0m00.23s | +1.06% 0m21.47s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.96s || +0m00.50s | +2.43% 0m21.43s | Specific/X25519/C32/fesub | 0m21.62s || -0m00.19s | -0.87% 0m20.97s | Specific/NISTP256/AMD64/fesub | 0m20.87s || +0m00.09s | +0.47% 0m20.68s | Specific/X25519/C64/femul | 0m20.39s || +0m00.28s | +1.42% 0m19.56s | Specific/X25519/C32/Synthesis | 0m19.55s || +0m00.00s | +0.05% 0m19.18s | Specific/X25519/C32/feadd | 0m19.13s || +0m00.05s | +0.26% 0m19.06s | Specific/NISTP256/AMD64/feadd | 0m19.12s || -0m00.06s | -0.31% 0m18.85s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m19.00s || -0m00.14s | -0.78% 0m18.04s | Compilers/Z/CNotations | 0m17.97s || +0m00.07s | +0.38% 0m17.68s | Specific/X25519/C64/freeze | 0m17.66s || +0m00.01s | +0.11% 0m17.44s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs | 0m17.56s || -0m00.11s | -0.68% 0m17.01s | Specific/X25519/C64/fesquare | 0m16.94s || +0m00.07s | +0.41% 0m15.88s | Specific/NISTP256/AMD64/feopp | 0m16.01s || -0m00.13s | -0.81% 0m14.93s | Specific/NISTP256/AMD128/fesub | 0m14.82s || +0m00.10s | +0.74% 0m14.89s | Specific/NISTP256/AMD128/feadd | 0m15.02s || -0m00.12s | -0.86% 0m14.33s | Specific/NISTP256/AMD64/fenz | 0m14.34s || -0m00.00s | -0.06% 0m14.12s | Specific/X25519/C64/fecarry | 0m14.02s || +0m00.09s | +0.71% 0m14.00s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.77s || +0m00.23s | +1.67% 0m13.66s | Arithmetic/Saturated/AddSub | 0m13.84s || -0m00.17s | -1.30% 0m13.53s | Specific/NISTP256/AMD128/fenz | 0m13.56s || -0m00.03s | -0.22% 0m13.18s | Specific/X25519/C64/fesub | 0m12.97s || +0m00.20s | +1.61% 0m13.10s | Experiments/NewPipeline/CStringification | 0m13.06s || +0m00.03s | +0.30% 0m12.48s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m12.53s || -0m00.04s | -0.39% 0m12.42s | Compilers/Z/Syntax/Equality | 0m12.57s || -0m00.15s | -1.19% 0m12.08s | Specific/NISTP256/AMD128/feopp | 0m12.18s || -0m00.09s | -0.82% 0m12.00s | Specific/X25519/C64/feadd | 0m11.94s || +0m00.06s | +0.50% 0m11.80s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs | 0m11.72s || +0m00.08s | +0.68% 0m11.46s | Arithmetic/Saturated/MontgomeryAPI | 0m11.59s || -0m00.12s | -1.12% 0m10.69s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.49s || +0m00.19s | +1.90% 0m10.66s | Arithmetic/Saturated/Core | 0m10.78s || -0m00.11s | -1.11% 0m10.64s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs | 0m10.62s || +0m00.02s | +0.18% 0m09.82s | Specific/X2448/Karatsuba/C64/Synthesis | 0m09.83s || -0m00.00s | -0.10% 0m09.44s | Util/ZRange/CornersMonotoneBounds | 0m09.37s || +0m00.07s | +0.74% 0m09.33s | LegacyArithmetic/Double/Proofs/Multiply | 0m09.28s || +0m00.05s | +0.53% 0m08.92s | LegacyArithmetic/ArchitectureToZLikeProofs | 0m08.73s || +0m00.18s | +2.17% 0m08.74s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.56s || +0m00.17s | +2.10% 0m08.50s | p384_64.c | 0m08.60s || -0m00.09s | -1.16% 0m08.32s | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m08.25s || +0m00.07s | +0.84% 0m08.12s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m08.20s || -0m00.08s | -0.97% 0m07.89s | Arithmetic/MontgomeryReduction/Proofs | 0m08.08s || -0m00.19s | -2.35% 0m06.98s | Specific/NISTP256/AMD64/Synthesis | 0m07.00s || -0m00.01s | -0.28% 0m06.62s | Arithmetic/Saturated/MulSplit | 0m06.62s || +0m00.00s | +0.00% 0m06.42s | Compilers/Z/Bounds/InterpretationLemmas/PullCast | 0m06.44s || -0m00.02s | -0.31% 0m06.41s | Util/FixedWordSizesEquality | 0m06.51s || -0m00.09s | -1.53% 0m06.33s | Util/ZUtil/Modulo | 0m06.10s || +0m00.23s | +3.77% 0m06.20s | Util/ZUtil/Morphisms | 0m06.25s || -0m00.04s | -0.79% 0m06.18s | Arithmetic/BarrettReduction/Generalized | 0m06.20s || -0m00.02s | -0.32% 0m05.92s | Specific/X25519/C64/Synthesis | 0m05.90s || +0m00.01s | +0.33% 0m05.70s | LegacyArithmetic/Pow2BaseProofs | 0m05.73s || -0m00.03s | -0.52% 0m05.66s | LegacyArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.62s || +0m00.04s | +0.71% 0m05.59s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.60s || -0m00.00s | -0.17% 0m05.54s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.36s || +0m00.17s | +3.35% 0m05.45s | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate | 0m05.37s || +0m00.08s | +1.48% 0m05.41s | Compilers/Z/HexNotationConstants | 0m05.40s || +0m00.00s | +0.18% 0m04.77s | Experiments/NewPipeline/RewriterWf1 | 0m04.78s || -0m00.01s | -0.20% 0m04.69s | Specific/Framework/ArithmeticSynthesis/Montgomery | 0m04.58s || +0m00.11s | +2.40% 0m04.64s | Arithmetic/BarrettReduction/HAC | 0m04.53s || +0m00.10s | +2.42% 0m04.50s | Compilers/Z/Bounds/Pipeline/Definition | 0m04.61s || -0m00.11s | -2.38% 0m04.36s | Compilers/Z/BinaryNotationConstants | 0m04.34s || +0m00.02s | +0.46% 0m04.06s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.06s || +0m00.00s | +0.00% 0m03.94s | Experiments/NewPipeline/MiscCompilerPassesProofs | 0m03.94s || +0m00.00s | +0.00% 0m03.90s | Arithmetic/MontgomeryReduction/WordByWord/Proofs | 0m03.78s || +0m00.12s | +3.17% 0m03.90s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m03.88s || +0m00.02s | +0.51% 0m03.76s | p256_32.c | 0m03.81s || -0m00.05s | -1.31% 0m03.76s | secp256k1_32.c | 0m03.86s || -0m00.10s | -2.59% 0m03.68s | LegacyArithmetic/Double/Proofs/ShiftRight | 0m03.60s || +0m00.08s | +2.22% 0m03.67s | Util/ZUtil/LandLorShiftBounds | 0m03.60s || +0m00.06s | +1.94% 0m03.57s | Util/ZUtil/Shift | 0m03.53s || +0m00.04s | +1.13% 0m03.50s | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy | 0m03.45s || +0m00.04s | +1.44% 0m03.49s | Compilers/Z/ArithmeticSimplifier | 0m03.48s || +0m00.01s | +0.28% 0m03.32s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.30s || +0m00.02s | +0.60% 0m03.31s | LegacyArithmetic/InterfaceProofs | 0m03.28s || +0m00.03s | +0.91% 0m03.27s | Specific/NISTP256/AMD128/Synthesis | 0m03.30s || -0m00.02s | -0.90% 0m03.18s | Util/ZUtil/Div | 0m03.19s || -0m00.00s | -0.31% 0m03.06s | LegacyArithmetic/Double/Proofs/Decode | 0m03.11s || -0m00.04s | -1.60% 0m03.06s | LegacyArithmetic/Double/Proofs/ShiftLeft | 0m03.04s || +0m00.02s | +0.65% 0m02.96s | Util/WordUtil | 0m02.98s || -0m00.02s | -0.67% 0m02.86s | LegacyArithmetic/ZBoundedZ | 0m02.86s || +0m00.00s | +0.00% 0m02.60s | LegacyArithmetic/BarretReduction | 0m02.66s || -0m00.06s | -2.25% 0m02.54s | Arithmetic/Saturated/Freeze | 0m02.60s || -0m00.06s | -2.30% 0m02.50s | Arithmetic/ModularArithmeticTheorems | 0m02.48s || +0m00.02s | +0.80% 0m02.34s | Specific/NISTP256/FancyMachine256/Montgomery | 0m02.34s || +0m00.00s | +0.00% 0m02.33s | Specific/NISTP256/FancyMachine256/Core | 0m02.33s || +0m00.00s | +0.00% 0m02.26s | Specific/NISTP256/FancyMachine256/Barrett | 0m02.29s || -0m00.03s | -1.31% 0m02.25s | Compilers/Z/RewriteAddToAdcInterp | 0m02.09s || +0m00.16s | +7.65% 0m02.19s | Compilers/Z/Bounds/Relax | 0m02.20s || -0m00.01s | -0.45% 0m02.17s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.46% 0m02.13s | Util/ZUtil/Quot | 0m02.13s || +0m00.00s | +0.00% 0m02.12s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m02.19s || -0m00.06s | -3.19% 0m02.12s | Util/ZRange/SplitBounds | 0m02.06s || +0m00.06s | +2.91% 0m02.11s | p224_32.c | 0m02.10s || +0m00.00s | +0.47% 0m01.90s | Compilers/Z/JavaNotations | 0m01.90s || +0m00.00s | +0.00% 0m01.89s | Util/ZUtil/AddGetCarry | 0m01.90s || -0m00.01s | -0.52% 0m01.78s | Specific/Framework/ReificationTypes | 0m01.70s || +0m00.08s | +4.70% 0m01.76s | LegacyArithmetic/MontgomeryReduction | 0m01.76s || +0m00.00s | +0.00% 0m01.73s | Util/ZUtil/Pow2Mod | 0m01.68s || +0m00.05s | +2.97% 0m01.65s | Arithmetic/CoreUnfolder | 0m01.67s || -0m00.02s | -1.19% 0m01.55s | p224_64.c | 0m01.69s || -0m00.13s | -8.28% 0m01.54s | Specific/Framework/OutputType | 0m01.48s || +0m00.06s | +4.05% 0m01.54s | Util/ZUtil/Ones | 0m01.42s || +0m00.12s | +8.45% 0m01.52s | p256_64.c | 0m01.64s || -0m00.11s | -7.31% 0m01.50s | secp256k1_64.c | 0m01.63s || -0m00.12s | -7.97% 0m01.48s | Specific/Framework/ArithmeticSynthesis/Base | 0m01.53s || -0m00.05s | -3.26% 0m01.44s | Arithmetic/BarrettReduction/Wikipedia | 0m01.39s || +0m00.05s | +3.59% 0m01.43s | Experiments/NewPipeline/CLI | 0m01.42s || +0m00.01s | +0.70% 0m01.43s | LegacyArithmetic/Double/Proofs/BitwiseOr | 0m01.39s || +0m00.04s | +2.87% 0m01.37s | curve25519_64.c | 0m01.38s || -0m00.00s | -0.72% 0m01.36s | Util/QUtil | 0m01.36s || +0m00.00s | +0.00% 0m01.34s | Arithmetic/PrimeFieldTheorems | 0m01.24s || +0m00.10s | +8.06% 0m01.34s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m01.37s || -0m00.03s | -2.18% 0m01.31s | Util/ZUtil/Testbit | 0m01.24s || +0m00.07s | +5.64% 0m01.30s | Util/ZRange/BasicLemmas | 0m01.23s || +0m00.07s | +5.69% 0m01.26s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.26s || +0m00.00s | +0.00% 0m01.25s | Compilers/Z/Syntax/Util | 0m01.17s || +0m00.08s | +6.83% 0m01.23s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.23s || +0m00.00s | +0.00% 0m01.19s | Experiments/NewPipeline/Language | 0m01.14s || +0m00.05s | +4.38% 0m01.18s | LegacyArithmetic/Double/Proofs/LoadImmediate | 0m01.12s || +0m00.05s | +5.35% 0m01.14s | Arithmetic/Saturated/CoreUnfolder | 0m01.16s || -0m00.02s | -1.72% 0m01.08s | Compilers/Z/RewriteAddToAdcWf | 0m01.09s || -0m00.01s | -0.91% 0m01.07s | Experiments/NewPipeline/CompilersTestCases | 0m01.02s || +0m00.05s | +4.90% 0m01.05s | Experiments/NewPipeline/AbstractInterpretation | 0m01.05s || +0m00.00s | +0.00% 0m01.01s | Util/ZUtil/Stabilization | 0m00.94s || +0m00.07s | +7.44% 0m00.99s | Experiments/NewPipeline/RewriterProofs | 0m00.89s || +0m00.09s | +11.23% 0m00.98s | Util/ZUtil/Modulo/PullPush | 0m00.95s || +0m00.03s | +3.15% 0m00.97s | Arithmetic/Saturated/WrappersUnfolder | 0m01.01s || -0m00.04s | -3.96% 0m00.94s | Compilers/Z/CommonSubexpressionElimination | 0m00.95s || -0m00.01s | -1.05% 0m00.94s | Specific/Framework/SynthesisFramework | 0m01.07s || -0m00.13s | -12.14% 0m00.90s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.93s || -0m00.03s | -3.22% 0m00.88s | Arithmetic/Saturated/UniformWeight | 0m01.02s || -0m00.14s | -13.72% 0m00.88s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.84s || +0m00.04s | +4.76% 0m00.87s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.79s || +0m00.07s | +10.12% 0m00.85s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.72s || +0m00.13s | +18.05% 0m00.84s | Specific/Framework/IntegrationTestDisplayCommon | 0m01.00s || -0m00.16s | -16.00% 0m00.84s | Util/NumTheoryUtil | 0m00.87s || -0m00.03s | -3.44% 0m00.80s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.74s || +0m00.06s | +8.10% 0m00.80s | Arithmetic/Saturated/MulSplitUnfolder | 0m00.94s || -0m00.13s | -14.89% 0m00.78s | Specific/Framework/MontgomeryReificationTypes | 0m00.72s || +0m00.06s | +8.33% 0m00.78s | Util/ZUtil/Log2 | 0m00.80s || -0m00.02s | -2.50% 0m00.77s | Util/ZUtil/Divide | 0m00.76s || +0m00.01s | +1.31% 0m00.77s | Util/ZUtil/ZSimplify/Simple | 0m00.80s || -0m00.03s | -3.75% 0m00.76s | Specific/Framework/ArithmeticSynthesis/HelperTactics | 0m00.72s || +0m00.04s | +5.55% 0m00.76s | Util/ZUtil/EquivModulo | 0m00.77s || -0m00.01s | -1.29% 0m00.74s | Experiments/NewPipeline/MiscCompilerPasses | 0m00.74s || +0m00.00s | +0.00% 0m00.74s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.71s || +0m00.03s | +4.22% 0m00.74s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.72s || +0m00.02s | +2.77% 0m00.74s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.68s || +0m00.05s | +8.82% 0m00.74s | Util/ZUtil/CC | 0m00.78s || -0m00.04s | -5.12% 0m00.73s | Arithmetic/Saturated/FreezeUnfolder | 0m00.77s || -0m00.04s | -5.19% 0m00.72s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.66s || +0m00.05s | +9.09% 0m00.71s | Arithmetic/Saturated/Wrappers | 0m00.75s || -0m00.04s | -5.33% 0m00.70s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.76s || -0m00.06s | -7.89% 0m00.70s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.73s || -0m00.03s | -4.10% 0m00.68s | Util/ZUtil/Rshi | 0m00.72s || -0m00.03s | -5.55% 0m00.67s | Specific/Framework/ReificationTypesPackage | 0m00.72s || -0m00.04s | -6.94% 0m00.65s | Arithmetic/Saturated/UniformWeightInstances | 0m00.69s || -0m00.03s | -5.79% 0m00.65s | LegacyArithmetic/Double/Proofs/SelectConditional | 0m00.65s || +0m00.00s | +0.00% 0m00.64s | Specific/Framework/ArithmeticSynthesis/Ladderstep | 0m00.75s || -0m00.10s | -14.66% 0m00.63s | Compilers/Z/Named/RewriteAddToAdc | 0m00.60s || +0m00.03s | +5.00% 0m00.61s | Compilers/Z/Bounds/MapCastByDeBruijnInterp | 0m00.58s || +0m00.03s | +5.17% 0m00.61s | Compilers/Z/Bounds/Pipeline | 0m00.68s || -0m00.07s | -10.29% 0m00.60s | Compilers/Z/Bounds/InterpretationLemmas/Tactics | 0m00.92s || -0m00.32s | -34.78% 0m00.57s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.46s || +0m00.10s | +23.91% 0m00.57s | Compilers/Z/Reify | 0m00.59s || -0m00.02s | -3.38% 0m00.56s | Compilers/Z/CommonSubexpressionEliminationWf | 0m00.52s || +0m00.04s | +7.69% 0m00.56s | Compilers/Z/MapCastByDeBruijnInterp | 0m00.53s || +0m00.03s | +5.66% 0m00.54s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.59s || -0m00.04s | -8.47% 0m00.54s | Compilers/Z/Bounds/RoundUpLemmas | 0m00.55s || -0m00.01s | -1.81% 0m00.54s | Compilers/Z/InlineConstAndOpInterp | 0m00.54s || +0m00.00s | +0.00% 0m00.54s | LegacyArithmetic/Double/Core | 0m00.60s || -0m00.05s | -9.99% 0m00.53s | Util/NUtil | 0m00.52s || +0m00.01s | +1.92% 0m00.52s | Arithmetic/ModularArithmeticPre | 0m00.52s || +0m00.00s | +0.00% 0m00.52s | Compilers/Z/CommonSubexpressionEliminationInterp | 0m00.52s || +0m00.00s | +0.00% 0m00.52s | Compilers/Z/MapCastByDeBruijn | 0m00.46s || +0m00.06s | +13.04% 0m00.52s | Compilers/Z/RewriteAddToAdc | 0m00.50s || +0m00.02s | +4.00% 0m00.51s | LegacyArithmetic/ArchitectureToZLike | 0m00.54s || -0m00.03s | -5.55% 0m00.50s | Compilers/Z/Bounds/Interpretation | 0m00.50s || +0m00.00s | +0.00% 0m00.50s | Compilers/Z/Bounds/MapCastByDeBruijn | 0m00.49s || +0m00.01s | +2.04% 0m00.50s | Compilers/ZExtended/MapBaseType | 0m00.48s || +0m00.02s | +4.16% 0m00.49s | Compilers/Z/Bounds/MapCastByDeBruijnWf | 0m00.50s || -0m00.01s | -2.00% 0m00.49s | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.49s || +0m00.00s | +0.00% 0m00.49s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.46s || +0m00.02s | +6.52% 0m00.48s | Compilers/Z/InlineConstAndOpByRewriteInterp | 0m00.48s || +0m00.00s | +0.00% 0m00.48s | Spec/EdDSA | 0m00.70s || -0m00.21s | -31.42% 0m00.47s | Compilers/Z/GeneralizeVarWf | 0m00.48s || -0m00.01s | -2.08% 0m00.47s | Compilers/Z/Inline | 0m00.44s || +0m00.02s | +6.81% 0m00.47s | Compilers/Z/InlineConstAndOpByRewriteWf | 0m00.43s || +0m00.03s | +9.30% 0m00.47s | Compilers/Z/InlineConstAndOpWf | 0m00.48s || -0m00.01s | -2.08% 0m00.47s | Compilers/Z/InlineInterp | 0m00.45s || +0m00.01s | +4.44% 0m00.47s | Compilers/Z/Syntax | 0m00.54s || -0m00.07s | -12.96% 0m00.45s | Compilers/Z/InlineConstAndOpByRewrite | 0m00.42s || +0m00.03s | +7.14% 0m00.45s | Compilers/Z/InlineWf | 0m00.42s || +0m00.03s | +7.14% 0m00.45s | Compilers/Z/InterpSideConditions | 0m00.46s || -0m00.01s | -2.17% 0m00.45s | Compilers/Z/Named/DeadCodeEliminationInterp | 0m00.49s || -0m00.03s | -8.16% 0m00.45s | Compilers/ZExtended/Syntax | 0m00.41s || +0m00.04s | +9.75% 0m00.45s | Util/ZUtil | 0m00.42s || +0m00.03s | +7.14% 0m00.44s | Compilers/Z/InlineConstAndOp | 0m00.44s || +0m00.00s | +0.00% 0m00.44s | Compilers/Z/MapCastByDeBruijnWf | 0m00.46s || -0m00.02s | -4.34% 0m00.43s | Compilers/Z/FoldTypes | 0m00.46s || -0m00.03s | -6.52% 0m00.42s | Compilers/Z/GeneralizeVarInterp | 0m00.44s || -0m00.02s | -4.54% 0m00.41s | Experiments/NewPipeline/UnderLets | 0m00.51s || -0m00.10s | -19.60% 0m00.40s | Util/ZRange/Operations | 0m00.44s || -0m00.03s | -9.09% 0m00.40s | Util/ZUtil/CPS | 0m00.42s || -0m00.01s | -4.76% 0m00.39s | Compilers/ZExtended/Syntax/Util | 0m00.36s || +0m00.03s | +8.33% 0m00.38s | Compilers/Z/Bounds/Pipeline/OutputType | 0m00.40s || -0m00.02s | -5.00% 0m00.38s | Compilers/Z/GeneralizeVar | 0m00.35s || +0m00.03s | +8.57% 0m00.38s | Compilers/Z/Named/DeadCodeElimination | 0m00.44s || -0m00.06s | -13.63% 0m00.38s | Compilers/ZExtended/InlineConstAndOpInterp | 0m00.32s || +0m00.06s | +18.75% 0m00.36s | Util/ZUtil/MulSplit | 0m00.30s || +0m00.06s | +20.00% 0m00.36s | Util/ZUtil/ZSimplify/Core | 0m00.35s || +0m00.01s | +2.85% 0m00.35s | Compilers/ZExtended/InlineConstAndOpByRewriteInterp | 0m00.32s || +0m00.02s | +9.37% 0m00.35s | Compilers/ZExtended/InlineConstAndOpByRewriteWf | 0m00.34s || +0m00.00s | +2.94% 0m00.34s | Arithmetic/MontgomeryReduction/Definition | 0m00.38s || -0m00.03s | -10.52% 0m00.34s | Compilers/ZExtended/InlineConstAndOpWf | 0m00.33s || +0m00.01s | +3.03% 0m00.34s | Util/ZUtil/Tactics/Ztestbit | 0m00.41s || -0m00.06s | -17.07% 0m00.33s | Compilers/ZExtended/InlineConstAndOpByRewrite | 0m00.33s || +0m00.00s | +0.00% 0m00.33s | Spec/ModularArithmetic | 0m00.35s || -0m00.01s | -5.71% 0m00.32s | Compilers/Z/OpInversion | 0m00.34s || -0m00.02s | -5.88% 0m00.32s | Compilers/Z/TypeInversion | 0m00.34s || -0m00.02s | -5.88% 0m00.32s | Compilers/ZExtended/InlineConstAndOp | 0m00.33s || -0m00.01s | -3.03% 0m00.32s | Util/ZUtil/Tactics | 0m00.29s || +0m00.03s | +10.34% 0m00.32s | Util/ZUtil/Tactics/SimplifyFractionsLe | 0m00.34s || -0m00.02s | -5.88% 0m00.32s | Util/ZUtil/Tactics/ZeroBounds | 0m00.33s || -0m00.01s | -3.03% 0m00.31s | Util/ZUtil/Hints | 0m00.32s || -0m00.01s | -3.12% 0m00.31s | Util/ZUtil/Tactics/PullPush/Modulo | 0m00.32s || -0m00.01s | -3.12% 0m00.30s | Util/ZUtil/ZSimplify | 0m00.28s || +0m00.01s | +7.14% 0m00.30s | Util/ZUtil/Zselect | 0m00.27s || +0m00.02s | +11.11% 0m00.29s | Util/ZUtil/Land | 0m00.30s || -0m00.01s | -3.33% 0m00.29s | Util/ZUtil/Tactics/PullPush | 0m00.28s || +0m00.00s | +3.57% 0m00.28s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition | 0m00.24s || +0m00.04s | +16.66% 0m00.28s | Util/ZUtil/Definitions | 0m00.30s || -0m00.01s | -6.66% 0m00.28s | Util/ZUtil/Tactics/LinearSubstitute | 0m00.34s || -0m00.06s | -17.64% 0m00.27s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition | 0m00.28s || -0m00.01s | -3.57% 0m00.27s | Util/ZUtil/AddModulo | 0m00.26s || +0m00.01s | +3.84% 0m00.27s | Util/ZUtil/Opp | 0m00.32s || -0m00.04s | -15.62% --- src/Util/ZRange/BasicLemmas.v | 7 + src/Util/ZRange/LandLorBounds.v | 159 ++++++++++++++++++++ src/Util/ZRange/Operations.v | 12 +- src/Util/ZUtil/Definitions.v | 1 + src/Util/ZUtil/LandLorBounds.v | 236 +++++++++++++++++++++++++----- src/Util/ZUtil/LandLorShiftBounds.v | 41 +++++- src/Util/ZUtil/Modulo.v | 11 ++ src/Util/ZUtil/Ones.v | 38 +++++ src/Util/ZUtil/Tactics/LinearSubstitute.v | 8 + src/Util/ZUtil/ZSimplify/Core.v | 10 +- src/Util/ZUtil/ZSimplify/Simple.v | 3 + 11 files changed, 469 insertions(+), 57 deletions(-) create mode 100644 src/Util/ZRange/LandLorBounds.v (limited to 'src') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 6cfdaaff8..4bdcb19ef 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -71,6 +71,9 @@ Module ZRange. | progress specialize_by omega | progress destruct_head'_or ]. + Lemma is_tighter_than_bool_extend_land_lor_bounds r : is_tighter_than_bool r (extend_land_lor_bounds r) = true. + Proof. repeat t2_step. Qed. + Lemma is_bounded_by_iff_is_tighter_than r1 r2 : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true) <-> (is_tighter_than_bool r1 r2 = true \/ goodb r1 = false). @@ -92,6 +95,10 @@ Module ZRange. rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; etransitivity; destruct_head'_and; eassumption. Qed. + Lemma is_bounded_by_of_is_tighter_than r1 r2 (H : is_tighter_than_bool r1 r2 = true) + : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true). + Proof. apply is_bounded_by_iff_is_tighter_than; auto. Qed. + Lemma is_bounded_by_bool_Proper_if_sumbool_union_dep {A B} (b : sumbool A B) x y rx ry : (A -> is_bounded_by_bool x rx = true) -> (B -> is_bounded_by_bool y ry = true) diff --git a/src/Util/ZRange/LandLorBounds.v b/src/Util/ZRange/LandLorBounds.v new file mode 100644 index 000000000..dd538d967 --- /dev/null +++ b/src/Util/ZRange/LandLorBounds.v @@ -0,0 +1,159 @@ +Require Import Coq.Classes.Morphisms. +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.LandLorBounds. +Require Import Crypto.Util.ZUtil.Morphisms. +Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZRange.BasicLemmas. +Require Import Crypto.Util.ZRange.CornersMonotoneBounds. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. + +Local Open Scope bool_scope. +Local Open Scope Z_scope. + +Module ZRange. + Import Operations.ZRange. + Import CornersMonotoneBounds.ZRange. + + Lemma is_bounded_by_bool_lor_land_bound_helper + f (Hf : f = Z.lor \/ f = Z.land) + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_tighter_than_bool + (constant (f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y))) + (four_corners_and_zero (fun x y => f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y)) x_bs y_bs) + = true. + Proof. + apply monotoneb_four_corners_and_zero_gen with (x:=x) (y:=y); + destruct_head'_or; subst f; eauto with typeclass_instances zarith core. + Qed. + + Local Existing Instances Z.land_round_Proper_pos_r + Z.land_round_Proper_pos_l + Z.lor_round_Proper_pos_r + Z.lor_round_Proper_pos_l + Z.land_round_Proper_neg_r + Z.land_round_Proper_neg_l + Z.lor_round_Proper_neg_r + Z.lor_round_Proper_neg_l. + + Lemma is_bounded_by_bool_land_lor_bounds_helper + f (Hf : f = Z.lor \/ f = Z.land) + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (f x y) (land_lor_bounds f x_bs y_bs) = true. + Proof. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs)) as H. + pose proof (fun pf1 pf2 => is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs) pf2 pf1) as H0x. + pose proof (fun pf1 pf2 => is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs) pf2 pf1) as Hm1x. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as H0y. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as Hm1y. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as H00. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as Hm10. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as H0m1. + pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as Hm1m1. + specialize_by (eapply ZRange.is_bounded_by_of_is_tighter_than; try eapply ZRange.is_tighter_than_bool_extend_land_lor_bounds; eassumption || reflexivity). + revert H H0x Hm1x H0y Hm1y H00 Hm1m1 H0m1 Hm10. + cbv [land_lor_bounds constant is_tighter_than_bool is_bounded_by_bool is_true] in *; cbn [lower upper] in *. + rewrite !Bool.andb_true_iff, !Z.leb_le in *. + cbv [extend_land_lor_bounds]. + cbn [lower upper] in *. + destruct (Z.round_lor_land_bound_bounds x) as [Hx|Hx], (Z.round_lor_land_bound_bounds y) as [Hy|Hy]. + all: repeat apply Z.min_case_strong; repeat apply Z.max_case_strong. + all: try (intros; exfalso; clear dependent f; lia). + all: destruct x as [|x|x], y as [|y|y]; try (intros; exfalso; clear dependent f; lia). + all: change (Z.round_lor_land_bound 0) with 0 in *. + all: change (Z.round_lor_land_bound (-1)) with (-1) in *. + all: intros. + all: repeat match goal with + | _ => assumption + | [ H : ?T, H' : ?T |- _ ] => clear H' + | [ H : 0 <= 0 <= 0 |- _ ] => clear H + | [ H : 0 <= -1 <= _ -> _ |- _ ] => clear H + | [ H : 0 <= -1 -> _ |- _ ] => clear H + | [ H : ?x <= ?x <= _ -> _ |- _ ] => specialize (fun pf => H (conj (@Z.le_refl x) pf)) + | [ H : _ <= ?x <= ?x -> _ |- _ ] => specialize (fun pf => H (conj pf (@Z.le_refl x))) + | [ H : ?T, H' : ?T /\ _ -> _ |- _ ] => specialize (fun pf => H' (conj H pf)) + | [ H : ?T, H' : _ /\ ?T -> _ |- _ ] => specialize (fun pf => H' (conj pf H)) + | _ => progress specialize_by_assumption + | _ => progress specialize_by (destruct_head'_and; assumption) + | [ H : _ <= Z.pos _ <= ?x |- _ ] => unique assert (0 <= x) by (clear -H; lia) + | [ H : ?x <= Z.neg _ <= _ |- _ ] => unique assert (x <= -1) by (clear -H; lia) + | [ H : ?a <= _ <= ?c, H' : ?c <= ?d, H'' : ?a <= ?d -> _ |- _ ] + => unique assert (a <= d) by (clear -H H'; lia) + | [ H : ?a <= ?b -> ?c <= ?d <= ?e -> _ |- _ ] => specialize (fun pf1 pf2 => H pf2 pf1) + end. + all: destruct Hf; subst f. + all: split. + all: destruct_head'_and. + all: split_and. + all: repeat lazymatch goal with + | [ |- Z.land _ (Z.pos ?x) <= _ ] + => is_var x; etransitivity; [ apply Z.land_round_bound_pos_r' | ] + | [ |- Z.land (Z.pos ?x) _ <= _ ] + => is_var x; etransitivity; [ apply Z.land_round_bound_pos_l' | ] + | [ |- _ <= Z.land _ (Z.pos ?x) ] + => is_var x; etransitivity; [ | apply Z.land_round_bound_pos_r ] + | [ |- _ <= Z.land (Z.pos ?x) _ ] + => is_var x; etransitivity; [ | apply Z.land_round_bound_pos_l ] + | [ |- Z.land _ (Z.neg ?x) <= _ ] + => is_var x; etransitivity; [ apply Z.land_round_bound_neg_r | ] + | [ |- Z.land (Z.neg ?x) _ <= _ ] + => is_var x; etransitivity; [ apply Z.land_round_bound_neg_l | ] + | [ |- _ <= Z.land _ (Z.neg ?x) ] + => is_var x; etransitivity; [ | apply Z.land_round_bound_neg_r' ] + | [ |- _ <= Z.land (Z.neg ?x) _ ] + => is_var x; etransitivity; [ | apply Z.land_round_bound_neg_l' ] + | [ |- Z.lor _ (Z.pos ?x) <= _ ] + => is_var x; etransitivity; [ apply Z.lor_round_bound_pos_r' | ] + | [ |- Z.lor (Z.pos ?x) _ <= _ ] + => is_var x; etransitivity; [ apply Z.lor_round_bound_pos_l' | ] + | [ |- _ <= Z.lor _ (Z.pos ?x) ] + => is_var x; etransitivity; [ | apply Z.lor_round_bound_pos_r ] + | [ |- _ <= Z.lor (Z.pos ?x) _ ] + => is_var x; etransitivity; [ | apply Z.lor_round_bound_pos_l ] + | [ |- Z.lor _ (Z.neg ?x) <= _ ] + => is_var x; etransitivity; [ apply Z.lor_round_bound_neg_r | ] + | [ |- Z.lor (Z.neg ?x) _ <= _ ] + => is_var x; etransitivity; [ apply Z.lor_round_bound_neg_l | ] + | [ |- _ <= Z.lor _ (Z.neg ?x) ] + => is_var x; etransitivity; [ | apply Z.lor_round_bound_neg_r' ] + | [ |- _ <= Z.lor (Z.neg ?x) _ ] + => is_var x; etransitivity; [ | apply Z.lor_round_bound_neg_l' ] + | [ |- Z.pos ?x <= _ ] + => is_var x; etransitivity; [ eassumption | ] + | [ |- _ <= Z.neg ?x ] + => is_var x; etransitivity; [ | eassumption ] + | [ |- _ <= Z.pos ?x ] + => is_var x; transitivity 0; [ assumption | lia ] + | [ |- Z.neg ?x <= _ ] + => is_var x; transitivity (-1); [ lia | assumption ] + | _ => idtac + end. + all: try assumption. + all: try (rewrite ?Z.lor_0_l, ?Z.lor_0_r, ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_m1_l, ?Z.lor_m1_r, ?Z.land_m1_l, ?Z.land_m1_r in *; reflexivity || assumption). + Qed. + + Lemma is_bounded_by_bool_land_bounds + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.land x y) (ZRange.land_bounds x_bs y_bs) = true. + Proof. apply is_bounded_by_bool_land_lor_bounds_helper; auto. Qed. + + Lemma is_bounded_by_bool_lor_bounds + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.lor x y) (ZRange.lor_bounds x_bs y_bs) = true. + Proof. apply is_bounded_by_bool_land_lor_bounds_helper; auto. Qed. +End ZRange. diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 130fdc0c4..c6f209e16 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -145,13 +145,13 @@ Module ZRange. rewrite Z.max_comm; reflexivity. Qed. - (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *) - Definition round_lor_land_bound (x : BinInt.Z) : BinInt.Z - := if (0 <=? x)%Z - then 2^(Z.log2_up (x+1))-1 - else -2^(Z.log2_up (-x)). + Definition extend_land_lor_bounds (v : zrange) : zrange + := let (l, u) := eta v in + r[ Z.min 0 l ~> Z.max (-1) u ]. + Definition land_lor_bounds (f : BinInt.Z -> BinInt.Z -> BinInt.Z) (x y : zrange) : zrange - := four_corners_and_zero (fun x y => f (round_lor_land_bound x) (round_lor_land_bound y)) x y. + := four_corners_and_zero (fun x y => f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y)) + (extend_land_lor_bounds x) (extend_land_lor_bounds y). Definition land_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.land. Definition lor_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.lor. diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index 4ef6b5403..8fe5772f5 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -85,6 +85,7 @@ Module Z. then mul_split_at_bitwidth (Z.log2 s) x y else ((x * y) mod s, (x * y) / s). + (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *) Definition round_lor_land_bound (x : Z) : Z := if (0 <=? x)%Z then 2^(Z.log2_up (x+1))-1 diff --git a/src/Util/ZUtil/LandLorBounds.v b/src/Util/ZUtil/LandLorBounds.v index 1b10ecf97..78866ec7f 100644 --- a/src/Util/ZUtil/LandLorBounds.v +++ b/src/Util/ZUtil/LandLorBounds.v @@ -3,8 +3,17 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Log2. Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. +Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.ZUtil.Ones. Require Import Crypto.Util.ZUtil.Lnot. Require Import Crypto.Util.ZUtil.Land. @@ -14,10 +23,34 @@ Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. Module Z. + Lemma round_lor_land_bound_bounds x + : (0 <= x <= Z.round_lor_land_bound x) \/ (Z.round_lor_land_bound x <= x <= -1). + Proof. + cbv [Z.round_lor_land_bound]; break_innermost_match; Z.ltb_to_lt. + all: constructor; split; try lia; []. + all: Z.replace_all_neg_with_pos. + all: match goal with |- context[2^Z.log2_up ?x] => pose proof (Z.log2_up_le_full x) end. + all: lia. + Qed. + Hint Resolve round_lor_land_bound_bounds : zarith. + + Lemma round_lor_land_bound_bounds_pos x + : (0 <= Z.pos x <= Z.round_lor_land_bound (Z.pos x)). + Proof. generalize (round_lor_land_bound_bounds (Z.pos x)); lia. Qed. + Hint Resolve round_lor_land_bound_bounds_pos : zarith. + + Lemma round_lor_land_bound_bounds_neg x + : Z.round_lor_land_bound (Z.neg x) <= Z.neg x <= -1. + Proof. generalize (round_lor_land_bound_bounds (Z.neg x)); lia. Qed. + Hint Resolve round_lor_land_bound_bounds_neg : zarith. + Local Ltac saturate := repeat first [ progress cbv [Z.round_lor_land_bound Proper respectful Basics.flip] in * - | progress cbn in * + | progress Z.ltb_to_lt | progress intros + | break_innermost_match_step + | lia + | rewrite !Pos2Z.opp_neg | match goal with | [ |- context[Z.log2_up ?x] ] => unique pose proof (Z.log2_up_nonneg x) @@ -29,13 +62,18 @@ Module Z. => unique assert (Z.pos x <= Z.pos y) by lia | [ H : Pos.le ?x ?y |- context[Z.pos (?x+1)] ] => unique assert (Z.pos (x+1) <= Z.pos (y+1)) by lia + | [ H : Z.le ?x ?y |- context[?x+1] ] + => unique assert (x+1 <= y+1) by lia | [ H : Z.le ?x ?y |- context[2^Z.log2_up ?x] ] => unique assert (2^Z.log2_up x <= 2^Z.log2_up y) by (Z.peel_le; lia) + | [ H : ?a^?b <= ?a^?c |- _ ] + => unique assert (a^(c-b) = a^c/a^b) by auto with zarith; + unique assert (a^c mod a^b = 0) by auto with zarith end ]. Local Ltac do_rewrites_step := match goal with | [ |- ?R ?x ?x ] => reflexivity - | [ |- context[Z.land (-2^_) (-2^_)] ] + (*| [ |- context[Z.land (-2^_) (-2^_)] ] => rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_lor, !Z.lor_ones_ones, !Z.lnot_ones_equiv | [ |- context[Z.lor (-2^_) (-2^_)] ] => rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_land, !Z.land_ones_ones, !Z.lnot_ones_equiv @@ -52,8 +90,45 @@ Module Z. | [ |- context[Z.lor (-2^?x) (2^?y-1)] ] => rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive (2^y-1)), <- !Z.lnot_land, ?Z.lnot_ones_equiv, (Z.lnot_sub1 (2^y)), !Z.ones_equiv, ?Z.lnot_equiv, <- !Z.sub_1_r | [ |- context[-?x mod ?y] ] - => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod - | [ H : ?x <= ?x |- _ ] => clear H + => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod*) + | [ |- context[Z.land (2^?y-1) ?x] ] + => is_var x; rewrite (Z.land_comm (2^y-1) x) + | [ |- context[Z.lor (2^?y-1) ?x] ] + => is_var x; rewrite (Z.lor_comm (2^y-1) x) + | [ |- context[Z.land (-2^?y) ?x] ] + => is_var x; rewrite (Z.land_comm (-2^y) x) + | [ |- context[Z.lor (-2^?y) ?x] ] + => is_var x; rewrite (Z.lor_comm (-2^y) x) + | [ |- context[Z.land _ (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones by auto with zarith + | [ |- context[Z.land ?x (-2^?y)] ] + => is_var x; + rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive x), <- !Z.lnot_lor, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r; + let x' := fresh in + remember (-x-1) as x' eqn:?; Z.linear_substitute x; + rename x' into x + | [ |- context[Z.lor ?x (-2^?y)] ] + => is_var x; + rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive x), <- !Z.lnot_land, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r; + let x' := fresh in + remember (-x-1) as x' eqn:?; Z.linear_substitute x; + rename x' into x + | [ |- Z.lor ?x (?y-1) <= Z.lor ?x (?y'-1) ] + => rewrite (Z.div_mod'' (Z.lor x (y-1)) y), (Z.div_mod'' (Z.lor x (y'-1)) y') by auto with zarith + | [ |- Z.lor ?x (?y-1) = _ ] + => rewrite (Z.div_mod'' (Z.lor x (y-1)) y) by auto with zarith + | [ |- context[?m1 - 1 + (?x - ?x mod ?m1)] ] + => replace (m1 - 1 + (x - x mod m1)) with ((m1 - x mod m1) + (x - 1)) by lia + | _ => progress rewrite ?Z.lor_pow2_div_pow2_r, ?Z.lor_pow2_div_pow2_l, ?Z.lor_pow2_mod_pow2_r, ?Z.lor_pow2_mod_pow2_l by auto with zarith + | _ => rewrite !Z.mul_div_eq by lia + | _ => progress rewrite ?(Z.add_comm 1) in * + | [ |- context[?x mod 2^(Z.log2_up (?x + 1))] ] + => rewrite (Z.mod_small x (2^Z.log2_up (x+1))) by (rewrite <- Z.le_succ_l, <- Z.add_1_r, Z.log2_up_le_pow2 by lia; lia) + | [ H : ?a^?b <= ?a^?c |- context[?x mod ?a^?b] ] + => rewrite (@Z.mod_pow_r_split x a b c) by auto with zarith; + (Z.div_mod_to_quot_rem; nia) + | _ => progress Z.peel_le + (*| [ H : ?x <= ?x |- _ ] => clear H | [ H : ?x < ?y, H' : ?y <= ?z |- _ ] => unique assert (x < z) by lia | [ H : ?x < ?y, H' : ?a <= ?x |- _ ] => unique assert (a < y) by lia | [ H : 2^?x < 2^?y |- context[2^?x mod 2^?y] ] @@ -65,8 +140,15 @@ Module Z. destruct (@Z.pow2_lt_or_divides x y ltac:(lia)) as [H|H]; [ repeat first [ rewrite (Z.mod_small (2^x) (2^y)) by lia | rewrite !(@Z_mod_nz_opp_full (2^x) (2^y)) ] - | rewrite H ] - | _ => progress autorewrite with zsimplify_const + | rewrite H ]*) + | _ => progress autorewrite with zsimplify_fast in * + | [ |- context[-(-?x-1)] ] => replace (-(-x-1)) with (1+x) by lia + | [ H : 0 > -(1+?x) |- _ ] => assert (0 <= x) by (clear -H; lia); clear H + | [ H : 0 > -(?x+1) |- _ ] => assert (0 <= x) by (clear -H; lia); clear H + | [ |- ?a - ?b = ?a' - ?b' ] => apply f_equal2; try reflexivity; [] + | [ |- -?a = -?a' ] => apply f_equal + | _ => rewrite <- !Z.sub_1_r + | _ => lia end. Local Ltac do_rewrites := repeat do_rewrites_step. Local Ltac fin_t := @@ -80,53 +162,129 @@ Module Z. | lia | progress Z.peel_le ]. Local Ltac t := - saturate; do_rewrites; fin_t. + saturate; do_rewrites. Local Instance land_round_Proper_pos_r x - : Proper (Pos.le ==> Z.le) - (fun y => - Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))). - Proof. destruct x; t. Qed. + : Proper (Pos.le ==> Z.le) (fun y => Z.land x (Z.round_lor_land_bound (Z.pos y))). + Proof. t. Qed. Local Instance land_round_Proper_pos_l y - : Proper (Pos.le ==> Z.le) - (fun x => - Z.land (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)). - Proof. destruct y; t. Qed. + : Proper (Pos.le ==> Z.le) (fun x => Z.land (Z.round_lor_land_bound (Z.pos x)) y). + Proof. t. Qed. Local Instance lor_round_Proper_pos_r x - : Proper (Pos.le ==> Z.le) - (fun y => - Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))). - Proof. destruct x; t. Qed. + : Proper (Pos.le ==> Z.le) (fun y => Z.lor x (Z.round_lor_land_bound (Z.pos y))). + Proof. t. Qed. Local Instance lor_round_Proper_pos_l y - : Proper (Pos.le ==> Z.le) - (fun x => - Z.lor (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)). - Proof. destruct y; t. Qed. + : Proper (Pos.le ==> Z.le) (fun x => Z.lor (Z.round_lor_land_bound (Z.pos x)) y). + Proof. t. Qed. Local Instance land_round_Proper_neg_r x - : Proper (Basics.flip Pos.le ==> Z.le) - (fun y => - Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))). - Proof. destruct x; t. Qed. + : Proper (Basics.flip Pos.le ==> Z.le) (fun y => Z.land x (Z.round_lor_land_bound (Z.neg y))). + Proof. t. Qed. Local Instance land_round_Proper_neg_l y - : Proper (Basics.flip Pos.le ==> Z.le) - (fun x => - Z.land (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)). - Proof. destruct y; t. Qed. + : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.land (Z.round_lor_land_bound (Z.neg x)) y). + Proof. t. Qed. Local Instance lor_round_Proper_neg_r x - : Proper (Basics.flip Pos.le ==> Z.le) - (fun y => - Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))). - Proof. destruct x; t. Qed. + : Proper (Basics.flip Pos.le ==> Z.le) (fun y => Z.lor x (Z.round_lor_land_bound (Z.neg y))). + Proof. t. Qed. Local Instance lor_round_Proper_neg_l y - : Proper (Basics.flip Pos.le ==> Z.le) - (fun x => - Z.lor (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)). - Proof. destruct y; t. Qed. + : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.lor (Z.round_lor_land_bound (Z.neg x)) y). + Proof. t. Qed. + + Lemma land_round_lor_land_bound_r x + : Z.land x (Z.round_lor_land_bound x) = if (0 <=? x) then x else Z.round_lor_land_bound x. + Proof. t. Qed. + Hint Rewrite land_round_lor_land_bound_r : zsimplify_fast zsimplify. + Lemma land_round_lor_land_bound_l x + : Z.land (Z.round_lor_land_bound x) x = if (0 <=? x) then x else Z.round_lor_land_bound x. + Proof. rewrite Z.land_comm, land_round_lor_land_bound_r; reflexivity. Qed. + Hint Rewrite land_round_lor_land_bound_l : zsimplify_fast zsimplify. + + Lemma lor_round_lor_land_bound_r x + : Z.lor x (Z.round_lor_land_bound x) = if (0 <=? x) then Z.round_lor_land_bound x else x. + Proof. t. Qed. + Hint Rewrite lor_round_lor_land_bound_r : zsimplify_fast zsimplify. + Lemma lor_round_lor_land_bound_l x + : Z.lor (Z.round_lor_land_bound x) x = if (0 <=? x) then Z.round_lor_land_bound x else x. + Proof. rewrite Z.lor_comm, lor_round_lor_land_bound_r; reflexivity. Qed. + Hint Rewrite lor_round_lor_land_bound_l : zsimplify_fast zsimplify. + + Lemma land_round_bound_pos_r v x + : 0 <= Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)). + Proof. + rewrite Z.land_nonneg; split; [ lia | ]. + replace (Z.pos x) with (Z.land (Z.pos x) (Z.round_lor_land_bound (Z.pos x))) at 1 + by now rewrite land_round_lor_land_bound_r. + rewrite (Z.land_comm (Z.pos x)), Z.land_assoc. + apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t. + Qed. + Hint Resolve land_round_bound_pos_r (fun v x => proj1 (land_round_bound_pos_r v x)) (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith. + Lemma land_round_bound_pos_l v x + : 0 <= Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v. + Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_pos_r. Qed. + Hint Resolve land_round_bound_pos_l (fun v x => proj1 (land_round_bound_pos_l v x)) (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith. + + Lemma land_round_bound_neg_r v x + : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x) <= v. + Proof. + assert (0 < 2 ^ Z.log2_up (Z.pos x)) by auto with zarith. + split; [ | apply Z.land_le; lia ]. + replace (Z.round_lor_land_bound (Z.neg x)) with (Z.land (Z.neg x) (Z.round_lor_land_bound (Z.neg x))) + by now rewrite land_round_lor_land_bound_r. + rewrite !Z.land_assoc. + etransitivity; [ apply Z.land_le; cbn; lia | ]; lia. + Qed. + Hint Resolve land_round_bound_neg_r (fun v x => proj1 (land_round_bound_neg_r v x)) (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith. + Lemma land_round_bound_neg_l v x + : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v <= v. + Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_neg_r. Qed. + Hint Resolve land_round_bound_neg_l (fun v x => proj1 (land_round_bound_neg_l v x)) (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith. + + Lemma lor_round_bound_neg_r v x + : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x) <= -1. + Proof. + change (-1) with (Z.pred 0); rewrite <- Z.lt_le_pred. + rewrite Z.lor_neg; split; [ | lia ]. + replace (Z.neg x) with (Z.lor (Z.neg x) (Z.round_lor_land_bound (Z.neg x))) at 2 + by now rewrite lor_round_lor_land_bound_r. + rewrite (Z.lor_comm (Z.neg x)), Z.lor_assoc. + cbn; rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive v), <- (Z.lnot_involutive (Z.neg x)), <- !Z.lnot_land, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r, !Pos2Z.opp_neg. + Z.peel_le. + apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t. + Qed. + Hint Resolve lor_round_bound_neg_r (fun v x => proj1 (lor_round_bound_neg_r v x)) (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith. + Lemma lor_round_bound_neg_l v x + : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v <= -1. + Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_neg_r. Qed. + Hint Resolve lor_round_bound_neg_l (fun v x => proj1 (lor_round_bound_neg_l v x)) (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith. + + Lemma lor_round_bound_pos_r v x + : v <= Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)). + Proof. + assert (0 < 2 ^ Z.log2_up (Z.pos (x + 1))) by auto with zarith. + split; [ apply Z.lor_lower; lia | ]. + replace (Z.round_lor_land_bound (Z.pos x)) with (Z.lor (Z.pos x) (Z.round_lor_land_bound (Z.pos x))) + by now rewrite lor_round_lor_land_bound_r. + rewrite !Z.lor_assoc. + etransitivity; [ | apply Z.lor_lower; rewrite ?Z.lor_nonneg; cbn; lia ]; lia. + Qed. + Hint Resolve lor_round_bound_pos_r (fun v x => proj1 (lor_round_bound_pos_r v x)) (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith. + Lemma lor_round_bound_pos_l v x + : v <= Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v. + Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_pos_r. Qed. + Hint Resolve lor_round_bound_pos_l (fun v x => proj1 (lor_round_bound_pos_l v x)) (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith. + + Lemma land_round_bound_pos_r' v x : Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed. + Lemma land_round_bound_pos_l' v x : Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed. + Lemma land_round_bound_neg_r' v x : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x). Proof. auto with zarith. Qed. + Lemma land_round_bound_neg_l' v x : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v. Proof. auto with zarith. Qed. + Lemma lor_round_bound_neg_r' v x : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x). Proof. auto with zarith. Qed. + Lemma lor_round_bound_neg_l' v x : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v. Proof. auto with zarith. Qed. + Lemma lor_round_bound_pos_r' v x : Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed. + Lemma lor_round_bound_pos_l' v x : Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed. End Z. diff --git a/src/Util/ZUtil/LandLorShiftBounds.v b/src/Util/ZUtil/LandLorShiftBounds.v index e978ab6b0..a8e0b2051 100644 --- a/src/Util/ZUtil/LandLorShiftBounds.v +++ b/src/Util/ZUtil/LandLorShiftBounds.v @@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.Testbit. Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. Require Import Crypto.Util.NUtil.WithoutReferenceToZ. Local Open Scope Z_scope. @@ -70,7 +71,7 @@ Module Z. Qed. Section ZInequalities. - Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z. + Lemma land_le' : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z. Proof. intros x y H; apply Z.ldiff_le; [assumption|]. rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc. @@ -79,14 +80,38 @@ Module Z. reflexivity. Qed. - Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z. + Lemma lor_lower : forall x y, (0 <= x -> 0 <= y)%Z -> (x <= Z.lor x y)%Z. Proof. - intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|]. - rewrite Z.ldiff_land. - apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. - rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec; - [|apply Z.ge_le; assumption]. - induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity. + intros x y H. + destruct (Z_lt_le_dec x 0). + { Z.replace_all_neg_with_pos. + replace (-x) with (Z.lnot (x - 1)) by (cbv [Z.pred Z.lnot]; lia). + rewrite <- (Z.lnot_involutive y). + rewrite <- Z.lnot_land. + cbv [Z.lnot]. + rewrite <- !Z.sub_1_r. + Z.peel_le. + apply land_le'; lia. } + { apply Z.ldiff_le; [apply Z.lor_nonneg; auto|]. + rewrite Z.ldiff_land. + apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. + rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec; + [|apply Z.ge_le; assumption]. + induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity. } + Qed. + + Lemma land_le : forall x y, (0 <= y -> 0 <= x)%Z -> (Z.land x y <= x)%Z. + Proof. + intros x y H. + destruct (Z_lt_le_dec y 0), (Z_lt_le_dec x 0); auto using land_le' with lia. + Z.replace_all_neg_with_pos. + replace (-x) with (Z.lnot (x - 1)) by (cbv [Z.pred Z.lnot]; lia). + replace (-y) with (Z.lnot (y - 1)) by (cbv [Z.pred Z.lnot]; lia). + rewrite <- Z.lnot_lor. + cbv [Z.lnot]. + rewrite <- !Z.sub_1_r. + Z.peel_le. + apply lor_lower; lia. Qed. Lemma lor_le : forall x y z, diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 567d106e3..9944c8124 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -297,6 +297,7 @@ Module Z. apply Z_mod_mult. Qed. Hint Rewrite mod_same_pow using zutil_arith : zsimplify. + Hint Resolve mod_same_pow : zarith. Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. Proof. @@ -369,4 +370,14 @@ Module Z. apply Z.mod_small. omega. Qed. + + Lemma mod_pow_r_split x b e1 e2 : 0 <= b -> 0 <= e1 <= e2 -> x mod b^e2 = (x mod b^e1) + (b^e1) * ((x / b^e1) mod b^(e2-e1)). + Proof. + destruct (Z_zerop b). + { destruct (Z_zerop e1), (Z_zerop e2), (Z.eq_dec e1 e2); subst; intros; cbn; autorewrite with zsimplify_fast; lia. } + intros. + replace (b^e2) with (b^e1 * b^(e2 - e1)) by (autorewrite with pull_Zpow; f_equal; lia). + rewrite Z.rem_mul_r by auto with zarith. + reflexivity. + Qed. End Z. diff --git a/src/Util/ZUtil/Ones.v b/src/Util/ZUtil/Ones.v index e856f23a0..37a0d184e 100644 --- a/src/Util/ZUtil/Ones.v +++ b/src/Util/ZUtil/Ones.v @@ -174,4 +174,42 @@ Module Z. end ]. Qed. Hint Rewrite lor_ones_ones : zsimplify. + + Lemma lor_pow2_mod_pow2_r x e (He : 0 <= e) : Z.lor x (2^e-1) mod (2^e) = 2^e-1. + Proof. + destruct (Z_zerop e). + { subst; autorewrite with zsimplify_const; reflexivity. } + assert (0 <= x mod 2^e < 2^e) by auto with zarith. + assert (0 <= x mod 2^e <= 2^e-1) by lia. + assert (Z.log2 (x mod 2^e) <= Z.log2 (2^e-1)) by (apply Z.log2_le_mono; lia). + assert (Z.log2 (x mod 2^e) < e) by (rewrite Z.sub_1_r, Z.log2_pred_pow2 in * by lia; lia). + rewrite <- Z.land_ones, Z.land_lor_distr_l by assumption. + rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones_ones, Z.min_id, Z.max_id, Bool.if_const. + rewrite Z.land_ones by assumption. + rewrite Z.lor_ones_low; auto with zarith. + Qed. + Hint Rewrite lor_pow2_mod_pow2_r using zutil_arith : zsimplify. + Hint Rewrite lor_pow2_mod_pow2_r using assumption : zsimplify_fast. + + Lemma lor_pow2_mod_pow2_l x e (He : 0 <= e) : Z.lor (2^e-1) x mod (2^e) = 2^e-1. + Proof. rewrite Z.lor_comm; apply lor_pow2_mod_pow2_r; assumption. Qed. + Hint Rewrite lor_pow2_mod_pow2_l using zutil_arith : zsimplify. + Hint Rewrite lor_pow2_mod_pow2_l using assumption : zsimplify_fast. + + Lemma lor_pow2_div_pow2_r x e (He : 0 <= e) : (Z.lor x (2^e-1)) / (2^e) = x / 2^e. + Proof. + destruct (Z_zerop e). + { subst; autorewrite with zsimplify_const; reflexivity. } + assert (0 < 2^e) by auto with zarith. + rewrite <- Z.shiftr_div_pow2, Z.shiftr_lor, !Z.shiftr_div_pow2 by lia. + rewrite (Z.div_small (_-1) _), Z.lor_0_r by lia. + reflexivity. + Qed. + Hint Rewrite lor_pow2_div_pow2_r using zutil_arith : zsimplify. + Hint Rewrite lor_pow2_div_pow2_r using assumption : zsimplify_fast. + + Lemma lor_pow2_div_pow2_l x e (He : 0 <= e) : (Z.lor (2^e-1) x) / (2^e) = x / 2^e. + Proof. rewrite Z.lor_comm; apply lor_pow2_div_pow2_r; assumption. Qed. + Hint Rewrite lor_pow2_div_pow2_l using zutil_arith : zsimplify. + Hint Rewrite lor_pow2_div_pow2_l using assumption : zsimplify_fast. End Z. diff --git a/src/Util/ZUtil/Tactics/LinearSubstitute.v b/src/Util/ZUtil/Tactics/LinearSubstitute.v index d03c9d196..960c06ce9 100644 --- a/src/Util/ZUtil/Tactics/LinearSubstitute.v +++ b/src/Util/ZUtil/Tactics/LinearSubstitute.v @@ -12,6 +12,8 @@ Module Z. Proof. omega. Qed. Lemma move_R_Xm x y z : y - x = z -> x = y - z. Proof. omega. Qed. + Lemma move_R_nX x y : -x = y -> x = -y. + Proof. omega. Qed. Lemma move_L_pX x y z : z = x + y -> z - y = x. Proof. omega. Qed. Lemma move_L_mX x y z : z = x - y -> z + y = x. @@ -20,6 +22,8 @@ Module Z. Proof. omega. Qed. Lemma move_L_Xm x y z : z = y - x -> y - z = x. Proof. omega. Qed. + Lemma move_L_nX x y : y = -x -> -y = x. + Proof. omega. Qed. (** [linear_substitute x] attempts to maipulate equations using only addition and subtraction to put [x] on the left, and then @@ -36,6 +40,8 @@ Module Z. | ?a - ?b => first [ contains for_var b; apply move_L_mX in H | contains for_var a; apply move_L_Xm in H ] + | -?a + => contains for_var a; apply move_L_nX in H | for_var => progress symmetry in H end @@ -46,6 +52,8 @@ Module Z. | ?a - ?b => first [ not contains for_var b; apply move_R_mX in H | not contains for_var a; apply move_R_Xm in H ] + | -?a + => contains for_var a; apply move_R_nX in H end ]. Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H. Ltac linear_solve_for for_var := diff --git a/src/Util/ZUtil/ZSimplify/Core.v b/src/Util/ZUtil/ZSimplify/Core.v index c850ddef6..06bc648ff 100644 --- a/src/Util/ZUtil/ZSimplify/Core.v +++ b/src/Util/ZUtil/ZSimplify/Core.v @@ -1,14 +1,16 @@ Require Import Coq.ZArith.ZArith. Require Export Crypto.Util.ZUtil.Hints.Core. -Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_fast. +Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r : zsimplify_fast. +Hint Rewrite Z.pow_0_l Z.pow_0_l' using assumption : zsimplify_fast. -Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify. -Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l using zutil_arith : zsimplify. +Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l Z.pow_0_l using zutil_arith : zsimplify. Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify. Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify. Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify. -Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l : zsimplify_const. +Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l Z.sub_diag : zsimplify_const. +Hint Rewrite Z.pow_0_l Z.pow_0_l' using assumption : zsimplify_const. Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const. diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v index 94fa05e1a..b176c0b21 100644 --- a/src/Util/ZUtil/ZSimplify/Simple.v +++ b/src/Util/ZUtil/ZSimplify/Simple.v @@ -13,6 +13,9 @@ Module Z. Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1. Proof. apply Z.pow_1_l; lia. Qed. Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_0_l_Zpos a : 0^Zpos a = 0. + Proof. apply Z.pow_0_l; lia. Qed. + Hint Rewrite pow_0_l_Zpos : zsimplify_fast zsimplify_const zsimplify. Lemma sub_same_minus (x y : Z) : x - (x - y) = y. Proof. lia. Qed. -- cgit v1.2.3