		Search-engine friendly clone of the ACL2 documentation.

Guard

Guards-and-evaluation

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.

(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)

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: :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 allow execution to proceed in the logic when there is a guard violation, do :set-guard-checking nil; or evaluate :set-guard-checking :none to skip guard checking entirely. To turn ``guard checking'' back on, execute the top-level form :set-guard-checking t. The status of guard checking 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). Also see set-guard-checking.

Guards and evaluation III: guard verification

Consider the definition 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 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 :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? In general we 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. (We say ``in general'' because there are exceptions, discussed in the ``Aside'' just below.) 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, aside from the following:

Aside. There are exceptions to the use of raw Lisp, discussed just above, to evaluate calls of :program mode functions. The primary one is that after :set-guard-checking :none, evaluation of user-defined :program mode function calls is done in the ACL2 logic, not in raw Lisp. The more obscure exception is that during expansion of macros and make-event forms, and during evaluation of defconst forms, ACL2 enters a ``safe mode'' in which this escape to raw Lisp is prevented. The following example illustrates how the user can experiment directly with safe mode, though it is preferred to use :set-guard-checking :none if you are happy to skip all guard checking and evaluate forms in the logic.

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.
[1] 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.
[1] ACL2(2):

The other exception occurs after set-guard-checking can be called with a value of :all; see set-guard-checking. End of aside.

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).  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 :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 (see compilation), 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 call this the ``submitted'' definition of the function. However, a corresponding executable-counterpart also executed. (See evaluation for an introduction to submitted and executable-counterpart definitions.) The executable-counterpart is a defun in raw lisp that checks guards at runtime and escapes to the submitted definition if the guard holds of the arguments and the function has already had its guards verified. Otherwise the executable-counterpart evaluates the body of the function by calling the executable-counterpart of each subroutine. Now it is true that compilation often speeds up execution significantly. However, the :comp command (see comp) compiles both of the raw lisp definitions associated with a function. Also, we have attempted to arrange that for every tail recursion removal done on the actual defun, a corresponding tail recursion removal is done on the executable-counterpart definition.

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 :split-types keyword.

To continue the discussion of guards, see guards-for-specification to read about the use of guards as a specification device.