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

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 thederef-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`.

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, `-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

- 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.