GUARD-MISCELLANY

Major Section:  GUARD

The discussion of guards concludes here with a few miscellaneous remarks. (Presumably you found this documentation by following a link; see guards-for-specification.) For further information related to guards other than what you find under ``guard,'' see any of the following documentation topics: guard-example, set-verify-guards-eagerness, set-guard-checking, verify-guards, and (for a discussion of keyword :SPLIT-TYPES) xargs.

Defun can be made to try to verify the guards on a function. This is controlled by the ``defun-mode'' of the defun; see defun-mode. The defun-mode is either as specified with the :mode xarg of the defun or else defaults to the default defun-mode. See default-defun-mode. If the defun-mode of the defun is :logic and either a guard is specified explicitly or :verify-guards t is specified in the xargs, then we attempt to verify the guards of the function. Otherwise we do not. (But see set-verify-guards-eagerness for how to modify this behavior.)

It is sometimes impossible for the system to verify the guards of a recursive function at definition time. For example, the guard conjectures might require the invention and proof of some inductively derived property of the function (as often happens when the value of a recursive call is fed to a guarded subroutine). So sometimes it is necessary to define the function using :verify-guards nil then to state and prove key theorems about the function, and only then have the system attempt guard verification. Post-defun guard verification is achieved via the event verify-guards. See verify-guards.

It should be emphasized that guard verification affects only two things: how fast ACL2 can evaluate the function and whether the function is executed correctly by raw Common Lisp, without guard violations. Since ACL2 does not use the raw Common Lisp definition of a function to evaluate its calls unless that function's guards have been verified, the latter effect is felt only if you run functions in raw Common Lisp rather than via ACL2's command loop.

Guard verification does not otherwise affect the theorem prover or the semantics of a definition. If you are not planning on running your function on ``big'' inputs and you don't care if your function runs correctly in raw Common Lisp (e.g., you have formalized some abstract mathematical property and just happened to use ACL2 as your language), there is no need to suffer through guard verification. Often users start by not doing guard verification and address that problem later. Sometimes you are driven to it, even in mathematical projects, because you find that you want to run your functions particularly fast or in raw Common Lisp.

If certify-book is used to compile a file, and the file contains functions with unverified guard conjectures, then you will be warned that the compiled file cannot be loaded into raw Common Lisp with the expectation that the functions will run correctly. This is just the same point we have been making: ACL2 and Common Lisp agree only on the restricted domains specified by our guards. When guards are violated, Common Lisp can do anything. When you call a compiled function on arguments violating its guards, the chances are only increased that Common Lisp will go berserk, because compiled functions generally check fewer things at runtime and tend to be more fragile than interpreted ones.

Finally, we note that ACL2 collects up guards from declare forms in order of appearance. So for example, the declare form

(declare (xargs :guard (foo x))
         (type string x)

(declare (type string x)
         (xargs :guard (foo x))