Verify-guards
Verify the guards of a function
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 Notes: (1) The first argument of verify-guards must be a
function symbol, the name of a defthm or defaxiom event, a
lambda$ expression, or an unquoted well-formed LAMBDA object; it
must not be a macro-alias for a function symbol (see macro-aliases-table). See verify-guards+ for a utility that does not
have this restriction. (2) When the guards of a defined function, fn,
are verified, verify-guards also includes the guards of all the functions
that are mutually recursive with fn, if any, plus the guards of all the
quoted well-formed LAMBDA objects used by fn or any function in its
mutually-recursive clique. Guard obligations for lambda$ and LAMBDA
objects are not included when the first argument is the name of a
theorem or axiom. Details are discussed further below.
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 t for if and
rationalp, (or (consp x) (equal x nil)) for both (car x) and
(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-guards the proof obligation from the body of f is 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 :guard itself 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 f.
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
calls of if are also assumed. (However, additional conjectures are
generated for loop$ statements. See the section Special Guard
Conjectures for LOOP$ in the documentation for loop$.)
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 x:
(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)))
:guard-debug t ; default = nil
:guard-simplify :limited ; default = t
:otf-flg t)
(verify-guards (lambda$ (x)
(declare (xargs :guard (natp x)))
(+ 1 x)))
(verify-guards
(LAMBDA (X)
(DECLARE (XARGS :GUARD (NATP X) :SPLIT-TYPES T))
(RETURN-LAST 'PROGN
'(LAMBDA$ (X)
(DECLARE (XARGS :GUARD (NATP X)))
(+ 1 X))
(BINARY-+ '1 X))))
General Form:
(verify-guards name
:hints hints
:guard-debug gdbg ; default generally nil; any value is legal
:guard-simplify gsmp ; default generally t; may be set to :limited
:otf-flg otf-flg)
In the General Form above, name may be the name of a :logic mode function (see defun-mode). In that case, the first three
keywords may default to values in an existing definition as discussed below.
Otherwise, name is the name of a theorem or axiom, or it is a lambda$ expression or a well-formed LAMBDA object (not quoted).
Mixed-mode-functions cannot be guard verified.
In the most common case name is the name of a function that has not
yet had its guards verified, each subroutine of which has had its guards verified. The values hints, otf-flg, and guard-debug are as described in the corresponding documentation
entries, but hints and guard-debug can be taken from the existing
definition of name; we return to that point later. The keyword arguments
above are all optional. To admit this event, the conjunction of the guard
proof obligations must be proved. If all the guard obligations are proved,
name is considered to have had its guards verified. The
:guard-simplify option controls certain simplifications that may be
applied to the guard conjecture while generating the initial goal: its default
is t, which doesn't restrict such simplification, and the other legal
value is :limited, which skips all simplifications that depend on the set
of currently enabled rules; but as with hints and
guard-debug, the value can be taken from the existing definition of
name, as described further below. See also guard-simplification.
If name is a lambda$ expression it is translated (to a quoted
well-formed LAMBDA object), the formals, declaration, and body are
extracted, and verify-guards behaves as though name were the name of
some defined function with those formals, declaration, and body. If name
is a LAMBDA object, it is checked for well-formedness (see well-formed-lambda-objectp), the formals, declaration, and body are extracted
verify-guards behaves as though name were the name of some defined
function with those formals, declaration, and body. for lambda$. We
henceforth limit our attention to name being the name of a function,
theorem or axiom.
Note: Since we encourage you to use lambda$ instead of trying to type
quoted well-formed LAMBDA objects, you might wonder why we allow
verify-guards to operate on well-formed LAMBDA objects instead of
lambda$ expressions. The answer is that in proof output and in print-cl-cache output you see quoted well-formed LAMBDA objects and we
expect you might grab the text of such an object and submit it to
verify-guards.
See guard-formula-utilities for related utilities, including ones
that let you view the formula to be proved by verify-guards, but without
creating an event.
If name is one of several functions in a mutually recursive clique,
verify-guards will attempt to verify the guards of all of the
functions.
As promised above, we now describe the case that name was defined
function symbol whose definition supplies the value of :hints,
:guard-debug, and/or :guard-simplify. This happens when those
keywords are not supplied with the verify-guards event but the existing
definition specifies :guard-hints, :guard-debug, and/or
:guard-simplify, respectively, in its xargs declaration.
Note that when name is defined as part of a mutual-recursion
event, only declarations in the definition of name are relevant, but
those in definitions of other functions in the clique. Consider the following
example.
(defun my-consp (x)
(declare (xargs :guard t))
(consp x))
(defun my-cdr (x)
(declare (xargs :guard (my-consp x)))
(cdr x))
(mutual-recursion
(defun evenlp (x)
(declare (xargs :verify-guards nil))
(if (consp x) (oddlp (my-cdr x)) t))
(defun oddlp (x)
(declare (xargs :guard-hints
(("Goal" :in-theory (disable my-consp (tau-system))))))
(if (consp x) (evenlp (my-cdr x)) nil)))
Each of the following succeeds or fails for the reason given.
; Succeeds: :guard-hints for oddlp are ignored.
(verify-guards evenlp)
; Fails: :guard-hints for oddlp defeat the proof attempt.
(verify-guards oddlp)
; Succeeds: guard-hints for oddlp are ignored because :hints was supplied
; explicitly (even though :hints is nil, which is the default).
(verify-guards oddlp :hints nil)
If the guard or body of name include any quoted well-formed
LAMBDA objects, verify-guards include their proof obligations in
those generated for name. Roughly speaking, the guard obligations for a
well-formed LAMBDA object are exactly those that would be generated for a
separately defined non-recursive function with the formals, guard, and body of
the LAMBDA object. We discuss this further in the ``Remarks on
LAMBDA objects in defined functions'' below. As a non-logical
side-effect of the successful verification of all the proof obligations, all
well-formed LAMBDA objects in the guard or body of name (including
name itself if it is a lambda$ expression or LAMBDA object) are
added to the compiled lambda cache. This will speed up the execution of
name in the evaluation theory when those well-formed LAMBDA objects
are apply$d. See print-cl-cache.
If 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-nil 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 app and 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 app is 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 car
and 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 a, b and c the formula
above evaluates to t in 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-app is 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 a and b are true lists then so is (app a b) to
establish that the guard on the outermost app on 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 state
guarded-assoc-of-app as
(implies (and (true-listp a)
(true-listp b))
(equal (app (app a b) c)
(app a (app b c))))
rather than using the if form of the theorem. We cannot! The reason
is technical: implies is defined as a function in ACL2. When it is
called, both arguments are evaluated and then the obvious truth table is
checked. That is, implies is not ``lazy.'' Hence, when we write the
guarded theorem in the implies form we have to prove the guards on the
conclusion without knowing that the hypothesis is true. It would have been
better had we defined implies as a macro that expanded to the if
form, making it lazy. But we did not and after we introduced guards we did
not want to make such a basic change. For a utility that deals with this sort
of problem automatically, see defthmg.
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.
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 a
true-listp. Consider
(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 rev is 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 app requires. 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
x is a true-listp, (cdr x) is a true-listp. (2)
When z is a true-listp, (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 rev is defined
and so is not known to the theorem prover when rev is defined.
Therefore, we might break the admission of rev into three steps:
define 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 defun event. 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.
Remarks on LAMBDA objects in defined functions. The guard
obligations of a function, name, include the guard obligations of every
quoted well-formed LAMBDA object occurring in either the guard or body of
name. We point this out because quoted well-formed LAMBDA objects
are, after all, just quoted constants and no other quoted constant generates
guard obligations! Note also that we collect all quoted well-formed
LAMBDA objects, not just the translations of lambda$ expressions
and not just objects in slots of ilk :FN. (We do not actually
expect the user to write quoted well-formed LAMBDA objects in
non-:FN slots -- it can't be done with lambda$ expressions -- but we
collect them all anyway. If such a quoted constant is not guard verifiable,
you could always use so-called Bypass 1 of gratuitous-lambda-object-restrictions and avoid quoting it.) We assume that
when calls of name are executed some of those LAMBDA objects may
reach apply$ and be applied. Those applications will be faster if the
guards for the LAMBDAs are verified too. The guard obligations of a
quoted well-formed LAMBDA object are just those obligations that would be
generated by a defined function with the same formals, guard, and body as the
LAMBDA object. Those obligations are unioned with the rest of the
obligations generated for name and all must be proved for
(verify-guards name) to be successful. If the guards of some LAMBDA
object requires hints to prove, the hints may be supplied to
verify-guards as you would for any other failing guard obligation in
name. When successful, the LAMBDA objects thus verified are added,
behind the scenes, to the compiled lambda cache (see print-cl-cache)
to speed up apply$ in the evaluation theory.
Since, in general, LAMBDA objects can be passed around or re-used in
different contexts, the guard obligations generated for a quoted well-formed
LAMBDA object occurring in name are entirely independent of the
guard on the name itself. This is best explained by example.
In the defun below, which contains a lambda$ expression in its
body, we assume each function has the guard shown below:
function formals guard
f (x) (fp x)
g (x y) (gp x y)
the lambda$ (x) (lp x)
r (x) (rp x)
s (x) (sp x)
We also assume that the ilks of g are :FN and NIL. Then the
guard obligations generated for
(defun f (x)
(declare (xargs :guard (fp x)))
(g (lambda$ (x)
(declare (xargs :guard (lp x)))
(r x))
(s x)))
is
(and
(implies (fp x) (sp x)) ; f can call s
(implies (fp x) ; f can call g
(gp (lambda$ (x)
(declare (xargs :guard (hg x)))
(r x))
(s x)))
(implies (lp x) (rp x)) ; the lambda$ can call r
)
Note: The actual obligation will have been generated from the fully
translated body of f and the lambda$ expression will have been
converted to a quoted well-formed LAMBDA object. But we will refer to it
as a lambda$ here for clarity.
In particular note that the last conjecture, establishing that the
lambda$ can call r, does not have f's guard as a hypothesis.
The lambda$ is being guard verified in a ``context free'' way because we
cannot (or at least do not) trace the hypotheses governing every time it is
called in g and the variable x in f and its guard is unrelated
to the local variable x in the lambda$. Furthermore, if apply$
ever encounters this lambda$ it will know it has been guard
verified (because it finds it marked as such in the cache) and it may well
not be under a call of f. Be that as it may, the guard
obligations of the lambda$ are included in the guard obligations for
f. As of ACL2 Version 8.1, the guard obligation that g can call the
lambda$ is checked by computation every time the lambda$ is
apply$d. That is, (lp x) is run on each object the lambda$ is
apply$d to and the compiled code for the lambda$ is run only if its
guard approves.
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 as
though :set-guard-checking :all had been executed, so that we can trust
that this evaluation takes place without guard violations; see set-guard-checking.
If you want to verify the guards on functions that are built into
ACL2, you will first need to put them into :logic mode. See
verify-termination, specifically the ``Remark on system functions'' in
that documentation.
Subtopics
- Verify-guards-for-system-functions
- Arranging that source functions come up as guard-verified
- ACL2-pc::prove-guard
- (macro)
Verify guards efficiently by using a previous guard theorem.
