Major Section: PROGRAMMING

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 guarantee termination (at least theoretically).

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 this call of `mbe`

are `(equal exec-code logic-code)`

together with
the proof obligations from `exec-code`

. See verify-guards and, for general
discussion of guards, see guard.

The form `(mbe :exec exec-code :logic logic-code)`

expands in the logic to
the function call `(`

`must-be-equal`

` logic-code exec-code)`

. The guard for
`(must-be-equal logic exec)`

is `(equal logic exec)`

. We recommend that
you use `mbe`

instead of `must-be-equal`

because the use of keywords
eliminates errors caused by unintentially reversing the order of arguments.
The `:exec`

and the `:logic`

code in an `mbe`

call must have the same
return type; for example, one cannot return `(`

`mv`

` * *)`

while the
other returns just a single value. Also, the `:exec`

code may not itself
contain any calls of `mbe`

(or `must-be-equal`

).

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 standard book to help with the arithmetic reasoning.

(include-book "books/arithmetic/top-with-meta")We may now do guard verification for(defthm fact1-fact (implies (integerp acc) (equal (fact1 n acc) (* acc (fact n)))))

`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 !>

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 is very unlikely
to see any logical difference than if this 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, and generation of constraints for
functional instantiation also treat the above `mbe`

call as if were
replaced by `logic-code`

.