Mbe
Attach code for execution
The macro mbe (``must be equal'') can be used in function
definitions in order to cause evaluation to use alternate code to that
provided for the logic. An example is given below. However, the use of
mbe can lead to non-terminating computations. See defexec,
perhaps after reading the present documentation, for a way to prove
termination.
In the ACL2 logic, (mbe :exec exec-code :logic logic-code) equals
logic-code; the value of exec-code is ignored. However, in raw Lisp
it is the other way around: this form macroexpands simply to exec-code.
ACL2's guard verification mechanism ensures that the raw Lisp code is
only evaluated when appropriate, since the guard proof obligations generated
for (the macroexpansion of) this call of mbe include not only the guard
proof obligations from exec-code, but also, under suitable contextual
assumptions, the term (equal exec-code logic-code). See verify-guards (in particular, for discussion of the contextual assumptions
from the :guard and if-tests) and, for general discussion of
guards, see guard.
Normally, during evaluation of an mbe call, only the :logic code
is evaluated unless the call is in the body of a guard-verified
function or under a call of a :program mode function; in those
cases only the :exec code is evaluated. This implies that equality of
:exec and :logic code is never checked at runtime. (Rather, such
equality is proved when verifying guards.) We qualified with ``normally''
above because there are two exceptions. During a ``safe mode'', which is used
in macroexpansion and evaluation of defconst forms, the :logic
and :exec code are both evaluated and their equality is checked. Second,
when guard-checking is set to :all or :none, then for any mbe
call in the body of a :logic mode definition, only the :logic code
will be evaluated.
Note that the :exec and the :logic code in an mbe call must
have the same output signature. For example, one cannot return (mv * *) while the other returns just a single value.
Also see mbt, which stands for ``must be true.'' You may find it
more natural to use mbt for certain applications, as described in its
documentation.
Here is an example of the use of mbe. Suppose that you want to define
factorial in the usual recursive manner, as follows.
(defun fact (n)
(if (zp n)
1
(* n (fact (1- n)))))
But perhaps you want to be able to execute calls of fact on large
arguments that cause stack overflows, perhaps during proofs. (This isn't a
particularly realistic example, but it should serve.) So, instead you can
define this tail-recursive version of factorial:
(defun fact1 (n acc)
(declare (xargs :guard (and (integerp n) (>= n 0) (integerp acc))))
(if (zp n)
acc
(fact1 (1- n) (* n acc))))
We are now ready to define fact using mbe. Our intention is that
logically, fact is as shown in the first definition above, but that
fact should be executed by calling fact1. Notice that we defer
guard verification, since we are not ready to prove the correspondence
between fact1 and fact.
(defun fact (n)
(declare (xargs :guard (and (integerp n) (>= n 0))
:verify-guards nil))
(mbe :exec (fact1 n 1)
:logic (if (zp n)
1
(* n (fact (1- n))))))
Next, we prove the necessary correspondence lemmas. Notice the inclusion
of a community book to help with the arithmetic reasoning.
(include-book "arithmetic/top-with-meta" :dir :system)
(defthm fact1-fact
(implies (integerp acc)
(equal (fact1 n acc)
(* acc (fact n)))))
We may now do guard verification for fact, which will allow the
execution of the raw Lisp fact function, where the above mbe call
expands simply to (fact1 n 1).
(verify-guards fact)
Now that guards have been verified, a trace of function calls illustrates
that the evaluation of calls of fact is passed to evaluation of calls of
fact1. The outermost call below is of the logical function stored for
the definition of fact; all the others are of actual raw Common Lisp
functions.
ACL2 !>(trace$ fact fact1)
NIL
ACL2 !>(fact 3)
1> (ACL2_*1*_ACL2::FACT 3)
2> (FACT 3)
3> (FACT1 3 1)
4> (FACT1 2 3)
5> (FACT1 1 6)
6> (FACT1 0 6)
<6 (FACT1 6)
<5 (FACT1 6)
<4 (FACT1 6)
<3 (FACT1 6)
<2 (FACT 6)
<1 (ACL2_*1*_ACL2::FACT 6)
6
ACL2 !>
You may occasionally get warnings when you compile functions defined using
mbe. (For commands that invoke the compiler, see compilation.)
These can be inhibited by using an ignorable declare form. Here
is a simple but illustrative example. Note that the declarations can
optionally be separated into two declare forms.
(defun foo (x y)
(declare (ignorable x)
(xargs :guard (equal x y)))
(mbe :logic x :exec y))
Finally, we observe that when the body of a function contains a term of the
form (mbe :exec exec-code :logic logic-code), the user would be unlikely
to notice any difference in the theorem prover if this term were replaced by
logic-code. ACL2 takes various steps to ensure this. For example, the
proof obligations generated for admitting a function treat the above mbe
term simply as logic-code. Function expansion, :use hints,
:definition rules, generation of constraints for
functional instantiation, and creation of rules of class :rewrite
and :forward-chaining also treat mbe calls as their
:logic code.
Subtopics
- Mbt
- Introduce a test into the logic that, however, evaluates to t
- Defexec
- Attach a terminating executable function to a definition
- Must-be-equal
- Attach code for execution
- Mbt*
- Introduce a guard proof obligation
- Mbe1
- Attach code for execution
