Verify the guards of a function

See guard for a general discussion of guards.

Before discussing the

Technical Notes: (1) The first argument of `defthm` or `defaxiom` event, a
`lambda$` expression, or an unquoted well-formed *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

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 `if` and
`rationalp`,

(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 `and`) for the term

(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
calls of `if` are also assumed. (However, additional conjectures are
generated for **Special Guard
Conjectures for LOOP$** in the documentation for `loop$`.)

As mentioned above, if the guard on a function is not

(defun foo (x) (declare (xargs :guard (car x))) x)

We turn now to the

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, `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, `lambda$` expression or a well-formed *quoted*).
Mixed-mode-functions cannot be guard verified.

In the most common case `hints`, `otf-flg`, and `guard-debug` are as described in the corresponding documentation
entries, but

If `well-formed-lambda-objectp`), the formals, declaration, and body are extracted

Note: Since we encourage you to use `print-cl-cache` output you see quoted well-formed

See guard-formula-utilities for related utilities, including ones
that let you view the formula to be proved by

If

As promised above, we now describe the case that `xargs` declaration.
Note that when `mutual-recursion`
event, only declarations in the definition of

(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 `print-cl-cache`.

If

For example, if

(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

(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

(equal (app (app 1 2) 3) (app 1 (app 2 3)))

we get an error or, perhaps, something worse like

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

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

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

One last complication: The careful reader might have thought we could state

(implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))))

rather than using the `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, `defthmg`.

Recall however that

`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 `true-listp`, since that is what the guard of `true-listp`? The most elegant
argument is a two-step one, appealing to the following two lemmas: (1) When
`true-listp`, `true-listp`. (2)
When `true-listp`, `true-listp`.
But the second lemma is a generalized property of

Therefore, we might break the admission of

(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 `defun` event. The reason is
that, in this particular case, the system's heuristics just happen to hit upon
the lemma

**Remarks on LAMBDA objects in defined functions**. The guard
obligations of a function,

Since, in general,

In the

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

(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

In particular note that the last conjecture, establishing that the
*not* be under a call of

**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
`enable`d. 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

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.

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