aboutsummaryrefslogtreecommitdiff
path: root/p521_64.c
Commit message (Collapse)AuthorAge
* Rebuild .c filesGravatar Jason Gross2019-03-31
| | | | It seems some commutativity has changed
* Use Preconditions: Postconditions:, rather than /\ and ->Gravatar Jason Gross2019-02-02
|
* Address code review comments to improve docstringsGravatar Jason Gross2019-02-02
|
* Add autogenerated docstrings to synthesized codeGravatar Jason Gross2019-02-02
| | | | | | | | | We now stringify the correctness conditions to generate docstrings for the synthesized code. Closes #512 Time commitment: about 6 hours
* Also display the carry chain in a commentGravatar Jason Gross2019-01-26
|
* Constant-propogate 0+x and x+0 after boundsGravatar Jason Gross2019-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43% -------------------------------------------------------------------------------------------- 4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88% 3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68% 2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22% 1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27% 1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01% 1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77% 0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34% 0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63% 0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25% 0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73% 0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80% 0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28% 0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28% 0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45% 0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75% 0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35% 0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77% 0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37% 0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09% 0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12% 0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73% 0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63% 0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18% 0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32% 0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93% 0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40% 0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73% 0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88% 0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16% 0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35% 0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58% 0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78% 0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22% 0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00%
* Add a rewrite rule to collapse constant castsGravatar Jason Gross2019-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If, e.g., we know from bounds analysis that the result of an operation fits in the range r[0~>0], we now just replace it with the literal constant. Fixes #493 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05% -------------------------------------------------------------------------------------------- 4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23% 3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11% 2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28% 1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42% 1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31% 1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20% 0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06% 0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38% 0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38% 0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39% 0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65% 0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49% 0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11% 0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75% 0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35% 0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94% 0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00% 0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09% 0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08% 0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39% 0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42% 0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59% 0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50% 0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33% 0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75% 0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57% 0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40% 0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49% 0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45% 0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33% 0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74% 0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73% 0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00% 0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14% 0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43%
* Fix computation of INTX_MINGravatar Jason Gross2019-01-15
| | | | The minimum is -2^(bitwidth-1), not -2^bitwidth. Oops.
* Don't cast signed to unsigned before shiftingGravatar Jason Gross2019-01-15
| | | | | | | | | | | Unfortunately, signed->unsigned casts do not commute with shifts. We take care to only extend the range when it needs extending, now. This was previously causing issues with subborrow. We should really get proofs about casts in C semantics at some point soon. Fixes #489
* Add some Z.le Proper hints to zarithGravatar Jason Gross2018-08-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will hopefully make them easier to use. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 58m46.26s | Total | 58m39.68s || +0m06.58s | +0.18% -------------------------------------------------------------------------------------------------------------------- 8m47.74s | Experiments/SimplyTypedArithmetic | 8m41.19s || +0m06.54s | +1.25% 0m32.25s | Specific/X25519/C32/fecarry | 0m25.53s || +0m06.71s | +26.32% 5m06.78s | Experiments/NewPipeline/Toplevel1 | 5m08.78s || -0m02.00s | -0.64% 6m02.08s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m03.44s || -0m01.36s | -0.37% 3m44.75s | Curves/Montgomery/XZProofs | 3m44.04s || +0m00.71s | +0.31% 2m12.59s | Specific/X25519/C64/ladderstep | 2m12.76s || -0m00.16s | -0.12% 1m51.27s | Specific/NISTP256/AMD64/femul | 1m52.13s || -0m00.85s | -0.76% 1m29.57s | Experiments/NewPipeline/Arithmetic | 1m29.61s || -0m00.04s | -0.04% 1m29.24s | Spec/Test/X25519 | 1m29.03s || +0m00.20s | +0.23% 1m22.90s | Compilers/Named/MapCastInterp | 1m23.00s || -0m00.09s | -0.12% 1m20.68s | Experiments/NewPipeline/Toplevel2 | 1m20.44s || +0m00.24s | +0.29% 1m18.39s | Specific/X2448/Karatsuba/C64/femul | 1m18.94s || -0m00.54s | -0.69% 0m59.68s | Specific/X25519/C32/femul | 0m59.76s || -0m00.07s | -0.13% 0m52.15s | Demo | 0m52.12s || +0m00.03s | +0.05% 0m48.67s | Compilers/Z/Named/RewriteAddToAdcInterp | 0m48.51s || +0m00.16s | +0.32% 0m47.22s | Compilers/Z/ArithmeticSimplifierInterp | 0m47.32s || -0m00.10s | -0.21% 0m42.84s | Specific/X25519/C32/fesquare | 0m43.50s || -0m00.65s | -1.51% 0m42.10s | Arithmetic/Karatsuba | 0m42.20s || -0m00.10s | -0.23% 0m38.01s | p521_32.c | 0m38.05s || -0m00.03s | -0.10% 0m36.32s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m36.66s || -0m00.33s | -0.92% 0m36.19s | Spec/Ed25519 | 0m36.12s || +0m00.07s | +0.19% 0m35.87s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m35.66s || +0m00.21s | +0.58% 0m33.46s | Specific/X25519/C32/freeze | 0m33.57s || -0m00.10s | -0.32% 0m31.65s | p521_64.c | 0m31.69s || -0m00.04s | -0.12% 0m31.00s | Compilers/Z/ArithmeticSimplifierWf | 0m30.88s || +0m00.12s | +0.38% 0m28.08s | Specific/NISTP256/AMD128/femul | 0m27.86s || +0m00.21s | +0.78% 0m26.96s | Primitives/EdDSARepChange | 0m26.98s || -0m00.01s | -0.07% 0m23.51s | p384_32.c | 0m23.44s || +0m00.07s | +0.29% 0m22.20s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m22.12s || +0m00.07s | +0.36% 0m21.52s | Specific/X25519/C32/fesub | 0m21.36s || +0m00.16s | +0.74% 0m21.50s | Arithmetic/Core | 0m21.60s || -0m00.10s | -0.46% 0m20.88s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs | 0m20.72s || +0m00.16s | +0.77% 0m20.80s | Specific/NISTP256/AMD64/fesub | 0m20.75s || +0m00.05s | +0.24% 0m20.61s | Specific/X25519/C64/femul | 0m20.53s || +0m00.07s | +0.38% 0m19.79s | Specific/X25519/C32/Synthesis | 0m19.83s || -0m00.03s | -0.20% 0m19.41s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m19.45s || -0m00.03s | -0.20% 0m19.24s | Specific/X25519/C32/feadd | 0m19.36s || -0m00.12s | -0.61% 0m19.09s | Specific/NISTP256/AMD64/feadd | 0m19.01s || +0m00.07s | +0.42% 0m18.07s | Compilers/Named/MapCastWf | 0m17.97s || +0m00.10s | +0.55% 0m17.41s | Specific/X25519/C64/freeze | 0m17.46s || -0m00.05s | -0.28% 0m17.06s | Specific/X25519/C64/fesquare | 0m17.11s || -0m00.05s | -0.29% 0m15.88s | Specific/NISTP256/AMD64/feopp | 0m15.94s || -0m00.05s | -0.37% 0m15.09s | Specific/NISTP256/AMD128/feadd | 0m15.15s || -0m00.06s | -0.39% 0m14.86s | Specific/NISTP256/AMD128/fesub | 0m14.86s || +0m00.00s | +0.00% 0m14.38s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m14.53s || -0m00.14s | -1.03% 0m14.31s | Specific/NISTP256/AMD64/fenz | 0m14.32s || -0m00.00s | -0.06% 0m14.21s | Specific/X25519/C64/fecarry | 0m14.31s || -0m00.09s | -0.69% 0m13.81s | Arithmetic/Saturated/AddSub | 0m13.77s || +0m00.04s | +0.29% 0m13.79s | Specific/NISTP256/AMD128/fenz | 0m13.76s || +0m00.02s | +0.21% 0m13.21s | Specific/X25519/C64/fesub | 0m13.11s || +0m00.10s | +0.76% 0m12.58s | Compilers/Z/Syntax/Equality | 0m12.60s || -0m00.01s | -0.15% 0m12.20s | Specific/NISTP256/AMD128/feopp | 0m12.28s || -0m00.08s | -0.65% 0m11.96s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs | 0m11.95s || +0m00.01s | +0.08% 0m11.91s | Specific/X25519/C64/feadd | 0m12.01s || -0m00.09s | -0.83% 0m11.46s | Arithmetic/Saturated/MontgomeryAPI | 0m11.53s || -0m00.06s | -0.60% 0m10.95s | Arithmetic/MontgomeryReduction/Proofs | 0m10.92s || +0m00.02s | +0.27% 0m10.84s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.67s || +0m00.16s | +1.59% 0m10.81s | LegacyArithmetic/Double/Proofs/Multiply | 0m10.85s || -0m00.03s | -0.36% 0m10.60s | Arithmetic/Saturated/Core | 0m10.73s || -0m00.13s | -1.21% 0m10.06s | Util/ZUtil | 0m10.07s || -0m00.00s | -0.09% 0m10.00s | Specific/X2448/Karatsuba/C64/Synthesis | 0m09.93s || +0m00.07s | +0.70% 0m08.62s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.65s || -0m00.03s | -0.34% 0m08.54s | LegacyArithmetic/ArchitectureToZLikeProofs | 0m08.66s || -0m00.12s | -1.38% 0m08.41s | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m08.50s || -0m00.08s | -1.05% 0m08.36s | p384_64.c | 0m08.38s || -0m00.02s | -0.23% 0m08.16s | Arithmetic/BarrettReduction/RidiculousFish | 0m08.18s || -0m00.01s | -0.24% 0m08.14s | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate | 0m08.20s || -0m00.05s | -0.73% 0m07.08s | LegacyArithmetic/Double/Proofs/RippleCarryAddSub | 0m07.09s || -0m00.00s | -0.14% 0m07.04s | Specific/NISTP256/AMD64/Synthesis | 0m07.04s || +0m00.00s | +0.00% 0m06.52s | Arithmetic/Saturated/MulSplit | 0m06.56s || -0m00.04s | -0.60% 0m06.51s | Arithmetic/BarrettReduction/Generalized | 0m06.52s || -0m00.00s | -0.15% 0m06.48s | LegacyArithmetic/Pow2BaseProofs | 0m07.09s || -0m00.60s | -8.60% 0m06.44s | Util/FixedWordSizesEquality | 0m06.47s || -0m00.02s | -0.46% 0m06.39s | Compilers/Z/Bounds/InterpretationLemmas/PullCast | 0m06.35s || +0m00.04s | +0.62% 0m06.03s | Specific/X25519/C64/Synthesis | 0m06.18s || -0m00.14s | -2.42% 0m05.48s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.50s || -0m00.01s | -0.36% 0m05.44s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.42s || +0m00.02s | +0.36% 0m05.02s | Arithmetic/BarrettReduction/HAC | 0m04.97s || +0m00.04s | +1.00% 0m04.76s | LegacyArithmetic/InterfaceProofs | 0m05.50s || -0m00.74s | -13.45% 0m04.72s | Specific/Framework/ArithmeticSynthesis/Montgomery | 0m04.70s || +0m00.01s | +0.42% 0m04.53s | Compilers/Z/Bounds/Pipeline/Definition | 0m04.63s || -0m00.09s | -2.15% 0m04.07s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.04s || +0m00.03s | +0.74% 0m03.97s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.09s || -0m00.11s | -2.93% 0m03.89s | LegacyArithmetic/ZBoundedZ | 0m03.91s || -0m00.02s | -0.51% 0m03.78s | Arithmetic/MontgomeryReduction/WordByWord/Proofs | 0m03.76s || +0m00.02s | +0.53% 0m03.72s | p256_32.c | 0m03.70s || +0m00.02s | +0.54% 0m03.72s | secp256k1_32.c | 0m03.81s || -0m00.08s | -2.36% 0m03.69s | LegacyArithmetic/Double/Proofs/ShiftRight | 0m03.62s || +0m00.06s | +1.93% 0m03.54s | Compilers/Z/ArithmeticSimplifier | 0m03.54s || +0m00.00s | +0.00% 0m03.39s | Arithmetic/ModularArithmeticTheorems | 0m03.47s || -0m00.08s | -2.30% 0m03.38s | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy | 0m03.44s || -0m00.06s | -1.74% 0m03.35s | Specific/NISTP256/AMD128/Synthesis | 0m03.40s || -0m00.04s | -1.47% 0m03.34s | LegacyArithmetic/Double/Proofs/Decode | 0m03.36s || -0m00.02s | -0.59% 0m03.24s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.20s || +0m00.04s | +1.25% 0m03.18s | LegacyArithmetic/Double/Proofs/ShiftLeft | 0m03.12s || +0m00.06s | +1.92% 0m03.04s | Util/WordUtil | 0m03.06s || -0m00.02s | -0.65% 0m02.78s | LegacyArithmetic/BarretReduction | 0m02.76s || +0m00.02s | +0.72% 0m02.60s | Arithmetic/Saturated/Freeze | 0m02.56s || +0m00.04s | +1.56% 0m02.28s | Specific/NISTP256/FancyMachine256/Core | 0m02.32s || -0m00.04s | -1.72% 0m02.26s | Specific/NISTP256/FancyMachine256/Montgomery | 0m02.31s || -0m00.05s | -2.16% 0m02.24s | Compilers/Z/Bounds/Relax | 0m02.23s || +0m00.01s | +0.44% 0m02.21s | Specific/NISTP256/FancyMachine256/Barrett | 0m02.24s || -0m00.03s | -1.33% 0m02.21s | p224_32.c | 0m02.22s || -0m00.01s | -0.45% 0m02.10s | Compilers/Z/RewriteAddToAdcInterp | 0m02.16s || -0m00.06s | -2.77% 0m02.06s | Arithmetic/BarrettReduction/Wikipedia | 0m02.14s || -0m00.08s | -3.73% 0m02.05s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m02.10s || -0m00.05s | -2.38% 0m02.03s | curve25519_32.c | 0m02.02s || +0m00.00s | +0.49% 0m01.84s | LegacyArithmetic/MontgomeryReduction | 0m01.85s || -0m00.01s | -0.54% 0m01.78s | Arithmetic/CoreUnfolder | 0m01.69s || +0m00.09s | +5.32% 0m01.68s | Specific/Framework/ReificationTypes | 0m01.73s || -0m00.05s | -2.89% 0m01.64s | p224_64.c | 0m01.52s || +0m00.11s | +7.89% 0m01.60s | p256_64.c | 0m01.58s || +0m00.02s | +1.26% 0m01.48s | Specific/Framework/ArithmeticSynthesis/Base | 0m01.46s || +0m00.02s | +1.36% 0m01.48s | secp256k1_64.c | 0m01.61s || -0m00.13s | -8.07% 0m01.44s | Specific/Framework/OutputType | 0m01.48s || -0m00.04s | -2.70% 0m01.42s | Experiments/NewPipeline/CLI | 0m01.52s || -0m00.10s | -6.57% 0m01.40s | Util/QUtil | 0m01.59s || -0m00.19s | -11.94% 0m01.38s | curve25519_64.c | 0m01.52s || -0m00.14s | -9.21% 0m01.37s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m01.36s || +0m00.01s | +0.73% 0m01.34s | LegacyArithmetic/Double/Proofs/BitwiseOr | 0m01.34s || +0m00.00s | +0.00% 0m01.32s | Arithmetic/PrimeFieldTheorems | 0m01.36s || -0m00.04s | -2.94% 0m01.30s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.19s || +0m00.11s | +9.24% 0m01.30s | LegacyArithmetic/Double/Proofs/LoadImmediate | 0m01.32s || -0m00.02s | -1.51% 0m01.29s | LegacyArithmetic/BaseSystemProofs | 0m01.30s || -0m00.01s | -0.76% 0m01.24s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.22s || +0m00.02s | +1.63% 0m01.18s | Util/ZRange/CornersMonotoneBounds | 0m01.17s || +0m00.01s | +0.85% 0m01.16s | Arithmetic/Saturated/CoreUnfolder | 0m01.24s || -0m00.08s | -6.45% 0m01.14s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.83s || +0m00.30s | +37.34% 0m01.06s | Util/ZUtil/Stabilization | 0m01.05s || +0m00.01s | +0.95% 0m01.00s | Arithmetic/Saturated/WrappersUnfolder | 0m00.97s || +0m00.03s | +3.09% 0m01.00s | Specific/Framework/SynthesisFramework | 0m01.09s || -0m00.09s | -8.25% 0m00.99s | Util/NumTheoryUtil | 0m00.96s || +0m00.03s | +3.12% 0m00.90s | Compilers/MapCastByDeBruijnInterp | 0m00.88s || +0m00.02s | +2.27% 0m00.89s | Arithmetic/Saturated/UniformWeight | 0m00.98s || -0m00.08s | -9.18% 0m00.89s | Compilers/Z/CommonSubexpressionElimination | 0m00.89s || +0m00.00s | +0.00% 0m00.87s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.92s || -0m00.05s | -5.43% 0m00.85s | Compilers/Z/Syntax/Util | 0m00.84s || +0m00.01s | +1.19% 0m00.82s | Arithmetic/Saturated/FreezeUnfolder | 0m00.81s || +0m00.00s | +1.23% 0m00.82s | Specific/Framework/ArithmeticSynthesis/HelperTactics | 0m00.71s || +0m00.10s | +15.49% 0m00.81s | Util/ZUtil/Morphisms | 0m00.75s || +0m00.06s | +8.00% 0m00.79s | Arithmetic/Saturated/MulSplitUnfolder | 0m00.81s || -0m00.02s | -2.46% 0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.77s || +0m00.02s | +2.59% 0m00.76s | Compilers/MapCastByDeBruijnWf | 0m00.73s || +0m00.03s | +4.10% 0m00.76s | LegacyArithmetic/Double/Core | 0m00.60s || +0m00.16s | +26.66% 0m00.76s | LegacyArithmetic/Interface | 0m00.81s || -0m00.05s | -6.17% 0m00.75s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.70s || +0m00.05s | +7.14% 0m00.74s | Arithmetic/Saturated/Wrappers | 0m00.77s || -0m00.03s | -3.89% 0m00.74s | Specific/Framework/ReificationTypesPackage | 0m00.73s || +0m00.01s | +1.36% 0m00.72s | Arithmetic/Saturated/UniformWeightInstances | 0m00.74s || -0m00.02s | -2.70% 0m00.72s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.70s || +0m00.02s | +2.85% 0m00.72s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.70s || +0m00.02s | +2.85% 0m00.72s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.72s || +0m00.00s | +0.00% 0m00.71s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.72s || -0m00.01s | -1.38% 0m00.70s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.69s || +0m00.01s | +1.44% 0m00.70s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.73s || -0m00.03s | -4.10% 0m00.69s | Compilers/Z/Bounds/Pipeline | 0m00.66s || +0m00.02s | +4.54% 0m00.68s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.72s || -0m00.03s | -5.55% 0m00.68s | Specific/Framework/ArithmeticSynthesis/Ladderstep | 0m00.73s || -0m00.04s | -6.84% 0m00.68s | Specific/Framework/MontgomeryReificationTypes | 0m00.72s || -0m00.03s | -5.55% 0m00.68s | Util/NUtil | 0m00.63s || +0m00.05s | +7.93% 0m00.67s | LegacyArithmetic/Double/Proofs/SelectConditional | 0m00.70s || -0m00.02s | -4.28% 0m00.66s | Compilers/Z/MapCastByDeBruijnWf | 0m00.82s || -0m00.15s | -19.51% 0m00.64s | Compilers/Z/Bounds/MapCastByDeBruijn | 0m00.59s || +0m00.05s | +8.47% 0m00.64s | Compilers/Z/Bounds/MapCastByDeBruijnInterp | 0m00.56s || +0m00.07s | +14.28% 0m00.63s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.55s || +0m00.07s | +14.54% 0m00.61s | Compilers/Z/CommonSubexpressionEliminationInterp | 0m00.51s || +0m00.09s | +19.60% 0m00.61s | Compilers/Z/Reify | 0m00.56s || +0m00.04s | +8.92% 0m00.58s | Compilers/Z/Bounds/InterpretationLemmas/Tactics | 0m00.60s || -0m00.02s | -3.33% 0m00.58s | Compilers/Z/Bounds/MapCastByDeBruijnWf | 0m00.56s || +0m00.01s | +3.57% 0m00.58s | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.56s || +0m00.01s | +3.57% 0m00.56s | Compilers/Z/MapCastByDeBruijnInterp | 0m00.56s || +0m00.00s | +0.00% 0m00.56s | LegacyArithmetic/ArchitectureToZLike | 0m00.60s || -0m00.03s | -6.66% 0m00.56s | LegacyArithmetic/ZBounded | 0m00.58s || -0m00.01s | -3.44% 0m00.55s | Arithmetic/ModularArithmeticPre | 0m00.56s || -0m00.01s | -1.78% 0m00.55s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.51s || +0m00.04s | +7.84% 0m00.54s | Compilers/Z/CommonSubexpressionEliminationWf | 0m00.53s || +0m00.01s | +1.88% 0m00.54s | Spec/ModularArithmetic | 0m00.44s || +0m00.10s | +22.72% 0m00.53s | Spec/EdDSA | 0m00.48s || +0m00.05s | +10.41% 0m00.52s | LegacyArithmetic/BaseSystem | 0m00.51s || +0m00.01s | +1.96% 0m00.51s | Compilers/Z/InlineInterp | 0m00.50s || +0m00.01s | +2.00% 0m00.50s | Compilers/Z/FoldTypes | 0m00.47s || +0m00.03s | +6.38% 0m00.50s | Compilers/Z/InlineConstAndOp | 0m00.48s || +0m00.02s | +4.16% 0m00.50s | Compilers/Z/InlineConstAndOpByRewrite | 0m00.49s || +0m00.01s | +2.04% 0m00.50s | Compilers/Z/InlineConstAndOpByRewriteWf | 0m00.51s || -0m00.01s | -1.96% 0m00.50s | Compilers/Z/InlineConstAndOpInterp | 0m00.50s || +0m00.00s | +0.00% 0m00.50s | Compilers/ZExtended/MapBaseType | 0m00.48s || +0m00.02s | +4.16% 0m00.49s | Compilers/Z/InlineConstAndOpWf | 0m00.48s || +0m00.01s | +2.08% 0m00.48s | Compilers/Z/InterpSideConditions | 0m00.46s || +0m00.01s | +4.34% 0m00.47s | Compilers/Z/InlineWf | 0m00.48s || -0m00.01s | -2.08% 0m00.46s | Compilers/Z/Inline | 0m00.50s || -0m00.03s | -7.99% 0m00.46s | Compilers/Z/InlineConstAndOpByRewriteInterp | 0m00.51s || -0m00.04s | -9.80% 0m00.46s | LegacyArithmetic/Pow2Base | 0m00.51s || -0m00.04s | -9.80% 0m00.43s | Arithmetic/MontgomeryReduction/Definition | 0m00.48s || -0m00.04s | -10.41%
* Revert "Improve rewriter speed"Gravatar Jason Gross2018-07-24
| | | | | | | This reverts commit 152094f4d9d83e4a5689536e0cd68d4f006517e1. It is actually incorrect. We need to bubble up failures, not just let-bind the default case. Will fix tomorrow.
* Improve rewriter speedGravatar Jason Gross2018-07-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Andres and I met today, and discovered that there's a source of non-linear complexity in the rewriter which is not type casts. In adding side-conditions to the rewrite rules (which are not discussed in the pattern-matching compilation paper), I represented them by allowing rewrite rules to fail. So, for example, # + x ~~> x (when # == 0) is represented as # + x ~~> if (# =? 0) then Some x else None In the case that a rewrite rule fails, we need to try all other rewrite rules that might still apply. However, doing this in the naive-CPS way leads to non-linear blowup, because wildcard rewrite rules get duplicated in the failure branches. (This is similar to the issue that `match x with "some string" => true | _ => false end%string` will generate a large number of "false" branches, and duplicate "false" across all of them, rather than having a single default case.) For example, if we had the rewrite rules # + # ~~> literal sum x + (-y) ~~> x - y (-x) + y ~~> y - x then the compiled code would look like fun x y => if x is a literal then if y is a literal then literal sum else if y is an opp then x - y else x + y else if y is an opp then x - y else if x is an opp then y - x else x + y where we actually want the code fun x y => if x is a literal then if y is a literal then return (literal sum); if y is an opp then return (x - y); if x is an opp then return (y - x); return (x + y) in the sequence+return monad. i.e., we want to not duplicate the "if y is an opp" code multiple times. I think the solution to this is to have the discrimination tree evaluator return an option, and to have the function that computes the discrimination tree not duplicate rewrite rules among different cases. Note that this leads to slightly inefficient matching sometimes: when two rules with the same structure are separated by a rule with a wildcard instead of structure, we will now try to match on the structure twice. It might be useful to be able to denote that some rewrite rules can be commuted. After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------------------------------------------- 40m35.83s | Total | 30m00.99s || +10m34.84s | +35.24% ---------------------------------------------------------------------------------------------------------------------- 21m46.37s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m01.39s || +15m44.97s | +261.48% 6m37.40s | p384_32.c | 0m22.47s || +6m14.92s | +1668.58% 0m18.00s | Experiments/NewPipeline/Rewriter | 5m16.50s || -4m58.50s | -94.31% 0m30.49s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 1m54.20s || -1m23.71s | -73.30% 0m27.41s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 1m39.40s || -1m11.99s | -72.42% 0m47.78s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 1m54.50s || -1m06.71s | -58.27% 0m40.28s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 1m23.77s || -0m43.48s | -51.91% 0m15.21s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m55.86s || -0m40.64s | -72.77% 0m23.39s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 1m00.22s || -0m36.82s | -61.15% 0m21.85s | p256_32.c | 0m04.01s || +0m17.84s | +444.88% 0m20.97s | secp256k1_32.c | 0m03.26s || +0m17.71s | +543.25% 0m04.60s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m20.33s || -0m15.72s | -77.37% 0m09.48s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m23.28s || -0m13.80s | -59.27% 1m33.63s | Experiments/NewPipeline/Toplevel2 | 1m45.56s || -0m11.93s | -11.30% 0m08.29s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m18.64s || -0m10.35s | -55.52% 0m05.93s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m16.74s || -0m10.80s | -64.57% 0m32.41s | p521_64.c | 0m41.42s || -0m09.01s | -21.75% 0m04.93s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m14.92s || -0m09.99s | -66.95% 0m04.40s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m12.57s || -0m08.16s | -64.99% 0m08.52s | p224_32.c | 0m01.95s || +0m06.56s | +336.92% 0m13.99s | p384_64.c | 0m10.64s || +0m03.34s | +31.48% 4m07.13s | Experiments/NewPipeline/Toplevel1 | 4m05.83s || +0m01.29s | +0.52% 0m38.96s | p521_32.c | 0m40.09s || -0m01.13s | -2.81% 0m02.28s | p224_64.c | 0m01.66s || +0m00.61s | +37.34% 0m02.27s | curve25519_32.c | 0m01.98s || +0m00.29s | +14.64% 0m01.78s | p256_64.c | 0m01.65s || +0m00.13s | +7.87% 0m01.70s | secp256k1_64.c | 0m01.96s || -0m00.26s | -13.26% 0m01.65s | curve25519_64.c | 0m01.51s || +0m00.13s | +9.27% 0m01.37s | Experiments/NewPipeline/CLI | 0m01.26s || +0m00.11s | +8.73% 0m01.15s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.21s || -0m00.06s | -4.95% 0m01.14s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.16s || -0m00.02s | -1.72% 0m01.07s | Experiments/NewPipeline/CompilersTestCases | 0m01.05s || +0m00.02s | +1.90%
* Add some primes to be synthesizedGravatar Jason Gross2018-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 07:52:30 +0000