  When ACL2 is used to model the operational semantics of computing machines,
machine states are typically represented by terms recording the contents of the
state components. When models are realistic and are stepped through thousands
of machine cycles, these terms can grow quite large and the cost of simplifying
them on each step grows. In this paper we describe an ACL2 book that uses HIDE
and metafunctions to facilitate the management of large terms representing such
states. Because the metafunctions for each state component updater are solely
responsible for creating state expressions (i.e., "writing") and the
metafunctions for each state component accessor are solely responsible for
extracting values (i.e., "reading") from such state expressions, they can
maintain their own normal form, use HIDE to prevent other parts of ACL2 from
inspecting them, and use honsing to uniquely represent state expressions. The
last feature makes it possible to memoize the metafunctions, which can improve
proof performance in some machine models. This paper describes a
general-purpose ACL2 book modeling a byte-addressed memory supporting "mixed"
reads and writes. By "mixed" we mean that reads need not correspond (in address
or number of bytes) with writes. Verified metafunctions simplify such
"read-over-write" expressions while hiding the potentially large state
expression. A key utility is a function that determines an upper bound on the
value of a symbolic arithmetic expression, which plays a role in resolving
writes to addresses given by symbolic expressions. We also report on a
preliminary experiment with the book, which involves the production of states
containing several million function calls.
