		Search-engine friendly clone of the ACL2 documentation.

Program-wrapper

Avoiding expensive guard checks using program-mode functions

Application programs can benefit from avoiding expensive guard checks. Imagine that expensive-guard-fn is a function whose calls may be slow to evaluate, and that expensive-fn is a function whose guard calls expensive-guard-fn. So, when you call expensive-fn at the top level, whether directly in the ACL2 read-eval-print loop or during make-event expansion, the guard check may be slow. If you are confident that the guard check will pass, you may thus prefer to avoid it.

The following contrived example shows how to avoid that guard check by using a program-mode wrapper: a function in program mode that calls the intended function directly. The example below illustrates that idea by defining expensive-fn-wrapper as a program-mode wrapper for expensive-fn. That wrapper has a computationally inexpensive guard, typically t, which avoids any expensive guard check: after the inexpensive guard check, the remaining computation takes place using raw Lisp computation, which doesn't do any guard checking. (See evaluation for relevant background.)

(defun fib (n) ; Fibonacci function, just for an example of slow computation
  (declare (xargs :guard (natp n)))
  (if (zp n)
      0
    (if (eql n 1)
        1
      (+ (fib (- n 1))
         (fib (- n 2))))))

(defun expensive-guard-fn (n)
  (declare (xargs :guard t))
  (and (natp n)
       (natp (fib n))))

(defun expensive-fn (n)
  (declare (xargs :guard (expensive-guard-fn n)))
  (* 2 n))

; The following may take about a second, virtually all in the guard check.
(time$ (expensive-fn 40))

(defun expensive-fn-wrapper (n)
  (declare (xargs :mode :program))
  (expensive-fn n))

; The following is virtually instantaneous.
(time$ (expensive-fn-wrapper 40))

This trick isn't necessary if your function call is made on behalf of a superior call of a function that is guard-verified (or in program mode, since that essentially brings us back to the wrapper situation). Consider the following definition, building on the example above.

(defun f (n)
  (declare (xargs :guard (natp n)))
  (expensive-fn n))

; The following is virtually instantaneous.
(time$ (f 40))

Then evaluation of (f 40) is virtually instantaneous, for the same reason that evaluation of (expensive-fn-wrapper 40) is virtually instantaneous: after the top-level guard check passes, the rest of the computation takes place without guard checks. Note however that if we change the definition by removing guard verification, then the trick is once again helpful, as shown by continuing the examples above.

; Define a logic-mode function that is not guard-verified:
(defun g (n)
  (expensive-fn n))

; The following may take about a second, virtually all in the guard check.
(time$ (g 40))

Remark. This trick may be less effective if you see an "Invariant-risk" warning, which prevents computation from taking place within raw Lisp, thus avoiding guard checks; see invariant-risk.