MBE

attach code for execution 
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")


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

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.