Nested-stobjs
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, stobj-let,
which provides the only way to read and write stobj components of stobjs. The
fourth section provides precise documentation for stobj-let. We conclude
by discussing the use of stobj-let with abstract stobjs (see defabsstobj); the discussion below ignores abstract stobjs until reaching
that section.
See also ACL2 community book demos/modeling/nested-stobj-toy-isa.lisp
for a worked example, which applies nested stobj structures to the problem of
defining interpreters. A variety of small additional examples may be found in
ACL2 community book books/system/tests/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, 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 :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 a second 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. The third field descriptor is
analogous to the second, but with a hash table instead of an array. (See
stobj-table for the fourth new kind of value for :type.)
(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 :initially keyword is illegal for fields whose :type is a
stobj, an array of stobjs, or a hash table of stobjs (or, not further
discussed here, a stobj-table). For a stobj field, the initial value
is provided by a corresponding call of the stobj creator for that stobj. For
a field that is 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.
For a hash-table field, the :initially keyword is not actually used
for the initial hash table, which is empty. Instead, the :initially
keyword typically determines the value returned when an accessor is applied to
a key that is not bound — but not for a hash table with stobj values.
In that case, a fresh copy of the indicated stobj is returned when applying
the accessor to an unbound key.
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, sub2-ar-field is an array of child stobjs of
type sub2 for parent stobj top, and sub2-ht-field is a hash
table 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.
ACL2 enforces the following restriction, which can allow for greater
efficiency in the raw Lisp code generated for stobj-let forms, as per the
discussion below about clearing memoization tables. If the parent stobj is
introduced by defstobj using keyword argument :non-memoizable t,
then this is required to have been the case for every child stobj as well.
SECTION: An aliasing problem
Before introducing stobj-let below, we provide motivation 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.
(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, (fld (fld2 (cdr (assoc-eq 'parent
*user-stobj-alist*)))) 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 or hash table of stobjs (or a stobj-table). 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.
- 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 of parent with the producer variable,
child.
- 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 for those
using memoization: destructive updating in raw Lisp lets us omit this
implicit extra step, though the raw Lisp code generated for stobj-let
will clear the memoization table for every function taking the parent stobj as
an input, if any child stobj bound in the bindings is among the producer
variables — unless the parent stobj was introduced by defstobj
using keyword argument :non-memoizable t.
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 books/system/tests/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 the producer does not modify any stobjs.
(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,
books/system/tests/nested-stobj-tests.lisp, contains a corresponding
checker immediately following this definition. Also see that book for an
analogous example using a hash-table field in place of an array field; search
there for ``hash tables with stobj value types''.
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). Each VAR may
occur only once, and to avoid aliasing, the same ACCESSOR may not be
bound more than once if at least one of the variables to which it's bound is
among the PRODUCER-VARIABLES. 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. Each of these accessors and (if
supplied) updaters is a stobj accessor for the same stobj, which is typically
ST but may be a stobj congruent to ST. In the case (ACC ST),
ACC is the accessor for a scalar (hence not array, hash-table, or
stobj-table) field. In the case (ACC I ST), ACC is the accessor for
an array or hash-table field and I is either a symbol, a natural number,
or a list (quote C). 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 ACC of ACCESSOR, obtained by prepending the string
"UPDATE-" to the symbol-name of ACC unless the name of
ACC ends in "-GET" (suggesting a hash-table field access), in
which case the implicit UPDATER is obtained by replacing the suffix
"-GET" with "-PUT". Finally, ACCESSOR has a signature specifying a return value that is either VAL or is a stobj
that is congruent to VAL. (This means that only stobjs may be bound in
these bindings.)
If the conditions above are met, then the General Form expands to one of
the expressions below, depending on whether the list
PRODUCER-VARIABLES has one member or more than one member, respectively.
(But see below for extra code, denoted ``<check>'', that may be inserted
if there are stobj array or hash-table accesses in BINDINGS.) We observe
the following conventions.
- Let BINDINGS' be the result of dropping each updater (if any) from
BINDINGS, that is, replacing each tuple (VAR ACCESSOR UPDATER) in
BINDINGS by (VAR ACCESSOR).
- Let STOBJ-LET-BOUND-VARIABLES be
the list of variables VAR discussed above, that is, (strip-cars
BINDINGS).
- Let UPDATES be 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
bodies. 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). When
FORM appears in the body of a definition then in some cases, its
translation into logic is an expression of the form (PROG2$ <check>
FORM'), where FORM' is the translation of FORM. (See term
for a discussion of translation.) The <check> expression generates an
extra guard proof obligation, which guarantees that no aliasing occurs
in BINDINGS for two variables bound to accesses of the same stobj array
or hash table, when at least one of the two variables is a producer variable.
When ACL2 determines that no such aliasing is possible, for example because
all the array or hash-table accesses use distinct numeric indices or because
there are no producer variables, then FORM does not undergo such
replacement. Warning: The use of :trans1 will not show this
addition of a check. But you can see it after admitting the definition of
FN (perhaps using skip-proofs if you are having difficult
admitting the definition) as follows.
(untranslate (body 'FN nil (w state)) nil (w state))
SECTION: Using stobj-let with abstract stobjs
This section shows how an abstract stobj may be considered to have child
stobj accessors and updaters that may be used with stobj-let, in
essentially in the same way that a child stobj of a concrete stobj may be
accessed and updated with stobj-let.
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 stobj-let specific to abstract stobjs.
Child stobj accessors and updaters for abstract stobjs
The documentation for defabsstobj notes a function spec in the
:EXPORTS may introduce a child stobj accessor by including the keyword,
:UPDATER, whose value is the corresponding child stobj updater. Here we
flesh out that brief summary.
An abstract stobj st is considered to have a child stobj with accessor
acc and updater upd if the defabsstobj event introducing
st has a pair of function specs of the following form.
(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 acc$c is a child stobj accessor for the
foundational stobj, st$c, of st. It is also required that
upd$c is the child stobj updater of st$c that corresponds to
acc$c. We may call acc and upd a child stobj accessor/updater
pair for st. Note that st$c may itself be an abstract stobj, in
which case its exports acc$c and upd$c must be a child stobj
accessor/updater pair for st$c.
For acc and acc$c as above, acc is considered to be a scalar
accessor if acc$c is a scalar accessor, and otherwise acc is an
array or hash-table accessor (unless it is a stobj-table accessor, discussed
elsewhere; see stobj-table); similarly for upd, which therefore is
a scalar accessor if and only if acc is a scalar accessor.
A child stobj accessor/updater pair may be used in stobj-let in the
same way when the parent is an abstract stobj as when the parent is a concrete
stobj.
Example uses of stobj-let for an abstract stobj
The following basic example comes from the community-book,
books/system/tests/abstract-stobj-nesting/two-usuallyequal-nums-stobj-simpler.lisp,
which is based on a book contributed by Sol Swords. This example introduces
an abstract stobj with child stobj fields, and uses stobj-let to read and
write those fields. For even simpler examples that illustrate array and
hash-table fields, see community books absstobj-with-arrays.lisp and
absstobj-with-hash-tables.lisp in the same directory as above.
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 (valid slot1 . slot2) for the valid bit and the two numbers. Here
is the recognizer for that abstract stobj.
(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 :updater keyword, which identifies child stobj fields of the new
abstract stobj. Thus, uenslot1 accesses a child stobj field of the
two-usuallyequal-nums stobj, and that field is updated by the specified
:updater, update-uenslot1; similarly for uenslot2 and its
corresponding updater, update-uenslot2.
(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 stobj-let in the same way that we use it for concrete
stobjs with child stobj fields. That point is illustrated by the following
definition, which accesses the numbers in the two child stobj fields.
(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 nil, consider the logical
translation of the stobj-let form above.
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 t before doing any updates, then
the guard proof obligation would fail for the first child stobj update, made
with update-uenslot1 (as defined above; see its guard).
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 !>
Aspects of stobj-let specific to abstract stobjs
As suggested by the example above, stobj-let operates about the same
whether the parent stobj is a concrete stobj or an abstract stobj. In this
section we discuss some differences.
One difference is that the only field accessors in the BINDINGS are
child stobj field accessors. After all those are the only exported functions
for an abstract stobj that may be considered to correspond to fields..
Another difference is in the aliasing checks. Recall that for an abstract
stobj st, each child stobj accessor has an :EXEC function that is a
child stobj accessor of the foundational stobj, st$c, for st. If
st$c is itself an abstract stobj then the :EXEC function for
st$c is a child stobj accessor for the foundation of st$c; and so
on. At the end of this chain we have a child stobj accessor for a concrete
stobj, which we may call the underlying concrete child stobj accessor. The
aliasing checks are actually done with respect to the underlying concrete
child stobj accessors that correspond to the accessors in the BINDINGS.
After all, under the hood those concrete stobj functions are the ones that are
actually executed on the ``live'' stobj.
Another aspect of stobj-let specific to abstract stobjs is how aborts
are handled. If an abort occurs in the middle of a stobj-let that
updates child stobjs, when the parent stobj is an abstract stobj, you may be
put into an illegal state, with instructions for how to continue at your own
risk. See illegal-state.
Subtopics
- Stobj-table
- A stobj field mapping stobj names to stobjs
