[This is from the ACL2 source file other-events.lisp, as modified for
support of nested stobjs.  I've removed the leading "; " at the
beginning of each line.]

.....

Essay on Nested Stobjs

After Version_6.1 we introduced a new capability: allowing fields of stobjs
to themselves be stobjs or arrays of stobjs.  Initially we resisted this idea
because of an aliasing problem, which we review now, as it is fundamental to
understanding our implementation.

Consider the following events.

  (defstobj st fld)
  (defstobj st2 (fld2 :type st))

Now suppose we could evaluate the following code, to be run immediately after
admitting the two defstobj events above.

  (let* ((st (fld2 st2))
         (st (update-fld 3 st)))
    (mv st st2))

A reasonable raw-Lisp implementation of nested stobjs, using destructive
updates, could be expected to have the property that for the returned st and
st2, st = (fld2 st2) and thus (fld (fld2 st2)) = (fld st) = 3.  However,
under an applicative semantics, st2 has not changed and thus, logically, it
follows that (fld (fld2 st2)) has its original value of nil, not 3.

In summary, a change to st can cause a logically-inexplicable change to st2.
But this problem can also happen in reverse: a change to st2 can cause a
logically-inexplicable change to st.  Consider evaluation of the following
code, to be run immediately after admitting the two defstobj events above.

  (let ((st2 (let* ((st (fld2 st2))
                    (st (update-fld 3 st)))
               (update-fld2 st st2))))
    (mv st st2))

With destructive updates in raw Lisp, we expect that st = (fld2 st2) for the
returned st and st2, and thus (fld st) = (fld (fld2 st2)) = 3.  But
logically, the returned st is as initially created, and hence (fld st) =
nil.

One can imagine other kinds of aliasing problems; imagine putting a single
stobj into two different slots of a parent stobj.

Therefore, we carefully control access to stobj fields of stobjs by
introducing a new construct, stobj-let.  Consider for example the following
events.

(defstobj st1 ...)
(defstobj st2 ...)
(defstobj st3 ...)
(defstobj st+ 
          (fld1 :type st1)
          (fld2 :type st2)
          (fld3 :type (array st3 (8))))

If producer and consumer are functions, then we can write the following
form.  Note that stobj-let takes four "arguments": bindings, producer
variables, a producer form, and a consumer form.

  (stobj-let
   ((st1 (fld1 st+))
    (st2 (fld2 st+))
    (st3 (fld3i 4 st+)))
   (x st1 y st3 ...) ; producer variables
   (producer st1 st2 st3 ...)
   (consumer st+ x y ...))

Updater names need to be supplied if not the default.  Thus, the form above
is equivalent to the following.

  (stobj-let
   ((st1 (fld1 st+) update-fld1)
    (st2 (fld2 st+) update-fld2)
    (st3 (fld3i 4 st+) update-fld3i))
   (x st1 y st3 ...) ; producer variables
   (producer st1 st2 st3 ...)
   (consumer st+ x y ...))

The form above expands as follows in the logic (or at least, essentially so).
The point is that we avoid the aliasing problem: there is no direct access to
the parent stobj when running the producer, which is updated to stay in sync
with updates to the child stobjs; and there is no direct access to the child
stobjs when running the consumer.  Note that since st2 is not among the
producer variables, fld2 is not updated.

  (let ((st1 (fld1 st+))
        (st2 (fld2 st+))
        (st3 (fld3i 4 st+)))
    (declare (ignorable st1 st2 st3)) ; since user has no way to do this
    (mv-let (x st1 y st3 ...) ; producer variables
            (check-vars-not-free (st+)
                                 (producer st1 st2 st3 ...))
            (let* ((st+ (update-fld1 st1 st+))
                   (st+ (update-fld3i 4 st3 st+)))
              (check-vars-not-free (st1 st2 st3)
                                   (consumer st+ x y ...)))))

We consider next whether the use of check-vars-not-free truly prevents access
to a stobj named in its variable list (first argument).  For example, if
<form> is the stobj-let form displayed above, might we let-bind foo to st+
above <form> and then reference foo in the producer?  Such aliasing is
prevented (or had better be!) by our implementation; in general, we cannot
have two variables bound to the same stobj, or there would be logical
problems: changes to a stobj not explained logically (because they result
from destructive changes to a "copy" of the stobj that is really EQ to the
original stobj).  On first glance, one might wonder if support for congruent
stobjs could present a problem, for example as follows.  Suppose that
function h is the identity function that maps stobj st1 to itself, suppose
that st2 is a stobj congruent to st1, and consider the form (let ((st2 (h
st1))) <term>).  If such a form could be legal when translating for execution
(which is the only way live stobjs can be introduced), then the aliasing
problem discussed above could arise, because st2 is bound to st1 and <term>
could mention both st1 and st2.  But our handling of congruent stobjs allows
h to map st1 to st2 and also to map st2 to st2, but not to map st1 to st2.
There are comments about aliasing in the definitions of translate11-let and
translate11-mv-let.

In the bindings, an index in an array access must be a symbol or a (possibly
quoted) natural number -- after all, there would be a waste of computation
otherwise, since we do updates at the end.  For each index that is a
variable, it must not be among the producer variables, to prevent its capture
in the generated updater call.

Of course, we make other checks too: for example, all of the top-level
let-bound stobj fields must be distinct stobj variables that suitably
correspond to distinct field calls on the same concrete (not abstract) stobj.
(If we want to relax that restriction, we need to think very carefully about
capture issues.)

In raw Lisp, the expansion avoids the expense of binding st+ to the updates,
or even updating st+ at all, since the updates to its indicated stobj fields
are all destructive.  IGNORE declarations take the place of those updates.
And the update uses let* instead of let at the top level, since (at least in
CCL) that adds efficiency.

  (let* ((st1 (fld1 st+))
         (st2 (fld2 st+))
         (st3 (fld3i 4 st+)))
    (declare (ignorable st1 st2 st3))
    (mv-let (x st1 y st3 ...)
            (producer st1 st2 st3 ...)
            (declare (ignore st1 st3))
            (consumer st+ x y ...)))

Note that bound variables of a stobj-let form must be unique.  Thus, if the
parent stobj has two fields of the same stobj type, then they cannot be bound
by the same stobj-let form unless different variables are used.  This may be
possible, since stobj-let permits congruent stobjs in the bindings.  For
example, suppose that we started instead with these defstobj events.

(defstobj st1 ...)
(defstobj st2 ... :congruent-to st1)
(defstobj st3 ...)
(defstobj st+ 
          (fld1 :type st1)
          (fld2 :type st1)
          (fld3 :type (array st3 (8))))

Then we can write the same stobj-let form as before.  ACL2 will check that
st2 is congruent to the type of fld2, which is st1.

The discussion above assumes that there are at least two producer variables
for a stobj-let.  However, one producer variable is permitted, which
generates a LET in place of an MV-LET.  For example, consider the following.

  (stobj-let
   ((st1 (fld1 st+))
    (st2 (fld2 st+))
    (st3 (fld3i 4 st+)))
   (st1) ; producer variable
   (producer st1 st2 st3 ...)
   (consumer st+ x y ...))

Here is the translation in the logic.

  (let ((st1 (fld1 st+))
        (st2 (fld2 st+))
        (st3 (fld3 st+)))
    (declare (ignorable st1 st2 st3))
    (let ((st1 (check-vars-not-free (st+)
                                    (producer st1 st2 st3 ...))))
      (let* ((st+ (update-fld1 st1 st+)))
        (check-vars-not-free (st1 st2 st3)
                             (consumer st+ x y ...)))))

For simplicity, each binding (in the first argument of stobj-let) should be
for a stobj field.

We had the following concern about *1* code generated for updaters of stobjs
with stobj fields.  Oneify-cltl-code generates a check for *1* updater calls,
for whether a stobj argument is live.  But should we consider the possibility
that one stobj argument is live and another stobj argument is not?
Fortunately, that's not an issue: if one stobj argument is live, then we are
running code, in which case translate11 ensures that all stobj arguments are
live.

End of Essay on Nested Stobjs