aboutsummaryrefslogtreecommitdiff
path: root/src/BoundsPipeline.v
Commit message (Collapse)AuthorAge
* sed s'/RewriterProofs/RewriterAll/g'Gravatar Jason Gross2019-04-11
|
* Make a single tactic to build the rewriterGravatar Jason Gross2019-04-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Parallelize across different rewriters, rather than across different parts of the rewriter. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m38.03s | Total | 20m17.67s || +0m20.36s | +1.67% ----------------------------------------------------------------------------------------------- N/A | RewriterFull.vo | 1m11.76s || -1m11.76s | -100.00% 0m56.15s | Rewriter/ToFancyWithCasts.vo | N/A || +0m56.14s | ∞ N/A | RewriterRulesInterpGood.vo | 0m51.06s || -0m51.06s | -100.00% 0m45.62s | Rewriter/NBE.vo | N/A || +0m45.61s | ∞ 0m44.32s | Rewriter/ArithWithCasts.vo | N/A || +0m44.32s | ∞ 0m24.56s | Rewriter/Arith.vo | N/A || +0m24.55s | ∞ N/A | RewriterRulesGood.vo | 0m21.60s || -0m21.60s | -100.00% 1m34.27s | RewriterWf2.vo | 1m43.16s || -0m08.88s | -8.61% 3m21.20s | p384_32.c | 3m28.08s || -0m06.87s | -3.30% 1m40.72s | Fancy/Barrett256.vo | 1m43.94s || -0m03.21s | -3.09% 0m41.11s | p521_64.c | 0m38.11s || +0m03.00s | +7.87% 0m47.88s | p521_32.c | 0m44.98s || +0m02.90s | +6.44% 0m23.68s | ExtractionOCaml/word_by_word_montgomery | 0m21.56s || +0m02.12s | +9.83% 0m58.92s | ExtractionHaskell/word_by_word_montgomery | 0m57.87s || +0m01.05s | +1.81% 0m20.05s | p448_solinas_64.c | 0m18.72s || +0m01.33s | +7.10% 0m15.19s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.76s || +0m01.42s | +10.39% 0m14.64s | ExtractionOCaml/unsaturated_solinas | 0m13.55s || +0m01.08s | +8.04% 0m09.19s | ExtractionOCaml/saturated_solinas | 0m10.69s || -0m01.50s | -14.03% 0m08.65s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.85s || -0m01.19s | -12.18% 0m07.71s | ExtractionOCaml/saturated_solinas.ml | 0m06.26s || +0m01.45s | +23.16% 0m05.93s | ExtractionHaskell/saturated_solinas.hs | 0m04.71s || +0m01.21s | +25.90% 0m01.16s | Rewriter/StripLiteralCasts.vo | N/A || +0m01.15s | ∞ 0m01.14s | Rewriter/ToFancy.vo | N/A || +0m01.13s | ∞ 0m44.44s | RewriterInterpProofs1.vo | 0m45.18s || -0m00.74s | -1.63% 0m39.85s | ExtractionHaskell/unsaturated_solinas | 0m40.68s || -0m00.82s | -2.04% 0m36.42s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.44s || -0m00.01s | -0.05% 0m36.21s | RewriterWf1.vo | 0m36.91s || -0m00.69s | -1.89% 0m34.81s | Fancy/Montgomery256.vo | 0m34.38s || +0m00.42s | +1.25% 0m30.85s | ExtractionHaskell/saturated_solinas | 0m31.77s || -0m00.91s | -2.89% 0m27.26s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.09s || +0m00.17s | +0.62% 0m26.88s | SlowPrimeSynthesisExamples.vo | 0m27.32s || -0m00.44s | -1.61% 0m20.88s | PushButtonSynthesis/BarrettReduction.vo | 0m21.17s || -0m00.29s | -1.36% 0m18.08s | secp256k1_32.c | 0m18.44s || -0m00.36s | -1.95% 0m17.39s | p256_32.c | 0m17.74s || -0m00.34s | -1.97% 0m15.12s | p434_64.c | 0m14.68s || +0m00.43s | +2.99% 0m09.02s | p224_32.c | 0m08.11s || +0m00.91s | +11.22% 0m07.91s | p384_64.c | 0m07.92s || -0m00.00s | -0.12% 0m07.89s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.50s || +0m00.38s | +5.19% 0m07.02s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.60s || -0m00.58s | -7.63% 0m06.91s | BoundsPipeline.vo | 0m06.92s || -0m00.00s | -0.14% 0m03.56s | PushButtonSynthesis/Primitives.vo | 0m03.53s || +0m00.03s | +0.84% 0m03.39s | PushButtonSynthesis/SmallExamples.vo | 0m03.25s || +0m00.14s | +4.30% 0m03.32s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.14s || +0m00.17s | +5.73% 0m02.83s | curve25519_32.c | 0m02.41s || +0m00.41s | +17.42% 0m02.72s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.62s || +0m00.10s | +3.81% 0m01.91s | secp256k1_64.c | 0m01.89s || +0m00.02s | +1.05% 0m01.75s | curve25519_64.c | 0m02.14s || -0m00.39s | -18.22% 0m01.60s | p224_64.c | 0m01.60s || +0m00.00s | +0.00% 0m01.43s | p256_64.c | 0m01.82s || -0m00.39s | -21.42% 0m01.30s | CLI.vo | 0m01.35s || -0m00.05s | -3.70% 0m01.22s | StandaloneOCamlMain.vo | 0m01.07s || +0m00.14s | +14.01% 0m01.18s | CompilersTestCases.vo | 0m01.14s || +0m00.04s | +3.50% 0m01.12s | StandaloneHaskellMain.vo | 0m01.14s || -0m00.01s | -1.75% 0m00.84s | RewriterProofsTactics.vo | N/A || +0m00.84s | ∞ 0m00.83s | RewriterProofs.vo | 0m01.06s || -0m00.23s | -21.69%
* Automate more of the rewriter, and factor out rule-specific thingsGravatar Jason Gross2019-04-11
|
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
| | | | This is needed to reify statements for the rewriter.
* Insert casts before literals during bounds analysisGravatar Jason Gross2019-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unless we explicitly say not to. The ability to explicitly say not to is required for, e.g., eta-expansion where we want to replace variable lists of known length with with cons cells indexing into the variable list, but don't want to pollute the code with casts. Uniformity in this way allows rewrite rules to not blow up exponentially (in the number of wildcards); we previously required a separate rewrite rule for each way of choosing between wildcard and literal. To preserve output of the pipeline, we add another pass that just strips the casts off of literals at the end. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 20m27.24s | Total | 22m39.70s || -2m12.46s | -9.74% -------------------------------------------------------------------------------------------- 0m44.27s | Rewriter.vo | 2m11.58s || -1m27.31s | -66.35% 1m15.23s | RewriterRulesInterpGood.vo | 1m50.28s || -0m35.04s | -31.78% 1m40.19s | RewriterRulesGood.vo | 1m58.05s || -0m17.85s | -15.12% 0m26.99s | AbstractInterpretationProofs.vo | 0m16.91s || +0m10.07s | +59.60% 3m15.98s | p384_32.c | 3m07.78s || +0m08.19s | +4.36% 0m42.52s | ExtractionHaskell/word_by_word_montgomery | 0m44.60s || -0m02.07s | -4.66% 0m28.63s | ExtractionHaskell/unsaturated_solinas | 0m31.38s || -0m02.75s | -8.76% 0m21.76s | ExtractionHaskell/saturated_solinas | 0m24.56s || -0m02.79s | -11.40% 0m09.87s | ExtractionOCaml/unsaturated_solinas | 0m11.28s || -0m01.41s | -12.50% 1m59.22s | RewriterWf2.vo | 2m00.09s || -0m00.87s | -0.72% 1m07.03s | Fancy/Montgomery256.vo | 1m07.31s || -0m00.28s | -0.41% 0m52.60s | Fancy/Barrett256.vo | 0m53.16s || -0m00.55s | -1.05% 0m48.17s | RewriterInterpProofs1.vo | 0m48.72s || -0m00.54s | -1.12% 0m40.16s | AbstractInterpretationWf.vo | 0m40.23s || -0m00.07s | -0.17% 0m38.35s | p521_32.c | 0m38.26s || +0m00.09s | +0.23% 0m31.56s | p521_64.c | 0m31.53s || +0m00.02s | +0.09% 0m24.64s | RewriterWf1.vo | 0m24.01s || +0m00.62s | +2.62% 0m23.54s | AbstractInterpretationZRangeProofs.vo | 0m23.64s || -0m00.10s | -0.42% 0m23.48s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.26s || +0m00.21s | +0.94% 0m20.92s | SlowPrimeSynthesisExamples.vo | 0m20.62s || +0m00.30s | +1.45% 0m19.92s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s || +0m00.12s | +0.60% 0m16.60s | ExtractionOCaml/word_by_word_montgomery | 0m17.56s || -0m00.95s | -5.46% 0m14.72s | p448_solinas_64.c | 0m14.66s || +0m00.06s | +0.40% 0m13.70s | secp256k1_32.c | 0m13.45s || +0m00.25s | +1.85% 0m13.68s | p256_32.c | 0m13.33s || +0m00.34s | +2.62% 0m13.28s | CStringification.vo | 0m13.26s || +0m00.01s | +0.15% 0m11.88s | p484_64.c | 0m11.74s || +0m00.14s | +1.19% 0m09.96s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.24s || -0m00.27s | -2.73% 0m07.47s | ExtractionOCaml/saturated_solinas | 0m07.93s || -0m00.46s | -5.80% 0m06.78s | BoundsPipeline.vo | 0m05.96s || +0m00.82s | +13.75% 0m06.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.03s || -0m00.31s | -4.40% 0m06.38s | p224_32.c | 0m06.54s || -0m00.16s | -2.44% 0m06.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s || -0m00.12s | -2.05% 0m05.45s | p384_64.c | 0m05.18s || +0m00.27s | +5.21% 0m04.82s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.84s || -0m00.01s | -0.41% 0m04.80s | ExtractionOCaml/saturated_solinas.ml | 0m05.07s || -0m00.27s | -5.32% 0m03.83s | ExtractionHaskell/saturated_solinas.hs | 0m04.07s || -0m00.24s | -5.89% 0m03.30s | PushButtonSynthesis/Primitives.vo | 0m03.31s || -0m00.01s | -0.30% 0m03.26s | PushButtonSynthesis/SmallExamples.vo | 0m03.24s || +0m00.01s | +0.61% 0m03.08s | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.96s || +0m00.12s | +4.05% 0m02.16s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.00% 0m01.57s | curve25519_64.c | 0m01.47s || +0m00.10s | +6.80% 0m01.40s | CLI.vo | 0m01.32s || +0m00.07s | +6.06% 0m01.27s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.19s || +0m00.08s | +6.72% 0m01.26s | StandaloneHaskellMain.vo | 0m01.18s || +0m00.08s | +6.77% 0m01.22s | PushButtonSynthesis/BarrettReduction.vo | 0m01.29s || -0m00.07s | -5.42% 0m01.13s | RewriterProofs.vo | 0m01.10s || +0m00.02s | +2.72% 0m01.10s | secp256k1_64.c | 0m01.01s || +0m00.09s | +8.91% 0m01.08s | StandaloneOCamlMain.vo | 0m01.13s || -0m00.04s | -4.42% 0m01.06s | p256_64.c | 0m01.02s || +0m00.04s | +3.92% 0m01.05s | AbstractInterpretation.vo | 0m01.00s || +0m00.05s | +5.00% 0m01.00s | CompilersTestCases.vo | 0m01.08s || -0m00.08s | -7.40% 0m01.00s | p224_64.c | 0m01.00s || +0m00.00s | +0.00%
* 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
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:17:00 +0000