MBE

attach code for execution 
Major Section:  ACL2-BUILT-INS

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, in which case 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 started with ``normally'' above because there is an exception: 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.

Note that 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 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.

Some Related Topics

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 "books/arithmetic/top-with-meta")

(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 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, generation of constraints for functional instantiation, and creation of rules of class :rewrite and :forward-chaining also treat mbe calls as their :logic code.