| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
| |
|
|
|
|
| |
This is needed to reify statements for the rewriter.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
|
|
|
|
|
|
|
|
| |
We now stringify the correctness conditions to generate docstrings for
the synthesized code.
Closes #512
Time commitment: about 6 hours
|
|
|