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