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 x, first
x is evaluated to some value v, and then (cons 1 (cdr x)) is
evaluated with x bound to v. For example, if v is (cons 'a 3), then
Common Lisp computes (cons 1 3). But if (for example) v is 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 foo in 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
of (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).
ACL2 !>
Guards and evaluation II: :set-guard-checking.
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 cdr
implies that the cdr of an atom is nil; see cdr. So:
should (cdr 7) cause a guard violation error or return nil?
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 :set-guard-checking nil.
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
x is such that
(consp x) holds, then the call of cdr in 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.
The 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 (verify-guards fn)
attempts to check the condition discussed above, that whenever fn
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,
namely, (or (consp x) (equal x nil)) (see cdr). Then the
evaluation of (foo (cons 'a 3)) will take place in raw Common
Lisp, because (cons 'a 3) satisfies the guard of foo.
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 :program mode.
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)))
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>>
See defun-mode-caveat.
However, here is a way to get ACL2 to do run-time guard checking for
user-defined :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
cdr is now being checked, because the executable counterpart of foo
is being called even though the guard is t.
ACL2 !>(f-put-global 'safe-mode t state)
<state>
ACL2 !>:program
ACL2 p!>(defun foo (x)
(declare (xargs :guard t))
(cons 1 (cdr x)))
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!>
If we go back into ``unsafe'' mode, then we once again see a raw Lisp error,
as we now illustrate.
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
as 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 defun is
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
a 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
the actual 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.