• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
      • Apt
      • Acre
      • Milawa
      • Smtlink
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Abnf
      • Proof-checker-array
      • Soft
      • Farray
      • Prime-field-constraint-systems
      • Rp-rewriter
        • Rp-ruleset
        • Rp-rewriter/meta-rules
        • Rp-utilities
        • Defthmrp
        • Rp-rewriter-demo
        • Rp-rewriter/debugging
        • Rp-rewriter/applications
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Bigmem
      • Regex
      • ACL2-programming-language
      • Java
      • Jfkr
      • X86isa
      • Equational
      • C
      • Cryptography
      • Where-do-i-place-my-book
      • Execloader
      • Json
      • Solidity
      • Paco
      • Concurrent-programs
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Projects
  • Clause-processor-tools

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 adds two distinctive features: 1. By introducing an invariant, it can retain properties about terms, which we call side-conditions. 2. In the case of alists in the theorems to be rewritten, it can create a corresponding fast-alist in the background. It also has some other improvements pertaining to meta-rules.

It supports a big set of rewrite rules existing in ACL2's world that may have syntaxp. For every other rule-classes, it treats them as rewrire-rules. It also provides a mechanism to run meta functions. The rest of the rule classes are not supported and are discarded by the rewriter. We also do not support rules with bind-free, ACL2::loop-stopper, ACL2::free-variables, force, case-split etc. Note that there is also no ACL2::type-alist or any form of type reasoning.

The rewriter enables users to attach certain properties (i.e., side-conditions) to terms as rewriting takes place. These properties can be used to relieve hypotheses efficiently without backchaining.

If a rewrite rule has hons-acons on its right hand side, rp-rewriter has a built-in mechanism that treats that as a trigger function to create a fast-alist in the background. When another term seems to be trying to read a value from that alist with a known instance of a function such as assoc-equal, the built in meta functions reads the value from the corresponding fast-alist instead of tracing it in the logical term. This may give great timing benefits when dealing with terms with large alists.

Subtopics

Rp-ruleset
Functions to manage RP-Rewriter's ruleset
Rp-rewriter/meta-rules
The steps necessary to add meta rules to RP-Rewriter
Rp-utilities
Some useful tools for rp-rewriter
Defthmrp
A defthm macro that calls RP-Rewriter as a clause processor with some capabilities.
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