| 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 | ∞
|