## VERIFY-GUARDS

verify the guards of a function
```Major Section:  EVENTS
```

```Examples:
(verify-guards flatten)
(verify-guards flatten
:hints (("Goal" :use (:instance assoc-of-app)))
:otf-flg t
:doc "string")

General Form:
(verify-guards name
:hints        hints
:otf-flg      otf-flg
:doc          doc-string)
```
See guard for a general discussion of guards. In the General Form above, `name` is the name of a `:``logic` function (see defun-mode) or of a theorem or axiom. 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. `hints` and `otf-flg` are as described in the corresponding `:``doc` entries; and `doc-string`, if supplied, is a string not beginning with ```:Doc-Section`''. The three keyword arguments above are all optional. `Verify-guards` will attempt to prove that the guard on the named function implies the guards of all of the subroutines called in the body of the function, and that the guards are satisfied for all function calls in the guard itself (under an implicit guard of `t`). If successful, `name` is considered to have had its guards verified.

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.

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.

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.

Because `name` is not uniquely associated with the `verify-guards` event (it necessarily names a previously defined function) the documentation string, `doc-string`, is not stored in the documentation data base. Thus, we actually prohibit `doc-string` from having the form of an ACL2 documentation string; see doc-string.

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

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