Define a new abstract single-threaded object

We assume familiarity with single-threaded objects; see stobj and see defstobj. The event

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`. *concrete* (introduced by `defstobj`) or *abstract* (introduced by

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

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, `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, `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 likefoo-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 `defstobj` or `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

We can picture a sequence of updates to an abstract stobj and its
foundational stobj. Initially in this picture,

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

**EXAMPLE**

We present examples, with detailed comments intended to explain abstract
stobjs, in two community books:

Here is the first of two closely related

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

(and (and (integerp k) (<= 0 k) (<= k 49)) (and (integerp val) (<= 0 val)) (st$ap st$a) (mem$c-entryp val))

The formals of

(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

(and (and (integerp i) (<= 0 i) (<= i 49)) (and (integerp v) (<= 0 v)) (stp st) (mem$c-entryp v))

Note that the

We turn now to the proof obligations, as promised above. There are three
types: `defthm` forms that must be admitted in order to
complete submission of the `rule-classes` you prefer, even though
the system creates

The detailed theory explaining the need for these lemmas may be found in
ACL2 source file

We start with the

(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

(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

(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

(defthm create-st{preserved} (st$ap (create-st$a)))

Here is a typical such lemma, for the exported function

(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

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

(defabsstobj st :foundation foundation :recognizer recognizer :creator creator :corr-fn corr-fn :congruent-to congruent-to :non-executable non-executable :protect-default protect-default :exports (e1 ... ek))

The keyword argument

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,

We are ready to describe the arguments of

St is a symbol, which names the new abstract stobj.

Foundation is the name of an existing stobj, which may have been introduced either withdefstobjor withdefabsstobj .

Recognizer is a function spec (for the recognizer function). The valid keywords are:LOGIC and:EXEC . The default forrecognizer is obtained by adding the suffix"P" toname . The default value for:LOGIC is formed by adding the suffix"$AP" torecognizer ; 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 forcreator is obtained by adding the prefix"CREATE-" toname . The default value for:LOGIC is formed by adding the suffix"$A" tocreator ; 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 forcorr-fn is obtained by adding the suffix"$CORR" toname .

Congruent-to should either benil (the default) or the name of an abstract stobj previously introduced (bydefabsstobj). 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 benil (the default) ort . Whent , 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 fordefabsstobj as it is fordefstobj .

Protect-default should either benil (the default) ort . It provides the value of keyword:PROTECT for each member ofexports that does not explicitly specify:PROTECT . See the discussion ofexports below.An important aspect of the

congruent-to parameter is that if it is notnil , 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. Eachei 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 isnil unless thedefabsstobj event specifies:PROTECT-DEFAULT t . If:UPDATER upd is supplied andupd is notnil , then function exported by the function spec is a child stobj accessor whose corresponding updater isupd ; see the discussion of:UPDATER in nested-stobjs.

Not shown is the keyword, `defabsstobj-missing-events`.

Note that a `local` to books and `encapsulate` events. If the `ld` special `ld-skip-proofsp` is

Let

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 ofdefabsstobj .) - 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 providingdefabsstobj 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 bookbooks/demos/defabsstobj-example-2.lisp .

For those who are interested, here is a more detailed discussion of

We conclude with some remarks.

Unlike `defstobj`, there is no `defstobj`, there is no

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.

- 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