Modeling State Machines

“*The meaning of a program is defined by its effect on the
state vector*” — John McCarthy, Towards a Mathematical Science
of Computation (1962).

Users of ACL2 (see bib::kmm00a and bib::kmm00b) and its predecessor, Nqthm (see bib::bm97), have long modeled state machines and verified interesting properties of programs running on those machines. The basic idea is to represent the state of the machine (including its programs) by an ACL2 object and then define an interpreter that computes a “final” state from an initial state. In this documentation topic we fill out that sketch of the methodology without being specific about any particular machine. We then dive into details in subsidiary topics.

If you have ideas for additions or other improvements to the documentation of the ACL2 approach to operational semantics, please add suitable documentation or simply send your comments to the ACL2 developers. Note that we have intentionally limited our literature survey to models and proof methods in ACL2 and Nqthm. Widening the focus to operational semantics in general is simply beyond the scope of this documentation topic. But if you see omissions or errors in our discussion of ACL2 or Nqthm models and proof methods, please either fix them or bring them to our attention, making your suggestions as detailed as possible, e.g., what documentation topic are you looking at and precisely how would you change it? If your change involves citing a paper or Nqthm or ACL2 file that we have left out, please include the appropriate bibliographic information as well as a URL to the paper or file if possible. The following documentation topics are of concern:

- operational-semantics (the current topic)
- operational-semantics-1__simple-example
- operational-semantics-2__other-examples
- operational-semantics-3__annotated-bibliography
- operational-semantics-4__how-to-find-things
- operational-semantics-5__history-etc

You won't be able to prove theorems about ACL2 functions interpreting
another language unless you can prove theorems about ACL2 functions. An
excellent way to test yourself is to think of a program you'd like to verify
in that other programming language. Code a function in ACL2 that computes
the same answer using the same algorithm, as nearly as possible in an
applicative setting. So for example, if your program destructively modifies
an array in that other programming language, perhaps model the array in ACL2
as a list but access elements with `nth` and “modify”
elements with `update-nth`. Then prove that the ACL2 function is
correct with ACL2. If you can do that, you're ready to try to embed that
other language (or some fragment of it) in ACL2 and reason about such
programs with ACL2.

In the approach ACL2 users most often take to model state machines the first step is to represents the relevant parts of the machine's state as an ACL2 object. Then the user defines a single-step (or “small step”) function to compute the next state from the current one (and possibly some inputs). Finally, the user defines a recursive function that iterates the single-step transition from a given initial state a given number of times or until some halting condition is detected in the state. That function is often called the “run” function and is our operational semantic model. See operational-semantics-1__simple-example for a model of an extremely simple machine, the way we configure ACL2 to prove things about it, some example proofs and other uses of the model.

The argument that controls the maximum number of steps taken is often called a “clock” but it has nothing to do with the passage of time. In some models the clock is just a natural number. In others it may be a finite list of inputs to be successively transferred into the state on each cycle. In any case, the clock guarantees that the run function terminates, which is a prerequisite for functions defined recursively in ACL2. But do not be fooled into thinking that all programs running on the machine always terminate. By appropriate use of quantification one can often prove that a given program never terminates or only terminates under certain pre-conditions. This is discussed further in operational-semantics-1__simple-example.

Such a model can be used as a prototype for the machine: the model can be
executed on concrete states for testing purposes. But because ACL2 is a
formal system, it is also possible to do symbolic simulation of the model and
to prove theorems involving the model. Such theorems might be loosely
classified as being “about” a particular program running on the
machine or “about” the machine itself. An example of the first
might be that a certain program for the machine computes the factorial
function. An example of the second might be that when the machine is run

To facilitate such proofs it is common to develop a book of rewrite (and other kinds of) rules that do such things as normalize compositions of functions used in the construction of states and clock expressions. The basic idea is to control the expansions of the step and run functions to contain case explosions that would otherwise occur. E.g., we usually configure the ACL2 database so that

- the step function only expands on a state when it is possible to determine what the “next instruction” is, rather than considering all possible cases,
- when the clock is constant (or, more precisely, when it is possible to determine the explicit number of steps the clock will allow) the run function is eliminated by expanding it to a composition of steps, and
- when the clock is given by a composition of functions, as in (+ 4 (loop-clk x y z)), a sequential composition rule is used to break it into a composition of runs.

Such a configuration of ACL2 generally makes it possible to prove certain styles of theorems by following a well-understood methodology.

For example, to express a conjecture about the final state produced by a
program on the machine, one might write an implication whose hypothesis
characterizes an acceptable initial state and whose conclusion is an equality
whose left-hand side is a call of run on that state and a clock expression
that measures exactly how many steps it will take to reach the halt state or
return, and whose right-hand side is the symbolic expression of the correct
final state. The two states just mentioned and the clock expression are
usually terms involving variables denoting values found in relevant locations
in the initial state. A very strong total correctness theorem for a
factorial program might be something like “if a natural number, *n!*, is found in the memory location used for
the program's return value — and the program counter is set to the
correct next instruction and no other part of the state has changed.”
Alternatively, the theorem might only express some post-condition of the
final state. The examples in operational-semantics-1__simple-example
will make this clearer. The methodology for proving such theorems is
demonstrated there too.

The clock term,

Proofs of such theorems are most often done by induction, appealing to similar lemmas about the effects of loops and subroutine calls. But proofs using inductive assertions and other mathematical techniques can be used.

The methodology described above generally limits the human to creative contributions (like identifying invariants being maintained) and relegates to ACL2 the tedious unwinding of possibly long chains of symbolic computation. The previously mentioned documentation topic, operational-semantics-1__simple-example, carries out this entire program for a simple machine, explicates the methodology, and uses it to prove a variety of theorems.

Following this approach, users of Nqthm and ACL2 have modeled and verified properties of many interesting machines. More precise references to the work mentioned below as well as models and proofs about other machines — and other kinds of properties, like absence of deadlock — may be found in operational-semantics-2__other-examples.

After you are familiar with how to use ACL2 and have studied some of the models described here, you are ready to try to develop your own models. We offer three pieces of advice.

- Start small, e.g., model half a dozen routine instructions and master the methodology so that you can “automatically” prove things about simple programs. Be sure that your proofs don't rely on the small size of the model; in particular, don't repeatedly enumerate all possible instructions. Then add one new feature to the model and elaborate the methodology. You will often find there are multiple ways to represent the state and state changes. By starting small you will be able to iterate more quickly to find the best way to formalize new features and cope with the resulting complexity.
- Consider the necessity of introducing multiple layers of abstraction. For example your most realistic model might have finite bounds on all resources, but it might be worth your while to “duplicate” the model with unbounded resources but with meters that record the maximal extent of the resources used. Then prove a theorem relating the two models.
- As usual with ACL2, think carefully about how the prover will use the lemmas you prove. They are not just expressing mathematical relations but are used operationally to transform the formulas being proved.

Our discussion of the details of operational semantics in ACL2 is structured as follows.

- operational-semantics-1__simple-example — carries out the generic methodology to formalize and prove theorems about a very simple machine, called M1. M1 is a toy Java Virtual Machine (JVM) supporting just stack-based arithmetic and branch instructions. We highly recommend this section, though users already familiar with this style of model may wish just to skim it.
- operational-semantics-2__other-examples — briefly summarizes some other examples of operational models with citations to the relevant source documents. The topic has several goals. One is to show how we can handle programming features omitted from M1, e.g., subroutine call and return, data types, threads, monitors, etc. A second goal is to demonstrate that the methodology allows really large complex models, like of the JVM or the x86, that can be executed in ACL2 to emulate the machine in question and as the basis of formal proofs about the machine. A third goal is to point out alternative ACL2 proof styles and tools that may be of use while trying to prove theorems about state machines.
- operational-semantics-3__annotated-bibliography — is just what it says: an annotated bibliography. The annotations you see in this bibliography are akin simply to keywords. But if you select a given citation you'll generally see a discussion of how the work fits into the scheme of things. This section is an alternative way to browse through Nqthm and ACL2 examples of state machines, proofs, proof styles, and tools.
- operational-semantics-4__how-to-find-things — the various
topics on operational semantics cite papers and files that are not part of
the ACL2 documentation; for example, in these topics you might see utterances
such as “Nqthm source file
prove.lisp ”, “ACL2 source filerewrite.lisp ”, “Nqthm proof scriptexamples/hunt/fm8501.lisp ” and “ACL2 directorybooks/models/jvm/m1/ ”; this brief topic explains how to dereference these utterances. - operational-semantics-5__history-etc — a discussion of early work in the 1970s and 1980s by members of the Boyer-Moore community to model state machines, and how that work influenced the evolution of Nqthm and ACL2.

- Operational-semantics-3__annotated-bibliography
- Annotated bibliography for operational-semantics
- Operational-semantics-1__simple-example
- M1: definition, rules, clocks, proofs
- Operational-semantics-2__other-examples
- Examples of other models and proof techniques
- Operational-semantics-5__history-etc
- A quick history of our style of modeling state machines
- Operational-semantics-4__how-to-find-things
- Citation conventions for doc operational-semantics