MBT

introduce a test not to be evaluated
Major Section:  PROGRAMMING

The macro mbt (``must be true'') can be used in order to add code in order to admit function definitions in :logic mode, without paying a cost in execution efficiency. Examples below illustrate its intended use.

Semantically, (mbt x) equals x. However, in raw Lisp (mbt x) ignores x entirely, and macroexpands to t. ACL2's guard verification mechanism ensures that the raw Lisp code is only evaluated when appropriate, since a guard proof obligation (equal x t) is generated. See verify-guards and, for general discussion of guards, see guard.

Also see mbe, which stands for ``must be equal.'' Although mbt is more natural in many cases, mbe has more general applicability. In fact, (mbt x) is essentially defined to be (mbe :logic x :exec t).

We can illustrate the use of mbt on the following generic example, where <g>, <test>, <rec-x>, and <base> are intended to be terms involving only the variable x.

(defun foo (x)
  (declare (xargs :guard <g>))
  (if <test>
      (foo <rec-x>)
    <base>))
In order to admit this function, ACL2 needs to discharge the proof obligation that <rec-x> is smaller than x, namely:
(implies <test>
         (o< (acl2-count <rec-x>)
              (acl2-count x)))
But suppose we need to know that <g> is true in order to prove this. Since <g> is only the guard, it is not part of the logical definition of foo. A solution is to add the guard to the definition of foo, as follows.
(defun foo (x)
  (declare (xargs :guard <g>))
  (if (mbt <g>)
      (if <test>
          (foo <rec-x>)
        <base>)
    nil))
If we do this using <g> rather than (mbt <g>), then evaluation of every recursive call of foo will cause the evaluation of (the appropriate instance of) <g>. But since (mbt <g>) expands to t in raw Lisp, then once we verify the guards of foo, the evaluations of <g> will be avoided (except at the top level, when we check the guard before allowing evaluation to take place in Common Lisp).

Other times, the guard isn't the issue, but rather, the problem is that a recursive call has an argument that itself is a recursive call. For example, suppose that <rec-x> is of the form (foo <expr>). There is no way we can hope to discharge the termination proof obligation shown above. A standard solution is to add some version of this test:

(mbt (o< (acl2-count <rec-x>) (acl2-count x)))
Here is a specific example based on one sent by Vernon Austel.
(defun recurX2 (n)
  (declare (xargs :guard (and (integerp n) (<= 0 n))
                  :verify-guards nil))
  (cond ((zp n) 0)
        (t (let ((call (recurX2 (1- n))))
             (if (mbt (< (acl2-count call) n))
                 (recurX2 call)
               1 ;; this branch is never actually taken
               )))))

(defthm recurX2-0 (equal (recurX2 n) 0))

(verify-guards recurX2)

If you (trace$ acl2-count), you will see that evaluation of (recurX2 2) causes several calls of acl2-count before the verify-guards. But this evaluation does not call acl2-count after the verify-guards, because the ACL2 evaluation mechanism uses raw Lisp to do the evaluation, and the form (mbt (< (acl2-count call) n)) macroexpands to t in Common Lisp.

You may occasionally get warnings when you compile functions defined using mbt. (For commands that invoke the compiler, see comp and see certify-book.) 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 t)))
  (and (mbt x) y))