Stobj-attachment-restrictions
Restrictions on attachments to supporters of stobj primitives
This topic assumes that the reader is familiar with the basics of
defattach and stobjs (which are introduced by defstobj
and defabsstobj). It concerns restrictions that disallow the use of
defattach on supporters of stobj recognizers and, for
defabsstobj, other stobj primitives that return the new stobj. Here,
a supporter of a function symbol f is a function symbol used in
the event that introduces f or, recursively, is a supporter of any of
those function symbols.
The community-book
books/system/tests/stobj-attach-unsoundness.lisp, developed by Sol
Swords, illustrates a soundness bug that existed through ACL2 Version_8.6.
That book shows several ways that nil could be proved by using defattach to falsify stobj invariants — either the recognizer or, for
abstract stobjs, the correspondence function.
Those proofs of nil no longer succeed because of the following two
restrictions now imposed by ACL2.
- No supporter of a stobj recognizer is allowed to have an attachment.
- For a defabsstobj event, there must be a correspondence function
whose supporters are not allowed to have attachments.
The second of these criteria may be met by the defabsstobj event in
either of the following two ways.
Keyword :CORR-FN-EXISTS has value t, and the value of
:CORR-FN is a function symbol whose supporters are not allowed to have
attachments.
OR
Keyword :CORR-FN-EXISTS has value nil (the default), and the
supporters of any stobj primitive (the creator and exports, in addition to the
recognizer) that returns the new stobj are not allowed to have
attachments.
Note that in the first sub-case, where keyword argument
:CORR-FN-EXISTS has value t, the definition of the :CORR-FN
symbol must be non-local. In the second sub-case, where keyword
argument :CORR-FN-EXISTS has value nil, the notion of
“supporter” of a stobj primitive is understood to include any
function symbol that is a supporter of either the :LOGIC or the
:EXEC function of that stobj primitive.
We conclude with an optional remark (for those interested in theory) that
discusses how the two sub-cases above are related. Namely, for an abstract
stobj st, there is always an implicit correspondence function definable
in terms of the primitives as follows. A concrete state c_k and abstract
state a_k correspond if there are corresponding sequences of values
c_i and a_i (i ≤ k) produced by corresponding applications of
primitives, each of which returns the new stobj, as follows.
- c_0 and a_0 are the initial concrete (foundational) and abstract
copies of st, that is, produced by applying the :EXEC and
:LOGIC creator of st, respectively.
- For all i < k, there is a stobj export fi returning st with
:EXEC function fi_E and :LOGIC function fi_L and
well-guarded parameter lists p_E and p_L for fi, such that the
following conditions hold. The lists p_E and p_L agree except in
one position,which is where st is returned. The actual parameter at that
positioni sc_i for p_E and a_i for p_L. Then c_j and
a_j are returned by the respective calls of fi_E on p_E and
fi_L on p_L.
For theoretical details pertaining to this topic, see the long comment,
“Essay on the Correctness of Abstract Stobjs”, in the ACL2 source
code.
