Rp-rewriter
A verified clause-processor and customized rewriter for large terms
that uses existing ACL2 rewrite rules to prove theorems.
RP-Rewriter (rp for 'retain property') is a verified clause processor
that can be used to replace ACL2's rewriter for some theorems, and for some
cases, can provide time efficiency and convenience when building lemmas. It
uses a subset of the heuristics of the ACL2's rewriter but has some
distinctive features:
- By introducing an invariant, it can retain
properties about terms, which we call side-conditions. These properties can
help relieve hypotheses or be used in meta functions even after large terms
went through drastic changes through rewriting that may have made it difficult
to confirm those properties through regular hyp relief system.
- In the case of
alists in the theorems to be rewritten, it can create a corresponding
fast-alist in the background for later fast search and access. It does that
by triggering a special mechanism when it encounters hons-acons and
hons-get in terms.
- Meta rules can return a dont-rw structure to prevent repeated rewriting of large
returned terms, which can provide large performance (time and memory)
benefits.
- It supports inside-out as well as outside-in rewriting in the same
rewriting pass.
The rewriter supports a big set of rewrite rules existing in
ACL2's world. For every other rule-classes, it treats
them as rewrite-rules if possible. It also provides a mechanism to run meta
functions. We do not support rules with bind-free, ACL2::loop-stopper, ACL2::free-variables, case-split etc. Note that there is also no ACL2::type-alist or any
form of type reasoning.
This rewriter is mainly used by an efficient integer multiplier-verification library.
Two papers are published that mainly discuss RP-Rewriter:
Subtopics
- Rp-ruleset
- Functions to manage RP-Rewriter's ruleset
- Defthmrp
- A defthm macro that calls RP-Rewriter as a clause processor with custom arguments.
- Rp-rewriter/meta-rules
- The steps necessary to add meta rules to RP-Rewriter
- Rp-utilities
- Some useful tools for rp-rewriter
- Rp-rewriter-demo
- A demo and a case where side-conditions of RP-Rewriter are used.
- Rp-rewriter/debugging
- Tools that may be used while debugging RP-Rewriter.
- Rp-rewriter/applications
- Applications of RP-Rewriter
