Using stobjs that contain stobjs

For this topic we assume that you already understand the basics of single-threaded objects in ACL2. See stobj, and in particular, see defstobj, which notes that a stobj field can itself be a stobj, an array or hash-tablle of stobjs, or a stobj-table. The present documentation topic expands on that point. However, we ignore stobj-table fields here; see stobj-table for such documentation.

Our presentation is in five 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,

See also ACL2 community book

Recall that the `defstobj` field descriptor
can be a ``type-indicator'' that specifies the type of the field as a
type-spec (see type-spec). For example, the following specifies an
integer field, a field that is an array of bytes, and a field that is a
hash table whose values are integers.

(defstobj st (int-field :type integer :initially 0) (ar-field :type (array unsigned-byte (10)) :initially 0) (ht-field :type (hash-table eql nil integer) :initially 0))

But the

(defstobj sub1 fld1) (defstobj sub2 fld2) (defstobj top (sub1-field :type sub1) (sub2-ar-field :type (array sub2 (10))) (sub2-ht-field :type (hash-table equal nil sub2)))

The

For a hash-table field, the

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,

ACL2 enforces the following restriction, which can allow for greater
efficiency in the raw Lisp code generated for `defstobj` using keyword argument

Before introducing

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

(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 `let*` form does in fact change the actual global stobj,

(Aside: Here is an explanation involving raw Lisp, for those who might find this useful. We escape to raw Lisp and execute the following.

(let ((parent (cdr (assoc-eq 'parent *user-stobj-alist*)))) (let* ((child (fld2 parent)) (child (update-fld 4 child))) (mv child parent)))

Then, in raw Lisp,

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

ACL2 provides a primitive,

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

(stobj-let ((child (fld2 parent))) ; bindings (child) ; producer variable(s) (update-fld 3 child) ; producer (update-fld3 'a parent)) ; consumer

The four lines under ``

- Bindings:

Bind

child to(fld2 parent) . - Producer variable(s) and producer:

Then bind the variable,

child , to the value of the producer,(update-fld 3 child) . - Implicit update of parent:

Update

fld2 ofparent with the producer variable,child . - Consumer:

Finally, return

(update-fld3 'a parent) .

Thus, the logical expansion of the

(let ((child (fld2 parent))) ; bindings (let ((child (update-fld 3 child))) ; bind producer vars to producer (let ((parent (update-fld2 child parent))) ; implicit update of 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 `defstobj` form for the parent stobj. Thus in
this case, for the unique binding, variable `defstobj`
using keyword argument

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,

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

You can experiment using `trans1` to see the single-step
macroexpansion of a `mv-let` form is generated to bind the two fields to their values returned by
the producer, rather than a `let` form as previously generated. First,
let's introduce some events.

(defstobj child1 child1-fld) (defstobj child2 child2-fld) (defstobj child3 child3-fld) (defstobj mom (fld1 :type child1) (fld2 :type child2) (fld3 :type child3)) ; Silly stub: (defun update-last-op (op mom) (declare (xargs :stobjs mom)) (declare (ignore op)) mom) (defun new-mom (mom) (declare (xargs :stobjs mom)) (stobj-let ((child1 (fld1 mom)) (child2 (fld2 mom)) (child3 (fld3 mom))) (child1 child3) (let* ((child1 (update-child1-fld 'one child1)) (child3 (update-child3-fld 'three child3))) (mv child1 child3)) (update-last-op 'my-compute mom)))

Now let's look at the single-step macroexpansion of the above

ACL2 !>:trans1 (stobj-let ((child1 (fld1 mom)) (child2 (fld2 mom)) (child3 (fld3 mom))) (child1 child3) (let* ((child1 (update-child1-fld 'one child1)) (child3 (update-child3-fld 'three child3))) (mv child1 child3)) (update-last-op 'my-compute mom)) (PROGN$ (LET ((CHILD1 (FLD1 MOM)) (CHILD2 (FLD2 MOM)) (CHILD3 (FLD3 MOM))) (DECLARE (IGNORABLE CHILD1 CHILD2 CHILD3)) (MV-LET (CHILD1 CHILD3) (CHECK-VARS-NOT-FREE (MOM) (LET* ((CHILD1 (UPDATE-CHILD1-FLD 'ONE CHILD1)) (CHILD3 (UPDATE-CHILD3-FLD 'THREE CHILD3))) (MV CHILD1 CHILD3))) (LET* ((MOM (UPDATE-FLD1 CHILD1 MOM)) (MOM (UPDATE-FLD3 CHILD3 MOM))) (CHECK-VARS-NOT-FREE (CHILD1 CHILD2 CHILD3) (UPDATE-LAST-OP 'MY-COMPUTE MOM)))))) ACL2 !>

If you try to evaluate a

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,

We labeled a `trans1` to that

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

; 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

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

(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

(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

(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

(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

(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

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

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

where

`defstobj` (not `defabsstobj`), such that each
`symbol-name` of

If the conditions above are met, then the General Form expands to one of
the expressions below, depending on whether the list

- Let
BINDINGS' be the result of dropping each updater (if any) fromBINDINGS , that is, replacing each tuple(VAR ACCESSOR UPDATER) inBINDINGS by(VAR ACCESSOR) . - Let
STOBJ-LET-BOUND-VARIABLES be the list of variablesVAR discussed above, that is,(strip-cars BINDINGS) . - Let
UPDATES be the result of mapping throughPRODUCER-VARIABLES and, for each variableVAR that has a binding(VAR ACCESSOR UPDATER) inBINDINGS (whereUPDATER may be implicit, as discussed above), collect intoUPDATES the tuple(ST (UPDATER VAR ST)) .

For

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

`make-event` expansion).

Finally, let `trans1` will not show this
addition of a check. But you can see it after admitting the definition of
`skip-proofs` if you are having difficult
admitting the definition) as follows.

(untranslate (body 'FN nil (w state)) nil (w state))

This section shows how an abstract stobj may be considered to have child
stobj accessors and updaters that may be used with

Below we assume familiarity with abstract stobjs; see defabsstobj.
We begin with a specification of child stobj accessor/updater pairs for
abstract stobjs. We then present an example. Finally we conclude by
discussing aspects of

The documentation for `defabsstobj` notes a function spec in the

An abstract stobj

(acc :logic acc$a :exec acc$c :updater upd) ; and optionally, other keywords (upd :logic upd$a :exec upd$c) ; and optionally, other keywords

It is required that

For

A child stobj accessor/updater pair may be used in

The following basic example comes from the community-book,

We start by introducing a concrete stobj with two child stobj fields, each of which represents a natural number, together with a ``valid bit'' that, when true, asserts the equality of those two numbers.

(defstobj n$ (n$val :type (integer 0 *) :initially 0)) (defstobj n$2 (n$val$c :type (integer 0 *) :initially 0) :congruent-to n$) (defstobj two-usuallyequal-nums$c (uenslot1$c :type n$) ; stobj slot ; (uenslot2$c :type n$2) ; stobj slot ; (uenvalid$c :type (member t nil) :initially nil))

We represent this concrete stobj abstractly using a cons structure of the
form

(defun-nx two-usuallyequal-nums$ap (x) ; A two-usuallyequal-nums contains three fields (valid slot1 . slot2). Valid ; is Boolean, and slot1 and slot2 are n$ stobjs that must be equal if valid is ; T. (declare (xargs :guard t)) (and (consp x) (consp (cdr x)) (let* ((valid (car x)) (slot1 (cadr x)) (slot2 (cddr x))) (and (booleanp valid) (n$p slot1) (n$p slot2) (implies valid (equal slot1 slot2))))))

The next step is to define functions in support of the abstract stobj that we intend to introduce. Here is one such definition.

(defun-nx update-uenslot1$a (n$ x) (declare (xargs :guard (and (two-usuallyequal-nums$ap x) (or (not (uenvalid$a x)) (non-exec (equal (n$val n$) (n$val (uenslot2$a x)))))) :stobjs n$)) (cons (car x) (cons n$ (cddr x))))

After introducing such functions we introduce our abstract stobj as
follows (see the aforementioned book if you want details). Notice the use of
the

(defabsstobj two-usuallyequal-nums :exports ((uenslot1 :logic uenslot1$a :exec uenslot1$c :updater update-uenslot1) (uenslot2 :logic uenslot2$a :exec uenslot2$c :updater update-uenslot2) (uenvalid :logic uenvalid$a :exec uenvalid$c) (update-uenslot1 :logic update-uenslot1$a :exec update-uenslot1$c) (update-uenslot2 :logic update-uenslot2$a :exec update-uenslot2$c) (update-uenvalid :logic update-uenvalid$a :exec update-uenvalid$c)))

We may now use

(defun fields-of-two-usuallyequal-nums (two-usuallyequal-nums) (declare (xargs :stobjs two-usuallyequal-nums)) (stobj-let ; bindings: ((n$ (uenslot1 two-usuallyequal-nums)) (n$2 (uenslot2 two-usuallyequal-nums))) ; producer variable: (n1 n2) ; producer: (mv (n$val n$) (n$val n$2)) ; consumer: (list :n n1 :n2 n2 :valid (uenvalid two-usuallyequal-nums))))

Here is what we get when we we this function before updating the abstract stobj.

ACL2 !>(fields-of-two-usuallyequal-nums two-usuallyequal-nums) (:N 0 :N2 0 :VALID NIL) ACL2 !>

We can update the abstract stobj by first setting the valid bit to nil, so that we can sequentially update the two child stobjs. We say more about that point below.

(defun update-two-usuallyequal-nums (n two-usuallyequal-nums) (declare (xargs :guard (natp n) :stobjs two-usuallyequal-nums)) (let* ((two-usuallyequal-nums (update-uenvalid nil two-usuallyequal-nums))) (stobj-let ((n$ (uenslot1 two-usuallyequal-nums)) (n$2 (uenslot2 two-usuallyequal-nums))) (n$ n$2) (let* ((n$ (update-n$val n n$)) (n$2 (update-n$val n n$2))) (mv n$ n$2)) (update-uenvalid t two-usuallyequal-nums))))

To see why we first update the valid bit to

ACL2 !>(untranslate (body 'update-two-usuallyequal-nums nil (w state)) nil (w state)) (LET ((TWO-USUALLYEQUAL-NUMS (UPDATE-UENVALID NIL TWO-USUALLYEQUAL-NUMS))) (LET ((N$ (UENSLOT1 TWO-USUALLYEQUAL-NUMS)) (N$2 (UENSLOT2 TWO-USUALLYEQUAL-NUMS))) (MV-LET (N$ N$2) (LET* ((N$ (UPDATE-N$VAL N N$)) (N$2 (UPDATE-N$VAL N N$2))) (LIST N$ N$2)) (LET* ((TWO-USUALLYEQUAL-NUMS (UPDATE-UENSLOT1 N$ TWO-USUALLYEQUAL-NUMS)) (TWO-USUALLYEQUAL-NUMS (UPDATE-UENSLOT2 N$2 TWO-USUALLYEQUAL-NUMS))) (UPDATE-UENVALID T TWO-USUALLYEQUAL-NUMS))))) ACL2 !>

We can see that if the valid bit were

The update works, as shown in the log below.

ACL2 !>(update-two-usuallyequal-nums 17 two-usuallyequal-nums) <two-usuallyequal-nums> ACL2 !>(fields-of-two-usuallyequal-nums two-usuallyequal-nums) (:N 17 :N2 17 :VALID T) ACL2 !>

As suggested by the example above,

One difference is that the only field accessors in the

Another difference is in the aliasing checks. Recall that for an abstract
stobj

Another aspect of

- Stobj-table
- A stobj field mapping stobj names to stobjs