diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-09 23:44:17 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-10-11 12:16:00 -0400 |
| commit | 330ee3a5e23ec66aeb9ade13f6298afcadefda51 (patch) | |
| tree | c2719d45c483f67fb4a9a882023fbb873261042d /_CoqProject | |
| parent | 9765692cdc24a1ad4fe86320df7dc288b4d1d86d (diff) | |
Add interp-correctness condition for rewriter
The NBE-rewrite rules are proven correct. The arith and fancy rewrite
rules are reduced to lemmas about Z, most of which are inconsistent (and
therefore indicate rewrite rules which are missing side-conditions).
One bad rewrite rule was found in this process, and corrected in
0842563b23f8d780f4ff1080d7620fc3f368191f
The next step after this will be using the rewrite rule correctness to
prove the rewriter correct.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 70fca8fd2..0b4816189 100644 --- a/_CoqProject +++ b/_CoqProject @@ -264,6 +264,7 @@ src/Experiments/NewPipeline/MiscCompilerPassesProofs.v src/Experiments/NewPipeline/Rewriter.v src/Experiments/NewPipeline/RewriterProofs.v src/Experiments/NewPipeline/RewriterRulesGood.v +src/Experiments/NewPipeline/RewriterRulesInterpGood.v src/Experiments/NewPipeline/RewriterWf1.v src/Experiments/NewPipeline/RewriterWf2.v src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v |