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,
verify-guards, and (for a discussion of
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
xarg of the
defun or else defaults to the default defun-mode.
See default-defun-mode. If the defun-mode of the
logic and either a guard is specified explicitly or
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
:verify-guards nil then to state and prove key theorems about the
function, and only then have the system attempt guard verification.
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.
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
in order of appearance. So for example, the
(declare (xargs :guard (foo x)) (type string x)will generate the guard
(and (foo x) (stringp x)), while the form
(declare (type string x) (xargs :guard (foo x))will generate the guard
(and (stringp x) (foo x)). The only exception to this rule is the case that
:stobjsare specified in the same
xargsform, in which case the
:stobjsform will be treated as through it comes before the