aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/UnderLetsProofs.v
Commit message (Collapse)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
|
* Fix an issue with setoid_rewrite being weaker before 8.9Gravatar Jason Gross2018-12-14
|
* Add reify_and_let_binds_base_interp_relatedGravatar Jason Gross2018-12-14
|
* Switch to a more precise version of interp_related for rewritesGravatar Jason Gross2018-12-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This version is hopefully the right one. It seems to be basically exactly what we want to say, and no more and no less. The rule for let-ins, which is almost the only freedom we have here, is chosen to match exactly with the rule for App+Abs. Note that using Leibniz equality is essential in the places where it's used. The recursive relation here might actually be a bit clearer as an inductive relation, but I wanted it to simplify under reduction. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 30m04.79s | Total | 29m51.25s || +0m13.54s | +0.75% -------------------------------------------------------------------------------------------------------------------- 1m53.11s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m35.74s || +0m17.36s | +18.14% 0m19.40s | Experiments/NewPipeline/RewriterWf1.vo | 0m24.54s || -0m05.14s | -20.94% 6m13.78s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m14.86s || -0m01.08s | -0.28% 4m39.23s | Experiments/NewPipeline/Toplevel1.vo | 4m38.21s || +0m01.02s | +0.36% 1m31.62s | Experiments/NewPipeline/Toplevel2.vo | 1m32.68s || -0m01.06s | -1.14% 0m40.01s | Experiments/NewPipeline/AbstractInterpretationWf.vo | 0m38.77s || +0m01.23s | +3.19% 3m19.74s | p384_32.c | 3m19.71s || +0m00.03s | +0.01% 1m58.86s | Experiments/NewPipeline/RewriterWf2.vo | 1m58.30s || +0m00.56s | +0.47% 1m02.04s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m02.41s || -0m00.36s | -0.59% 0m40.71s | p521_32.c | 0m40.51s || +0m00.20s | +0.49% 0m39.90s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m39.85s || +0m00.04s | +0.12% 0m36.76s | Experiments/NewPipeline/Rewriter.vo | 0m36.81s || -0m00.05s | -0.13% 0m35.34s | Experiments/NewPipeline/LanguageInversion.vo | 0m35.16s || +0m00.18s | +0.51% 0m33.80s | p521_64.c | 0m33.82s || -0m00.02s | -0.05% 0m28.97s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo | 0m29.54s || -0m00.57s | -1.92% 0m27.65s | Experiments/NewPipeline/LanguageWf.vo | 0m28.11s || -0m00.46s | -1.63% 0m25.94s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m25.39s || +0m00.55s | +2.16% 0m25.63s | Experiments/NewPipeline/UnderLetsProofs.vo | 0m25.15s || +0m00.48s | +1.90% 0m22.84s | Experiments/NewPipeline/AbstractInterpretationZRangeProofs.vo | 0m23.11s || -0m00.26s | -1.16% 0m18.51s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m18.69s || -0m00.17s | -0.96% 0m17.42s | Experiments/NewPipeline/AbstractInterpretationProofs.vo | 0m17.29s || +0m00.13s | +0.75% 0m15.12s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m14.96s || +0m00.15s | +1.06% 0m14.43s | secp256k1_32.c | 0m14.22s || +0m00.20s | +1.47% 0m14.19s | p256_32.c | 0m14.46s || -0m00.27s | -1.86% 0m12.72s | Experiments/NewPipeline/CStringification.vo | 0m12.80s || -0m00.08s | -0.62% 0m10.88s | p384_64.c | 0m10.99s || -0m00.10s | -1.00% 0m09.16s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m08.87s || +0m00.29s | +3.26% 0m09.14s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.33s || -0m00.18s | -2.03% 0m07.96s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo | 0m07.96s || +0m00.00s | +0.00% 0m06.61s | p224_32.c | 0m06.52s || +0m00.09s | +1.38% 0m06.37s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.29s || +0m00.08s | +1.27% 0m05.96s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m05.60s || +0m00.36s | +6.42% 0m05.92s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.82s || +0m00.09s | +1.71% 0m04.70s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.35s || +0m00.35s | +8.04% 0m04.50s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.63s || -0m00.12s | -2.80% 0m03.82s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.62s || +0m00.19s | +5.52% 0m02.62s | Experiments/NewPipeline/MiscCompilerPassesProofs.vo | 0m02.56s || +0m00.06s | +2.34% 0m02.31s | curve25519_32.c | 0m02.40s || -0m00.08s | -3.74% 0m02.09s | secp256k1_64.c | 0m02.18s || -0m00.09s | -4.12% 0m02.05s | p224_64.c | 0m02.04s || +0m00.00s | +0.49% 0m01.96s | p256_64.c | 0m01.94s || +0m00.02s | +1.03% 0m01.56s | curve25519_64.c | 0m01.54s || +0m00.02s | +1.29% 0m01.53s | Experiments/NewPipeline/CLI.vo | 0m01.57s || -0m00.04s | -2.54% 0m01.26s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.26s || +0m00.00s | +0.00% 0m01.22s | Experiments/NewPipeline/Language.vo | 0m01.26s || -0m00.04s | -3.17% 0m01.22s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.21s || +0m00.01s | +0.82% 0m01.08s | Experiments/NewPipeline/CompilersTestCases.vo | 0m00.99s || +0m00.09s | +9.09% 0m01.06s | Experiments/NewPipeline/AbstractInterpretation.vo | 0m01.02s || +0m00.04s | +3.92% 0m00.87s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.97s || -0m00.09s | -10.30% 0m00.74s | Experiments/NewPipeline/MiscCompilerPasses.vo | 0m00.72s || +0m00.02s | +2.77% 0m00.48s | Experiments/NewPipeline/UnderLets.vo | 0m00.52s || -0m00.04s | -7.69%
* Add UnderLets.wf_interp_ProperGravatar Jason Gross2018-11-15
|
* Also inline Z_cast thingsGravatar Jason Gross2018-11-01
|
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
| | | | | | | | | | | | When we do rewriting after casts, we will need to do extra passes of DCE and subst01 to fully reduce things, so we generalize some of the interp proofs over cast behavior. For ease of rewriting, we make [ident.interp] an alias (notation) for [ident.gen_interp], rather than a [Definition]. We also factor out the rewriting wrapper inside the pipeline module into its own definition.
* Add interp_reify_and_let_binds_baseGravatar Jason Gross2018-10-25
|
* Add more interp lemmasGravatar Jason Gross2018-08-09
|
* Add wf_splice_list, wf_splice_list_no_orderGravatar Jason Gross2018-08-03
|
* More precise wf_Proper_list_implGravatar Jason Gross2018-07-31
|
* Comment out wf_splice_listGravatar Jason Gross2018-07-31
| | | | It wasn't actually ready yet
* Add wf_Proper_list, wf_splice_listGravatar Jason Gross2018-07-31
|
* Add UnderLets.wf_Proper_listGravatar Jason Gross2018-07-30
|
* Add wf_spliceGravatar Jason Gross2018-07-30
|
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
Now the only admits remaining in Toplevel1 are glue ones about freeze/to_bytes/from_bytes/fe_nonzero. What remains (beyond those admits, and the ones about word-by-word montgomery building blocks in Arithmetic), are the proofs about abstract interpretation and the rewriter. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------- 12m13.17s | Total | 11m45.42s || +0m27.75s | +3.93% -------------------------------------------------------------------------------------------------------- 3m47.20s | Experiments/NewPipeline/Toplevel1 | 3m27.51s || +0m19.68s | +9.48% 0m17.98s | Experiments/NewPipeline/UnderLetsProofs | N/A || +0m17.98s | ∞ N/A | Experiments/NewPipeline/UnderLetsWf | 0m17.94s || -0m17.94s | -100.00% 4m49.57s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 4m45.22s || +0m04.34s | +1.52% 1m16.28s | Experiments/NewPipeline/Toplevel2 | 1m13.33s || +0m02.95s | +4.02% 0m02.96s | Experiments/NewPipeline/MiscCompilerPassesProofs | N/A || +0m02.96s | ∞ N/A | Experiments/NewPipeline/MiscCompilerPassesWf | 0m02.91s || -0m02.91s | -100.00% 0m58.32s | Experiments/NewPipeline/Rewriter | 0m58.58s || -0m00.25s | -0.44% 0m28.19s | Experiments/NewPipeline/LanguageInversion | 0m28.02s || +0m00.17s | +0.60% 0m13.14s | Experiments/NewPipeline/LanguageWf | 0m13.09s || +0m00.05s | +0.38% 0m10.11s | Experiments/NewPipeline/CStringification | 0m10.12s || -0m00.00s | -0.09% 0m01.21s | Experiments/NewPipeline/CLI | 0m01.19s || +0m00.02s | +1.68% 0m01.11s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.13s || -0m00.01s | -1.76% 0m01.09s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m01.08s || +0m00.01s | +0.92% 0m01.05s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.07s || -0m00.02s | -1.86% 0m00.98s | Experiments/NewPipeline/Language | 0m00.96s || +0m00.02s | +2.08% 0m00.96s | Experiments/NewPipeline/AbstractInterpretation | 0m00.90s || +0m00.05s | +6.66% 0m00.90s | Experiments/NewPipeline/CompilersTestCases | 0m00.92s || -0m00.02s | -2.17% 0m00.66s | Experiments/NewPipeline/RewriterProofs | N/A || +0m00.66s | ∞ 0m00.64s | Experiments/NewPipeline/MiscCompilerPasses | 0m00.65s || -0m00.01s | -1.53% 0m00.42s | Experiments/NewPipeline/UnderLets | 0m00.38s || +0m00.03s | +10.52% 0m00.40s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m00.42s || -0m00.01s | -4.76%
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 11:53:50 +0000