| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now we actually make use of the rewrite-rule-specific proofs, rather
than duplicating them inline.
We now support reifying `ident.gets_inlined` to
`SubstVarLike.is_var_fst_snd_pair_opp_cast`.
We also now fix a bug where we previously incorrectly substituted
context variables when reifying side conditions (needed for correct
reification of split-mul things, coming up soon).
Things are unfortunately a bit slow.
I'm not sure what's up with my proof of
`reflect_ident_iota_interp_related`; it seems more complicated than it
should be (maybe partly due to funext concerns).
Next up is to split out the rewrite rule generation bits into separate
files and have a single tactic that builds the entire package for us (in
prep for making the rewriter builder a vernacular). After that I want
to more fully parameterize things over `ident`, and then also over the
non-container base-types (which will require some reworking of how we
handle special identifiers). Additionally, I want to make the rewrite
rule definitions not depend on Language.v.
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------
20m50.18s | Total | 23m01.24s || -2m11.06s | -9.48%
-----------------------------------------------------------------------------------------------
0m27.24s | RewriterRulesGood.vo | 1m34.94s || -1m07.70s | -71.30%
0m54.89s | RewriterRulesInterpGood.vo | 1m57.72s || -1m02.82s | -53.37%
1m37.88s | RewriterWf2.vo | 1m47.69s || -0m09.81s | -9.10%
1m16.71s | Rewriter.vo | 1m12.61s || +0m04.10s | +5.64%
0m37.14s | ExtractionHaskell/unsaturated_solinas | 0m40.06s || -0m02.92s | -7.28%
0m36.10s | RewriterWf1.vo | 0m33.12s || +0m02.98s | +8.99%
0m18.31s | p256_32.c | 0m20.70s || -0m02.39s | -11.54%
1m43.31s | Fancy/Barrett256.vo | 1m42.09s || +0m01.21s | +1.19%
0m32.46s | ExtractionHaskell/saturated_solinas | 0m30.92s || +0m01.53s | +4.98%
0m23.44s | ExtractionOCaml/word_by_word_montgomery | 0m22.26s || +0m01.17s | +5.30%
0m12.17s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.58s || -0m01.41s | -10.38%
0m10.04s | p224_32.c | 0m08.20s || +0m01.83s | +22.43%
0m09.98s | ExtractionOCaml/saturated_solinas | 0m11.67s || -0m01.68s | -14.48%
0m07.80s | ExtractionOCaml/saturated_solinas.ml | 0m06.16s || +0m01.63s | +26.62%
0m06.87s | ExtractionHaskell/saturated_solinas.hs | 0m04.98s || +0m01.88s | +37.95%
3m23.11s | p384_32.c | 3m22.61s || +0m00.50s | +0.24%
0m59.32s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || +0m00.56s | +0.95%
0m46.19s | p521_32.c | 0m47.16s || -0m00.96s | -2.05%
0m45.26s | RewriterInterpProofs1.vo | 0m45.64s || -0m00.38s | -0.83%
0m39.50s | p521_64.c | 0m38.97s || +0m00.53s | +1.36%
0m36.38s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.00s || +0m00.38s | +1.05%
0m34.40s | Fancy/Montgomery256.vo | 0m34.63s || -0m00.23s | -0.66%
0m26.95s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.44s || +0m00.50s | +1.92%
0m25.62s | SlowPrimeSynthesisExamples.vo | 0m26.04s || -0m00.41s | -1.61%
0m24.39s | RewriterRulesProofs.vo | 0m24.18s || +0m00.21s | +0.86%
0m20.49s | PushButtonSynthesis/BarrettReduction.vo | 0m20.62s || -0m00.13s | -0.63%
0m18.54s | p448_solinas_64.c | 0m19.15s || -0m00.60s | -3.18%
0m17.37s | secp256k1_32.c | 0m17.70s || -0m00.32s | -1.86%
0m14.80s | p434_64.c | 0m14.16s || +0m00.64s | +4.51%
0m14.05s | ExtractionOCaml/unsaturated_solinas | 0m14.28s || -0m00.22s | -1.61%
0m09.17s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.58s || -0m00.41s | -4.27%
0m08.47s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.22s || +0m00.25s | +3.04%
0m07.69s | p384_64.c | 0m07.72s || -0m00.02s | -0.38%
0m06.80s | BoundsPipeline.vo | 0m06.65s || +0m00.14s | +2.25%
0m06.49s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.59s || +0m00.90s | +16.10%
0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.08s | +2.31%
0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.36s || -0m00.00s | -0.29%
0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.15s || +0m00.04s | +1.26%
0m02.79s | curve25519_32.c | 0m03.32s || -0m00.52s | -15.96%
0m02.66s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s || -0m00.06s | -2.56%
0m02.55s | RewriterRules.vo | 0m02.52s || +0m00.02s | +1.19%
0m01.98s | curve25519_64.c | 0m01.57s || +0m00.40s | +26.11%
0m01.78s | p224_64.c | 0m01.30s || +0m00.48s | +36.92%
0m01.60s | secp256k1_64.c | 0m01.74s || -0m00.13s | -8.04%
0m01.45s | p256_64.c | 0m01.55s || -0m00.10s | -6.45%
0m01.34s | RewriterProofs.vo | 0m01.16s || +0m00.18s | +15.51%
0m01.33s | CLI.vo | 0m01.40s || -0m00.06s | -4.99%
0m01.12s | StandaloneOCamlMain.vo | 0m01.09s || +0m00.03s | +2.75%
0m01.10s | CompilersTestCases.vo | 0m01.08s || +0m00.02s | +1.85%
0m01.08s | StandaloneHaskellMain.vo | 0m01.02s || +0m00.06s | +5.88%
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Move rewrite rule definitions, and the proofs about them, into separate
files.
We don't yet make use of the separate interp proofs of rewrite rules;
the next step is to refactor the interp proof machinery so that we can
easily prove the relevant interp relations, given the equality proofs in
`src/RewriterRulesProofs.v`
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
23m01.93s | Total | 22m37.08s || +0m24.84s | +1.83%
--------------------------------------------------------------------------------------------
0m24.10s | RewriterRulesProofs.vo | N/A || +0m24.10s | ∞
1m12.13s | Rewriter.vo | 1m20.61s || -0m08.48s | -10.51%
0m41.17s | ExtractionHaskell/unsaturated_solinas | 0m37.57s || +0m03.60s | +9.58%
1m42.40s | Fancy/Barrett256.vo | 1m40.22s || +0m02.18s | +2.17%
0m45.56s | p521_32.c | 0m48.16s || -0m02.59s | -5.39%
0m14.48s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.47s || +0m02.00s | +16.11%
1m48.48s | RewriterWf2.vo | 1m46.70s || +0m01.77s | +1.66%
0m15.06s | ExtractionOCaml/unsaturated_solinas | 0m14.06s || +0m01.00s | +7.11%
0m06.26s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.29s || -0m01.03s | -14.12%
0m04.71s | ExtractionHaskell/saturated_solinas.hs | 0m06.05s || -0m01.33s | -22.14%
3m22.17s | p384_32.c | 3m23.06s || -0m00.88s | -0.43%
1m57.31s | RewriterRulesInterpGood.vo | 1m56.61s || +0m00.70s | +0.60%
1m35.20s | RewriterRulesGood.vo | 1m35.80s || -0m00.59s | -0.62%
0m57.50s | ExtractionHaskell/word_by_word_montgomery | 0m56.53s || +0m00.96s | +1.71%
0m45.71s | RewriterInterpProofs1.vo | 0m46.13s || -0m00.42s | -0.91%
0m39.66s | p521_64.c | 0m38.90s || +0m00.75s | +1.95%
0m36.22s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.42s || -0m00.20s | -0.54%
0m34.39s | Fancy/Montgomery256.vo | 0m34.45s || -0m00.06s | -0.17%
0m33.16s | RewriterWf1.vo | 0m32.96s || +0m00.19s | +0.60%
0m32.21s | ExtractionHaskell/saturated_solinas | 0m31.53s || +0m00.67s | +2.15%
0m26.94s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.20s || -0m00.25s | -0.95%
0m25.89s | SlowPrimeSynthesisExamples.vo | 0m25.59s || +0m00.30s | +1.17%
0m23.37s | ExtractionOCaml/word_by_word_montgomery | 0m22.90s || +0m00.47s | +2.05%
0m21.19s | PushButtonSynthesis/BarrettReduction.vo | 0m20.79s || +0m00.40s | +1.92%
0m18.30s | p256_32.c | 0m18.54s || -0m00.23s | -1.29%
0m18.29s | p448_solinas_64.c | 0m18.58s || -0m00.28s | -1.56%
0m17.92s | secp256k1_32.c | 0m18.41s || -0m00.48s | -2.66%
0m14.06s | p434_64.c | 0m13.92s || +0m00.14s | +1.00%
0m11.61s | ExtractionOCaml/saturated_solinas | 0m11.57s || +0m00.03s | +0.34%
0m08.90s | p224_32.c | 0m09.12s || -0m00.21s | -2.41%
0m08.49s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.85s || -0m00.35s | -4.06%
0m08.45s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.62s || -0m00.16s | -1.97%
0m08.02s | p384_64.c | 0m07.04s || +0m00.97s | +13.92%
0m07.01s | ExtractionOCaml/saturated_solinas.ml | 0m06.57s || +0m00.43s | +6.69%
0m06.67s | BoundsPipeline.vo | 0m06.87s || -0m00.20s | -2.91%
0m03.39s | PushButtonSynthesis/Primitives.vo | 0m03.44s || -0m00.04s | -1.45%
0m03.36s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.02s | -0.59%
0m03.23s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.21s || +0m00.02s | +0.62%
0m03.04s | curve25519_32.c | 0m02.68s || +0m00.35s | +13.43%
0m02.74s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.55s || +0m00.19s | +7.45%
0m02.19s | curve25519_64.c | 0m01.81s || +0m00.37s | +20.99%
0m01.72s | secp256k1_64.c | 0m01.46s || +0m00.26s | +17.80%
0m01.56s | p256_64.c | 0m01.22s || +0m00.34s | +27.86%
0m01.49s | p224_64.c | 0m01.56s || -0m00.07s | -4.48%
0m01.32s | CLI.vo | 0m01.32s || +0m00.00s | +0.00%
0m01.14s | StandaloneHaskellMain.vo | 0m01.08s || +0m00.05s | +5.55%
0m01.06s | CompilersTestCases.vo | 0m01.04s || +0m00.02s | +1.92%
0m01.06s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.06s | -5.35%
0m01.00s | RewriterProofs.vo | 0m01.13s || -0m00.12s | -11.50%
0m00.64s | RewriterRules.vo | N/A || +0m00.64s | ∞
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 taking the convention that failures during constr
construction emit a type error from `I : I` with the actual error
message `idtac`d above them (because Coq has no way to emit multiple
things on stderr), we instead factor everything through a new
`constr_fail` or `constr_fail_with msg_tac`, which emit more helpful
messages instructing the user to look in `*coq*` or to use `Fail`/`try`
to see the more informative error message. When we can make our own
version that does both `idtac` and `fail` (c.f.
https://github.com/coq/coq/issues/3913), then we can do something a bit
more sane, hopefully.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently we don't handle rules that require "concrete list of cons
cells" nor rules that require "concrete nat literal to do recursion on";
both of these require special treatment, to be implemented in an
upcoming commit.
The reifier is kind-of slow, alas.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m52.72s | Total | 21m20.90s || +0m31.82s | +2.48%
--------------------------------------------------------------------------------------------
1m12.22s | Rewriter.vo | 0m47.38s || +0m24.83s | +52.42%
3m14.35s | p384_32.c | 3m19.59s || -0m05.24s | -2.62%
1m45.12s | RewriterRulesGood.vo | 1m39.44s || +0m05.68s | +5.71%
0m40.82s | ExtractionHaskell/unsaturated_solinas | 0m37.58s || +0m03.24s | +8.62%
1m35.04s | RewriterRulesInterpGood.vo | 1m32.48s || +0m02.56s | +2.76%
0m59.49s | ExtractionHaskell/word_by_word_montgomery | 0m56.71s || +0m02.78s | +4.90%
1m45.10s | Fancy/Barrett256.vo | 1m47.00s || -0m01.90s | -1.77%
0m40.21s | p521_64.c | 0m38.97s || +0m01.24s | +3.18%
0m24.42s | SlowPrimeSynthesisExamples.vo | 0m25.67s || -0m01.25s | -4.86%
0m20.48s | secp256k1_32.c | 0m19.27s || +0m01.21s | +6.27%
1m47.10s | RewriterWf2.vo | 1m47.22s || -0m00.12s | -0.11%
0m47.85s | p521_32.c | 0m47.47s || +0m00.38s | +0.80%
0m45.66s | RewriterInterpProofs1.vo | 0m45.74s || -0m00.08s | -0.17%
0m37.18s | Fancy/Montgomery256.vo | 0m37.14s || +0m00.03s | +0.10%
0m36.26s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.14s || +0m00.11s | +0.33%
0m28.38s | ExtractionHaskell/saturated_solinas | 0m28.04s || +0m00.33s | +1.21%
0m26.80s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.83s || -0m00.02s | -0.11%
0m24.00s | RewriterWf1.vo | 0m23.96s || +0m00.03s | +0.16%
0m19.82s | ExtractionOCaml/word_by_word_montgomery | 0m20.34s || -0m00.51s | -2.55%
0m19.65s | p256_32.c | 0m19.24s || +0m00.41s | +2.13%
0m18.54s | p448_solinas_64.c | 0m19.24s || -0m00.69s | -3.63%
0m16.18s | p434_64.c | 0m16.49s || -0m00.30s | -1.87%
0m13.67s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.47s || -0m00.80s | -5.52%
0m13.22s | ExtractionOCaml/unsaturated_solinas | 0m13.72s || -0m00.50s | -3.64%
0m09.91s | p224_32.c | 0m09.89s || +0m00.01s | +0.20%
0m09.85s | ExtractionOCaml/saturated_solinas | 0m09.83s || +0m00.01s | +0.20%
0m08.66s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.86s || +0m00.79s | +10.17%
0m08.36s | p384_64.c | 0m08.46s || -0m00.10s | -1.18%
0m07.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.29s || -0m00.56s | -6.87%
0m06.66s | BoundsPipeline.vo | 0m06.73s || -0m00.07s | -1.04%
0m06.50s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.56s || -0m00.05s | -0.91%
0m06.22s | ExtractionOCaml/saturated_solinas.ml | 0m05.69s || +0m00.52s | +9.31%
0m05.50s | ExtractionHaskell/saturated_solinas.hs | 0m05.88s || -0m00.37s | -6.46%
0m03.51s | PushButtonSynthesis/Primitives.vo | 0m03.48s || +0m00.02s | +0.86%
0m03.34s | PushButtonSynthesis/SmallExamples.vo | 0m03.32s || +0m00.02s | +0.60%
0m03.31s | curve25519_32.c | 0m03.13s || +0m00.18s | +5.75%
0m03.15s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.12s || +0m00.02s | +0.96%
0m03.11s | PushButtonSynthesis/BarrettReduction.vo | 0m03.08s || +0m00.02s | +0.97%
0m02.80s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.86s || -0m00.06s | -2.09%
0m02.13s | curve25519_64.c | 0m02.02s || +0m00.10s | +5.44%
0m01.58s | p256_64.c | 0m01.66s || -0m00.07s | -4.81%
0m01.53s | p224_64.c | 0m01.60s || -0m00.07s | -4.37%
0m01.49s | secp256k1_64.c | 0m01.72s || -0m00.23s | -13.37%
0m01.34s | CLI.vo | 0m01.23s || +0m00.11s | +8.94%
0m01.16s | RewriterProofs.vo | 0m01.10s || +0m00.05s | +5.45%
0m01.16s | StandaloneOCamlMain.vo | 0m01.13s || +0m00.03s | +2.65%
0m01.10s | CompilersTestCases.vo | 0m01.09s || +0m00.01s | +0.91%
0m01.07s | StandaloneHaskellMain.vo | 0m01.04s || +0m00.03s | +2.88%
|
| |
|
|
|
|
|
| |
Also move lam_type_of_list to Rewriter (in prep for reifying rewrite
rules).
|
|
|
|
| |
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 never used the cps form, and this form is easier to read.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
|
|