		Search-engine friendly clone of the ACL2 documentation.

Defrstobj

Record-like stobjs combine the run-time efficiency of stobjs with the reasoning efficiency of records. They are designed for modeling, e.g., the state of a processor or virtual machine.

Introduction

A Record-like stobj ("rstobj") is a way to model a processor's state that allows for both good execution efficiency and good reasoning efficiency.

The state is implemented as a stobj so that it can be accessed efficiently and updated destructively, without, e.g., lots of consing just to build the new state object. This is good since it's useful for processor models to execute efficiently.

The state is reasoned about as if it were a "record," in the sense of the misc/records book. The top-level field accessors and updators of the stobj are (logically) defined as g and s. This style of reasoning seems good. It has been used in the compositional cutpoint techniques developed by John Matthews, J Moore, Sandip Ray, and Daron Vroon, the "wormhole abstraction" of Dave Greve at Rockwell Collins, the work of Eric Smith for automated cutpoint-based proofs, etc. There are probably other people who are also using records, e.g., Rob Sumners.

Using defrstobj

The syntax of defrstobj is nearly that of defstobj, except that:

Simply typed (non-array) fields require an additional :fix argument that says how to coerce "bad" objects into an object of the appropriate type. This should be a term mentioning acl2::x.
Array fields require an additional :typed-record argument that names recognizer function for a typed record; see def-typed-record.
Optionally, you can have defrstobj define a universal accessor and a universal updater function using keywords :accessor and :updater respectively. These functions can come in handy when using community book std/stobjs/updater-independence.

Example:

(include-book "centaur/defrstobj/defrstobj" :dir :system)

(defrstobj st

  (regs :type (array (unsigned-byte 64) (32))
        :initially 0
        :typed-record u32-tr-p)

  (pc   :type (unsigned-byte 64)
        :initially 0
        :fix (unsigned-byte-fix 64 x))

  (mem  :type (array (unsigned-byte 8) (*mem-size*))
        :initially 0
        :typed-record u8-tr-p)

  :inline t
  ;; [Optional] Universal accessor and updater functions
  :accessor sr
  :updater sw)

See also centaur/defrstobj/basic-tests.lisp for several more examples, including examples of how to use def-typed-record.

Working with Universal Accessor and Updater Functions

The universal accessor and updater functions have the following signature:

(sr field index stobj)       -> value 
(sw field index value stobj) -> new-stobj

where field is a keyword corresponding to a stobj field (e.g., :mem in the above example). Their definition is pretty straightforward --- depending on the field, the appropriate accessor/updater (e.g., get-mem/set-mem) is called. However, due to the case-split on field, these two functions would be expensive for execution, so we've made them non-executable.

In addition to these two functions, we also provide top-level field accessors and updaters (e.g., @mem/!mem for the mem field above) which have an mbe --- the :logic definition is in terms of the universal accessor or updater, and the :exec definition is the stobj field accessor or updater (e.g., get-mem/set-mem). These top-level field accessors and updaters are inlined for execution performance.

We recommend the following strategy when working with the universal accessor and updater functions. You probably want all your theorems to be in terms of the two universal accessor/updater functions. Keep the top-level field accessors/updaters enabled --- you probably want to use them in functions you define on top of the stobj so that you get the performance of the underlying concrete stobj while you reason about the universal accessor/updater functions.

In addition to facilitating use with stobjs::stobj-updater-independence, a benefit of this strategy is that it can reduce the term size during reasoning. E.g., writing v to the ith location of the mem field using set-mem (which is enabled by default) would look like the following:

(s :mem (u8-tr-set i v (g :mem st)) st)

When using the universal accessor/updater functions, it'll look like the following:

(sw :mem i v st)

Notes

Record-like stobjs are now based on abstract stobjs. This offers various benefits over a previous version of rstobjs that didn't use abstract stobjs. For instance, you no longer need any kind of good-stobj predicate, and the top-level logical story is now just in terms of g and s instead of stobj-specific functions.

A subtlety of treating the state as a record is that you (logically) "lose" any type information about the top-level fields. For instance, you would expect to know that the pc field above is a 64-bit natural.

With rstobjs, the state is logically just a record, so logically there is no restriction on the pc. However, the executable accessor for the pc will logically be defined as, e.g.,

(unsigned-byte-fix 64 (g :pc st))

Note that this fixing is free in the execution; the abstract stobj invariant allows us to assume that pc is well-formed so we don't need to do any fixing.

Arrays complicate things. If a stobj only has non-array fields, then viewing it as a record is pretty straightforward—we basically have a key corresponding to each field. But how do we handle array fields, which have their own collections of elements?

One approach might be to try to keep viewing the stobj as a flat record. For instance, we might try to have the story be something like arr[3] corresponds to the field (:ARR . 3) or similar. This is probably possible, but something I didn't like about it was that it means we would also lose the type information on the array elements.

Instead, I set things up so that the whole array looks like just one field in the stobj. The array itself is represented as a typed record, with its own get/set functions that satisfy the theorems of Greve and Wilding's typed records book. See def-typed-record.

Subtopics

Def-typed-record: Introduce a typed record for use with defrstobj.