Major Section: STOBJ

When a `defun`

uses one of its formals (other than `state`

)
as a single-threaded object (stobj), the `defun`

*must*
include a declaration that the formal it to be so used.

If the formal in question is `counters`

then an appropriate declaration
is

(declare (xargs :stobjs counters))or, more generally,

(declare (xargs :stobjs (... counters ...)))where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the names
have previously been defined as single-threaded objects with `defstobj`

.

The obvious question then arises: Why does ACL2 insist that you declare
stobj names before using them in `defun`

s if you can only declare names
that have already been defined with `defstobj`

? What would go wrong if
a formal were treated as a single-threaded object if and only if it had
already been so defined?

Suppose that one user, say Jones, creates a book in which `counters`

is defined as a single-threaded object. Suppose another user, Smith,
creates a book in which `counters`

is used as an ordinary formal
parameter. Finally, suppose a third user, Brown, wishes to use both
books. If Brown includes Jones' book first and then Smith's, then
Smith's function treats `counters`

as single-threaded. But if Brown
includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to insure that the definition is
processed the same way no matter what the context.

Major Section: STOBJ

Suppose we want to sweep a tree and (1) count the number of interior nodes, (2) count the number of tips and (3) keep a record of every tip we encounter that is an integer. We could use a single-threaded object as our ``accumulator''. Such an object would have three fields, one holding the number of nodes seen so far, one holding the number of tips, and one holding all the integer tips seen.

The following event declares `counters`

to be a single-threaded object.

(defstobj counters (NodeCnt :type integer :initially 0) (TipCnt :type integer :initially 0) (IntTipsSeen :type t :initially nil))It has three fields,

`NodeCnt`

, `TipCnt`

, and `IntTipsSeen`

.
(As always in ACL2, capitalization is irrelevant in simple symbol
names, so the first name could be written `nodecnt`

or
`NODECNT`

, etc.) Those are the name of the accessor functions for
the object. The corresponding update functions are named
`update-NodeCnt`

, `update-TipCnt`

and `update-IntTipsSeen`

.
If you do not like the default function names chosen above, there is
a feature in the `defstobj`

event that allows you to specify other
names.

If you want to see the ACL2 definitions of all the functions defined by this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level ``global variable''
`counters`

in the ACL2 read-eval-print loop we get:

ACL2 !>counters <counters>Note that the value printed is ``

`<counters>`

''. Actually, the
value of `counters`

is `(0 0 NIL)`

. But ACL2 always prints
single-threaded objects in this non-informative way because they are
usually so big that to do otherwise would be unpleasant.
Had you tried to evaluate the ``global variable'' `counters`

before
declaring it a single-threaded object, ACL2 would have complained that
it does not support global variables. So a lesson here is that
once you have declared a new single-threaded object your top-level
forms can reference it. In versions of ACL2 prior to Version 2.4
the only variable enjoying this status was `STATE`

. single-threaded
objects are a straightforward generalization of the long-implemented
von Neumann `state`

feature of ACL2.

We can access the fields of `counters`

as with:

ACL2 !>(NodeCnt counters) 0 ACL2 !>(IntTipsSeen counters) NILand we can set the fields of

`counters`

as with:
ACL2 !>(update-NodeCnt 3 counters) <counters> ACL2 !>(NodeCnt counters) 3Observe that when we evaluate an expression that returns a counter object, that object becomes the ``current value'' of

`counters`

.
Here is a function that ``converts'' the `counters`

object to its
``ordinary'' representation:

(defun show-counters (counters) (declare (xargs :stobjs (counters))) (list (NodeCnt counters) (TipCnt counters) (IntTipsSeen counters)))Observe that we

`defun`

, that
we mean to use the formal parameter `counters`

as a single-threaded
object! If we did not make this declaration, the body of
`show-counters`

would be processed as though `counters`

were an
ordinary object. An error would be caused because the accessors
used above cannot be applied to anything but the single-threaded
object `counters`

. If you want to know why we insist on this
declaration, see declare-stobjs.
When `show-counters`

is admitted, the following message is printed:

Since SHOW-COUNTERS is non-recursive, its admission is trivial. We observe that the type of SHOW-COUNTERS is described by the theorem (AND (CONSP (SHOW-COUNTERS COUNTERS)) (TRUE-LISTP (SHOW-COUNTERS COUNTERS))). We used primitive type reasoning.(SHOW-COUNTERS COUNTERS) => *.

The last line of the message is the ``signature'' of `show-counters`

and conveys the information that the first argument is the single-threaded
object `counters`

and the only result is an ordinary object.

Here is an example of `show-counters`

being called:

ACL2 !>(show-counters counters) (3 0 NIL)This is what we would see had we set the

`NodeCnt`

field of the
initial value of `counters`

to `3`

, as we did earlier in this
example.
We next wish to define a function to reset the `counters`

object.
We could define it this way:

(defun reset-counters (counters) (declare (xargs :stobjs (counters))) (let ((counters (update-NodeCnt 0 counters))) (let ((counters (update-TipCnt 0 counters))) (update-IntTipsSeen nil counters))))which ``successively'' sets the

`NodeCnt`

field to `0`

, then the
`TipCnt`

field to `0`

, and then the `IntTipsSeen`

field to `nil`

and
returns the resulting object.
However, the nest of `let`

expressions is tedious and we use this
definition instead. This definition exploits a macro, here named
```seq`

'' (for ``sequentially'') which evaluates each of the forms
given, binding their results successively to the stobj name given.

(defun reset-counters (counters) (declare (xargs :stobjs (counters))) (seq counters (update-NodeCnt 0 counters) (update-TipCnt 0 counters) (update-IntTipsSeen nil counters)))This definition is syntactically identical to the one above, after macro expansion. Our definition of

`seq`

is shown below and is not part of
native ACL2.
(defmacro seq (stobj &rest rst) (cond ((endp rst) stobj) ((endp (cdr rst)) (car rst)) (t `(let ((,stobj ,(car rst))) (seq ,stobj ,@(cdr rst))))))

The signature printed for `reset-counters`

is

(RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example.

ACL2 !>(show-counters counters) (3 0 NIL) ACL2 !>(reset-counters counters) <counters> ACL2 !>(show-counters counters) (0 0 NIL)

Here finally is a function that uses `counters`

as a single-threaded
accumulator to collect the desired information about the tree `x`

.

(defun sweep-tree (x counters) (declare (xargs :stobjs (counters))) (cond ((atom x) (seq counters (update-TipCnt (+ 1 (TipCnt counters)) counters) (if (integerp x) (update-IntTipsSeen (cons x (IntTipsSeen counters)) counters) counters))) (t (seq counters (update-NodeCnt (+ 1 (NodeCnt counters)) counters) (sweep-tree (car x) counters) (sweep-tree (cdr x) counters)))))We can paraphrase this definition as follows. If

`x`

is an atom,
then increment the `TipCnt`

field of `counters`

and `x`

is an integer, add `x`

to the `IntTipsSeen`

field, and
return `counters`

. On the other hand, if `x`

is not
an atom, then increment the `NodeCnt`

field of `counters`

, and
`car`

of `x`

and `cdr`

of `x`

and return the result.Here is an example of its execution. We have displayed the input tree in full dot notation so that the number of interior nodes is just the number of dots.

ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3) . (4 . (5 . d))) counters) <counters> ACL2 !>(show-counters counters) (7 8 (5 4 3 2 1)) ACL2 !>(reset-counters counters) <counters> ACL2 !>(show-counters counters) (0 0 NIL)

The `counters`

object has two integer fields and a field whose
type is unrestricted. single-threaded objects support other types of
fields, such as arrays. We deal with that in the stobj-example-2.
But we recommend that you first consider the implementation issues for
the `counters`

example (in stobj-example-1-implementation) and
then consider the proof issues (in stobj-example-1-proofs).

`counters`

stobj
Major Section: STOBJ

Consider the event shown in stobj-example-1:

(defstobj counters (NodeCnt :type integer :initially 0) (TipCnt :type integer :initially 0) (IntTipsSeen :type t :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the `counters`

argument below is
*not* declared with the `:stobjs`

`xarg`

even though we
insist that the argument be a stobj in calls of these functions.
This ``mystery'' is explained below.

(defun NodeCntp (x) ;;; Recognizer for 1st field (declare (xargs :guard t)) (integerp x))(defun TipCntp (x) ;;; Recognizer for 2nd field (declare (xargs :guard t)) (integerp x))

(defun IntTipsSeenp (x) ;;; Recognizer for 3rd field (declare (xargs :guard t) (ignore x)) t)

(defun countersp (counters) ;;; Recognizer for object (declare (xargs :guard t)) (and (true-listp counters) (= (length counters) 3) (NodeCntp (nth 0 counters)) (TipCntp (nth 1 counters)) (IntTipsSeenp (nth 2 counters))))

(defun NodeCnt (counters) ;;; Accessor for 1st field (declare (xargs :guard (countersp counters))) (nth 0 counters))

(defun update-NodeCnt (v counters) ;;; Updater for 1st field (declare (xargs :guard (and (integerp v) (countersp counters)))) (update-nth 0 v counters))

(defun TipCnt (counters) ;;; Accessor for 2nd field (declare (xargs :guard (countersp counters))) (nth 1 counters))

(defun update-TipCnt (v counters) ;;; Updater for 2nd field (declare (xargs :guard (and (integerp v) (countersp counters)))) (update-nth 1 v counters))

(defun IntTipsSeen (counters) ;;; Accessor for 3rd field (declare (xargs :guard (countersp counters))) (nth 2 counters))

(defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field (declare (xargs :guard (countersp counters))) (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and
then a recognizer for the `counters`

object itself. Then, for each
field, there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a
`counterp`

for their `counter`

argument and an appropriate value
for the new field values.

You can see all of the `defuns`

added by a `defstobj`

event by
executing the event and then using the `:pcb!`

command on the stobj
name. E.g.,

ACL2 !>:pcb! counterswill print the defuns above.

We now clear up the ``mystery'' mentioned above. Note, for example
in `TipCnt`

, that the formal `counters`

is used. From the
discussion in stobj-example-1 it has been made clear that
`TipCnt`

can only be called on the `counters`

object. And yet,
in that same discussion it was said that an argument is so treated
only if it it declared among the `:stobjs`

in the definition of
the function. So why doesn't `TipCnt`

include something like
`(declare (xargs :stobjs (counters)))`

?

The explanation of this mystery is as follows. At the time
`TipCnt`

was defined, during the introduction of the `counters`

stobj, the name ```counters`

'' was not yet a single-threaded
object. The introduction of a new single-threaded object occurs in
three steps: (1) The new primitive recognizers, accessors, and
updaters are introduced as ``ordinary functions,'' producing their
logical axiomatizations. (2) The executable counterparts are
defined in raw Lisp to support destructive updating. (3) The new
name is declared a single-threaded object to insure that all future
use of these primitive respects the single-threadedness of the
object. The functions defined as part of the introduction of a new
single-threaded object are the only functions in the system that
have undeclared stobj formals other than `state`

.

You may return to stobj-example-1 here.

`counters`

stobj
Major Section: STOBJ

the event

(defstobj counters (NodeCnt :type integer :initially 0) (TipCnt :type integer :initially 0) (IntTipsSeen :type t :initially nil))discussed in stobj-example-1, creates a Common Lisp object to represent the current value of

`counters`

. That object is created
by evaluating the following ``raw'' (non-ACL2) Common Lisp form:
(list (make-array 1 :element-type 'integer :initial-element '0) (make-array 1 :element-type 'integer :initial-element '0) 'nil)and the value is stored in the Common Lisp global variable named

`*the-live-counters*`

.
Thus, the `counters`

object is a list of length three. The first
two elements are arrays of size 1 and are used to hold the
`NodeCnt`

and `TipCnt`

fields. The third element is the
`IntTipsSeen`

field. The first two fields are represented by
arrays so that we can implement the `integer`

type specification
efficiently. Generally, integers are ``boxed'' in Common Lisp.
Creating a new integer requires creating a new box to put it in.
But in some lisps the integers inside arrays of integers are not
boxed.

The function `update-NodeCnt`

is defined in raw Lisp as:

(defun NodeCnt (counters) (the integer (cond ((eq counters *the-live-counters*) (aref (the (array integer (1)) (car counters)) 0)) (t (nth 0 counters)))))Observe that if

`NodeCnt`

is called on ``the live `counters`

''
the function accesses the `car`

, to get an array of size 1, and
then uses `aref`

to access the 0th element of that array.
The function `update-NodeCnt`

is defined in raw Lisp as:

(defun update-NodeCnt (v counters) (declare (type integer v)) (cond ((eq counters *the-live-counters*) (setf (aref (the (array integer (1)) (car counters)) 0) (the integer v)) counters) (t (update-nth 0 v counters))))Note that when this function is called on the live

`counters`

it
does not create a new list of length three, but ``smashes'' the existing
one.
One way to see all the functions defined by a given `defstobj`

is to
evaluate the `defstobj`

event and then evaluate, in the ACL2 loop,
the expression `(global-val 'cltl-command (w state))`

. That will
print a lisp object that you can probably figure out.

We now recommend that you look at stobj-example-1-proofs.

`counters`

stobj
Major Section: STOBJ

Consider again the event

(defun reset-counters (counters) (declare (xargs :stobjs (counters))) (seq counters (update-NodeCnt 0 counters) (update-TipCnt 0 counters) (update-IntTipsSeen nil counters)))which, because of the

`seq`

macro in stobj-example-1, is just
syntactic sugar for
(defun reset-counters (counters) (declare (xargs :stobjs (counters))) (let ((counters (update-NodeCnt 0 counters))) (let ((counters (update-TipCnt 0 counters))) (update-IntTipsSeen nil counters)))).

Here is a simple theorem about `reset-counters`

.

(defthm reset-counters-is-constant (implies (countersp x) (equal (reset-counters x) '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem is unusual in two respects.

First, it calls `reset-counters`

on an argument other than the
variable `counters`

! That is allowed in theorems; logically
speaking, the stobj functions are indistinguishable from ordinary
functions. Their use is syntactically restricted only in
`defun`

s, which might be compiled and run in raw Lisp. Those
restrictions allow us to implement stobj modification destructively.
But logically speaking, `reset-counters`

and other stobj
``modifying'' functions just create new objects, constructively.

Second, the theorem above explicitly provides the hypothesis that
`reset-counters`

is being applied to an object satisfying
`countersp`

. Such a hypothesis is not always required:
`reset-counters`

is total and will do something no matter what
`x`

is. But in this particular case, the result is not `'(0 0 nil)`

unless `x`

is, at least, a true-list of length three.

To make a long story short, to prove theorems about stobj functions you behave in exactly the way you would to prove the same theorems about the same functions defined without the stobj features.

How can we prove the above theorem? Unfolding the definition of
`reset-counters`

shows that `(reset-counters x)`

is equal to

(update-IntTipsSeen nil (update-TipCnt 0 (update-NodeCnt 0 x)))which in turn is

(update-nth 2 nil (update-nth 1 0 (update-nth 0 0 x))).Opening up the definition of

`update-nth`

reduces this to
(list* 0 0 nil (cdddr x)).This is clearly equal to

`'(0 0 nil)`

, provided we know that `(cdddr x)`

is `nil`

.Unfortunately, that last fact requires a lemma. The most specific lemma we could provide is

(defthm special-lemma-for-counters (implies (countersp x) (equal (cdddr x) nil)))but if you try to prove that lemma you will find that it requires some reasoning about

`len`

and `true-listp`

. Furthermore, the special
lemma above is of interest only for `counters`

.
The following lemma about `len`

is the one we prefer.

(defthm equal-len-n (implies (syntaxp (quotep n)) (equal (equal (len x) n) (if (integerp n) (if (< n 0) nil (if (equal n 0) (atom x) (and (consp x) (equal (len (cdr x)) (- n 1))))) nil))))This lemma will simplify any equality in which a

`len`

expression
is equated to any explicitly given constant `3`

, reducing the equation to a conjunction of `consp`

terms
about the first `cdr`

s.If the above lemma is available then ACL2 immediately proves

(defthm reset-counters-is-constant (implies (countersp x) (equal (reset-counters x) '(0 0 nil))))

The point is presumably well made: proving theorems about single- threaded object accessors and updaters is no different than proving theorems about other recursively defined functions on lists.

Another lemma that is useful in reasoning about single-threaded objects is

(defthm update-nth-update-nth-diff (implies (not (equal (nfix i1) (nfix i2))) (equal (update-nth i1 v1 (update-nth i2 v2 l)) (update-nth i2 v2 (update-nth i1 v1 l)))) :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))This lemma is due to Matt Wilding.

We now recommend that you see stobj-example-2.

Major Section: STOBJ

The following event

(defstobj ms (pcn :type integer :initially 0) (mem :type (array integer (100000)) :initially -1) (code :type t :initially nil))introduces a single-threaded object named

`ms`

(which stands for
``machine state''). The object has three fields, a `pcn`

or program
counter, a `mem`

or memory, and a `code`

field.
The `mem`

field is occupied by an object of type
`(array integer (100000))`

. Logically speaking, this is a list of
length `100000`

, each element of which is an integer. But in the
underlying implementation of the `ms`

object, this field is occupied
by a raw Lisp array of size 1000000.

You might expect the above `defstobj`

to define the accessor function
`mem`

and the updater `update-mem`

. *That does not happen!*.

The above event defines the accessor function `memi`

and the updater
`update-memi`

. These functions do not access/update the `mem`

field of
the `ms`

object; they access/update the individual elements of the
array in that field.

In particular, the logical definitions of the two functions are:

(defun memi (i ms) (declare (xargs :guard (and (integerp i) (<= 0 i) (< i 100000) (msp ms)))) (nth i (nth 1 ms)))(defun update-memi (i v ms) (declare (xargs :guard (and (integerp i) (<= 0 i) (< i 100000) (integerp v) (msp ms)))) (update-nth 1 (update-nth i v (nth 1 ms)) ms))

For example, to access thef 511th (0-based) memory location of the
current `ms`

you could evaluate:

ACL2 !>(memi 511 ms) -1The answer is

`-1`

initially, because that is the above-specified
initial value of the elements of the `mem`

array.To set that element you could do

ACL2 !>(update-memi 511 777 ms) <ms> ACL2 !>(memi 511 ms) 777

The raw Lisp implementing these two functions is shown below.

(defun memi (i ms) (declare (type (integer 0 99999) i)) (the integer (cond ((eq ms *the-live-ms*) (aref (the (array integer (100000)) (car (cdr ms))) (the (integer 0 99999) i))) (t (nth i (nth 1 ms))))))(defun update-memi (i v ms) (declare (type (integer 0 99999) i) (type integer v)) (cond ((eq ms *the-live-ms*) (setf (aref (the (array integer (100000)) (car (cdr ms))) (the (integer 0 99999) i)) (the integer v)) ms) (t (update-nth 1 (update-nth i v (nth 1 ms)) ms))))

If you want to see the raw Lisp supporting a `defstobj`

, execute the
`defstobj`

and then evaluate the ACL2 form
`(global-val 'cltl-command (w state))`

. The s-expression printed
will probably be self-explanatory given the examples here.

We now recommend that you read stobj-example-3.

Major Section: STOBJ

The event

(defstobj $s (x :type integer :initially 0) (a :type (array (integer 0 9) (3)) :initially 9))introduces a stobj named

`$S`

. The stobj has two fields, `X`

and
`A`

. The `A`

field is an array. The `X`

field contains an
integer and is initially 0. The `A`

field contains a list of three
integers, each between 0 and 9, inclusively. Initially, each of the
elements of the `A`

field is 9.
This event introduces the following sequence of definitions:

(DEFUN XP (X) ...) ; recognizer for X field (DEFUN AP1 (X N) ...) ; aux fn for recogizer of A field (DEFUN AP (X) ...) ; recognizer of A field (DEFUN $SP ($S) ...) ; top-level recognizer for stobj $S (DEFUN X ($S) ...) ; accessor for X field (DEFUN UPDATE-X (V $S) ...) ; updater for X field (DEFUN AI (I $S) ...) ; accessor for A field at index I (DEFUN UPDATE-AI (I V $S) ...) ; updater for A field at index I

Here is the definition of `$SP`

:

(DEFUN $SP ($S) (DECLARE (XARGS :GUARD T)) (AND (TRUE-LISTP $S) (= (LENGTH $S) 2) (XP (NTH 0 $S)) (AP (NTH 1 $S))))This reveals that in order to satisfy

`$SP`

an object must be
a true list of length 2 whose first element satisfies `XP`

and whose
second satisfies `AP`

. By printing the definition of `AP`

one
learns that it requires its argument to be a list of length 3, each
element of which is an integer between 0 and 9.
Here is the definition of `UPDATE-AI`

, the updater for the `A`

field
at index `I`

:

(DEFUN UPDATE-AI (I V $S) (DECLARE (XARGS :GUARD (AND (INTEGERP I) (<= 0 I) (< I 3) (AND (INTEGERP V) (<= 0 V) (<= V 9)) (SP $S)))) (UPDATE-NTH 1 (UPDATE-NTH I V (NTH 1 $S)) $S))This may be a little surprising but should be perfectly clear.

First, ignore the guard, since it is irrelevant in the logic.
Reading from the inside out, `(UPDATE-AI I V $S)`

extracts `(NTH 1 $S)`

,
which is array `a`

of `$S`

. (Recall that `NTH`

is
0-based.) The next higher expression in the definition above,
`(UPDATE-NTH I V a)`

, ``modifies'' `a`

by setting its `I`

th
element to `V`

. Call this `a'`

. The next higher expression,
`(UPDATE-NTH 1 a' $S)`

, ``modifies'' `$S`

by setting its 1st
component to `a'`

. Call this result `$s'`

. Then `$s'`

is
the result returned by `UPDATE-AI`

.

So the first useful observation is that from the perspective of the logic, the type ``restrictions'' on stobjs are irrelevant. They are ``enforced'' by ACL2's guard mechanism, not by the definitions of the updater functions.

As one might also imagine, the accessor functions do not really
``care,'' logically, whether they are applied to well-formed stobjs
or not. For example, `(AI I $S)`

is defined to be `(NTH I (NTH 1 $S))`

.

Thus, you will not be able to prove that (AI 2 $S) is an integer. That is,

(integerp (AI 2 $S))is not a theorem, because

`$S`

may not be well-formed.
Now `(integerp (AI 2 $S))`

will always evaluate to `T`

in the
top-level ACL2 command loop, because we insist that the current value of
the stobj `$S`

always satisfy `$SP`

by enforcing the guards on
the updaters whether guard checking is on or off (see
`set-guard-checking`

). But in a theorem `$S`

is just another
variable, implicitly universally quantified.

So `(integerp (AI 2 $S))`

is not a theorem because it is not true when
the variable `$S`

is instantiated with, say,

'(1 (0 1 TWO))because, logically speaking,

`(AI 2 '(1 (0 1 TWO)))`

evaluates to
the symbol `TWO`

. That is,
(equal (AI 2 '(1 (0 1 TWO))) 'TWO)is true.

However,

(implies ($SP $S) (integerp (AI 2 $S)))is a theorem. To prove it, you will have to prove a lemma about

`AP1`

. The following will do:
(defthm ap1-nth (implies (and (AP1 x n) (integerp n) (integerp i) (<= 0 i) (< i n)) (integerp (nth i x)))).

Similarly,

(implies (and (integerp i) (<= 0 i) (< i 3) (integerp v) (<= 0 v) (<= v 9)) ($SP (UPDATE-AI i v $S)))is not a theorem until you add the additional hypothesis

`($SP $S)`

.The moral here is that from the logical perspective, you must provide the hypotheses that, as a programmer, you think are implicit on the structure of your stobjs, and you must prove their invariance. This is a good area for further support, perhaps in the form of a library of macros.

This completes the tour through the documentation of stobjs.
However, you may now wish to read the documentatin for the event
that introduces a new single-threaded object, `defstobj`

.