Preservation-thms
Automation for proving that stobj-modifying functions preserve
certain properties
A major pain when programming in logic mode with stobjs is maintaining
all the invariants necessary to prove guards. We provide utilities to define a
set of theorem templates and to prove those theorems of a function.
Usage:
(def-stobj-preservation-thms fnname
:stobjname my-stobj
:templates my-stobj-pres-templates
:omit (my-thm-template-x my-thm-template-y)
:history my-stobj-pres-history)
tries to prove a set of preservation theorems as stored in the table
my-st-pres-templates.
To add a new preservation theorem to the existing set, use, for example,
(add-stobj-preservation-thm
nth-of-field-preserved
:vars (id)
:body `(implies (< id (my-index ,orig-stobj))
(equal (nth id (nth ',*fieldi* ,new-stobj))
(nth id (nth ',*fieldi* ,orig-stobj))))
:hints `(,@expand/induct-hints
(and stable-under-simplificationp
'(:in-theory (enable my-index))))
:enable '(my-rule my-ruleset)
:disable '(bad-rule other-rules)
:rule-classes `(:rewrite (:linear :trigger-terms (,new-stobj)))
:templates my-stobj-pres-templates
:history my-stobj-pres-history)
Certain placeholder variables can be used in the body, hints, enable, disable,
and rule-classes fields:
- orig-stobj is the variable denoting the original stobj before modification
- new-stobj is the term giving the modified stobj after the function
call: for example, (mv-nth 1 (modify-my-stobj my-stobj))
- call is the call of the function without the possible
mv-nth, for example, (modify-my-stobj my-stobj)
- expand/induct-hints are a generated set of hints specific to each
function for which the preservation theorem is to be proved, which expand and
(if recursive) induct on that function
- fn is the function being worked on
- fn$ is the deref-macro-name of that function,
e.g. binary-logior if the fn were logior
- formals is the formals of the function, possibly with some
modification to the names, but the same ones used in call and
new-stobj.
The
:vars argument should be a list containing all of the variable
names used in the theorem body; if the formals of the function contain any of
these variables, we will use a modified list of formals that avoids them.
One additional keyword argument, :deps, is allowed; if provided,
this should be a list of stobj-preservation-thm template names such as
nth-node-preserved above. This signifies that this theorem should
only be proved of functions for which the dependencies were also proved.
Two additional macros, retroactive-add-stobj-preservation-thm and
retroactive-add-stobj-preservation-thm-local are similar to
add-stobj-preservation-thm but additionally prove the new theorem for all
existing functions for which other stobj-preservation-thms have already been
proved, modulo the dependencies of the new theorem. The -local version
makes the addition of the new theorem local to the current book or encapsulate,
so that nonlocal calls of def-stobj-preservation-thms won't include
it.
All of these macros take keyword arguments templates and
history, which should be symbols. These symbols are the ACL2 table
names in which the templates and usage history are stored. (The history is
used mainly for checking dependencies). In order to simplify the usage of this
utility, we supply a macro-generating macro:
(def-stobj-preservation-macros :name hello
:default-stobjname my-stobj
:templates my-templates-table
:history my-history-table)
which defines simple wrapper macros
(def-hello-preservation-thms ...)
(add-hello-preservation-thm ...)
(retroactive-add-hello-preservation-thm ...)
(retroactive-add-hello-preservation-thm-local ...)
that behave the same as the ones above, execpt that they don't take the
:templates or
:history arguments and they use
my-stobj by default for
:stobjname.
Subtopics
- Retroactive-add-stobj-preservation-thm-local
- Localy add a theorem template to the def-stobj-preservation-thms database
and (nonlocally) prove it about existing functions
- Retroactive-add-stobj-preservation-thm
- Add a theorem template to the def-stobj-preservation-thms database
and prove it about existing functions
- Def-stobj-preservation-thms
- Prove the existing set of aigstobj preservation theorems for a given function
- Retroactive-add-sat-lits-preservation-thm-local
- Generated by def-stobj-preservation-macros.
- Retroactive-add-sat-lits-preservation-thm
- Generated by def-stobj-preservation-macros.
- Def-sat-lits-preservation-thms
- Generated by def-stobj-preservation-macros.
- Add-sat-lits-preservation-thm
- Generated by def-stobj-preservation-macros.
- ACL2::retroactive-add-aignet-preservation-thm-local
- Generated by def-stobj-preservation-macros.
- ACL2::retroactive-add-aignet-preservation-thm
- Generated by def-stobj-preservation-macros.
- Def-aignet-preservation-thms
- Generated by def-stobj-preservation-macros.
- Add-stobj-preservation-thm
- Add a theorem template to the def-stobj-preservation-thms database
- Add-aignet-preservation-thm
- Generated by def-stobj-preservation-macros.
