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 produced 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