Misc/records
A misc/record is an alist-like
data structure that associates keys to values, but features efficient,
unconditional rewrite rules about its get and set operations.
Introduction
Note: See also the following paper:
Matt Kaufmann and Rob Sumners. Efficient
Rewriting of Data Structures in ACL2. In: Proceedings of ACL2 Workshop
2002. (Slides)
We define properties of a generic record accessor function and updater
function. The basic functions are:
- (g a r) — returns the value at address a in record
r
- (s a v r) — returns a new record by setting address a to
value v in record r
The following main lemmas are ``exported'' about record get and set:
(defthm g-same-s
(equal (g a (s a v r))
v))
(defthm g-diff-s
(implies (not (equal a b))
(equal (g a (s b v r))
(g a r))))
(defthm s-same-g
(equal (s a (g a r) r)
r))
(defthm s-same-s
(equal (s a y (s a x r))
(s a y r)))
(defthm s-diff-s
(implies (not (equal a b))
(equal (s b y (s a x r))
(s a x (s b y r))))
:rule-classes ((:rewrite :loop-stopper ((b a s)))))
We also include some auxiliary lemmas which have proven useful.
(defthm access-of-nil-is-nil
(not (g a nil)))
(defthm record-set-cannot-be-nil
(implies v (s a v r)))
(defthm record-get-non-nil-cannot-be-nil
(implies (g a r) r))
Extensions and Related Books
The misc/records book has been widely popular, especially for
representing memories and heaps. This popularity has led to some variants and
extensions.
Records make no distinction between addresses that are unbound versus
addresses that are bound to nil. This generally makes it difficult to
reason about the domain of a record, and difficult to iterate through the keys
of a record. The coi/records books add several theorems, as well as
functions like rkeys and useful lemmas like rkeyquiv-by-multiplicity
that allow you to prove records are equal by showing that they agree for any
arbitrary key in a ``pick-a-point'' fashion. These are generally not well
documented, so see the books themselves for details.
The memory library defines memory data structures which are very
similar to misc/records and provide the same read-over-write theorems, but
which are intended to be more efficient for representing processor memories.
These functions have restrictive guards that require addresses must be natural
numbers below 2^n for some n, but use a tree-like structure for
O(\log_2 n) performance.
The defrstobj library allows certain stobjs to be reasoned
about as if they were misc/records. This may be useful for developing
efficient processor models.
The keys and values of misc/records are essentially untyped. The book
coi/records/defrecord provides a way to introduce alternate ``typed''
records. See also: David Greve and Matthew Wilding. Typed
ACL2 Records. ACL2 Workshop 2003. An alternative typed record
implementation is also provided by the defrstobj books, see def-typed-record.
Implementation Notes
We normalize the record structures (which allows the equality based rewrite
rules) as alists where the keys (cars) are ordered using the total-order <<. We define a set of ``-aux'' functions which assume well-formed records,
defined by rcdp, and then prove the desired properties using hypothesis
assuming well-formed records.
We then remove these well-formed record hypothesis by defining an invertible
mapping, acl2->rcd taking any ACL2 object and returning a well-formed
record. We then prove the desired properties using the proper translations of
the -aux functions to the acl2 objects, and subsequently remove the well-formed
record hypothesis.
Subtopics
- G
- Basic accessor for misc/records.
- Memory
- Special records designed for array-like usage.
- S
- Basic update function for misc/records.
