Stateman: Using Metafunctions to Manage Large Terms Representing Machine States

TL;DR

This paper introduces an ACL2 framework using metafunctions and HIDE to efficiently manage and simplify large terms representing machine states, improving proof performance in modeling complex machine behaviors.

Contribution

It presents a novel ACL2 approach employing metafunctions, HIDE, and honsing for handling large state terms, including a general-purpose memory model with verified metafunctions for read/write operations.

Findings

Enabled handling of several million function calls in state representations.

Improved proof performance through memoization of metafunctions.

Successfully modeled complex memory read/write behaviors with symbolic addresses.

Abstract

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.