| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
22m23.84s | Total | 21m34.63s || +0m49.21s | +3.80%
--------------------------------------------------------------------------------------------
1m52.62s | RewriterRulesInterpGood.vo | 1m37.14s || +0m15.48s | +15.93%
3m25.91s | p384_32.c | 3m14.24s || +0m11.66s | +6.00%
1m32.94s | RewriterRulesGood.vo | 1m42.36s || -0m09.42s | -9.20%
0m33.72s | RewriterWf1.vo | 0m24.30s || +0m09.41s | +38.76%
1m17.31s | Rewriter.vo | 1m12.10s || +0m05.21s | +7.22%
0m43.01s | ExtractionHaskell/unsaturated_solinas | 0m39.84s || +0m03.16s | +7.95%
0m45.21s | p521_32.c | 0m42.86s || +0m02.35s | +5.48%
1m46.30s | Fancy/Barrett256.vo | 1m45.08s || +0m01.21s | +1.16%
0m38.74s | p521_64.c | 0m37.49s || +0m01.25s | +3.33%
0m23.16s | ExtractionOCaml/word_by_word_montgomery | 0m21.44s || +0m01.71s | +8.02%
0m18.74s | p256_32.c | 0m16.88s || +0m01.85s | +11.01%
0m15.00s | ExtractionOCaml/unsaturated_solinas | 0m13.98s || +0m01.01s | +7.29%
0m11.92s | ExtractionOCaml/saturated_solinas | 0m10.13s || +0m01.78s | +17.67%
0m07.82s | ExtractionOCaml/saturated_solinas.ml | 0m05.98s || +0m01.83s | +30.76%
1m47.42s | RewriterWf2.vo | 1m47.81s || -0m00.39s | -0.36%
0m58.35s | ExtractionHaskell/word_by_word_montgomery | 0m57.41s || +0m00.94s | +1.63%
0m45.47s | RewriterInterpProofs1.vo | 0m45.67s || -0m00.20s | -0.43%
0m37.34s | Fancy/Montgomery256.vo | 0m37.09s || +0m00.25s | +0.67%
0m36.14s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.52s || -0m00.38s | -1.04%
0m29.91s | ExtractionHaskell/saturated_solinas | 0m29.70s || +0m00.21s | +0.70%
0m26.77s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.72s || +0m00.05s | +0.18%
0m25.87s | SlowPrimeSynthesisExamples.vo | 0m25.49s || +0m00.38s | +1.49%
0m18.72s | p448_solinas_64.c | 0m19.16s || -0m00.44s | -2.29%
0m16.94s | secp256k1_32.c | 0m17.18s || -0m00.23s | -1.39%
0m13.92s | p434_64.c | 0m13.08s || +0m00.83s | +6.42%
0m13.15s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.58s || +0m00.57s | +4.53%
0m08.97s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.95s || +0m00.02s | +0.22%
0m08.37s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s || -0m00.14s | -1.64%
0m08.35s | p224_32.c | 0m08.10s || +0m00.25s | +3.08%
0m07.77s | p384_64.c | 0m07.29s || +0m00.47s | +6.58%
0m06.92s | BoundsPipeline.vo | 0m06.85s || +0m00.07s | +1.02%
0m05.70s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.14s || -0m00.43s | -7.16%
0m05.12s | ExtractionHaskell/saturated_solinas.hs | 0m06.09s || -0m00.96s | -15.92%
0m03.53s | PushButtonSynthesis/Primitives.vo | 0m03.55s || -0m00.02s | -0.56%
0m03.38s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.04s | +1.19%
0m03.16s | PushButtonSynthesis/BarrettReduction.vo | 0m03.24s || -0m00.08s | -2.46%
0m03.06s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.23s || -0m00.16s | -5.26%
0m02.81s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.84s || -0m00.02s | -1.05%
0m02.62s | curve25519_32.c | 0m02.22s || +0m00.39s | +18.01%
0m01.88s | p224_64.c | 0m01.47s || +0m00.40s | +27.89%
0m01.68s | curve25519_64.c | 0m02.19s || -0m00.51s | -23.28%
0m01.32s | CLI.vo | 0m01.33s || -0m00.01s | -0.75%
0m01.24s | secp256k1_64.c | 0m01.30s || -0m00.06s | -4.61%
0m01.22s | p256_64.c | 0m01.47s || -0m00.25s | -17.00%
0m01.16s | RewriterProofs.vo | 0m01.16s || +0m00.00s | +0.00%
0m01.10s | StandaloneHaskellMain.vo | 0m01.00s || +0m00.10s | +10.00%
0m01.05s | CompilersTestCases.vo | 0m01.09s || -0m00.04s | -3.66%
0m01.04s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.00s | +0.00%
|
|
|
|
|
|
|
|
| |
Rather than using Forall2 in some places and a combination of length,
combine, and In in others, we now primarily use Forall2.
There is probably some dead tactic code as a result of this that I just
haven't bothered to clean up.
|
| |
|
|
|
|
| |
These will be useful for extending the AST with `option` types.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
|
|