aboutsummaryrefslogtreecommitdiff
path: root/src/Curves
Commit message (Collapse)AuthorAge
* parenthesize proofs in Weierstrass.Projective (closes #456)Gravatar Andres Erbsen2018-11-11
|
* Adapt to Coq's PR#8555Gravatar Maxime Dénès2018-10-02
|
* Import prim token notations before using themGravatar Jason Gross2018-08-24
| | | | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362 Almost all changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Compatibility after Coq PR#262.Gravatar Hugo Herbelin2018-05-14
| | | | | | | | | Coq PR#262 makes the inference of return clauses more uniform and general but unification is sometimes not strong enough to deal with this generality. See #5107 for details. One reduces the search space for a return clause by forbidding it to be obtained by small inversion.
* Generalize Jacobian.v over all a.Gravatar David Benjamin2018-04-25
| | | | | | | | | | | | | | | | The immediate motivation is BoringSSL's generic EC code is sadly stuck with supporting arbitrary curves, including those where a <> -3, but it may be more generally useful. This makes the file slightly more general: - It now proves that the addition formula works independent of a = -3. - It proves a generic doubling implementation, based on http://www.hyperelliptic.org/EFD/g1p/auto-shortw-jacobian.html#doubling-dbl-2007-bl - There's a place to stick in other specializations should someone want them. (I hear some folks are interested in secp256k1 for some reason.)
* move Loops from Experiments to UtilGravatar Andres Erbsen2018-03-27
|
* cleanup2Gravatar Andres Erbsen2018-03-27
|
* Combine the zero and non-zero cases together.Gravatar David Benjamin2018-01-15
| | | | | | This required tending to montladder not being proved Feq-preserving (sidestepped by proving for all P = 0), and then some wrestling with scalarmult to show the right-hand side was indeed zero when x is (0, 0).
* Factor out fsatz lemmasGravatar Jason Gross2018-01-09
| | | | | | | | | After | File Name | Before || Change | % Change ------------------------------------------------------------------------- 1m11.42s | Total | 1m53.75s || -0m42.33s | -37.21% ------------------------------------------------------------------------- 1m06.02s | Curves/Weierstrass/Jacobian | 1m53.76s || -0m47.73s | -41.96% 0m05.40s | Util/FsatzAutoLemmas | N/A || +0m05.40s | ∞
* Replace char_ge_12 with char_ge_3Gravatar Jason Gross2018-01-09
| | | | We no longer seem to need the stronger hypothesis.
* Massively speed up JacobianGravatar Jason Gross2018-01-09
| | | | | | | | After | File Name | Before || Change | % Change --------------------------------------------------------------------------- 1m52.31s | Total | 13m36.75s || -11m44.44s | -86.24% --------------------------------------------------------------------------- 1m52.31s | Curves/Weierstrass/Jacobian | 13m36.75s || -11m44.44s | -86.24%
* Revert "Replace char_ge_12 with char_ge_3"Gravatar Jason Gross2018-01-09
| | | | | | This reverts commit d33d8be154dbce048ac10d82bc0b39468abd5fdb. Hmm, apparently there's an error on Qed... maybe a bug in fsatz?
* Replace char_ge_12 with char_ge_3Gravatar Jason Gross2018-01-09
| | | | We no longer seem to need the stronger hypothesis.
* Jabobian.v: par -> allGravatar Andres Erbsen2018-01-09
|
* src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_*Gravatar Andres Erbsen2018-01-09
|
* @davidben merged Jacobian+affine into Jacobian+JacobianGravatar Andres Erbsen2018-01-09
|
* Jacobian coordinatesGravatar Andres Erbsen2018-01-09
|
* Prove montladder correct in the zero case.Gravatar David Benjamin2018-01-08
|
* restore fastpath logic in Curves.Montgomery.XZProofsGravatar Andres Erbsen2017-12-22
|
* prove montgomery ladder for non-zero inputsGravatar Andres Erbsen2017-12-22
|
* Montgomery.XZ, Loops: montladder proof scaffoldingGravatar Andres Erbsen2017-12-22
|
* specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* expose missing proof in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* clean up src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* Curves.Montgomery.XZ: add+check boringssl ladderstep (#278)Gravatar Andres Erbsen2017-12-05
|
* projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptionalGravatar Andres Erbsen2017-10-18
| | | | (Squashed and rebased by Jason Gross)
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
|
* match C code in Jacobian additionGravatar Andres Erbsen2017-06-27
|
* Weierstrass Jacobian mixed additionGravatar Andres Erbsen2017-06-23
|
* Edwards coordinates precomputed addition formulaGravatar Andres Erbsen2017-06-15
|
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
|
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
| | | | | | | With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
* use ladderstep from donna (2% faster?)Gravatar Andres Erbsen2017-05-15
|
* Prove relationship between `xzladderstep` and M.add (#162)Gravatar Andres Erbsen2017-04-28
| | | | | | | | | | | | | | * hopefully all proofs we need about xzladderstep * Better automation in xzproofs * Speed up xzproofs with heuristic clearing * Remove useless hypotheses * XZProofs cleanup * fix "group by isomorphism" proofs, use in XZProofs
* clean elliptic curve proofs, use par: in WeierstrassAffineProofsGravatar Andres Erbsen2017-04-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This required working fsatz around <https://coq.inria.fr/bugs/show_bug.cgi?id=5452> par: abstract (abstract tac) raises anomalies Curves/Weierstrass/AffineProofs is still affected by something like <https://coq.inria.fr/bugs/show_bug.cgi?id=4831> par: Goals randomly not solved The timing script ran out of memory the first time, so I winged the last couple of files that were left. src/Curves/Weierstrass/AffineProofs (real: 516.30, user: 757.86, sys: 2.52, mem: 2808940 ko), was: 14m49s src/Curves/Montgomery/AffineProofs (real: 51.38, user: 50.82, sys: 0.48, mem: 1509924 ko), was: 55s src/Curves/Edwards/Montgomery (real: 4.55, user: 4.43, sys: 0.09, mem: 542008 ko), was: 5s src/Curves/Montgomery/XZProofs (real: 36.27, user: 35.87, sys: 0.32, mem: 1391216 ko), was: 39s src/Specific/IntegrationTestLadderstep (real: 158.95, user: 158.42, sys: 0.50, mem: 1827860 ko)was: 3m10s 0m43.48s | Specific/IntegrationTestLadderstep | 3m10.35s || -2m00.87s 3m08.45s | Curves/Weierstrass/Projective | 2m39.76s || +0m00.68s 2m13.43s | Spec/Test/X25519 | 2m11.48s || +0m00.95s 1m23.64s | Specific/IntegrationTestLadderstep130 | 1m20.78s || +0m00.85s 1m05.88s | Compilers/Z/ArithmeticSimplifierWf | 1m01.03s || +0m00.84s 1m01.96s | Spec/Ed25519 | 0m55.02s || +0m00.93s 0m33.80s | Curves/Edwards/XYZT | 0m25.10s || +0m00.69s 0m30.97s | Curves/Edwards/AffineProofs | 0m29.76s || +0m00.20s 0m24.12s | Compilers/Named/MapCastWf | 0m24.19s || -0m00.07s 0m23.94s | Primitives/EdDSARepChange | 0m23.28s || +0m00.66s 0m23.52s | Util/ZUtil | 0m22.27s || +0m00.25s 0m18.63s | Compilers/Named/ContextProperties/SmartMap | 0m17.26s || +0m00.36s 0m18.44s | Compilers/Named/ContextProperties/NameUtil | 0m17.95s || +0m00.49s 0m16.18s | Specific/IntegrationTestMul | 0m16.41s || -0m00.23s 0m15.14s | Compilers/Z/ArithmeticSimplifierInterp | 0m14.43s || +0m00.71s 0m14.41s | Algebra/Field | 0m15.30s || -0m00.89s 0m14.18s | Specific/IntegrationTestSquare | 0m14.60s || -0m00.41s 0m14.08s | Compilers/CommonSubexpressionEliminationWf | 0m14.07s || +0m00.00s 0m13.82s | Specific/ArithmeticSynthesisTest | 0m10.24s || +0m00.58s 0m13.34s | Specific/IntegrationTestSub | 0m13.49s || -0m00.15s 0m11.72s | Primitives/MxDHRepChange | 0m11.02s || +0m00.70s 0m11.30s | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy | 0m11.49s || -0m00.18s 0m11.17s | Arithmetic/MontgomeryReduction/Proofs | 0m10.42s || +0m00.75s 0m11.13s | Compilers/Named/MapCastInterp | 0m11.12s || +0m00.01s 0m10.54s | LegacyArithmetic/ArchitectureToZLikeProofs | 0m11.01s || -0m00.47s 0m10.21s | Compilers/InlineWf | 0m11.00s || -0m00.78s 0m10.21s | LegacyArithmetic/Double/Proofs/Multiply | 0m10.51s || -0m00.29s 0m10.07s | Specific/ArithmeticSynthesisTest130 | 0m06.78s || +0m00.29s 0m09.96s | Compilers/Named/RegisterAssignInterp | 0m10.03s || -0m00.06s 0m09.70s | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m10.77s || -0m00.07s 0m08.93s | Arithmetic/Core | 0m08.42s || +0m00.50s 0m08.87s | Algebra/Ring | 0m08.99s || -0m00.12s 0m08.61s | Util/FixedWordSizesEquality | 0m08.39s || +0m00.21s 0m08.15s | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate | 0m08.99s || -0m00.83s 0m07.97s | Bedrock/Word | 0m07.77s || +0m00.20s 0m07.92s | Compilers/LinearizeWf | 0m08.05s || -0m00.13s 0m07.04s | Util/ListUtil | 0m06.56s || +0m00.48s 0m06.78s | Curves/Edwards/Pre | 0m06.90s || -0m00.12s 0m06.76s | LegacyArithmetic/Pow2BaseProofs | 0m06.88s || -0m00.12s 0m06.60s | LegacyArithmetic/Double/Proofs/RippleCarryAddSub | 0m06.60s || +0m00.00s 0m05.80s | Algebra/Field_test | 0m06.11s || -0m00.31s 0m04.49s | Compilers/EtaWf | 0m04.42s || +0m00.07s 0m04.39s | Util/ForLoop/Unrolling | 0m04.52s || -0m00.12s 0m04.32s | Arithmetic/BarrettReduction/HAC | 0m04.39s || -0m00.06s 0m04.26s | Compilers/Named/CompileWf | 0m04.50s || -0m00.24s 0m04.25s | LegacyArithmetic/InterfaceProofs | 0m03.92s || +0m00.33s 0m04.13s | Compilers/WfProofs | 0m03.88s || +0m00.25s 0m04.07s | Compilers/TestCase | 0m04.19s || -0m00.12s 0m03.92s | Arithmetic/Saturated | 0m04.18s || -0m00.25s 0m03.91s | Specific/FancyMachine256/Montgomery | 0m03.86s || +0m00.05s 0m03.69s | LegacyArithmetic/ZBoundedZ | 0m03.43s || +0m00.25s 0m03.68s | Curves/Montgomery/Affine | 0m03.38s || +0m00.30s 0m03.62s | Arithmetic/ModularArithmeticTheorems | 0m03.35s || +0m00.27s 0m03.51s | Specific/FancyMachine256/Barrett | 0m03.47s || +0m00.03s 0m03.43s | Compilers/Named/CompileInterp | 0m03.47s || -0m00.04s 0m03.37s | Arithmetic/BarrettReduction/Generalized | 0m03.49s || -0m00.12s 0m03.29s | LegacyArithmetic/Double/Proofs/ShiftLeft | 0m04.16s || -0m00.87s 0m03.27s | Spec/MontgomeryCurve | 0m03.57s || -0m00.29s 0m03.26s | Compilers/Named/ContextProperties | 0m03.18s || +0m00.07s 0m03.12s | Compilers/InlineInterp | 0m03.16s || -0m00.04s 0m03.09s | LegacyArithmetic/Double/Proofs/ShiftRight | 0m04.30s || -0m00.20s 0m02.97s | LegacyArithmetic/Double/Proofs/Decode | 0m03.05s || -0m00.07s 0m02.89s | Compilers/Z/Bounds/Relax | 0m02.76s || +0m00.13s 0m02.86s | Compilers/Named/NameUtilProperties | 0m02.86s || +0m00.00s 0m02.79s | Compilers/CommonSubexpressionEliminationProperties | 0m02.68s || +0m00.10s 0m02.77s | Compilers/Z/Bounds/InterpretationLemmas/PullCast | 0m02.73s || +0m00.04s 0m02.63s | LegacyArithmetic/BarretReduction | 0m02.50s || +0m00.12s 0m02.59s | Specific/FancyMachine256/Core | 0m02.21s || +0m00.37s 0m02.32s | Util/ForLoop/InvariantFramework | 0m02.15s || +0m00.16s 0m02.28s | Util/WordUtil | 0m02.36s || -0m00.08s 0m02.27s | Compilers/WfReflective | 0m02.19s || +0m00.08s 0m02.04s | Spec/WeierstrassCurve | 0m00.61s || +0m00.43s 0m01.95s | LegacyArithmetic/MontgomeryReduction | 0m01.80s || +0m00.14s N/A | Curves/Weierstrass/Pre | 0m01.94s || -0m00.94s 0m01.82s | Util/NatUtil | 0m01.80s || +0m00.02s 0m01.71s | Arithmetic/BarrettReduction/Wikipedia | 0m01.72s || -0m00.01s 0m01.71s | Compilers/Z/Bounds/Pipeline/Definition | 0m01.52s || +0m00.18s 0m01.65s | Util/Tuple | 0m01.64s || +0m00.01s 0m01.64s | Arithmetic/PrimeFieldTheorems | 0m01.67s || -0m00.03s 0m01.59s | Compilers/Named/InterpretToPHOASWf | 0m01.60s || -0m00.01s 0m01.55s | Algebra/Group | 0m01.51s || +0m00.04s 0m01.54s | Compilers/Z/Syntax/Equality | 0m01.48s || +0m00.06s 0m01.26s | Compilers/Relations | 0m01.25s || +0m00.01s 0m01.18s | Compilers/LinearizeInterp | 0m01.35s || -0m00.17s 0m01.13s | Compilers/WfInversion | 0m01.02s || +0m00.10s 0m01.09s | Algebra/IntegralDomain | 0m01.50s || -0m00.40s 0m01.05s | Compilers/Named/CompileProperties | 0m00.93s || +0m00.12s 0m01.04s | Util/NumTheoryUtil | 0m01.01s || +0m00.03s 0m01.02s | Compilers/Named/InterpretToPHOASInterp | 0m00.90s || +0m00.12s 0m00.98s | LegacyArithmetic/Double/Proofs/BitwiseOr | 0m00.95s || +0m00.03s 0m00.97s | Util/PartiallyReifiedProp | 0m00.93s || +0m00.03s 0m00.97s | LegacyArithmetic/Double/Proofs/LoadImmediate | 0m01.09s || -0m00.12s 0m00.93s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.86s || +0m00.07s 0m00.86s | Compilers/Z/CNotations | 0m00.82s || +0m00.04s 0m00.85s | Arithmetic/Karatsuba | 0m00.87s || -0m00.02s 0m00.85s | Compilers/Z/Syntax/Util | 0m00.75s || +0m00.09s 0m00.84s | LegacyArithmetic/BaseSystemProofs | 0m00.89s || -0m00.05s 0m00.80s | Compilers/MapCastByDeBruijnInterp | 0m00.99s || -0m00.18s 0m00.78s | Compilers/MultiSizeTest | 0m00.78s || +0m00.00s 0m00.75s | Util/IterAssocOp | 0m00.70s || +0m00.05s 0m00.74s | Util/ZUtil/Stabilization | 0m00.74s || +0m00.00s 0m00.73s | LegacyArithmetic/Interface | 0m00.64s || +0m00.08s 0m00.67s | Compilers/WfReflectiveGen | 0m00.62s || +0m00.05s 0m00.67s | Util/CPSUtil | 0m00.58s || +0m00.09s 0m00.67s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.70s || -0m00.02s 0m00.67s | Curves/Montgomery/XZ | 0m00.57s || +0m00.10s 0m00.66s | Compilers/MapCastByDeBruijnWf | 0m00.71s || -0m00.04s 0m00.64s | Compilers/InterpByIsoProofs | 0m00.60s || +0m00.04s 0m00.63s | Compilers/Z/JavaNotations | 0m00.62s || +0m00.01s 0m00.62s | Arithmetic/ModularArithmeticPre | 0m00.54s || +0m00.07s 0m00.61s | Spec/CompleteEdwardsCurve | 0m00.60s || +0m00.01s 0m00.60s | Util/HList | 0m00.53s || +0m00.06s 0m00.59s | Util/Decidable | 0m00.63s || -0m00.04s 0m00.59s | Compilers/CommonSubexpressionEliminationInterp | 0m00.80s || -0m00.21s 0m00.58s | Compilers/Z/CommonSubexpressionElimination | 0m00.54s || +0m00.03s 0m00.58s | LegacyArithmetic/Double/Proofs/SelectConditional | 0m00.90s || -0m00.32s 0m00.57s | Compilers/InterpWfRel | 0m00.60s || -0m00.03s 0m00.57s | Compilers/Named/AListContext | 0m00.53s || +0m00.03s 0m00.57s | Util/AdditionChainExponentiation | 0m00.51s || +0m00.05s 0m00.56s | Compilers/Z/Bounds/RoundUpLemmas | 0m00.59s || -0m00.02s 0m00.56s | Compilers/InputSyntax | 0m00.54s || +0m00.02s 0m00.55s | Compilers/Named/FMapContext | 0m00.55s || +0m00.00s 0m00.55s | Curves/Weierstrass/Affine | 0m00.61s || -0m00.05s 0m00.54s | Spec/EdDSA | 0m00.53s || +0m00.01s 0m00.54s | Compilers/Z/Bounds/Pipeline | 0m00.55s || -0m00.01s 0m00.53s | Compilers/Z/Bounds/InterpretationLemmas/Tactics | 0m00.45s || +0m00.08s 0m00.53s | LegacyArithmetic/Double/Core | 0m00.51s || +0m00.02s 0m00.53s | Compilers/CommonSubexpressionElimination | 0m00.51s || +0m00.02s 0m00.51s | Util/NUtil | 0m00.53s || -0m00.02s 0m00.51s | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.47s || +0m00.04s 0m00.51s | Util/ForLoop/Tests | 0m00.45s || +0m00.06s 0m00.51s | Compilers/Z/Reify | 0m00.52s || -0m00.01s 0m00.51s | Compilers/Z/Bounds/MapCastByDeBruijnInterp | 0m00.50s || +0m00.01s 0m00.50s | LegacyArithmetic/ZBounded | 0m00.51s || -0m00.01s 0m00.50s | Compilers/Z/ArithmeticSimplifier | 0m00.47s || +0m00.03s 0m00.50s | LegacyArithmetic/ArchitectureToZLike | 0m00.49s || +0m00.01s 0m00.49s | Compilers/InterpWf | 0m00.49s || +0m00.00s 0m00.49s | Compilers/Z/Bounds/Interpretation | 0m00.47s || +0m00.02s 0m00.48s | Specific/IntegrationTestDisplayCommon | 0m00.45s || +0m00.02s 0m00.47s | Spec/ModularArithmetic | 0m00.41s || +0m00.06s 0m00.47s | Compilers/Z/Bounds/MapCastByDeBruijn | 0m00.47s || +0m00.00s 0m00.47s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.49s || -0m00.02s 0m00.46s | Algebra/Nsatz | 0m00.62s || -0m00.15s 0m00.46s | Compilers/Reify | 0m00.45s || +0m00.01s 0m00.46s | Compilers/Z/CommonSubexpressionEliminationWf | 0m00.48s || -0m00.01s 0m00.46s | Compilers/Z/MapCastByDeBruijnInterp | 0m00.47s || -0m00.00s 0m00.46s | Compilers/Z/Bounds/MapCastByDeBruijnWf | 0m00.49s || -0m00.02s 0m00.45s | LegacyArithmetic/BaseSystem | 0m00.44s || +0m00.01s 0m00.45s | Util/ZRange | 0m00.44s || +0m00.01s 0m00.45s | Util/BoundedWord | 0m00.43s || +0m00.02s 0m00.44s | Util/Factorize | 0m00.57s || -0m00.12s 0m00.44s | Compilers/Z/Syntax | 0m00.44s || +0m00.00s 0m00.44s | Compilers/Z/CommonSubexpressionEliminationInterp | 0m00.59s || -0m00.14s 0m00.44s | Compilers/Z/MapCastByDeBruijnWf | 0m00.45s || -0m00.01s 0m00.43s | Compilers/Z/Inline | 0m00.39s || +0m00.03s 0m00.43s | Compilers/Named/PositiveContext/DefaultsProperties | 0m00.44s || -0m00.01s 0m00.42s | Compilers/Z/HexNotationConstants | 0m00.43s || -0m00.01s 0m00.42s | LegacyArithmetic/Pow2Base | 0m00.42s || +0m00.00s 0m00.42s | Compilers/Z/FoldTypes | 0m00.38s || +0m00.03s 0m00.42s | Compilers/Z/InlineInterp | 0m00.40s || +0m00.01s 0m00.42s | Compilers/Z/MapCastByDeBruijn | 0m00.45s || -0m00.03s 0m00.41s | Compilers/Tuple | 0m00.41s || +0m00.00s 0m00.41s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.44s || -0m00.03s 0m00.40s | Compilers/Named/DeadCodeElimination | 0m00.39s || +0m00.01s 0m00.39s | Arithmetic/MontgomeryReduction/Definition | 0m00.43s || -0m00.03s 0m00.39s | Compilers/Z/Bounds/Pipeline/OutputType | 0m00.42s || -0m00.02s 0m00.39s | Compilers/Z/InlineWf | 0m00.41s || -0m00.01s 0m00.38s | Compilers/Named/EstablishLiveness | 0m00.40s || -0m00.02s 0m00.37s | Compilers/Z/BinaryNotationConstants | 0m00.38s || -0m00.01s 0m00.37s | Compilers/Named/WeakListContext | 0m00.35s || +0m00.02s 0m00.36s | Compilers/FilterLive | 0m00.36s || +0m00.00s 0m00.36s | Algebra/ScalarMult | 0m00.33s || +0m00.02s 0m00.35s | Bedrock/Nomega | 0m00.39s || -0m00.04s 0m00.34s | Util/FixedWordSizes | 0m00.34s || +0m00.00s 0m00.34s | Compilers/Named/WfInterp | 0m00.32s || +0m00.02s 0m00.34s | Compilers/Named/PositiveContext | 0m00.33s || +0m00.01s 0m00.33s | Compilers/ExprInversion | 0m00.32s || +0m00.01s 0m00.32s | Util/ForLoop/Instances | 0m00.34s || -0m00.02s 0m00.32s | Algebra/Monoid | 0m00.29s || +0m00.03s 0m00.31s | Compilers/Equality | 0m00.29s || +0m00.02s 0m00.31s | Compilers/Z/OpInversion | 0m00.38s || -0m00.07s 0m00.31s | Compilers/Named/RegisterAssign | 0m00.32s || -0m00.01s 0m00.31s | Compilers/MapCastByDeBruijn | 0m00.31s || +0m00.00s 0m00.30s | Algebra/Hierarchy | 0m00.32s || -0m00.02s 0m00.30s | Compilers/Named/PositiveContext/Defaults | 0m00.29s || +0m00.01s 0m00.29s | Util/Sum | 0m00.30s || -0m00.01s 0m00.29s | Spec/MxDH | 0m00.26s || +0m00.02s 0m00.28s | Compilers/SmartMap | 0m00.28s || +0m00.00s 0m00.27s | Compilers/EtaInterp | 0m00.26s || +0m00.01s 0m00.26s | Compilers/Named/ContextDefinitions | 0m00.22s || +0m00.04s 0m00.24s | Compilers/CommonSubexpressionEliminationDenote | 0m00.24s || +0m00.00s 0m00.23s | Util/ForLoop | 0m00.22s || +0m00.01s 0m00.23s | Compilers/Named/ContextOn | 0m00.25s || -0m00.01s 0m00.21s | Util/LetInMonad | 0m00.20s || +0m00.00s 0m00.21s | Compilers/Named/ContextProperties/Tactics | 0m00.23s || -0m00.02s 0m00.20s | Compilers/InterpProofs | 0m00.22s || -0m00.01s 0m00.17s | Util/Sigma | 0m00.10s || +0m00.07s 0m00.17s | Compilers/RewriterWf | 0m00.14s || +0m00.03s 0m00.15s | Util/Option | 0m00.16s || -0m00.01s 0m00.14s | Compilers/Named/Compile | 0m00.13s || +0m00.01s 0m00.13s | Compilers/Wf | 0m00.14s || -0m00.01s 0m00.12s | Util/Relations | 0m00.12s || +0m00.00s 0m00.11s | Compilers/Named/NameUtil | 0m00.12s || -0m00.00s 0m00.11s | Compilers/Conversion | 0m00.12s || -0m00.00s 0m00.11s | Compilers/Named/IdContext | 0m00.11s || +0m00.00s 0m00.10s | Util/Equality | 0m00.10s || +0m00.00s 0m00.10s | Util/Prod | 0m00.10s || +0m00.00s 0m00.10s | Util/PointedProp | 0m00.11s || -0m00.00s 0m00.09s | Compilers/TypeInversion | 0m00.09s || +0m00.00s 0m00.09s | Compilers/Named/MapCast | 0m00.07s || +0m00.01s 0m00.07s | Compilers/Syntax | 0m00.05s || +0m00.02s 0m00.07s | Compilers/Linearize | 0m00.06s || +0m00.01s 0m00.06s | Util/HProp | 0m00.05s || +0m00.00s 0m00.06s | Util/Bool | 0m00.06s || +0m00.00s 0m00.06s | Util/Tower | 0m00.03s || +0m00.03s 0m00.06s | Util/Tactics/BreakMatch | 0m00.03s || +0m00.03s 0m00.06s | Util/LetIn | 0m00.05s || +0m00.00s 0m00.06s | Compilers/Inline | 0m00.06s || +0m00.00s 0m00.06s | Compilers/RewriterInterp | 0m00.06s || +0m00.00s 0m00.06s | Compilers/Named/Syntax | 0m00.06s || +0m00.00s 0m00.06s | Compilers/Named/Wf | 0m00.05s || +0m00.00s 0m00.06s | Compilers/Named/SmartMap | 0m00.06s || +0m00.00s 0m00.06s | Compilers/Eta | 0m00.06s || +0m00.00s 0m00.06s | Compilers/FoldTypes | 0m00.06s || +0m00.00s 0m00.06s | Compilers/InterpByIso | 0m00.05s || +0m00.00s 0m00.06s | Compilers/Named/InterpretToPHOAS | 0m00.07s || -0m00.01s 0m00.05s | Compilers/Map | 0m00.03s || +0m00.02s 0m00.05s | Compilers/Rewriter | 0m00.04s || +0m00.01s 0m00.04s | Util/Tactics/DebugPrint | 0m00.04s || +0m00.00s 0m00.04s | Util/Isomorphism | 0m00.05s || -0m00.01s 0m00.04s | Util/Tactics/Test | 0m00.04s || +0m00.00s 0m00.04s | Util/Tactics/ConvoyDestruct | 0m00.03s || +0m00.01s 0m00.04s | Util/Tactics/DestructTrivial | 0m00.02s || +0m00.02s 0m00.04s | Util/Tactics/ETransitivity | 0m00.03s || +0m00.01s 0m00.04s | Util/Curry | 0m00.03s || +0m00.01s 0m00.04s | Util/Sigma/Associativity | 0m00.03s || +0m00.01s 0m00.04s | LegacyArithmetic/VerdiTactics | 0m00.03s || +0m00.01s 0m00.04s | Util/Tactics/Head | 0m00.04s || +0m00.00s 0m00.04s | Util/Tactics/Not | 0m00.02s || +0m00.02s 0m00.04s | Util/Tactics/UniquePose | 0m00.03s || +0m00.01s 0m00.04s | Util/Tactics/DestructHead | 0m00.03s || +0m00.01s 0m00.04s | Compilers/TypeUtil | 0m00.03s || +0m00.01s 0m00.04s | Util/AutoRewrite | 0m00.04s || +0m00.00s 0m00.04s | Compilers/CountLets | 0m00.06s || -0m00.01s 0m00.04s | Compilers/Named/Context | 0m00.05s || -0m00.01s 0m00.03s | Util/GlobalSettings | 0m00.04s || -0m00.01s 0m00.03s | Util/Tactics/Revert | 0m00.02s || +0m00.00s 0m00.03s | Util/Tactics/Contains | 0m00.03s || +0m00.00s 0m00.03s | Util/IffT | 0m00.06s || -0m00.03s 0m00.03s | Util/Tactics/ClearDuplicates | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/ESpecialize | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/Forward | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/PrintContext | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/SetoidSubst | 0m00.04s || -0m00.01s 0m00.03s | Util/Tactics/SideConditionsBeforeToAfter | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/SubstEvars | 0m00.02s || +0m00.00s 0m00.03s | Util/Tactics/VM | 0m00.02s || +0m00.00s 0m00.03s | Util/Sigma/MapProjections | 0m00.03s || +0m00.00s 0m00.03s | Util/ChangeInAll | 0m00.02s || +0m00.00s 0m00.03s | Util/Sigma/Lift | 0m00.03s || +0m00.00s 0m00.03s | Util/Sumbool | 0m00.09s || -0m00.06s 0m00.03s | Util/FixCoqMistakes | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/SpecializeBy | 0m00.04s || -0m00.01s 0m00.03s | Util/Tactics/DestructHyps | 0m00.02s || +0m00.00s 0m00.03s | Util/Tactics/SplitInContext | 0m00.03s || +0m00.00s 0m00.03s | Util/Logic | 0m00.04s || -0m00.01s 0m00.03s | Util/Tactics/RewriteHyp | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/MoveLetIn | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics | 0m00.04s || -0m00.01s 0m00.03s | Compilers/RenameBinders | 0m00.05s || -0m00.02s 0m00.02s | Util/Tactics/OnSubterms | 0m00.04s || -0m00.02s 0m00.02s | Util/Tactics/GetGoal | 0m00.01s || +0m00.01s 0m00.02s | Util/Tactics/ChangeInAll | 0m00.04s || -0m00.02s 0m00.02s | Util/Tactics/ClearAll | 0m00.04s || -0m00.02s 0m00.02s | Util/Tactics/SetEvars | 0m00.03s || -0m00.00s 0m00.02s | Util/Tactics/SimplifyRepeatedIfs | 0m00.02s || +0m00.00s 0m00.02s | Util/Tactics/SubstLet | 0m00.02s || +0m00.00s 0m00.02s | Util/Tactics/TransparentAssert | 0m00.02s || +0m00.00s 0m00.02s | Util/Tactics/UnifyAbstractReflexivity | 0m00.03s || -0m00.00s 0m00.02s | Util/Logic/ImplAnd | 0m00.03s || -0m00.00s 0m00.02s | Util/Unit | 0m00.06s || -0m00.03s 0m00.02s | Util/Tactics/DoWithHyp | 0m00.03s || -0m00.00s 0m00.02s | Util/Notations | 0m00.03s || -0m00.00s 0m00.01s | Util/Tactics/EvarExists | 0m00.02s || -0m00.01s 0m00.01s | Util/Tactics/SimplifyProjections | 0m00.03s || -0m00.01s
* Respond to code review commentsGravatar Jason Gross2017-04-17
|
* Use the for-loop notation in Montgomery.XZGravatar Jason Gross2017-04-17
| | | | | We also need to stuff the local notations in a scope so that we can still access the notations in core_scope
* lemmas about ladderstep on zeroGravatar Andres Erbsen2017-04-14
|
* stronger ladderstep correctness proof courtesy TeoGravatar Andres Erbsen2017-04-14
|
* rename-everythingGravatar Andres Erbsen2017-04-06
|
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
|
* port some edwards curve theoremsGravatar Andres Erbsen2016-02-12
|
* removed lingering Check/SearchAbout statementsGravatar Jade Philipoom2016-02-07
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-02-07
|\
* | EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and ↵Gravatar Jade Philipoom2016-02-07
| | | | | | | | the sign bit of x, then solves the curve equation for x ^ 2. Required adding several lemmas to GaloisField (and moving others there from PointFormats).
| * PointFormats: prove dangling admitGravatar Andres Erbsen2016-02-07
|/
* PointFOrmats,EdDSA: remove redundant axiomsGravatar Andres Erbsen2016-01-16
|
* remove duplicate axiomGravatar Andres Erbsen2016-01-16
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:06:18 +0000