The relationship between guards and evaluation
For relevant background see evaluation.
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. For in-depth discussion of the interaction between the defun-mode and guard checking, see set-guard-checking, see guard-evaluation-table, see guard-evaluation-examples-script, and see guard-evaluation-examples-log. 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.
First consider how raw Common Lisp behaves when evaluating calls of this
function. To evaluate
Now by default, ACL2 evaluates calls of
ACL2 !>(foo 7) 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 !>
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.
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 cdr
implies that the cdr of an atom is
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 allow
execution to proceed in the logic when there is a guard violation, do
means guard checking is on and
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)
Guards and evaluation III: guard verification
Consider the definition of
We say ``reasonable guard'' above because if
The verify-guards event has been provided for this purpose.
Details may be found elsewhere; see verify-guards. Briefly, for any
Returning to our example above, the
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 signaled 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
Aside. There are exceptions to the use of raw Lisp, discussed just
above, to evaluate calls of
ACL2 !>(defun foo (x) (declare (xargs :mode :program :guard t)) (car x)) Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(foo 3) Error: Attempt to take the car of 3 which is not listp. [condition type: SIMPLE-ERROR] Restart actions (select using :continue): 0: Return to Top Level (an "abort" restart). 1: Abort entirely from this process.  ACL2(2): :pop ACL2 !>(assign safe-mode t) T ACL2 !>(foo 3) ACL2 Error in TOP-LEVEL: The guard for the function symbol CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). See :DOC trace for a useful debugging utility. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>(assign safe-mode nil) NIL ACL2 !>(foo 3) Error: Attempt to take the car of 3 which is not listp. [condition type: SIMPLE-ERROR] Restart actions (select using :continue): 0: Return to Top Level (an "abort" restart). 1: Abort entirely from this process.  ACL2(2):
Notice that by treating functions in
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>>
However, here is a way to get ACL2 to do run-time guard checking for
(f-put-global 'safe-mode t state)
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). See :DOC trace for a useful debugging utility. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. 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
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 (see
compilation), enormous speed-ups are possible. Third, if your Common
Lisp or its compiler does such optimizations as
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
We believe that in most cases, the executable-counterpart executes almost as fast as the submitted 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 submitted 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.
Note that while type declarations contributed to the guard by default, they
can be proved from the guard instead; see xargs for a discussion of the
To continue the discussion of guards, see guards-for-specification to read about the use of guards as a specification device.