Major Section: EVENTS
See guard for a general discussion of guards.
Before discussing the
verify-guards event, we first discuss guard
verification, which can take place at definition time or, later, using
verify-guards. Typically, guard verification takes place at definition
time if a guard (or type, or stobjs) has been supplied explicitly unless
:verify-guards nil has been specified; see defun and see xargs, and
see set-verify-guards-eagerness for how to change this default. The point
of guard verification is to ensure that during evaluation of an expression
without free variables, no guard violation takes place.
Technical note: the first argument of
verify-guards must be a function
symbol or the name of a
defaxiom event, not a
macro-alias for a function symbol (see macro-aliases-table).
See verify-guards+ for a utility that does not have this restriction.
Guard verification is intended to guarantee that for any call of a given function, if its guard holds for that call then the guard will hold for every function call in the body of that function. Moreover, in order to avoid guard violations during evaluation of the function's guard itself, guard verification also is intended to guarantee that the guards are satisfied for all calls in the guard itself. Consider the following simple example.
(defun f (x) (declare (xargs :guard (and (consp x) (integerp (car x))))) (if (rationalp (cdr x)) (+ (car x) (cdr x)) 17))If you evaluate
(f t), for example, in the top-level loop, you will (by default) get a guard error. The point of guard verification is to guarantee the absence of guard errors, and we start by using this example to illustrate the proof obligations that guarantee such absence.
The body of the above definition has the following function calls, where the first is the entire body.
(if (rationalp (cdr x)) (< (car x) (cdr x)) 17) (rationalp (cdr x)) ; the test of the top-level IF call (cdr x) ; from (rationalp (cdr x)) (< (car x) (cdr x)) ; the true branch of the top-level IF call (car x) ; from (< (car x) (cdr x)) (cdr x) ; from (< (car x) (cdr x))We thus see potentially six conditions to prove, one for each call. The guards of the function symbols of those calls are
(or (consp x) (equal x nil))for both
(cdr x), and finally that both arguments are rationals for
<. Moreover, we can take advantage of ``contextual assumptions'': the
if-test conditions and the top-level
:guard. Thus, for
verify-guardsthe proof obligation from the body of
fis as follows.
(implies (and (consp x) (integerp (car x))) ; from the :guard (and t ; from the top-level IF call t ; from (rationalp (cdr x)) (or (consp x) (equal x nil)) ; from the first (cdr x) (implies (rationalp (cdr x)) ; IF-test for calls in the true branch (and (or (consp x) (equal x nil)) ; from (car x) (or (consp x) (equal x nil)) ; from the second (cdr x) (and (rationalp (car x)) (rationalp (cdr x))) ; from the < call ))))But the
:guarditself generates a similar sort of proof obligation. Note that the guard
(and (consp x) (integerp (car x)))is really an abbreviation (i.e. via the macro
AND) for the term
(if (consp x) (integerp (car x)) nil). The guard proof obligation for the guard itself is thus as follows.
(and t ; from (consp x) (implies (consp x) (and t ; from (integerp (car x)) ; (consp x) ; from (car x) ; )))All of the above proof obligations are indeed theorems, and guard verification succeeds for the above definition of
The example above illustrates the general procedure for generating the guard
proof obligation. Each function call is considered in the body or guard of
the function, and it is required that the guard is met for that call, under
certain ``contextual assumptions'', which are as follows. In the case of the
body of the named function, it is assumed that the guard holds for that
function on its formal parameters. And in both cases -- the body of the
named function and also its guard -- the governing tests from superior
IF are also assumed.
As mentioned above, if the guard on a function is not
t, then guard
verification requires not only consideration of the body under the assumption
that the guard is true, but also consideration of the guard itself. Thus,
for example, guard verification fails in the following example, even though
there are no proof obligations arising from the body, because the guard
itself can cause a guard violation when evaluated for an arbitrary value of
(defun foo (x) (declare (xargs :guard (car x))) x)
We turn now to the
verify-guards event as a way of verifying the
guards for a function or theorem.
Examples: (verify-guards flatten) (verify-guards flatten :hints (("Goal" :use (:instance assoc-of-app))) :otf-flg t :guard-debug t ; default = nil :doc "string") General Form: (verify-guards name :hints hints :otf-flg otf-flg :guard-debug t ; typically t, but any value is legal :doc doc-string)In the General Form above,
nameis the name of a
logicfunction (see defun-mode) or of a theorem or axiom. In the most common case
nameis the name of a function that has not yet had its guards verified, each subroutine of which has had its guards verified. The values
guard-debugare as described in the corresponding documentation entries; and
doc-string, if supplied, is a string not beginning with ``
:Doc-Section''. The four keyword arguments above are all optional. To admit this event, the conjunction of the guard proof obligations must be proved. If that proof is successful,
nameis considered to have had its guards verified.
See verify-guards-formula for a utility that lets you view the formula to be
verify-guards, but without creating an event.
name is one of several functions in a mutually recursive clique,
verify-guards will attempt to verify the guards of all of the
name is a theorem or axiom name,
verify-guards verifies the
guards of the associated formula. When a theorem has had its guards
verified then you know that the theorem will evaluate to non-
in all Common Lisps, without causing a runtime error (other than possibly
a resource error). In particular, you know that the theorem's validity
does not depend upon ACL2's arbitrary completion of the domains of partial
Common Lisp functions.
For example, if
app is defined as
(defun app (x y) (declare (xargs :guard (true-listp x))) (if (endp x) y (cons (car x) (app (cdr x) y))))then we can verify the guards of
appand we can prove the theorem:
(defthm assoc-of-app (equal (app (app a b) c) (app a (app b c))))However, if you go into almost any Common Lisp in which
appis defined as shown and evaluate
(equal (app (app 1 2) 3) (app 1 (app 2 3)))we get an error or, perhaps, something worse like
nil! How can this happen since the formula is an instance of a theorem? It is supposed to be true!
It happens because the theorem exploits the fact that ACL2 has completed
the domains of the partially defined Common Lisp functions like
cdr, defining them to be
nil on all non-conses. The formula
above violates the guards on
app. It is therefore ``unreasonable''
to expect it to be valid in Common Lisp.
But the following formula is valid in Common Lisp:
(if (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))) t)That is, no matter what the values of
cthe formula above evaluates to
tin all Common Lisps (unless the Lisp engine runs out of memory or stack computing it). Furthermore the above formula is a theorem:
(defthm guarded-assoc-of-app (if (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))) t))This formula,
guarded-assoc-of-app, is very easy to prove from
assoc-of-app. So why prove it? The interesting thing about
guarded-assoc-of-appis that we can verify the guards of the formula. That is,
(verify-guards guarded-assoc-of-app)succeeds. Note that it has to prove that if
bare true lists then so is
(app a b)to establish that the guard on the outermost
appon the left is satisfied. By verifying the guards of the theorem we know it will evaluate to true in all Common Lisps. Put another way, we know that the validity of the formula does not depend on ACL2's completion of the partial functions or that the formula is ``well-typed.''
One last complication: The careful reader might have thought we could
(implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))))rather than using the
ifform of the theorem. We cannot! The reason is technical:
impliesis defined as a function in ACL2. When it is called, both arguments are evaluated and then the obvious truth table is checked. That is,
impliesis not ``lazy.'' Hence, when we write the guarded theorem in the
impliesform we have to prove the guards on the conclusion without knowing that the hypothesis is true. It would have been better had we defined
impliesas a macro that expanded to the
ifform, making it lazy. But we did not and after we introduced guards we did not want to make such a basic change.
Recall however that
verify-guards is almost always used to verify
the guards on a function definition rather than a theorem. We now
return to that discussion.
name is not uniquely associated with the
(it necessarily names a previously defined function) the
doc-string, is not stored in the
documentation database. Thus, we actually prohibit
from having the form of an ACL2 documentation string;
Verify-guards must often be used when the value of a recursive call
of a defined function is given as an argument to a subroutine that
is guarded. An example of such a situation is given below. Suppose
app (read ``append'') has a guard requiring its first argument to be
(defun rev (x) (declare (xargs :guard (true-listp x))) (cond ((endp x) nil) (t (app (rev (cdr x)) (list (car x))))))Observe that the value of a recursive call of
revis being passed into a guarded subroutine,
app. In order to verify the guards of this definition we must show that
(rev (cdr x))produces a
true-listp, since that is what the guard of
apprequires. How do we know that
(rev (cdr x))is a
true-listp? The most elegant argument is a two-step one, appealing to the following two lemmas: (1) When
(cdr x)is a
true-listp. (2) When
(rev z)is a
true-listp. But the second lemma is a generalized property of
rev, the function we are defining. This property could not be stated before
revis defined and so is not known to the theorem prover when
Therefore, we might break the admission of
rev into three steps:
rev without addressing its guard verification, prove some
general properties about
rev, and then verify the guards. This can
be done as follows:
(defun rev (x) (declare (xargs :guard (true-listp x) :verify-guards nil)) ; Note this additional xarg. (cond ((endp x) nil) (t (app (rev (cdr x)) (list (car x)))))) (defthm true-listp-rev (implies (true-listp x2) (true-listp (rev x2)))) (verify-guards rev)The ACL2 system can actually admit the original definition of
rev, verifying the guards as part of the
defunevent. The reason is that, in this particular case, the system's heuristics just happen to hit upon the lemma
true-listp-rev. But in many more complicated functions it is necessary for the user to formulate the inductively provable properties before guard verification is attempted.
Remark on computation of guard conjectures and evaluation. When ACL2
computes the guard conjecture for the body of a function, it
evaluates any ground subexpressions (those with no free variables), for
calls of functions whose
executable-counterpart runes are
enabled. Note that here, ``enabled'' refers to the current global
theory, not to any
hints given to the guard verification
process; after all, the guard conjecture is computed even before its initial
goal is produced. Also note that this evaluation is done in an environment
:set-guard-checking :all had been executed, so that we can
trust that this evaluation takes place without guard violations;
If you want to verify the guards on functions that are built into ACL2,
you will first need to put them into
See verify-termination, specifically the ``Remark on system functions'' in