diff options
Diffstat (limited to 'src/README.md')
| -rw-r--r-- | src/README.md | 197 |
1 files changed, 197 insertions, 0 deletions
diff --git a/src/README.md b/src/README.md new file mode 100644 index 000000000..400a2e005 --- /dev/null +++ b/src/README.md @@ -0,0 +1,197 @@ +The ordering of files (eliding `*Proofs.v` files) is: + +``` + Language.v ←──────────────────────────────────────────────────┬───────────────────────────────┐ + ↗ ↖ │ │ + ↗ ↖ │ │ + UnderLets.v GENERATEDIdentifiersWithoutTypes.v MiscCompilerPasses.v PushButtonSynthesis/ReificationCache.v + ↑ ↖ ↗ ↑ ↑ +AbstractInterpretation.v Rewriter.v │ │ + ↑ ↑ ┌────────────────────────────────────────────────────┘ │ +CStringification.v │ │ Arithmetic.v │ + ↑ ┌───────────────────┴─┘ ↑ │ +BoundsPipeline.v COperationSpecifications.v │ + ↑ ↑ │ + │ ┌────────────────────────────────────────┴────────────────────────────────────────────────────────────────┘ +PushButtonSynthesis.v ←── Toplevel2.v ←───────────┐ + ↑ │ +CLI.v SlowPrimeSynthesisExamples.v +↑ ↑ +│ └────────────────────────────┐ +StandaloneHaskellMain.v StandaloneOCamlMain.v + ↑ ↑ +ExtractionHaskell.v ExtractionOCaml.v +``` + +The files contain: + +- Arithmetic.v: All of the high-level field arithmetic stuff + +- Language.v: + + PHOAS + + reification + + denotation/intepretation + + utilities for inverting PHOAS exprs + + default/dummy values of PHOAS exprs + + default instantiation of generic PHOAS types + + gallina reification of ground terms + + Flat/indexed syntax trees, and conversions to and from PHOAS + Defines the passes: + + ToFlat + + FromFlat + + GeneralizeVar + +- UnderLets.v: the UnderLets monad, a pass that does substitution of var-like + things, a pass that inserts let-binders in the next-to-last line of code, + substituting away var-like things (this is used to ensure that when we output + C code, aliasing the input and the output arrays doesn't cause issues). + Defines the passes: + + SubstVarFstSndPairOppCast + +- AbstractInterpretation.v: type-code-based ZRange definitions, abstract + interpretation of identifiers (which does let-lifting, for historical reasons, + and the dependency on UnderLets should probably be removed), defines the + passes: + + PartialEvaluateWithBounds + + PartialEvaluateWithListInfoFromBounds + + CheckPartialEvaluateWithBounds + +- GENERATEDIdentifiersWithoutTypes.v: generated by a python script which is + included in a comment in the file, this is an untyped version of identifiers + for the rewriter + +- Rewriter.v: rewrite rules, rewriting. Defines the passes: + + Rewrite + + RewriteToFancy + + PartialEvaluate (which is just a synonym for Rewrite) + +- MiscCompilerPasses.v: Defines the passes: + + EliminateDead (dead code elimination) + + Subst01 (substitute let-binders used 0 or 1 times) + +- CStringification.v: conversion to C code as strings. (Depends on + AbstractInterpretation.v for ZRange utilities.) Defines the passes: + + ToString.ToFunctionLines + + ToString.ToFunctionString + + ToString.LinesToString + +- CompilersTestCases.v: Various test cases to ensure everything is working + +- BoundsPipeline.v: Assemble the various compiler passes together into + a composed pipeline. It is the final interface for the compiler. + Also contains some tactics for applying the BoundsPipeline + correctness lemma. + +- COperationSpecifications.v: The specifications for the various + operations to be synthesized. + +- PushButtonSynthesis/ReificationCache.v: Defines the cache that holds + reified versions of operations, as well as the tactics that reify + and apply things from the cache. + +- PushButtonSynthesis.v: Reifies the various operations from + Arithmetic.v, definies the compositions of the BoundsPipeline with + these operations, proves that their interpretations satisfies the + specs from COperationSpecifications.v, assembles the reified + post-bounds operations into synthesis targets. This is the file + that CLI.v depends on. + +- Toplevel2.v: Some not-quite-finished-but-kind-of-slow pipeline stuff + + all the stuff that uses compilers + arithmetic, together with more + examples. Also has semi-broken fancy-machine stuff. This should + probably be merged into Toplevel1.v when working on the pipeline. + +- SlowPrimeSynthesisExamples.v: Additional uses of the pipeline for + primes that are kind-of slow, which I don't want extraction blocking + on. + +- CLI.v: Setting up all of the language-independent parts of extraction; relies + on having a list of strings-or-error-messages for each pipeline, and on the + arguments to that pipeline, and builds a parser for command line arguments for + that. + +- StandaloneHaskellMain.v, StandaloneOCamlMain.v, ExtractionHaskell.v, + ExtractionOCaml.v: Extraction of pipeline to various languages + + +Proofs files: +For Language.v, there is a semi-arbitrary split between two files +`LanguageInversion` and `LanguageWf`. +- LanguageInversion.v: + + classifies equality of type codes and exprs + + type codes have decidable equality + + correctness of the various type-transport definitions + + correctness lemmas for the various `expr.invert_*` definitions + + correctness lemmas for the various `reify_*` definitions in Language.v + + inversion_type, which inverts equality of type codes + + type_beq_to_eq, which converts boolean equality of types to + Leibniz equality + + rewrite_type_transport_correct, which rewrites with the + correctness lemmas of the various type-transport definitions + + `type.invert_one e` which does case analysis on any inductive type + indexed over type codes, in a way that preserves information + about the type of `e`, and generally works even when the goal is + dependently typed over `e` and/or its type + + ident.invert, which does case-anaylsis on idents whose type has + structure (i.e., is not a var) + + ident.invert_match, which does case-analysis on idents appearing as + the discriminee of a `match` in the goal or in any hypothesis + + expr.invert, which does case-anaylsis on exprs whose type has + structure (i.e., is not a var) + + expr.invert_match, which does case-analysis on exprs appearing as + the discriminee of a `match` in the goal or in any hypothesis + + expr.invert_subst, which does case-analysis on exprs which show up + in hypotheses of the form `expr.invert_* _ = Some _` + + expr.inversion_expr, which inverts equalities of exprs + +- LanguageWf.v: Depends on LanguageInversion.v + Defines: + + expr.wf, expr.Wf, expr.wf3, expr.Wf3 + + GeneralizeVar.Flat.wf + + expr.inversion_wf (and variants), which invert `wf` hypotheses + + expr.wf_t (and variants wf_unsafe_t and wf_safe_t) which make + progress on `wf` goals; `wf_safe_t` should never turn a provable + goal into an unprovable one, while `wf_unsafe_t` might. + + expr.interp_t (and variants), which should make progress on + equivalence-of-interp hypotheses and goals, but is not used much + (mainly because I forgot I had defined it) + + prove_Wf, which proves wf goals on concrete syntax trees in a more + optimized way than `repeat constructor` + Proves: + + funext → (type.eqv ↔ Logic.eq) (`eqv_iff_eq_of_funext`) + + type.related and type.eqv are PERs + + Proper instances for type.app_curried, type.and_for_each_lhs_of_arrow + + type.is_not_higher_order → Reflexive (type.and_for_each_lhs_of_arrow type.eqv) + + iff between type.related{,_hetero} and related of type.app_curried + + various properties of type.and{,b_bool}for_each_lhs_of_arrow + + various properties of type.eqv and ident.{gen_,}interp + + various properties of ident.cast + + various properties of expr.wf (particularly of things defined in Language.v) + + interp and wf proofs for the passes to/from Flat + +- UnderLetsProofs.v: wf and interp lemmas for the various passes defined in UnderLets.v +- MiscCompilerPassesProofs.v: wf and interp lemmas for the various passes defined in MiscCompilerPasses.v +- GENERATEDIdentifiersWithoutTypesProofs.v: various lemmas about the definitions in GENERATEDIdentifiersWithoutTypes.v +- AbstractInterpretationZRangeProofs.v: Proves correctness lemmas of the per-operation zrange-bounds-analysis functions +- AbstractInterpretationWf.v: wf lemmas for the AbstractInterpretation pass +- AbstractInterpretationProofs.v: interp lemmas for the + AbstractInterpretation pass, and also correctness lemmas that + combine Wf and interp +- RewriterWf1.v: a semi-arbitrary collection of proofs and definitions + that are mostly shared between the wf proofs and the interp proofs. + Importantly, this file defines everything needed to state and prove + that specific rewrite rules are correct. +- RewriterRulesGood.v: Proves that all specific rewriter rules are + good enough for wf proofs (as specified in RewriterWf1.v) +- RewriterRulesInterpGood.v: Proves that all specific rewriter rules + are good enough for interp proofs (as specified in RewriterWf1.v) +- RewriterWf2.v: Proves wf of the generic rewriter pass, taking in + specific-rewriter-rule-correctness as a hypothesis +- RewriterInterpProofs1.v: Proves interp-correctness of the generic + rewriter pass, taking in specific-rewriter-rule-correctness as a + hypothesis +- RewriterProofs.v: assembles the proofs from RewriterRulesGood.v, + RewriterRulesInterpGood.v, RewriterWf2.v, and + RewriterInterpProofs1.v into correctness lemmas for the overall + rewriter pass, specialized and pre-evaluated for specific rewrite + rules |