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.
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
The syntax of
(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)
The universal accessor and updater functions have the following signature:
(sr field index stobj) -> value (sw field index value stobj) -> new-stobj
In addition to these two functions, we also provide top-level field
accessors and updaters (e.g.,
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
(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)
Record-like stobjs are now based on abstract stobjs. This offers various
benefits over a
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
With rstobjs, the state is logically just a record, so logically there is no
restriction on the
(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
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 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.