aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross <jgross@mit.edu>2019-04-09 22:37:02 -0400
committerJason Gross <jasongross9@gmail.com>2019-04-11 11:01:29 -0400
commit606f334bbbf480f8e08c57945a7d4001dc267af6 (patch)
tree017eb03c6350699d6edfd7d0e94fd26481806a3c
parent301af21a0d908762a83ebbd9c009bcd8d3af3100 (diff)
Update README.md with new structure of the rewriter
-rw-r--r--README.md134
1 files changed, 102 insertions, 32 deletions
diff --git a/README.md b/README.md
index 4aeb68c33..57ef3edf1 100644
--- a/README.md
+++ b/README.md
@@ -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: