Major Section: GUARD
ACL2 guard verification (see guard) is often best avoided by beginning users of ACL2. When guard verification is employed, it can generate numerous goals, some of which may not be theorems if the definition being processed has bugs. It can be difficult to find such bugs. This documentation topic explains a capability provided by ACL2 to help find such bugs.
(Extra-info x y) always returns t by definition. However, if
guard verification takes place with a non-nil setting of
guard-debug (see below), then the goals generated for guard verification
can include hypotheses that are calls of extra-info. Typically, such a
hypothesis is of the following form:
(extra-info '(:guard (:body F))
'(G ARG1 ... ARGk))
The above form indicates that the goal in which it occurs was generated to
verify that the guard of the function F is satisfied by the
arguments ARG1 through ARGk, where the term (G ARG1 ... ARGk)
occurs in the body of the function F whose guard verification is in
progress. If however the above call of G occurs in the guard of F
instead of the body of F, then :body is replaced by :guard above:
(extra-info '(:guard (:guard F))
'(G ARG1 ... ARGk))
If the same proof obligation (goal clause) arises from more than one
occurrence of the same call, then a single goal will be generated, which has
several extra-info hypotheses added to show the multiple sources of that
proof obligation.
All rules (see rune) associated with extra-info are disabled by
default, so that hypotheses of the form described above are not simplified to
t. These hypotheses are intended to ride along for free: you can
generally expect the proof to have the same structure whether or not the
:guard-debug option is supplied, though on rare occasions the proofs may
diverge.
It remains to explain the notion of a guard-debug setting of t, that
is, to explain how to obtain the additional hypotheses described above. If
guards are being verified during processing of a defun event (whether
or not inside a call of mutual-recursion), then one specifies
:guard-debug t in an xargs declaration of a declare form;
see xargs. If however the guard verification is on behalf of a
verify-guards call, whether for a definition or a theorem, then one
specifies the keyword argument :guard-debug t.
Also see print-gv for a utility for debugging guard violations, in contrast
to the above guard-debug mechanism, which is for debugging failed proofs
arising from guard verification.