Major Section: GUARD
The guard has no effect on the logical axiom added by the definition of a function. It does, however, have consequences for how calls of that function are evaluated in ACL2. We begin by explaining those consequences, when ACL2 is in its default ``mode,'' i.e., as originally brought up. In subsequent discussion we'll consider other ways that guards can interact with evaluation. For more about guards in general, see guard. Also see generalized-booleans for discussion about a subtle issue in the evaluation of certain Common Lisp functions.
Guards and evaluation I: the default
Consider the following very simple definition.
(defun foo (x) (cons 1 (cdr x)))First consider how raw Common Lisp behaves when evaluating calls of this function. To evaluate
(foo x)for some expression
xis evaluated to some value
v, and then
(cons 1 (cdr x))is evaluated with
v. For example, if
(cons 'a 3), then Common Lisp computes
(cons 1 3). But if (for example)
vis a number, e.g.,
7, then there is no way to predict what Common Lisp might do. Some implementations would cause ``sensible'' errors, others might return nonsense, still others might crash the host machine. The results tend toward the catastrophic if the call of
fooin question is in compiled code.
Now by default, ACL2 evaluates calls of
foo exactly as Common
Lisp does, except that it uses guards to check the ``legality'' of
each function call. So for example, since
(cdr x) has a guard
(or (consp x) (equal x nil)), the call
(foo 7) would cause a
``guard violation,'' as illustrated below.
ACL2 !>(foo 7)Thus, the relation between evaluation in ACL2 and evaluation in Common Lisp is that the two produce the very same results, provided there is no guard violation.
ACL2 Error in TOP-LEVEL: The guard for the function symbol CDR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CDR 7).
Guards and evaluation II:
The ACL2 logic is a logic of total functions. That is, every application of a function defined has a completely specified result. See the documentation for each individual primitive for the specification of what it returns when its guard is violated; for example, see cdr.
The presence of guards thus introduces a choice in the sense of
evaluation. When you type a form for evaluation do you mean for
guards to be checked or not? Put another way, do you mean for the
form to be evaluated in Common Lisp (if possible) or in the ACL2
logic? Note: If Common Lisp delivers an answer, it will be the
same as in the logic, but it might be erroneous to execute the form
in Common Lisp. For example, the ACL2 logic definition of
implies that the
cdr of an atom is
nil; see cdr. So:
(cdr 7) cause a guard violation error or return
The top-level ACL2 loop has a variable which controls which sense of
execution is provided. By default, ``guard checking'' is on, by
which we mean that guards are checked at runtime, in the sense
already described. To turn it off, do
To turn ``guard checking'' back on, execute the top-level form
:set-guard-checking t. The status of this variable is reflected
in the prompt; guard-checking is ``on'' when the prompt contains an
exclamation mark (also see default-print-prompt). For example,
ACL2 !>means guard checking is on and
ACL2 >means guard checking is off. The exclamation mark can be thought of as ``barring'' certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example
ACL2 !>(car 'abc)will signal an error, while
ACL2 >(car 'abc)will return
nil. To return to our previous example: with guard checking off,
(foo 7)evaluates to
(cons 1 nil).
Guards and evaluation III: guard verification
Consider the defininition of
foo given above, but modified so
that a reasonable guard of
(consp x) is specified, as shown below.
(defun foo (x) (declare (xargs :guard (consp x))) (cons 1 (cdr x)))We say ``reasonable guard'' above because if
xis such that
(consp x)holds, then the call of
cdrin the evaluation of
(foo x)will not cause a guard violation. Thus, it ``should'' be legal to evaluate
(foo x), for any such
x, simply by evaluating this form in raw Common Lisp.
verify-guards event has been provided for this purpose.
Details may be found elsewhere; see verify-guards. Briefly,
for any defined function
fn, the event
attempts to check the condition discussed above, that whenever
is called on arguments that satisfy its guard, the evaluation of
this call will proceed without any guard violation. (Moreover, the
guard itself should be evaluable without any guard violation.) If
this check is successful, then future calls of this sort will be
evaluated in raw Common Lisp.
Returning to our example above, the
(verify-guards foo) will
succeed because the guard
(consp x) of
foo implies the guard
generated from the call
(cdr x) in the body of the definition,
(or (consp x) (equal x nil)) (see cdr). Then the
(foo (cons 'a 3)) will take place in raw Common
(cons 'a 3) satisfies the guard of
This ability to dive into raw Common Lisp hinges on the proof that the guards you attach to your own functions are sufficient to ensure that the guards encountered in the body are satisfied. This is called ``guard verification.'' Once a function has had its guards verified, then ACL2 can evaluate the function somewhat faster (but see ``Guards and evaluation V: efficiency issues'' below). Perhaps more importantly, ACL2 can also guarantee that the function will be evaluated correctly by any implementation of Common Lisp (provided the guard of the function is satisfied on the input). That is, if you have verified the guards of a system of functions and you have determined that they work as you wish in your host ACL2 (perhaps by proving it, perhaps by testing), then they will work identically in any Common Lisp.
There is a subtlety to our treatment of evaluation of calls of functions whose guards have been verified. If the function's guard is not satisfied by such a call, then no further attempt is made to evaluate any call of that function in raw lisp during the course of evaluation of that call. This is obvious if guard checking is on, because an error is signalled the first time its guard is violated; but in fact it is also true when guard checking is off. See guard-example for an example.
Guards and evaluation IV: functions having :program mode
Strictly speaking, functions in
program mode (see defun-mode)
do not have definitions in the ACL2 logic. So what does it mean to
evaluate calls of such functions in ACL2? Our decision is to treat
program functions much as we treat
logic functions whose guards
have been verified, except that when no error occurs then the
corresponding raw Lisp function is always called. Note that when
the guard of a function in
logic mode is violated, there is still a
value that the ACL2 logic proves is equal to the given call. But
the same cannot be said for a function in
Nevertheless, for the sake of convenience we go ahead and evaluate
the corresponding raw Lisp function except in the situation where
the guard is violated and guard-checking is on.
Thus, as with
logic functions: when a guard has been
satisfied on a call of a function with
program mode, no subsidiary
guard checking will be done.
Notice that by treating functions in
program mode like functions
whose guards have been verified, we are using raw lisp to compute
their values when their guards are met. We do not check guards any
further once raw lisp is invoked. This can lead to hard lisp errors
if the guards are not appropriate, as illustrated below.
ACL2 >:program ACL2 p>(defun foo (x) (declare (xargs :guard t)) (cons 1 (cdr x)))See defun-mode-caveat.
Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.02) FOO ACL2 p>(foo 3)
Error: 3 is not of type LIST. Fast links are on: do (use-fast-links nil) for debugging Error signalled by CDR. Broken at COND. Type :H for Help. ACL2>>
However, here is a way to get ACL2 to do run-time guard checking for
program mode functions. With this method, ACL2 will
evaluate calls of user-defined
:program mode functions in a manner
that follows their ACL2 definitions. Simply execute the following in the
ACL2 loop to put ACL2 into a ``safe mode.''
(f-put-global 'safe-mode t state)Let us revisit the example above, using safe mode. Notice that the guard of
cdris now being checked, because the executable counterpart of
foois being called even though the guard is
ACL2 !>(f-put-global 'safe-mode t state) <state> ACL2 !>:program ACL2 p!>(defun foo (x) (declare (xargs :guard t)) (cons 1 (cdr x)))If we go back into ``unsafe'' mode, then we once again see a raw Lisp error, as we now illustrate.
Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 p!>(foo 3)
ACL2 Error in TOP-LEVEL: The guard for the function symbol CDR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CDR 3). You may be able to see a trace of calls leading up to this violation by executing (wet <form>), where <form> is the form you submitted to the ACL2 loop. See :DOC wet for how to get an error backtrace.
ACL2 p!>(wet (foo 3))
ACL2 Error in WITH-ERROR-TRACE: The guard for the function symbol CDR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CDR 3). (Backtrace is below.)
1> (ACL2_*1*_ACL2::FOO 3)
ACL2 p!>(f-put-global 'safe-mode nil state) <state> ACL2 p!>(foo 3)
Error: 3 is not of type LIST. Fast links are on: do (si::use-fast-links nil) for debugging Error signalled by CDR. Broken at COND. Type :H for Help. ACL2>>
Guards and evaluation V: efficiency issues
We have seen that by verifying the guards for a
logic function, we
arrange that raw lisp is used for evaluation of calls of such
functions when the arguments satisfy its guard.
This has several apparent advantages over the checking of guards as
we go. First, the savings is magnified as your system of functions
gets deeper: the guard is checked upon the top-level entry to your
system and then raw Common Lisp does all the computing. Second, if
the raw Common Lisp is compiled, enormous speed-ups are possible.
Third, if your Common Lisp or its compiler does such optimizations
tail-recursion removal, raw Common Lisp may be able to
compute your functions on input much ``bigger'' than ACL2 can.
The first of these advantages is quite important if you have complicated guards. However, the other two advantages are probably not very important, as we now explain.
When a function is defined in
logic mode, its
executed in raw Common Lisp. (We might call this the ``primary''
raw lisp definition of the function.) However, a corresponding
``logic definition'' is also executed. The ``logic definition'' is
defun in raw lisp that checks guards at runtime and escapes to
the primary raw lisp definition if the guard holds of the arguments
and the function has already had its guards verified. Otherwise the
logic definition executes the body of the function by calling the
logic definitions of each subroutine. Now it is true that
compilation generally speeds up execution enormously. However, the
comp command (see comp) compiles both of the raw lisp
definitions associated with a
logic function. Also, we have
attempted to arrange that for every tail recursion removal done on
defun, a corresonding tail recursion removal is done
on the ``logic definition.''
We believe that in most cases, the logic definition executes almost as fast as the primary raw lisp definition, at least if the evaluation of the guards is fast. So, the main advantage of guard verification is probably that it lets you know that the function may be executed safely in raw lisp, returning the value predicted by the ACL2 logic, whenever its arguments satisfy its guard. We envision the development of systems of applicative lisp functions that have been developed and reasoned about using ACL2 but which are intended for evaluation in raw Common Lisp (perhaps with only a small ``core'' of ACL2 loaded), so this advantage of guard verification is important.
Nevertheless, guard verification might be important for optimal
efficiency when the functions make use of type declarations. For
example, at this writing, the GCL implementation of Common Lisp can
often take great advantage of
declare forms that assign small
integer types to formal parameters.
To continue the discussion of guards,
see guards-for-specification to read about the use of guards as
a specification device.