| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
Also remove a rewrite rule using cast from the non-cast arith rules,
regenerate the .out files, add ident.gets_inlined for eventual use in
the rewriter, and generalize the rewrite rule lemmas over
cast_out_of_range so that we can actually make use of their proofs for
interp.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
|
|