Finding the source of a term in prover output

When a proof attempt fails, a good first step is typically to look
at *checkpoints*; see the-method. That step is often sufficient.
But occasionally a checkpoint contains an undesirable term whose source is a
mystery, and it may be useful to find the origin of that term.

Example: ; Collect brr-data when attempting the indicated proof: (with-brr-data (thm (equal (append x y) (append y x)))) ; Show a path leading to a rewrite result that contains ; (append y (cdr x)) as a subterm: (cw-gstack-for-subterm (append y (cdr x))) ; Same as above, except enter a loop to query for additional such results: (cw-gstack-for-subterm* (append y (cdr x)))

The rest of this documentation topic is structured as follows. It may suffice to read only the first two sections.

- Introduction
- Connections with break-rewrite
- General form of
with-brr-data calls - General forms of queries
- Keyword arguments of
with-brr-data (optional) - Low-level details (optional)
- Using attachments to modify functionality of
with-brr-data

The collection of break-rewrite data can slow down the theorem prover, but the slowdown will probably be modest, perhaps adding an extra 15% or so to the time.

We turn now to examples that illustrate how

Our first illustration of

(with-brr-data (thm (equal (append x y) (append y x))))

ACL2 produces the following checkpoints, exactly as though the `thm`
call were evaluated without the surrounding call of

*** Key checkpoint at the top level: *** Goal (EQUAL (APPEND X Y) (APPEND Y X)) *** Key checkpoints under a top-level induction before generating a goal of NIL (see :DOC nil-goal): *** Subgoal *1/2'' (IMPLIES (AND (CONSP X) (EQUAL (APPEND (CDR X) Y) (APPEND Y (CDR X)))) (EQUAL (CONS (CAR X) (APPEND Y (CDR X))) (APPEND Y X))) Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (EQUAL Y (APPEND Y X))) ACL2 Error [Failure] in ( THM ...): See :DOC failure. ******** FAILED ******** ACL2 Observation: (LENGTH (@ BRR-DATA-LST)) = 16 ACL2 !>

Consider the term `cw-gstack`, followed by the result of the
bottom-most rewriter call, which contains the given term as a subterm. (See
term for discussion of “translated” and
“untranslated” terms.)

ACL2 !>(cw-gstack-for-subterm (append y (cdr x))) 1. Simplifying the clause ((NOT (CONSP X)) (NOT (EQUAL (BINARY-APPEND (CDR X) Y) (BINARY-APPEND Y (CDR X)))) (EQUAL (BINARY-APPEND X Y) (BINARY-APPEND Y X))) 2. Rewriting (to simplify) the atom of the third literal, (EQUAL (BINARY-APPEND X Y) (BINARY-APPEND Y X)), 3. Rewriting (to simplify) the first argument, (BINARY-APPEND X Y), 4. Attempting to apply (:DEFINITION BINARY-APPEND) to (BINARY-APPEND X Y) The resulting (translated) term is (CONS (CAR X) (BINARY-APPEND Y (CDR X))). ACL2 !>

One might realize that `binary-append`. With that information
one can issue a `monitor!` command as follows.

:monitor! (:definition binary-append) (equal (brr@ :target) '(binary-append x y))

We now issue the `thm` call above, with or without the wrapper of

1 ACL2 >:type-alist Decoded type-alist: ----- Terms with type *TS-T*: (EQUAL (APPEND (CDR X) Y) (APPEND Y (CDR X))) ----- Terms with type *TS-CONS*: X ========== Use (GET-BRR-LOCAL 'TYPE-ALIST STATE) to see actual type-alist. 1 ACL2 >:target (BINARY-APPEND X Y) 1 ACL2 >:eval 1! (:DEFINITION BINARY-APPEND) produced (CONS (CAR X) (BINARY-APPEND Y (CDR X))). 1 ACL2 >

The log above shows how the term

We can find more sources of the same term by using the “

(cw-gstack-for-subterm* (append y (cdr x)))

While *exactly* a given term rather than paths to a term *containing* that
term (as above). The queries

(cw-gstack-for-term (append y (cdr x))) (cw-gstack-for-term* (append y (cdr x)))

Finally, these queries support searching for *instances* of a term or
subterm, by supplying a “term” of the form

(cw-gstack-for-term (:free (u v) (cons u v))) (cw-gstack-for-term* (:free (u v) (cons u v)))

Notice that the use of this

Consider the following (admittedly contrived) example.

(defstub f0 (x) t) (defun f1 (x) (cons x x)) (defun f2 (x) (f1 (f0 x))) (defun f3 (x) (if (atom x) (f2 x) (f2 (car x)))) (with-brr-data (thm (equal (f3 x) yyy)))

The call of `thm` produces the following checkpoint.

(IMPLIES (CONSP X) (EQUAL (CONS (F0 (CAR X)) (F0 (CAR X))) YYY))

In this simple example it's easy to figure out how the term

ACL2 !>(cw-gstack-for-term (F0 (CAR X))) There are no results. ACL2 !>

To see why there are no results, recall that

ACL2 !>(cw-gstack-for-subterm (F0 (CAR X))) 1. Simplifying the clause ((EQUAL (F3 X) YYY)) 2. Rewriting (to simplify) the atom of the first literal, (EQUAL (F3 X) YYY), 3. Rewriting (to simplify) the first argument, (F3 X), 4. Attempting to apply (:DEFINITION F3) to (F3 X) 5. Rewriting (to simplify) the body, (IF (CONSP X) (F2 (CAR X)) (F2 X)), under the substitution X : X 6. Rewriting (to simplify) the second argument, (F2 (CAR X)), under the substitution X : X 7. Attempting to apply (:DEFINITION F2) to (F2 (CAR X)) 8. Rewriting (to simplify) the rhs of the conclusion, (F1 (F0 X)), under the substitution X : (CAR X) 9. Attempting to apply (:DEFINITION F1) to (F1 (F0 (CAR X))) The resulting (translated) term is (CONS (F0 (CAR X)) (F0 (CAR X))). Note: The first lemma application above that provides a suitable result is at frame 4, and that result is (IF (CONSP X) (CONS (F0 (CAR X)) (F0 (CAR X))) (CONS (F0 X) (F0 X))). ACL2 !>

We see that the term

It is also interesting to look at the “Note” printed at the
end. The query utilities search for the first rule application that produced
a suitable result, and then they search from that point for a maximally deeper
rule application that produced a suitable result. In this case, the first
rule that produced a term containing

Next we'll explore a limitation of these tools and how to get around it. We start as follows (following the definitions above).

(with-brr-data (thm (equal (append (f3 x) y) z) :hints (("Goal" :in-theory (disable append)))))

This proof attempt results in the following checkpoint.

(IMPLIES (CONSP X) (EQUAL (APPEND (CONS (F0 (CAR X)) (F0 (CAR X))) Y) Z))

The following log may be surprising, especially since the indicated term need only be a subterm of a rewriter result, and we see this exact term in the checkpoint above!

ACL2 !>(cw-gstack-for-subterm (APPEND (CONS (F0 (CAR X)) (F0 (CAR X))) Y)) There are no results. ACL2 !>

A solution is to choose a subterm of that input term, as shown in the log
below. The resulting output shows why the query above yielded no results:
frame 6 below shows that the first argument,

ACL2 !>(cw-gstack-for-subterm (cons (f0 (car x)) (f0 (car x)))) 1. Simplifying the clause ((EQUAL (BINARY-APPEND (F3 X) Y) Z)) 2. Rewriting (to simplify) the atom of the first literal, (EQUAL (BINARY-APPEND (F3 X) Y) Z), 3. Rewriting (to simplify) the first argument, (BINARY-APPEND (F3 X) Y), 4. Rewriting (to simplify) the first argument, (F3 X), 5. Attempting to apply (:DEFINITION F3) to (F3 X) 6. Rewriting (to simplify) the body, (IF (CONSP X) (F2 (CAR X)) (F2 X)), under the substitution X : X 7. Rewriting (to simplify) the second argument, (F2 (CAR X)), under the substitution X : X 8. Attempting to apply (:DEFINITION F2) to (F2 (CAR X)) 9. Rewriting (to simplify) the rhs of the conclusion, (F1 (F0 X)), under the substitution X : (CAR X) 10. Attempting to apply (:DEFINITION F1) to (F1 (F0 (CAR X))) The resulting (translated) term is (CONS (F0 (CAR X)) (F0 (CAR X))). Note: The first lemma application above that provides a suitable result is at frame 5, and that result is (IF (CONSP X) (CONS (F0 (CAR X)) (F0 (CAR X))) (CONS (F0 X) (F0 X))). ACL2 !>

The careful reader may notice another reason that the

The moral of this story is that if a term fails to give you a match, then
use a subterm of it. You can also use the

(cw-gstack-for-subterm (:free (v) (cons (f0 v) (f0 v))))

We noted above that after running

But there are these additional connections between

- The same rewriting processes are considered by
with-brr-data as by break-rewrite; in particular, abbreviation rules are not considered during preprocessing (see monitor). - When a query command (
cw-gstack-for-term etc.) finds a match with a rewriting result, it discards the result if the input — the:target , in the parlance of break-rewrite — contains that match. - Monitored runes are indeed monitored during evaluation of a
call of
with-brr-data , even if break-rewrite has not been enabled globally (using: `brr`or`monitor!`). If this is not desired, then unmonitor runes before callingwith-brr-data . - There is the following low-level way to collect brr-data for queries such
as
cw-gstack-for-term without callingwith-brr-data :(assign gstack :brr-data) . But you may want to clear such data afterwards, which you can do by evaluating the form,(clear-brr-data-lst) . Otherwise the brr-data from later proof attempts will be combined, probably in unexpected ways, with brr-data from earlier proof attempts. With-brr-data and its queries pay no attention to “near-miss” breaks (see break-rewrite for discussion of these breaks).

The first item above is worth emphasizing. Consider the following example.

(include-book "std/lists/rev" :dir :system) (with-brr-data (thm (implies (and (natp n) (< n (len x))) (equal (nth n (revappend x y)) (nth n (reverse x)))) :hints (("Goal" :do-not '(preprocess))))) (cw-gstack-for-subterm (APPEND (REV X) Y))

The `hints`. If we use `pso` on the proof attempt without the *preprocess* process for simplification, which avoids the usual rewriter.
If we instead query the no-hints version with

ACL2 !>(cw-gstack-for-subterm (REV X)) 1. Simplifying the clause ((NOT (INTEGERP N)) (< N '0) (NOT (< N (LEN X))) (EQUAL (NTH N (BINARY-APPEND (REV X) Y)) (NTH N (REVERSE X)))) 2. Rewriting (to simplify) the atom of the fourth literal, (EQUAL (NTH N (BINARY-APPEND (REV X) Y)) (NTH N (REVERSE X))), 3. Rewriting (to simplify) the second argument, (NTH N (REVERSE X)), 4. Rewriting (to simplify) the second argument, (REVERSE X), 5. Attempting to apply (:DEFINITION REVERSE) to (REVERSE X) 6. Rewriting (to simplify) the body, (IF (STRINGP X) (COERCE (REVAPPEND (COERCE X 'LIST) 'NIL) 'STRING) (REVAPPEND X 'NIL)), under the substitution X : X 7. Rewriting (to simplify) the third argument, (REVAPPEND X 'NIL), under the substitution X : X 8. Attempting to apply (:REWRITE REVAPPEND-REMOVAL) to (REVAPPEND X 'NIL) 9. Rewriting (to simplify) the rhs of the conclusion, (BINARY-APPEND (REV X) Y), under the substitution Y : 'NIL X : X 10. Attempting to apply (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV) to (BINARY-APPEND (REV X) 'NIL) The resulting (translated) term is (REV X). Note: The first lemma application above that provides a suitable result is at frame 5, and that result is (IF (STRINGP X) (COERCE (REV (COERCE X 'LIST)) 'STRING) (REV X)). ACL2 !>

The version of this example without

The general form, including optional keyword arguments, is

(with-brr-data form :global-var var :brr-data-returned bool)

where

There is probably little reason for most users to supply either keyword argument. They are documented in the section after next.

**Notes**.

- The data collected by a call of
`with-brr-data`will persist until the next call ofwith-brr-data . - Behavior is undefined for nested calls of
with-brr-data . (If this presents a problem then you may ask the ACL2 implementors to consider specifying that behavior.)

The four queries (all illustrated above) are as follows, where the keyword argument is optional.

(cw-gstack-for-subterm u :global-var var) (cw-gstack-for-subterm* u :global-var var) (cw-gstack-for-term u :global-var var) (cw-gstack-for-term* u :global-var var)

In each case,

These queries are effective after data collection using

This notion of “matches” depends on the call, as follows.
First assume that the input is a term. For

When a matching node

The discussion above characterizes the behavior of
`symbol-name` is

As noted above, the general form of a call of

(with-brr-data form :global-var var :brr-data-returned bool)

The keywords have aspects that are quite technical, so unless you are somewhat familiar with ACL2 implementation issues you will probably want to skip this section.

Neither keyword argument is evaluated. The behavior of the keyword
arguments depends on a list,

We now explain the keyword arguments in terms of the list

:global-var var

The symbolvar defaults to the symbol,brr-data-lst .Var is eithernil or a state global variable (see programming-with-state), which by default isbrr-data-lst . Ifvar is notnil , then thewith-brr-data call modifies state by setting the value of the state global,var , toBDL .:brr-data-returned bool

Suppose that theform argument of thewith-brr-data call evaluates to(mv erp val state) . Then whenbool isnil (which is the default), thewith-brr-data call returns that same error-triple,(mv erp val state) . If howeverbool is notnil , then instead thewith-brr-data call returns(mv erp BDL state) .

This implementation-level section further describes the

A

(defrec brr-data (pre post . completed) nil) (defrec brr-data-1 (((lemma . target) . (unify-subst . type-alist)) . ((pot-list . ancestors) . (rcnst initial-ttree . gstack))) nil) (defrec brr-data-2 ((failure-reason unify-subst . brr-result) . (rcnst final-ttree . gstack)) nil)

The

We have seen above that the use of `trans1` on a `brr`

The programmer who manipulates

It is easy to see the list of

ACL2 Observation: (LENGTH (@ BRR-DATA-LST)) = 16

The form

The behavior of

books/kestrel/utilities/brr-data-all.lisp books/kestrel/utilities/brr-data-failures.lisp

When the macro is called with no arguments, i.e.,
`symbol-name`. The indicated string, which we write below as `defattach` calls rather than `defattach-system` calls, so that
their effect is not local to the enclosing book.

(defattach (brkpt1-brr-data-entry brkpt1-brr-data-entry-<S> :system-ok t) (defattach (brkpt2-brr-data-entry brkpt2-brr-data-entry-<S> :system-ok t) (defattach (update-brr-data-1 update-brr-data-1-<S>) :system-ok t) (defattach (update-brr-data-2 update-brr-data-2-<S>) :system-ok t)

The four

(brkpt1-brr-data-entry ancestors gstack rcnst state) => * (brkpt2-brr-data-entry ancestors gstack rcnst state) => * (update-brr-data-1 lemma target unify-subst type-alist ancestors initial-ttree gstack rcnst pot-lst whs-data) => * (update-brr-data-2 wonp failure-reason unify-subst gstack brr-result final-ttree rcnst ancestors whs-data) => *

Note that