Defabsstobj
Define a new abstract single-threaded object
We assume familiarity with single-threaded objects; see stobj and see defstobj. The event defabsstobj defines a
so-called ``abstract stobj'', a notion we introduce briefly now and then
explain in more depth below.
Recall that a defstobj event produces logical definitions for
several functions: a recognizer, which characterizes the stobj in terms
of lists; a creator, which produces an initial suitable list structure; and
field accessors and updaters, defined in terms of nth and update-nth. Defabsstobj provides a way to define alternate definitions
for ``stobj primitives'' for a corresponding single-threaded object. These
stobj primitives include a recognizer, a creator, and other ``exported''
functions. In essence, defabsstobj establishes interface functions, or
``exports'', on a new stobj that is a copy of an existing stobj, its
``foundation'', which is either concrete (introduced by defstobj) or abstract (introduced by defabsstobj).
We begin below with an introduction to abstract stobjs. We then
explain the defabsstobj event by way of an example. We conclude by
giving summary documentation for the defabsstobj event.
For another introduction to abstract stobjs, see the paper ``Abstract
Stobjs and Their Application to ISA Modeling'' by Shilpi Goel, Warren A. Hunt,
Jr., and Matt Kaufmann, in the proceedings of ACL2 Workshop 2013.
INTRODUCTION
We start with a brief review of stobjs and some potential problems
with them, followed by an introduction to abstract stobjs and how they can
avoid these problems. Prior experience with stobjs will probably help the
reader to absorb the ideas below.
Recall that single-threaded objects, or stobjs, provide a way for
ACL2 users to stay within the ACL2 logic — where every data object is an
atom or a cons of data objects — while obtaining the benefits of
fast evaluation through destructive updates. Consider for example this very
simple event.
(defstobj st fld)
This event introduces a recognizer, stp, and a creator,
create-st, for a data structure consisting of a single field accessed and
updated by functions fld and update-fld, respectively. Each of
these four primitive functions has both a logical definition, which is used
when the prover reasons about the function, and an executable definition,
which is used in raw Lisp. In the logic, stp recognizes objects that
have the requisite fields. In raw Lisp, there is a ``live stobj'', which is
typically an array object whose fields correspond to those specified by the
defstobj event. (If there is a single stobj field that is an array or
hash-table field, then that field is the entire stobj in raw Lisp; but we
ignore that case below.)
Here are the logical definition and the executable definition,
respectively, that are introduced for the field accessor, fld, introduced
above. Notice that since a stobj is represented in raw Lisp using an array,
the raw Lisp accessor uses a raw Lisp array accessor, svref. (You can
see all the logical and executable definitions by evaluating the form
(trace$ defstobj-axiomatic-defs defstobj-raw-defs) before evaluating the
defstobj form.)
; logical definition
(defun fld (st)
(declare (xargs :guard (stp st)
:verify-guards t))
(nth 0 st))
; executable (raw Lisp) definition
(defun fld (st)
(svref st 0))
Sophisticated programming with stobjs can provide efficient implementations
of algorithms, but may require the preservation of a complex invariant. One
can, of course, define a function to implement such an invariant after
introducing the stobj, as follows.
; Introduce a stobj.
(defstobj st fld1 ... fldk)
; Define an invariant on that stobj.
(defun good-stp (st)
(declare (xargs :stobjs st))
...)
; Define some basic functions that update the stobj and preserve the
; invariant.
(defun update-st (... st ...)
(declare (xargs :stobjs st
:guard (and (good-stp st) ...)))
...)
...
; Prove that the invariant is indeed preserved by those basic functions.
(defthm good-stp-update-st
(implies (and (good-stp st)
...)
(good-stp (update-st ... st ...))))
...
; Implement algorithms built on the basic functions.
(defun foo (... st ...)
(declare (xargs :stobjs st
:guard (and (good-stp st) ...)))
... (update-st ... st ...) ...)
; Prove invariance theorems about these algorithms.
(defthm good-stp-foo
(implies (and (good-stp st)
...)
(good-stp (foo ... st ...))))
...
; Prove other properties of these algorithms.
(defthm foo-is-correct
(implies (and (good-stp st)
...)
(some-property (foo ... st ...))))
...
But there are at least two potential difficulties in using stobjs as
described above.
- When foo is executed on concrete data in the ACL2 loop,
the guard check may be expensive because (good-stp st) is expensive.
- Reasoning about foo (using rules like foo-is-correct above)
involves proving hypotheses of invariance theorems, which may be complicated
for the user to manage or slow for the theorem prover.
The defabsstobj event offers an opportunity to address these issues.
It introduces a new stobj, which we call an ``abstract stobj'', which is
associated with a corresponding ``foundational stobj'' introduced by an
earlier defstobj or defabsstobj event. The defabsstobj
event specifies a logical (:LOGIC) and an executable (:EXEC)
definition for each primitive operation, or ``stobj primitive'', involving
that stobj. As is the case for defstobj, the logical definition is
what ACL2 reasons about, and is appropriate to apply to an ACL2 object
satisfying the logical definition of the recognizer function for the stobj.
The executable definition is applied in raw Lisp to a live stobj (as discussed
above).
Remark. It is common to use ``a'' and ``c'' in a suffix to suggest
``abstract'' and ``concrete'', respectively. The foundational stobj was, at
one time, called the ``corresponding concrete stobj''. That old terminology
may still be appropriate in the common case that the foundational stobj is a
concrete stobj (rather than another abstract stobj). So below, a name like
st$c0 suggests a foundational (``concrete'') stobj for an abstract stobj
named st, whose abstract stobj recognizer is st$ap, and so on. End
of Remark.
We can picture a sequence of updates to an abstract stobj and its
foundational stobj. Initially in this picture, st$a0 and st$c0 are
an abstract stobj and its foundation (respectively). Then an update, u1,
is applied with :LOGIC and :EXEC functions u$a1 and u$c1,
respectively. The resulting abstract and foundational stobj, st$a1 and
st$c1, correspond as before. Then a second update, u2, is applied
with :LOGIC and :EXEC functions u$a2 and u$c2,
respectively — again preserving the correspondence. And so on.
Abstract u$a1 u$a2 u$a3
(:logic) st$a0 --> st$a1 --> st$a2 --> ...
^ ^ ^ ^
Correspondence | | | ... |
v v v v
u$c1 u$c2 u$c3
Foundation st$c0 --> st$c1 --> st$c2 --> ...
(:exec)
We conclude this introduction with some remarks about implementation.
Consider an abstract stobj st with corresponding foundation st$c.
The live stobjs for st and st$c have the same structure, but are
distinct arrays. Indeed, the raw Lisp creator function for st$c is
called to create a new initial live stobj for st. As we will see below,
reads and writes in raw Lisp to the live stobj for st are ultimately
performed using the primitive accessors and updaters defined for st$c.
One might think of the live stobjs for st and st$c as being
congruent stobjs (see defstobj), except that the stobjs themselves are
not truly congruent: in particular, the stobj primitives introduced for
st may be applied to st, but field updaters of st$c may not.
As one might expect, the :EXEC function for an exported function is
applied to the live stobj for st in raw Lisp.
EXAMPLE
We present examples, with detailed comments intended to explain abstract
stobjs, in two community books: books/demos/defabsstobj-example-1.lisp
and books/demos/defabsstobj-example-2.lisp. In this section we outline
the first of these. We suggest that after you finish this documentation topic, you read through those two books. There are other books
books/dmeos/defabsstobj-example-*.lisp that may be helpful to read; in
particular, books/demos/defabsstobj-example-5.lisp illustrates building
an abstract stobj on top of another abstract stobj (as its so-called
``foundation'', as described below).
Here is the first of two closely related defabsstobj events
from the book defabsstobj-example-1.lisp, but in expanded form. We will
show the abbreviated form later, which omits most of the data in the form that
is immediately below. Thus most of the information shown here is default
information. We believe that the comments below explain most or all of what
you need to know in order to start using defabsstobj, and that you will
learn the remainder when you see error messages. For example, we do not say
in the comments below that every :LOGIC and :EXEC function must be
guard-verified, but that is indeed a requirement.
(defabsstobj st ; The new abstract stobj is named st.
; The foundational stobj for st is st$c:
:foundation st$c
; The recognizer for the new abstract stobj is stp, which is defined to be
; st$ap in the logic, and is executed on the live stobj in raw Lisp using
; st$cp.
:recognizer (stp :logic st$ap :exec st$cp)
; The initial stobj is defined as create-st (a function of no arguments),
; which is defined logically as create-st$a, though create-st$c is invoked to
; create the initial live stobj for st. The :correspondence and :preserved
; keywords refer to proof obligations, discussed below.
:creator (create-st :logic create-st$a :exec create-st$c
:correspondence create-st{correspondence}
:preserved create-st{preserved})
; Proof obligations are generated that involve a correspondence between the
; new abstract stobj and corresponding foundational stobj. The function
; st$corr, which need not be executable (see :DOC defun-nx), takes two
; arguments, a foundational stobj and an abstract stobj. This function symbol
; is used in the statements of the proof obligations.
:corr-fn st$corr
; In this example we have four exports. In each case a new function is
; introduced that has the same signature as its :EXEC function, except that
; st$c is replaced by st. The :LOGIC and :EXEC functions are as specified,
; and the other keywords refer to proof obligations that we discuss below.
:exports ((lookup :logic lookup$a
:exec mem$ci
:correspondence lookup{correspondence}
:guard-thm lookup{guard-thm})
(update :logic update$a
:exec update-mem$ci
:correspondence update{correspondence}
:preserved update{preserved}
:guard-thm update{guard-thm})
(misc :logic misc$a
:exec misc$c
:correspondence misc{correspondence})
(update-misc :logic update-misc$a
:exec update-misc$c
:correspondence update-misc{correspondence}
:preserved update-misc{preserved})))
Note that all stobj primitives (recognizer, creator, and exported
functions) are defined in the ACL2 loop in terms of their :LOGIC
functions and in raw Lisp in terms of their :EXEC functions. In the ACL2
loop, a defun form defines a function, while in raw Lisp, a defmacro form defines a macro (for efficiency). We first illustrate how that
works for the recognizer. (You can see all the logical and executable
definitions by evaluating the form (trace$ defabsstobj-axiomatic-defs
defabsstobj-raw-defs) before evaluating the defstobj form.)
; In the ACL2 loop:
(defun stp (st)
(declare (xargs :guard 't))
(st$ap st))
; In raw Lisp:
(defmacro stp (&rest args) (cons 'st$cp args))
The definitions are made similarly for exported functions. Guards
are derived from their :LOGIC functions as follows. Consider the
exported function update in our example. Its :LOGIC function,
update$a, has formals (k val st$a) and the following guard.
(and (and (integerp k) (<= 0 k) (<= k 49))
(and (integerp val) (<= 0 val))
(st$ap st$a)
(mem$c-entryp val))
The formals of update are obtained by starting with the formals of its
:EXEC function, update-mem$ci — which are (i v st$c)
— and replacing the foundational stobj name st$c by the new stobj
name st. The formals of update are thus (i v st). The guard
for update is obtained in two steps. The first step is to substitute the
formals of update for the formals of update$a in the guard for
update$a, to obtain the following.
(and (and (integerp i) (<= 0 i) (<= i 49))
(and (integerp v) (<= 0 v))
(st$ap st)
(mem$c-entryp v))
The second step is to replace, for each new stobj primitive p, the
:LOGIC function for p by p itself. The only :LOGIC
function occurring in the formula just above is st$ap, which is the
:LOGIC function for stp. The guard for update is thus as
follows.
(and (and (integerp i) (<= 0 i) (<= i 49))
(and (integerp v) (<= 0 v))
(stp st)
(mem$c-entryp v))
Note that the :EXEC version of an abstract stobj export must
not include the abstract stobj name among its formals.
We turn now to the proof obligations, as promised above. There are three
types: :CORRESPONDENCE, :PRESERVED, and :GUARD-THM. All
required lemmas may be printed simply by defining the necessary :LOGIC
and :EXEC functions and then submitting the defabsstobj event. (To
advanced users: also see defabsstobj-missing-events for a utility that
returns the required formulas in translated form.) Although the
defabsstobj event will fail if the required lemmas have not been proved,
first it will print the defthm forms that must be admitted in order to
complete submission of the defabsstobj event. (Note that although those
theorems are stated exactly in the form expected by the system, you are
welcome to supply whatever :rule-classes you prefer, even though
the system creates :rule-classes nil by default.)
The detailed theory explaining the need for these lemmas may be found in
ACL2 source file other-events.lisp, in a comment entitled ``Essay on the
Correctness of Abstract Stobjs''. Here, we give an informal sense of the
importance of these lemmas as we present examples of them. Fundamental is the
notion of evaluation in the logic versus evaluation using live stobjs, where
one imagines tracking the current value of each abstract stobj during each of
these two evaluations.
We start with the :CORRESPONDENCE lemmas. These guarantee that
evaluation in the logic agrees with evaluation using live stobjs, in the sense
that the only difference is between a logical stobj and a live stobj, where
the two correspond in the sense of the function specified by :CORR-FN.
We start with the :CREATOR function where the statement is quite simple,
stating that the :CORR-FN holds initially.
(defthm create-st{correspondence}
(st$corr (create-st$c) (create-st$a)))
For the exported functions, there are essentially two cases. If an
exported function returns other than the new abstract stobj, then the theorem
asserts the equality of the results of applying the :LOGIC and :EXEC
functions for the exported function. Hypotheses include the :CORR-FN
correspondence followed by the guard for the :LOGIC function,
which is stated in terms of the formal parameters of the :EXEC function
except using the abstract stobj (here, st) in place of the foundational
stobj (here, st$c). The conclusion uses the :EXEC formals, modified
in the call of the :LOGIC function (here, lookup$a) to use the
abstract stobj, as in the hypotheses.
(defthm lookup{correspondence}
(implies (and (st$corr st$c st)
(integerp i) (<= 0 i) (<= i 49)
(st$ap st))
(equal (mem$ci i st$c)
(lookup$a i st)))
:rule-classes nil)
By contrast, if the exported function returns the new abstract stobj, then
the conclusion uses the correspondence function instead of EQUAL, as in
the following.
(defthm update{correspondence}
(implies (and (st$corr st$c st)
(integerp i) (<= 0 i) (<= i 49)
(integerp v) (<= 0 v)
(st$ap st)
(mem$c-entryp v))
(st$corr (update-mem$ci i v st$c)
(update$a i v st)))
:rule-classes nil)
For exported functions that return multiple values, such conclusions are
conjoined together over the returned values.
The :PRESERVED lemmas guarantee that updates to the abstract stobj
preserve its recognizer. The fact that every exported function has this
property provides justification for an optimization performed by ACL2 during
generation of proof obligations for guard verification, by assuming
that the recognizer always holds. The :PRESERVED lemma for the
:CREATOR shows that the recognizer holds initially.
(defthm create-st{preserved}
(st$ap (create-st$a)))
Here is a typical such lemma, for the exported function update. Note
that there is no such lemma for lookup, since lookup does not return
st.
(defthm update{preserved}
(implies (and (integerp i) (<= 0 i) (<= i 49)
(integerp v) (<= 0 v)
(st$ap st)
(mem$c-entryp v))
(st$ap (update$a i v st))))
Finally, we consider the :GUARD-THM lemmas. These serve to guarantee
that the guard holds for each call of an :EXEC function. During
guard verification, logical definitions are used; in particular, since each
exported function is defined in the logic as the corresponding call of its
:LOGIC function, guard verification shows that each call of the
:LOGIC function for an exported function satisfies that function's guard.
But why is this true for raw Lisp evaluation using live stobjs, where the
:EXEC function is called for an exported function? The :GUARD-THM
lemmas provide the answer, as they state that if the :LOGIC function's
guard holds, then the :EXEC function's guard holds. Here is an example.
Note that the hypotheses come from the correspondence of the foundational and
abstract function as guaranteed by the :CORR function, together with the
guard of the :LOGIC function; and the conclusion comes from the guard of
the :EXEC function.
(defthm lookup{guard-thm}
(implies (and (st$corr st$c c)
(integerp i)
(<= 0 i)
(<= i 49)
(st$ap st))
(and (integerp i)
(<= 0 i)
(< i (mem$c-length st$c))))
:rule-classes nil)
We conclude this EXAMPLE section by showing a short form for the
defabsstobj form displayed above.
(defabsstobj st
:exports ((lookup :exec mem$ci)
(update :exec update-mem$ci)
misc update-misc))
SUMMARY DOCUMENTATION
The General Form is as shown below, where the order of keywords is
unimportant. Duplicate keywords are discouraged; while permitted, only the
first (leftmost) occurrence of a given keyword is used. Only the
:exports keyword is required.
(defabsstobj st
:foundation foundation
:recognizer recognizer
:creator creator
:corr-fn corr-fn
:congruent-to congruent-to
:non-executable non-executable
:protect-default protect-default
:attachable att
:exports (e1 ... ek))
The keyword argument :EXPORTS must be supplied, and missing or
nil keyword arguments have defaults as indicated below. All arguments
must satisfy the conditions below.
Before we describe the arguments, we define a notion of a ``function spec''
and its ``completion''. A function spec is either a symbol or else a list of
the form
(fn :kwd1 val1 ... :kwdn valn),
that is, a symbol followed by a keyword-value-listp. We view the
case of a symbol, s, as the function spec (s), with no keywords.
There must be no duplicate keywords. In each case that we expect a function
spec, the context provides a set of valid keywords for that function spec; it
is an error to provide any other keyword in the function spec. Each function
spec is interpreted as its ``completion'', obtained by extending the function
spec with a default value for each valid keyword as indicated below. With
that interpretation, the ``exported function'' of a function spec is its
car, and that function symbol and each keyword value must be a
guard-verified function symbol; and moreover, the :EXEC function must not
include the new abstract stobj name, st, among its formals.
We are ready to describe the arguments of defabsstobj.
St is a symbol, which names the new abstract stobj.
Foundation is the name of an existing stobj, which may have been
introduced either with defstobj or with defabsstobj.
Recognizer is a function spec (for the recognizer function). The
valid keywords are :LOGIC and :EXEC. The default for
recognizer is obtained by adding the suffix "P" to name. The
default value for :LOGIC is formed by adding the suffix "$AP" to
recognizer; for :EXEC, by adding the suffix "$CP". The
:EXEC function must be the recognizer for the foundational stobj (which
can be specified using the :FOUNDATION keyword).
Creator is a function spec (for the creator function). The valid
keywords are :LOGIC and :EXEC. The default for creator is
obtained by adding the prefix "CREATE-" to name. The default
value for :LOGIC is formed by adding the suffix "$A" to
creator; for :EXEC, by adding the suffix "$C". The
:EXEC function must be the creator for the foundational stobj (which can
be specified using the :FOUNDATION keyword).
Corr-fn is a known function symbol that takes two arguments (for the
correspondence theorems). The default for corr-fn is obtained by adding
the suffix "$CORR" to name.
Congruent-to should either be nil (the default) or the name of an
abstract stobj previously introduced (by defabsstobj). In the latter
case, the current and previous abstract stobj should have the same
foundational stobj (not merely congruent foundational stobjs), and their
:EXPORTS fields should have the same length and also correspond, as
follows: the ith export of each should have the same :LOGIC and
:EXEC symbols. See defstobj for more about congruent stobjs.
Note that if two names are congruent, then they are either both ordinary
stobjs or both abstract stobjs.
Non-executable should either be nil (the default) or t.
When t, a global stobj is not created for the given name; see defstobj, Section “Specifying Non-executable Stobjs”, for
details, as the meaning of :non-executable is the same for
defabsstobj as it is for defstobj.
Protect-default should either be nil (the default) or t. It
provides the value of keyword :PROTECT for each member of exports
that does not explicitly specify :PROTECT. See the discussion of
exports below.
Attachable should be nil (the default) or t. See attach-stobj for a discussion of this keyword.
An important aspect of the congruent-to parameter is that if it is not
nil, then the checks for lemmas — {CORRESPONDENCE},
{GUARD-THM}, and {PRESERVED} — are omitted. Thus, the values
of keyword :CORR-FN, and the values of keywords :CORRESPONDENCE,
:GUARD-THM, and :PRESERVED in each export (as we discuss next), are
irrelevant; they are not inferred and they need not be supplied.
The value of :EXPORTS is a non-empty true list. Each ei is a
function spec (for an exported function). The valid keywords are :LOGIC,
:EXEC, :CORRESPONDENCE, and :GUARD-THM, :PROTECT,
:UPDATER, and also :PRESERVED if and only if the specified
:EXEC function returns the foundational stobj. The default values for
all of these keywords except :UPDATER and :PROTECT are obtained by
respectively adding the suffix "$A" "$C",
"{CORRESPONDENCE}", "{GUARD-THM}", or "{PRESERVED}". For
:PROTECT, the default is nil unless the defabsstobj event
specifies :PROTECT-DEFAULT t. If :UPDATER upd is supplied and
upd is not nil, then function exported by the function spec is a
child stobj accessor whose corresponding updater is upd; see the
discussion of :UPDATER in nested-stobjs.
Not shown is the keyword, :MISSING; the effect of :missing t is
to turn the call of defabsstobj into a corresponding call of defabsstobj-missing-events.
Note that a defabsstobj event will fail if the required lemmas —
that is, those for valid keywords :CORRESPONDENCE, :GUARD-THM, and
:PRESERVED — have not been proved, unless proofs are being skipped.
The exemption when skipping proofs allows the supporting lemmas to be local to books and encapsulate events. If the ld special ld-skip-proofsp is t, then the missing events
are printed with a warning before the defabsstobj event is admitted; but
if ld-skip-proofsp is the symbol INCLUDE-BOOK, then that warning is
omitted. (Also see skip-proofs and see ld-skip-proofsp.) If
however proofs are not being skipped, then the defabsstobj event will
fail after printing the missing events. Advanced users may wish to see defabsstobj-missing-events for a utility that returns a data structure
containing the missing lemmas.
Let st be an abstract stobj with corresponding foundational stobj
st$c. Let f be an exported function for st and let f$a
and f$c be the corresponding :LOGIC and :EXEC functions,
respectively. The formals of f are obtained by taking the formals of
f$c and replacing st$c by st. The guard for f is
derived as follows from the guard of f$a. First, the formals of f$a
are replaced by the formals of f in the guard of f$a, to obtain a
term we denote here as guard-pre. Now for each exported function symbol
g of st with corresponding :LOGIC function g$a, form a
functional substitution by consing g$a with g. Finally, apply that
functional substitution to guard-pre; the result is the guard of f.
That guard must satisfy the usual conditions of a guard: thus, it must return
a single non-stobj value and satisfy normal syntactic restrictions,
including single-threadedness in its handling of stobjs.
Remark. Because of how guards are created for exported functions, and
in particular because :LOGIC functions are replaced as discussed above, a
good discipline is to define :LOGIC functions that are not intended for
general use, but are intended only for use as :LOGIC functions of
corresponding stobj primitives. For example, suppose that you use length
as the :LOGIC function for some stobj primitive, f (as opposed to
using your own function, say, foo-length or foo$a). Then every call
of length will be replaced by f when creating the guard of a stobj
primitive from the guard of its :LOGIC function. This might not be what
you intended if you were using length in that guard simply to compute the
length of an ordinary list.
Additional restrictions include the following.
- All exported function names must be new (unless redefinition is on; see
ld-redefinition-action), and there must be no duplicates among
them.
- The foundational stobj name must be a formal parameter of the :EXEC
function of every function spec, except for the :CREATOR function
spec.
- The :LOGIC and :EXEC function for a function spec must agree on
both the number of inputs and the number of outputs.
- The foundational stobj must not be a declared stobj of the
:LOGIC function of any function spec. (This restriction could perhaps be
removed, but it is convenient for the implementation of the events generated
by a call of defabsstobj.)
- The :PROTECT keyword is something that you should ignore unless you
get an error message about it, pertaining to modifying the foundational stobj
non-atomically. In that case, you can eliminate the error by providing
:PROTECT t in the function spec, or by providing defabsstobj keyword
argument :PROTECT-DEFAULT t at the top level, in order to restore the
required atomicity. The above explanation is probably all you need to know
about :PROTECT, but just below is a more complete explanation for those
who desire it. Further information is also available if you need it; see
set-absstobj-debug, and see the example uses of these keywords in
community book books/demos/defabsstobj-example-2.lisp.
For those who are interested, here is a more detailed discussion of
:PROTECT and :PROTECT-DEFAULT, as promised above. It applies to any
function spec for an export (hence not to the :CREATOR function spec).
If the :EXEC function is a stobj primitive, then clearly the following
property holds: any execution of a call of that function can only update the
foundational stobj at most once — i.e., modification of the foundational
stobj is atomic. ACL2 can deduce this property not only for stobj primitives
but for many other functions as well. However, if ACL2 cannot deduce this
property, then it will cause an error saying that the :EXEC function
``appears capable of modifying the foundational stobj, <stobj_name>,
non-atomically.'' That message also explains how to eliminate this error:
provide :PROTECT t for the function spec. Alternatively, all function
specs without an explicit :PROTECT keyword can be implicitly supplied
:PROTECT t by supplying the value t for the :PROTECT-DEFAULT
keyword parameter of the defabsstobj event. However, beware that when
:PROTECT is t, the generated raw Lisp code runs slightly less
efficiently — though perhaps with negligible efficiency loss if the
:EXEC function is not trivial. Community books
books/demos/defabsstobj-example-3.lisp and
books/demos/defabsstobj-example-4.lisp provide related information. Also
see set-absstobj-debug for a potentially dangerous way to eliminate
that inefficiency using argument :ignore.
We conclude with some remarks.
Unlike defstobj, there is no :renaming argument. Instead, the
scheme described above provides a flexible way to assign names. Also unlike
defstobj, there is no :inline or :non-memoizable argument;
:inline is essentially t, in the sense that stobj primitives are macros
in raw Lisp; and the :non-memoizable argument is derived implicitly, to
agree with non-memoizability of the foundational stobj.
Those who use hons-enabled features, including function
memoization (see memoize), may be aware that the memo table for a
function is flushed whenever it is the case that one of its stobj inputs is
updated. In fact, such flushing happens even when a stobj that is congruent
to one of its stobj inputs is updated. For that purpose, an abstract stobj is
considered to be congruent to its foundational stobj.
Subtopics
- Attach-stobj
- Attach an “implementation stobj” to an attachable
stobj
- Set-absstobj-debug
- Get more information when atomic update fails for an abstract stobj
- Defabsstobj-events
- Alternative to defabsstobj that tries to prove the necessary
correspondence and preservation theorems instead of making you prove them
ahead of time.
- Illegal-state
- Illegal ACL2 state
