The full paper refers to an ACL2 script containing an ACL2 model of a ``small machine.''
The ``small machine'' model discussed in this paper was first developed in 1991 for a course on how to use the Boyer-Moore theorem prover, Nqthm, to model microprocessors. The Nqthm model is a distillation of the microprocessor modeling approach developed by the Nqthm community at the University of Texas at Austin and Computational Logic, Inc., in the 1980s. The small machine model was transcribed to ACL2 in 1995 and described in the paper:
Thus, there are two ACL2 scripts formalizing the small machine, the 1996 one and the present one (1998). They are different! The differences stem from the fact that the 1996 model was not Common Lisp compliant. In order to do the performance measuring reported in the present paper, I decided to change the model to make (and prove) it compliant. I list the differences between the two models below.
statepmerely recognizes true lists of length 5, whereas in the compliant script, it recognizes syntactically well-formed states:
(defun statep (x) (declare (xargs :guard t)) (and (true-listp x) (equal (len x) 5) (pcp (pc x)) ; pc = (symbol . nat) (stkp (stk x)) ; stk = (pc ... pc) (memp (mem x)) ; mem = (int ... int) (codep (code x)))) ; code = ((symbol ins ... ins) ; ... ; (symbol ins ... ins))where an
insis a syntactically well-formed instruction. Note in particular that the 1998
stateprequires that the memory contain integers. The main reason for this has to do with the guard for the arithmetic instructions in the instruction set. The
ADDinstruction, for example, adds the contents of two memory locations. For that to be compliant, we must either know or check that the two values are numeric. If we check, we slow down the execution and we have to invent the semantics of
ADDon non-numeric values. We can avoid these two burdens by choosing the guard on memory. That, however, requires that we prove that every operation that changes memory writes integers into it.
put. What happens if we
putbeyond the end of memory? In the non-compliant script,
nils into the slots between the end of represented memory and the location to be written. That behavior violates our new guard on memory, so
putwas changed to deposit 0s into those slots. In a realistic processor we would enforce the additional guard that no instruction writes beyond the end of represented memory. This was done both in the CAP proofs by Brock and the Piton proofs by me. But I chose not to deal with such resource bounds in this small machine. Analogous to
get. In the 1996 model, we used the Lisp function
nthto retrieve memory contents -- and
nils beyond the end of memory. In the new model we use
getand define it to return 0s in that situation. Occurrences of
nthused to access memory in the old model were replaced by
getin the new.
JUMPZinstruction uses the ACL2 test
zpwhich coerces the tested value to a natural. This is artificial in the new model, where the tested value is known to be an integer. So I changed
zerop, which tests simple equality to 0. This, of course, changes the semantics of the instruction set, but makes it more realistic.
ctimes. In the 1996 model they were defined recursively to be + and * on naturals, using the Peano definitions. That way, they would suggest inductions and expand in the way needed to unwind loops in induction arguments. I proved two lemmas ``revealing'' that they were actually + and *, but kept those lemmas disabled except where I wanted to eliminate the clock functions for closed arithmetic expressions. This approach suffers the problem that if you try to compute with
ctimeson ``large'' input, e.g.,
(cplus 1000 1), as done in the clock expressions for my performance testing, you get stack overflows because of the recursive definitions. I avoid this in the new script by defining these two functions to be their natural arithmetic expressions. I then prove rewrite rules (actually
:definitionrules) that cause them to expand as though they were recursively defined. And I provide
:inductionrules so they suggest the appropriate inductions. Then I disable them. Enabling them is analogous to enabling the ``revelation'' rules of old. The neat thing about this approach is that I can now compute with simple arithmetic rather than recursion.
statepinsures that memory contents are integral. It was therefore unnecessary to write certain
(natp i)expressions; they were replaced with
(<= 0 i). Also, some theorems were generalized slightly. For example the
TIMESprogram multiplies a natural times an integer, not just a natural times a natural. The program was not changed; I just proved a stronger theorem. No new lemmas were necessary.