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,
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 using
: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