GUARDS-AND-EVALUATION

the relationship between guards and evaluation
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)

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 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.