diff options
| -rw-r--r-- | README.md | 134 |
1 files changed, 102 insertions, 32 deletions
@@ -57,7 +57,7 @@ Here are some examples of ways to invoke the binaries (from the directories that # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1) ./word_by_word_montgomery 'p256' '2^256' '2^224,1;2^192,-1;2^96,-1;1,1' '32' > p256_32.c ./word_by_word_montgomery 'p256' '2^256' '2^224,1;2^192,-1;2^96,-1;1,1' '64' > p256_64.c - + Reading About The Code ---------------------- @@ -82,11 +82,11 @@ The ordering of files (eliding `*Proofs.v` files) is: ``` Language.v ←──────────────────────────────────────────────────┬───────────────────────────────┐ - ↗ ↖ │ │ - ↗ ↖ │ │ - UnderLets.v GENERATEDIdentifiersWithoutTypes.v MiscCompilerPasses.v PushButtonSynthesis/ReificationCache.v - ↑ ↖ ↗ ↑ ↑ -AbstractInterpretation.v Rewriter.v │ │ + ↑ │ │ + │ │ │ + UnderLets.v MiscCompilerPasses.v PushButtonSynthesis/ReificationCache.v + ↑ ↖ ↑ ↑ +AbstractInterpretation.v "Rewriter" │ │ ↑ ↑ ┌────────────────────────────────────────────────────┘ │ CStringification.v │ │ Arithmetic.v │ ↑ ┌───────────────────┴─┘ ↑ │ @@ -136,14 +136,15 @@ The files contain: + 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 +- "Rewriter": rewrite rules, rewriting. See below for actual stucture + of files. Defines the passes: + + RewriteNBE + + RewriteArith + + RewriteArithWithCasts + + RewriteStripLiteralCasts + RewriteToFancy - + PartialEvaluate (which is just a synonym for Rewrite) + + RewriteToFancyWithCasts + + PartialEvaluate (which is just a synonym for RewriteNBE) - MiscCompilerPasses.v: Defines the passes: + EliminateDead (dead code elimination) @@ -194,6 +195,94 @@ The files contain: ExtractionOCaml.v: Extraction of pipeline to various languages +The files defined for "Rewriter" are split up into the following +dependency graph: +``` +GENERATEDIdentifiersWithoutTypes.v ←── GENERATEDIdentifiersWithoutTypesProofs.v + ↑ ↑ +Rewriter.v ←───────────────────────── RewriterWf1.v + ↗ ↖ + RewriterWf2.v RewriterInterpProofs1.v + ↖ ↗ +RewriterRules.v RewriterProofsTactics.v + ↑ ↑ +RewriterRulesProofs.v │ + ↑ │ + ├────────┬─────────────┬───────────────┴────────┬─────────────────────────────┐ + │ Rewriter/NBE.v Rewriter/Arith.v Rewriter/ArithWithCasts.v Rewriter/StripLiteralCasts.v + │ ↑ ↑ ↑ ↑ + │ └─────────────┴────────────────────────┴─────────────────────────────┴─────────────┐ + │ │ + └────────┬──────────────────────────┐ │ + Rewriter/ToFancy.v Rewriter/ToFancyWithCasts.v │ + ↑ ↑ │ + └───────┬──────────────────┴───────────────────────────────────────────────────────┘ + │ + RewriterProofs.v +``` + +- RewriterRules.v: Defines the list of types of the rewrite rules that + will be reified. Largely independent of the expression language. + +- RewriterRulesProofs.v: Proves all of the Gallina versions of the + rewrite rules correct. + +- 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 + +- GENERATEDIdentifiersWithoutTypesProofs.v: proofs about identifiers + in GENERATEDIdentifiersWithoutTypes.v + +- Rewriter.v: Defines the rewriter machinery, reification of rewrite + rules, and culminates in the tactic + `RewriteRules.Tactic.Build_RewriterT` and the tactic notation + `make_Rewriter` which define a package of type + `RewriteRules.GoalType.RewriterT`. The `Build_*` tactic returns a + `constr`, while the `make_*` tactic notation refines that `constr` + in the goal. Both tactics take two arguments: first a boolean + `include_interp` which specifies whether (`true`) or not (`false`) + to prefix the list of rewrite rules with the reduction-to-literal + rewrite rules; and second a list of `bool * Prop` which is the list + of rewrite rule types to reify, each paired with a boolean saying + whether or not to try rewriting again in the output of the + replacement for that rule. + +- RewriterWf1.v: Defines the notion of interp-goodness and wf-goodness + for rewrite rules, defines tactics to prove these notions, and + contains 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. Additionally defines a + package `RewriteRules.GoalType.VerifiedRewriter` which describes the + type of the overall specialized rewriter together with its `Wf` and + `Interp` proofs. (This package should perhaps move to another file?) + +- RewriterWf2.v: Proves wf-preservation of the generic rewriter, + taking in wf-goodness of rewrite rules as a hypothesis. + +- RewriterInterpProofs1.v: Proves interp-correctness of the generic + rewriter, taking in interp-goodness of rewrite rules as a + hypothesis. + +- RewriterProofsTactics.v: Defines the tactic + `RewriteRules.Tactic.make_rewriter` (and a similar tactic notation) + which build the entire `VerifiedRewriter`. They take in the + `include_interp` as in Rewriter.v tactics, as well as an hlist of + proofs of rewrite rules indexed over a `list (bool * Prop)` of + rewrite rule types. This is the primary interface for defining a + rewriter from a list of rewrite rules. + +- Rewriter/{NBE, Arith, ArithWithCasts, StripLiteralCasts, ToFancy, + ToFancyWithCasts}.v: Use the tactic from RewriterProofsTactics.v + together with the proven list of rewrite rules from + RewriterRulesProofs.v to reify and reduce the corresponding pass and + generate a rewriter. + +- RewriterProofs.v: `Definition`less file that `Export`s the rewriters + defined in `Rewriter/*.v` + + Proofs files: For Language.v, there is a semi-arbitrary split between two files `LanguageInversion` and `LanguageWf`. @@ -251,30 +340,11 @@ For Language.v, there is a semi-arbitrary split between two files - 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 There are also proofs about elliptic curves, for example: |