Proving Theorems about Models
But ACL2 is a logic. We can prove theorems about the model.
Theorem. MC 'mult is a multiplier (implies (and (natp x) (natp y)) (equal (lookup 'z (mc (s 'mult x y) (mclk x))) (* x y))).
This theorem says that a certain program running on the mc machine will correctly multiply any two natural numbers.
It is a statement about an infinite number of test cases!
We know it is true about the model because we proved it.
Of course, models of actual machines usually only accept a finite number of
different inputs. For example, engineers at Advanced Micro Devices (AMD),
Centaur, and IBM have ACL2 models of floating point units that operate on
double precision IEEE floating point numbers. These are finite models. But
the size of their inputs is sufficiently large that they are verified by the
same mathematical methods used to prove theorems about infinite state systems
like our little