farray -- A data structure for a field-addressable array.

Stobjs provide constant time lookup for stobj fields/arrays in ACL2, as
opposed to lists which require linear time lookup for nth/update-nth
operations. If one wants to store multiple fields within a stobj, they need to
prove theorems about how writes to each field interact with each other field.
This leads to poor *proof convenience* and *proof efficiency* (I
believe these terms were used by J Moore at some point in our discussions and
I've latched onto it) because each field leads to a quadratic number of
theorems.

Instead, a stobj `st` can be defined with just one field: an array for
memory, or `mem`. This field can be subdivided further into other
arrays and scalars. In this way, a single array in a stobj can simulate a
stobj with multiple fields. To accomplish this, an offset table is defined
that redirects reads and writes to the proper field/subarray. With the proper
invariants, one can show that writes to any field do not interfere with other
fields. Furthermore, the addition of a field to an farray structure does not
create any extra proof effort. This solves the problem of quadratic blowup of
theorems for stobj data structures. (This approach is a generalization of an
abstraction J Moore used in the M1 model.) The only catch is that all arrays
and scalars will share the same type (60-bit signed-integers in this
definition).

This approach is somewhat analogous to memory usage in a traditional C or C-like language. In theory, farrays can be embedded; that is, a field of an farray may contain another farray. This could very well be similar in execution efficiency and proof efficiency to record-like stobjs (Jared Davis) or abstract stobjs (Shilpi Goel and Matt Kaufmann).

The layout of this book is as follows:

- Define the stobj in which the farray will reside.
- Define and analyze recursive predicate for checking farray field table.
- Define farray predicate.
- Define types, accessors, and updaters including:
- num-fields
- fieldp
- flength
- field-offsetp
- fread
- fwrite
- Prove theorems about fread and fwrite such as read of write, write of write, etc.
- Define functions for easily reading lists from and writing lists to stobj
- Define and analyze a membership operator for ranges within a field

This material is further described in Nathan Wetzler's dissertation available as a preprint or on the UT Digital Repository.

A talk on farray was presented at the ACL2 Seminar and the slides and figure are available online.