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 mc.