Miscellaneous remarks about guards
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
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
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
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)
will generate the guard
(declare (type string x) (xargs :guard (foo x))
will generate the guard