aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add reflect_list_cps_idGravatar Jason Gross2018-08-03
|
* Better rewrite_type_transport_correctGravatar Jason Gross2018-08-02
|
* Adjust GENERATEDIdentifiersWithoutTypesProofs.v, add eta_ident_cps_correctGravatar Jason Gross2018-08-02
|
* Add GENERATEDIdentifiersWithoutTypesProofs.vGravatar Jason Gross2018-08-02
|
* Also generate decidable equality for pattern.identGravatar Jason Gross2018-08-02
|
* Make wf_safe_t a bit strongerGravatar Jason Gross2018-08-02
|
* Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'edGravatar Jason Gross2018-08-02
| | | | | | | This allows us to prove things on the basis of it being the identity function, which we need to do to prove well-formedness without being able to compute the natural types of rewrite rules (which will be coming later).
* Generalize option_eq to support heterogenous relationsGravatar Jason Gross2018-08-02
|
* Add nth_error_combineGravatar Jason Gross2018-08-01
|
* 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 type.related_heteroGravatar Jason Gross2018-07-30
|
* Fix some issues in previous commitGravatar Jason Gross2018-07-30
|
* Add nat_rect_Proper_nondep_genGravatar Jason Gross2018-07-30
|
* Allow proving force ∘ thunk = id extensionallyGravatar Jason Gross2018-07-30
|
* Add UnderLets.wf_Proper_listGravatar Jason Gross2018-07-30
|
* Add wf_spliceGravatar Jason Gross2018-07-30
|
* Generalize type.eqv a bitGravatar Jason Gross2018-07-30
|
* Some WIP on Rewiter correctnessGravatar 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%
* Add wf and interp proofs for LetBindReturnGravatar Jason Gross2018-07-27
| | | | | | | | After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------- 0m17.96s | Total | 0m00.90s || +0m17.07s | +1896.66% ---------------------------------------------------------------------------------- 0m17.97s | Experiments/NewPipeline/UnderLetsWf | 0m00.90s || +0m17.07s | +1896.66%
* More proofs about wf / interpGravatar Jason Gross2018-07-27
|
* Add wf about reify/reflect listGravatar Jason Gross2018-07-27
|
* Stronger inversionGravatar Jason Gross2018-07-27
|
* Add invert_nil, invert_consGravatar Jason Gross2018-07-27
|
* Set arguments of ident.{gen_,}interpGravatar Jason Gross2018-07-27
|
* Move rewrites to the correct tacticGravatar Jason Gross2018-07-26
|
* Shuffle transport lemmas around, add more inversionGravatar Jason Gross2018-07-26
|
* Add Wf proofs about MiscCompilerPassesGravatar Jason Gross2018-07-26
|
* Move the associator pass to the rewriterGravatar Jason Gross2018-07-26
| | | | | | This makes it somewhat more ad-hoc (we don't support arbitrary numbers of multiplications), but it should hopefully be much easier to prove things about.
* Improve wf tacticsGravatar Jason Gross2018-07-26
|
* Minor improvements to wf frameworkGravatar Jason Gross2018-07-26
|
* Move some tactics to their proper placeGravatar Jason Gross2018-07-26
|
* Add Wf lemmas about SubstVarGravatar Jason Gross2018-07-26
| | | | | | | | | After | File Name | Before || Change | % Change --------------------------------------------------------------------------------- 0m11.74s | Total | 0m10.83s || +0m00.91s | +8.40% --------------------------------------------------------------------------------- 0m10.85s | Experiments/NewPipeline/LanguageWf | 0m10.83s || +0m00.01s | +0.18% 0m00.89s | Experiments/NewPipeline/UnderLetsWf | N/A || +0m00.89s | ∞
* Put == in type_scope, so that we don't need to go around opening etype_scopeGravatar Jason Gross2018-07-26
|
* Add basic wf proofsGravatar Jason Gross2018-07-26
| | | | | | | | After | File Name | Before || Change | % Change -------------------------------------------------------------------------------- 0m10.67s | Total | 0m00.00s || +0m10.67s | N/A -------------------------------------------------------------------------------- 0m10.68s | Experiments/NewPipeline/LanguageWf | N/A || +0m10.67s | ∞
* Actually improve expr.invert_oneGravatar Jason Gross2018-07-26
|
* Try again to fix expr inversionGravatar Jason Gross2018-07-26
|
* Improve expr.invert_one (hopefully)Gravatar Jason Gross2018-07-26
|
* Add more proper instancesGravatar Jason Gross2018-07-26
|
* Add type.eqv for interp equivalenceGravatar Jason Gross2018-07-26
|
* Add some inversion lemmas and tacticsGravatar Jason Gross2018-07-25
|
* Add invert_LetInGravatar Jason Gross2018-07-25
|
* Reserve ==, ===, ~=Gravatar Jason Gross2018-07-25
|
* Improve rewriter speedGravatar Jason Gross2018-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Andres and I met yesterday, and discovered that there's a source of non-linear complexity in the rewriter which is not type casts. In adding side-conditions to the rewrite rules (which are not discussed in the pattern-matching compilation paper), I represented them by allowing rewrite rules to fail. So, for example, # + x ~~> x (when # == 0) is represented as # + x ~~> if (# =? 0) then Some x else None In the case that a rewrite rule fails, we need to try all other rewrite rules that might still apply. However, doing this in the naive-CPS way leads to non-linear blowup, because wildcard rewrite rules get duplicated in the failure branches. (This is similar to the issue that `match x with "some string" => true | _ => false end%string` will generate a large number of "false" branches, and duplicate "false" across all of them, rather than having a single default case.) For example, if we had the rewrite rules # + # ~~> literal sum x + (-y) ~~> x - y (-x) + y ~~> y - x then the compiled code would look like fun x y => if x is a literal then if y is a literal then literal sum else if y is an opp then x - y else x + y else if y is an opp then x - y else if x is an opp then y - x else x + y where we actually want the code fun x y => if x is a literal then if y is a literal then return (literal sum); if y is an opp then return (x - y); if x is an opp then return (y - x); return (x + y) in the sequence+return monad. i.e., we want to not duplicate the "if y is an opp" code multiple times. I think the solution to this is to have the discrimination tree evaluator return an option, and to have the function that computes the discrimination tree not duplicate rewrite rules among different cases. Note that this leads to slightly inefficient matching sometimes: when two rules with the same structure are separated by a rule with a wildcard instead of structure, we will now try to match on the structure twice. It might be useful to be able to denote that some rewrite rules can be commuted. Also, we remove `Module pident := pattern.ident.` to work around https://github.com/coq/coq/issues/8152, now that we're no longer unfolding all of the `pattern.ident` stuff (because not unfolding it gives slightly nicer output code). After | File Name | Before || Change | % Change --------------------------------------------------------------------------------------------------------------------- 17m41.82s | Total | 29m58.10s || -12m16.27s | -40.94% --------------------------------------------------------------------------------------------------------------------- 1m08.84s | Experiments/NewPipeline/Rewriter | 5m16.96s || -4m08.11s | -78.28% 0m37.50s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 2m03.59s || -1m26.09s | -69.65% 0m17.35s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 1m41.56s || -1m24.21s | -82.91% 0m24.10s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 1m43.33s || -1m19.22s | -76.67% 0m38.44s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 1m28.64s || -0m50.20s | -56.63% 0m20.86s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 1m06.91s || -0m46.04s | -68.82% 0m11.46s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m55.64s || -0m44.17s | -79.40% 0m04.17s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m22.22s || -0m18.04s | -81.23% 1m31.73s | Experiments/NewPipeline/Toplevel2 | 1m49.50s || -0m17.76s | -16.22% 0m06.12s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m23.22s || -0m17.09s | -73.64% 0m08.69s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m22.12s || -0m13.43s | -60.71% 0m05.80s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m15.32s || -0m09.51s | -62.14% 0m04.10s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m13.20s || -0m09.09s | -68.93% 0m03.30s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m13.02s || -0m09.71s | -74.65% 5m47.58s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m52.86s || -0m05.28s | -1.49% 4m02.15s | Experiments/NewPipeline/Toplevel1 | 4m04.75s || -0m02.59s | -1.06% 0m11.40s | p384_64.c | 0m09.04s || +0m02.36s | +26.10% 0m34.20s | p521_64.c | 0m32.80s || +0m01.40s | +4.26% 0m23.40s | p384_32.c | 0m21.95s || +0m01.44s | +6.60% 0m38.90s | p521_32.c | 0m39.34s || -0m00.44s | -1.11% 0m03.40s | p256_32.c | 0m03.63s || -0m00.23s | -6.33% 0m03.24s | secp256k1_32.c | 0m03.37s || -0m00.12s | -3.85% 0m02.14s | curve25519_32.c | 0m02.00s || +0m00.14s | +7.00% 0m02.13s | p256_64.c | 0m01.72s || +0m00.40s | +23.83% 0m01.82s | p224_32.c | 0m01.82s || +0m00.00s | +0.00% 0m01.44s | p224_64.c | 0m01.48s || -0m00.04s | -2.70% 0m01.40s | secp256k1_64.c | 0m01.97s || -0m00.57s | -28.93% 0m01.35s | curve25519_64.c | 0m01.34s || +0m00.01s | +0.74% 0m01.34s | Experiments/NewPipeline/CLI | 0m01.32s || +0m00.02s | +1.51% 0m01.20s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.16s || +0m00.04s | +3.44% 0m01.20s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.25s || -0m00.05s | -4.00% 0m01.08s | Experiments/NewPipeline/CompilersTestCases | 0m01.07s || +0m00.01s | +0.93%
* Add option sequencing/returnGravatar Jason Gross2018-07-25
|
* Reserve ;;;, fix level of prefix # to not clash with infix #Gravatar Jason Gross2018-07-25
|
* Revert "Improve rewriter speed"Gravatar Jason Gross2018-07-24
| | | | | | | This reverts commit 152094f4d9d83e4a5689536e0cd68d4f006517e1. It is actually incorrect. We need to bubble up failures, not just let-bind the default case. Will fix tomorrow.
* Improve rewriter speedGravatar Jason Gross2018-07-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Andres and I met today, and discovered that there's a source of non-linear complexity in the rewriter which is not type casts. In adding side-conditions to the rewrite rules (which are not discussed in the pattern-matching compilation paper), I represented them by allowing rewrite rules to fail. So, for example, # + x ~~> x (when # == 0) is represented as # + x ~~> if (# =? 0) then Some x else None In the case that a rewrite rule fails, we need to try all other rewrite rules that might still apply. However, doing this in the naive-CPS way leads to non-linear blowup, because wildcard rewrite rules get duplicated in the failure branches. (This is similar to the issue that `match x with "some string" => true | _ => false end%string` will generate a large number of "false" branches, and duplicate "false" across all of them, rather than having a single default case.) For example, if we had the rewrite rules # + # ~~> literal sum x + (-y) ~~> x - y (-x) + y ~~> y - x then the compiled code would look like fun x y => if x is a literal then if y is a literal then literal sum else if y is an opp then x - y else x + y else if y is an opp then x - y else if x is an opp then y - x else x + y where we actually want the code fun x y => if x is a literal then if y is a literal then return (literal sum); if y is an opp then return (x - y); if x is an opp then return (y - x); return (x + y) in the sequence+return monad. i.e., we want to not duplicate the "if y is an opp" code multiple times. I think the solution to this is to have the discrimination tree evaluator return an option, and to have the function that computes the discrimination tree not duplicate rewrite rules among different cases. Note that this leads to slightly inefficient matching sometimes: when two rules with the same structure are separated by a rule with a wildcard instead of structure, we will now try to match on the structure twice. It might be useful to be able to denote that some rewrite rules can be commuted. After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------------------------------------------- 40m35.83s | Total | 30m00.99s || +10m34.84s | +35.24% ---------------------------------------------------------------------------------------------------------------------- 21m46.37s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m01.39s || +15m44.97s | +261.48% 6m37.40s | p384_32.c | 0m22.47s || +6m14.92s | +1668.58% 0m18.00s | Experiments/NewPipeline/Rewriter | 5m16.50s || -4m58.50s | -94.31% 0m30.49s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 1m54.20s || -1m23.71s | -73.30% 0m27.41s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 1m39.40s || -1m11.99s | -72.42% 0m47.78s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 1m54.50s || -1m06.71s | -58.27% 0m40.28s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 1m23.77s || -0m43.48s | -51.91% 0m15.21s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m55.86s || -0m40.64s | -72.77% 0m23.39s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 1m00.22s || -0m36.82s | -61.15% 0m21.85s | p256_32.c | 0m04.01s || +0m17.84s | +444.88% 0m20.97s | secp256k1_32.c | 0m03.26s || +0m17.71s | +543.25% 0m04.60s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m20.33s || -0m15.72s | -77.37% 0m09.48s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m23.28s || -0m13.80s | -59.27% 1m33.63s | Experiments/NewPipeline/Toplevel2 | 1m45.56s || -0m11.93s | -11.30% 0m08.29s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m18.64s || -0m10.35s | -55.52% 0m05.93s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m16.74s || -0m10.80s | -64.57% 0m32.41s | p521_64.c | 0m41.42s || -0m09.01s | -21.75% 0m04.93s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m14.92s || -0m09.99s | -66.95% 0m04.40s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m12.57s || -0m08.16s | -64.99% 0m08.52s | p224_32.c | 0m01.95s || +0m06.56s | +336.92% 0m13.99s | p384_64.c | 0m10.64s || +0m03.34s | +31.48% 4m07.13s | Experiments/NewPipeline/Toplevel1 | 4m05.83s || +0m01.29s | +0.52% 0m38.96s | p521_32.c | 0m40.09s || -0m01.13s | -2.81% 0m02.28s | p224_64.c | 0m01.66s || +0m00.61s | +37.34% 0m02.27s | curve25519_32.c | 0m01.98s || +0m00.29s | +14.64% 0m01.78s | p256_64.c | 0m01.65s || +0m00.13s | +7.87% 0m01.70s | secp256k1_64.c | 0m01.96s || -0m00.26s | -13.26% 0m01.65s | curve25519_64.c | 0m01.51s || +0m00.13s | +9.27% 0m01.37s | Experiments/NewPipeline/CLI | 0m01.26s || +0m00.11s | +8.73% 0m01.15s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.21s || -0m00.06s | -4.95% 0m01.14s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.16s || -0m00.02s | -1.72% 0m01.07s | Experiments/NewPipeline/CompilersTestCases | 0m01.05s || +0m00.02s | +1.90%
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:28:17 +0000