NESTED-STOBJS

using stobjs that contain stobjs 
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 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 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 this form. 
  (stobj-let
   ((child (fld2 parent)))  ; bindings
   (child)                  ; producer variable(s)
   (update-fld 3 child)     ; producer
   (update-fld3 'a parent)) ; consumer
The four lines under ``stobj-let'' just above can be understood as follows. 
o Bindings:
    Bind child to (fld2 parent).
o Producer variable(s) and producer:
    Then bind the variable, child, to
    the value of the producer, (update-fld 3 child).
o Implicit update of parent:
    Update fld2 of parent with the producer variable, child.
o Consumer:
    Finally, return (update-fld3 'a parent).
Thus, the logical expansion of the 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))) ; 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 :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

You can experiment using :trans1 to see the single-step macroexpansion of a stobj-let form in the logic. For example, here is how that works for a stobj-let form that binds three fields and updates two of them. Notice that because more than one field is updated, an 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 stobj-let form. 
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 stobj-let form directly in the top-level loop, rather than from within a function body, you will get an error. The example above illustrates how stobj-let may be used in function bodies; here is another example, presented using an edited log. 

  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.

We labeled a stobj-let expansion above as ``approximate'' for two reasons, which we give here informally. (Now you know how to apply :trans1 to that stobj-let call to see the precise 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.