Major Section: STOBJ

For this topic we assume that you already understand the basics of single-threaded objects in ACL2. See stobj, and in particular, see defstobj. The latter topic defers discussion of the ability to specify a stobj field that is itself a stobj or an array of stobjs. That discussion is the subject of the present documentation topic.

Our presentation is in four sections. First we augment the documentation for
`defstobj`

by explaining how stobjs may be specified for fields in a new
stobj definition. Then we explain an aliasing problem, which accounts for a
prohibition against making direct calls to accessors and updaters involving
stobj fields of stobjs. Next, we introduce an ACL2 primitive, `stobj-let`

,
which provides the only way to read and write stobj components of stobjs.
The final section provides precise documentation for `stobj-let`

.

See also ACL2 community book `demos/modeling/nested-stobj-toy-isa.lisp`

for
a worked example, which applies nested stobj structures to defining
interpreters. A variety of small additional examples may be found in ACL2
community book `misc/nested-stobj-tests.lisp`

. For further discussion, you
are welcome to read the ``Essay on Nested Stobjs'', a long comment in ACL2
source file `other-events.lisp`

. However, this documentation topic is
intended to be self-contained for those familiar with stobjs.

SECTION: Extension of `defstobj`

to permit stobjs within stobjs

Recall that the `:type`

keyword of a `defstobj`

field descriptor can
specify the type of the field as a type-spec (see type-spec). For example,
the following specifies an integer field and a field that is an array of
bytes.

(defstobj st (int-field :type integer :initially 0) (ar-field :type (array unsigned-byte (10)) :initially 0))But the

`:type`

of a stobj field descriptor may instead be based on a
stobj. For example, the following sequence of three events is legal.
The first field descriptor of `top`

, named `sub1-field`

, illustrates one
new kind of value for `:type`

: the name of a previously-introduced stobj,
which here is `sub1`

. The second field descriptor of `top`

, named
`sub2-ar-field`

, illustrates the other new kind of value for `:type`

: an
array whose elements are specified by the name of a previously-introduced
stobj, in this case, the stobj `sub2`

.
(defstobj sub1 fld1) (defstobj sub2 fld2) (defstobj top (sub1-field :type sub1) (sub2-ar-field :type (array sub2 (10))))The

`:initially`

keyword is illegal for fields whose `:type`

is a stobj
or an array of stobjs. Each such initial value is provided by a
corresponding call of the stobj creator for that stobj. In particular, in
the case of an array of stobjs, the stobj creator is called once for each
element of the array, so that the array elements are distinct. For example,
each element of `sub2-ar-field`

in the example above is initially provided
by a separate call of `create-sub2`

. Each initial element is thus unique,
and in particular is distinct from the initial global value of the stobj.
Similarly, the initial global stobj for `sub1`

is distinct from the initial
`sub1-field`

field of the global stobj for `top`

, as these result from
separate calls of `create-sub1`

.When a stobj is used in a field of another stobj, we may refer to the former
field as a ``child stobj'' and the latter stobj as a ``parent stobj''. So in
the example above, `sub1-field`

is a child stobj of type `sub1`

for
parent stobj `top`

, and `sub2-ar-field`

is an array of child stobjs of
type `sub2`

for parent stobj `top`

. A child stobj has the same
structural shape as the global stobj of its type, but as explained above,
these are distinct structures. We follow standard terminology by saying
``isomorphic'' to indicate the same structural shape. So for example, (the
value of) `sub1-field`

is isomorphic to `sub1`

, though these are distinct
structures.

SECTION: An aliasing problem

Before introducing `stobj-let`

below, we provide motivatation for this
ACL2 primitive.

Consider the following events.

(defstobj child fld) (defstobj parent (fld2 :type child))Now suppose we could evaluate the following code, to be run immediately after admitting the two

`defstobj`

events above.
(let* ((child (fld2 parent)) (child (update-fld 3 child))) (mv child parent))Now logically there is no change to

`parent`

: `parent`

is passed through
unchanged. We can indeed prove that fact!
(thm (equal (mv-nth 1 (let* ((child (fld2 parent)) (child (update-fld 3 child))) (mv child parent))) parent))But recall that stobjs are updated with destructive assignments. That is, we really are updating

`(fld2 parent)`

to be the new value of `child`

,
whether this is explained logically or not. Thus, evaluation of the above
`let*`

form does in fact change the actual global stobj, `parent`

.(Aside: Here is an explanation involving raw Lisp, for those who might find
this useful. We escape to raw Lisp and execute the following; note that
`*the-live-parent*`

is the Lisp variable representing the global value of
`parent`

.

(let ((parent *the-live-parent*)) (let* ((child (fld2 parent)) (child (update-fld 4 child))) (mv child parent)))Then, in raw Lisp,

`(fld (fld2 *the-live-parent*))`

evaluates to `4`

,
illustrating the destructive update. End of Aside.)Such aliasing can permit a change to a child stobj to cause a
logically-inexplicable change to the parent stobj. Similarly, unfettered
accessing of stobj fields can result in logically inexplicable changes to the
child stobj when the parent stobj is changed. Thus, ACL2 disallows direct
calls of stobj accessors and updaters for fields whose `:type`

is a stobj
or an array of stobjs. Instead, ACL2 provides `stobj-let`

for reading and
writing such fields in a sound manner.

SECTION: Accessing and updating stobj fields of stobjs using `stobj-let`

ACL2 provides a primitive, `stobj-let`

, to access and update stobj fields
of stobjs, in a manner that avoids the aliasing problem discussed above. In
this section we provide an informal introduction to `stobj-let`

, using
examples, to be followed in the next section by precise documentation.

We begin by returning to a slight variant of the example above.

(defstobj child fld) (defstobj parent (fld2 :type child) fld3)The following form returns the result of updating the

`fld2`

field of
`parent`

, which is a stobj isomorphic to `child`

, to have a value of 3.
Below we explain the terms ``bindings'', ``producer variables'',
``producer'', and ``consumer'', as well as how to understand the form above.
(stobj-let ((child (fld2 parent))) ; bindings (child) ; producer variable(s) (update-fld 3 child) ; producer (update-fld3 'a parent)) ; consumerThe four lines under ``

`stobj-let`

'' just above can be understood,
respectively, as follows.
o Bindings: BindThus, the logical expansion of the`child`

to`(fld2 parent)`

. o Producer variable(s) and producer: Bind the producer variable,`child`

, to the value of the producer,`(update-fld 3 child)`

. o Implicit extra step: Update`fld2`

of`parent`

with the producer variable,`child`

. o Consumer: Finally, return`(update-fld3 'a parent)`

.

`stobj-let`

form above is the following
expression, though this is approximate (see below).
(let ((child (fld2 parent))) ; bindings (let ((child (update-fld 3 child))) ; bind producer vars to producer (let ((parent (update-fld2 child parent))) ; update parent (update-fld3 'a parent))))The bindings always bind distinct names to child stobjs of a unique parent stobj, where the child stobj corresponds to the

`:type`

associated with the
indicated accessor in the `defstobj`

form for the parent stobj. Thus in
this case, for the unique binding, variable `child`

is bound to the stobj
of `type' `child`

for accessor `fld2`

of the parent stobj, `parent`

.
We refer to `child`

from the bindings as a ``stobj-let-bound variable''.
Note also that the ``implicit extra step'' mentioned above is generated by
macroexpansion of `stobj-let`

; it logically updates the parent with new
child values, just before calling the consumer. Implementation note:
Destructive updating in raw Lisp lets us omit this implicit extra step.The form above is equivalent to the form displayed just below, which differs
only in specifying an explicit stobj updater corresponding to the stobj
accessor, `fld2`

. Here we show the default updater name, whose name has
`"UPDATE-"`

prepended to the name of the accessor. But if the
`:RENAMING`

field of the `defstobj`

event specified a different updater
name corresponding to `fld2`

, then that would need to be included where we
have added `update-fld2`

below.

(stobj-let ((child (fld2 parent) update-fld2)) ; bindings, including updater(s) (child) ; producer variables (update-fld 3 child) ; producer (update-fld3 'a parent)) ; consumer

If you try to evaluate (either version of) the above `stobj-let`

form in
the top-level loop, you will get an error. For technical reasons, ACL2
limits `stobj-let`

computation on ``live'' stobjs (as opposed to list
structures that happen to satisfy stobj recognizers) to be within function
bodies. The following edited log illustrates how `stobj-let`

may be used
in function bodies.

ACL2 !>(defstobj child fld) Summary Form: ( DEFSTOBJ CHILD ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) CHILD ACL2 !>(defstobj parent (fld2 :type child) fld3) Summary Form: ( DEFSTOBJ PARENT ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) PARENT ACL2 !>(defun f (parent) (declare (xargs :stobjs parent)) (stobj-let ((child (fld2 parent))) ; bindings (child) ; producer variables (update-fld 3 child) ; producer (update-fld3 'a parent))) ; consumer [[output omitted]] F ACL2 !>(f parent) <parent> ACL2 !>(defun check-f (parent) ; returns the value of the field of the child stobj (declare (xargs :stobjs parent)) (stobj-let ((child (fld2 parent))) ; bindings (val) ; producer variables (fld child) ; producer val)) ; consumer [[output omitted]] CHECK-F ACL2 !>(check-f parent) 3 ACL2 !>

Notice that the second function defined above, `check-f`

, uses a
`stobj-let`

form that returns an ordinary value: it reads a value from a
child stobj, but does not write to the child stobj, as indicated by the lack
of a child stobj among the producer variables. So for that `stobj-let`

form, there is no implicit extra step.

For the `stobj-let`

expansion displayed earlier above, we said it was
``approximate'' for two reasons, which we give here informally. (You can
apply `:`

`trans1`

to the `stobj-let`

call above to see the formal
expansion.) First, `stobj-let`

declares the stobj-let-bound variables to
be `ignorable`

for the top `let`

bindings. Second, and more importantly,
`stobj-let`

imposes the following restrictions on the producer and
consumer, to avoid the aliasing problem: it disallows references to the
parent stobj in the producer and it also disallows references to any bound
stobj (i.e., bound in the bindings) in the consumer.

We conclude this section with examples based on a slight variation of the
nested stobj example from the first section above. These events can also be
found in ACL2 community book `misc/nested-stobj-tests.lisp`

, immediately
under the following comment:

; As promised in :doc stobj-let, we begin with an example from that :doc.Note that some lemmas were needed in order to complete the guard proof for the function

`update-top`

, which may be found in the above file; they
are omitted below.First we introduce three stobjs.

(defstobj kid1 fld1) (defstobj kid2 fld2) (defstobj mom (kid1-field :type kid1) (kid2-ar-field :type (array kid2 (5))) last-op)The next function takes a given index and a

`mom`

stobj, and swaps the
value stored in the stobj in `mom`

's `kid2-ar-field`

array at that index
with the value stored in the stobj in `mom`

's `kid1-field`

field.
(defun mom-swap-fields (index mom) (declare (xargs :stobjs mom :guard (and (natp index) (< index (kid2-ar-field-length mom))))) (stobj-let ((kid1 (kid1-field mom)) (kid2 (kid2-ar-fieldi index mom))) (kid1 kid2) (let* ((val1 (fld1 kid1)) (val2 (fld2 kid2)) (kid1 (update-fld1 val2 kid1)) (kid2 (update-fld2 val1 kid2))) (mv kid1 kid2)) (update-last-op 'swap mom)))Function

`mom.kid1-fld1`

stores a given value in the given `mom`

's
`kid1-fld1`

field.
(defun mom.kid1-fld1 (val mom) (declare (xargs :stobjs mom)) (stobj-let ((kid1 (kid1-field mom))) (kid1) (update-fld1 val kid1) (update-last-op val mom)))We next combine the two functions above, according to an

`op`

argument, as
indicated by the following definition.
(defun update-mom (op mom) (declare (xargs :stobjs mom)) (cond ((and (consp op) (eq (car op) 'swap) (natp (cdr op)) (< (cdr op) (kid2-ar-field-length mom))) (mom-swap-fields (cdr op) mom)) (t (mom.kid1-fld1 op mom))))The following checker function uses a

`stobj-let`

form like the ones above,
a major difference being that the producer variable is not a stobj, since it
does not modify the input stobj, `mom`

.
(defun check-update-mom (index val1 val2 last-op mom) (declare (xargs :stobjs mom :mode :program :guard (or (null index) (and (natp index) (< index (kid2-ar-field-length mom)))))) (and (equal (last-op mom) last-op) (stobj-let ((kid1 (kid1-field mom)) (kid2 (kid2-ar-fieldi index mom))) (val) ; producer variables (and (equal val1 (fld1 kid1)) (equal val2 (fld2 kid2))) val)))Now let us run our update function to populate some fields within the

`mom`

stobj.
(let* ((mom ; set mom to (3 (x0 x1 x2 x3 x4)) (update-mom 3 mom)) (mom ; set mom to (x1 (x0 3 x2 x3 x4)) (update-mom '(swap . 1) mom)) (mom ; set mom to (7 (x0 3 x2 x3 x4)) (update-mom 7 mom)) (mom ; set mom to (x0 (7 3 x2 x3 x4)) (update-mom '(swap . 0) mom)) (mom ; set mom to (5 (7 3 x2 x3 x4)) (update-mom 5 mom)) (mom ; set mom to (7 (5 3 x2 x3 x4)) (update-mom '(swap . 0) mom))) mom)Are the above values of 7, 5, and 3 as expected, with a last operation being a swap? Yes!

ACL2 !>(and (check-update-mom 0 7 5 'swap mom) (check-update-mom 1 7 3 'swap mom)) T ACL2 !>Notice that above, we never tried to access two different entries of the array. This can be done, but we need to bind two different stobjs to those fields. Fortunately, congruent stobjs make this possible; see defstobj, in particular the discussion of congruent stobjs. Since we want to bind two stobjs to values in the array that are isomorphic to the stobj

`kid2`

, we
introduce a stobj congruent to `kid2`

.
(defstobj kid2a fld2a :congruent-to kid2)Then we can define our swapping function as follows. The guard proof obligation includes the requirement that the two indices be distinct, again to avoid an aliasing problem.

(defun mom-swap-indices (i1 i2 mom) (declare (xargs :stobjs mom :guard (and (natp i1) (< i1 (kid2-ar-field-length mom)) (natp i2) (< i2 (kid2-ar-field-length mom)) (not (equal i1 i2))))) (stobj-let ((kid2 (kid2-ar-fieldi i1 mom)) (kid2a (kid2-ar-fieldi i2 mom))) (kid2 kid2a) (let* ((val2 (fld2 kid2)) (val2a (fld2 kid2a)) (kid2 (update-fld2 val2a kid2)) (kid2a (update-fld2 val2 kid2a))) (mv kid2 kid2a)) mom))The aforementioned community book,

`misc/nested-stobj-tests.lisp`

, contains
a corresponding checker immediately following this definition.SECTION: Precise documentation for `stobj-let`

General Form: (stobj-let BINDINGS PRODUCER-VARIABLES PRODUCER CONSUMER)where

`PRODUCER-VARIABLES`

is a non-empty true list of legal variable names
without duplicates, `PRODUCER`

and `CONSUMER`

are expressions, and
`BINDINGS`

is a list subject to the following requirements.`BINDINGS`

is a non-empty true list of tuples, each of which has the form
`(VAR ACCESSOR)`

or `(VAR ACCESSOR UPDATER)`

. There is a stobj name,
`ST`

, previously introduced by `defstobj`

(not `defabsstobj`

), such
that each `accessor`

is of the form `(ACC ST)`

or `(ACCi I ST)`

, with
the same stobj name (`ST`

) for each binding. In the case `(ACC ST)`

,
`ACC`

is the accessor for a non-array field of `ST`

. In the case
`(ACCi I ST)`

, `ACCi`

is the accessor for an array field of `ST`

, and
`I`

is either a variable, a natural number, a list `(quote N)`

where
`N`

is a natural number, or a symbol introduced by `defconst`

. If
`UPDATER`

is supplied, then it is a symbol that is the name of the stobj
updater for the field of `ST`

accessed by `ACCESSOR`

. If `UPDATER`

is
not supplied, then for the discussion below we consider it to be, implicitly,
the symbol in the same package as the function symbol of `ACCESSOR`

(i.e.,
`ACC`

or `ACCi`

), obtained by prepending the string `"UPDATE-"`

to
the `symbol-name`

of that function symbol. Finally, `ACCESSOR`

has a
signature specifying a return value that is either `ST`

or is stobj
that is congruent to `ST`

.

If the conditions above are met, then the General Form expands to the one of
the following expressions, depending on whether the list
`PRODUCER-VARIABLES`

has one member or more than one member, respectively.
(But see below for extra code that may be inserted if there are stobj array
accesses in `BINDINGS`

.) Here we write `STOBJ-LET-BOUND-VARS`

for the
list of variables `VAR`

discussed above, i.e., for
`(strip-cars BINDINGS)`

. And, we write `UPDATES`

for the result of
mapping through `PRODUCER-VARIABLES`

and, for each variable `VAR`

that
has a binding `(VAR ACCESSOR UPDATER)`

in `BINDINGS`

(where `UPDATER`

may be implicit, as discussed above), collect into `UPDATES`

the tuple
`(ST (UPDATER VAR ST))`

.

For `PRODUCER-VARIABLES`

= `(PRODUCER-VAR)`

:

(let BINDINGS (declare (ignorable . STOBJ-LET-BOUND-VARIABLES)) (let ((PRODUCER-VAR PRODUCER)) (let* UPDATES CONSUMER)))

Otherwise:

(let BINDINGS (declare (ignorable . STOBJ-LET-BOUND-VARIABLES)) (mv-let PRODUCER-VARS PRODUCER (let* UPDATES CONSUMER)))Moreover, ACL2 places restrictions on the resulting expression:

`ST`

must
not occur free in `PRODUCER`

, and every variable in
`STOBJ-LET-BOUND-VARIABLES`

must not occur free in `CONSUMER`

.`Stobj-let`

forms can be evaluated using ordinary objects in theorem
contexts, much as any form. They can also, of course, appear in function
bodis. However, a `stobj-let`

form cannot be evaluated directly in the
top-level loop or other top-level contexts for execution (such as during
`make-event`

expansion).

Finally, let `FORM`

denote the form displayed above (either case). We
explain how `FORM`

is actually replaced by an expression of the form
`(PROGN$ ... FORM)`

. This expression generates an extra guard proof
obligation, which guarantees that no aliasing occurs from binding two
stobj-let-bound variables to the same array access. So fix a stobj array
accessor `ACCi`

for which some stobj is bound to `(ACCi I ST)`

in
`BINDINGS`

; we define an expression `ACCi-CHECK`

as follows. Collect up
all such index expressions `I`

, where if `I`

is of the form `(quote N)`

then replace `I`

by `N`

. If the resulting list of index expressions for
`ACCi`

consists solely of distinct numbers, or if it is of length 1, then
no extra check is generated for `ACCi`

. Otherwise, let `ACCi-CHECK`

be
the form `(chk-no-duplicatesp (list I1 ... Ik))`

, where `I1`

, ..., `Ik`

are the index expressions for `ACCi`

. Note: `chk-no-duplicatesp`

is a
function that returns nil, but has a guard that its argument is an
`eqlable-listp`

that satisfies `no-duplicatesp`

. Finally, `FORM`

is replaced by `(PROGN$ CHK1 ... CHKn FORM)`

, where the `CHKm`

range over
all of the above `ACCi-CHECK`

.