Generate markers to indicate sources of guard proof obligations
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.
For a similar utility appropriate for proving measure conjectures (that is, for termination proofs), see measure-debug.
We begin with the following example. Although it is contrived and a bit simplistic, it illustrates how the guard-debug utility works.
(defun length-repeat (x) (length (append x x))) (verify-guards length-repeat :guard-debug t)
The output produces two top-level key checkpoints, as follows.
Subgoal 2 (IMPLIES (EXTRA-INFO '(:GUARD (:BODY LENGTH-REPEAT)) '(APPEND X X)) (TRUE-LISTP X)) Subgoal 1 (IMPLIES (AND (EXTRA-INFO '(:GUARD (:BODY LENGTH-REPEAT)) '(LENGTH (APPEND X X))) (NOT (TRUE-LISTP (APPEND X X)))) (STRINGP (APPEND X X)))
The upper subgoal (numbered 2) says that the body of the definition of
Of course, the example above is a bit obvious. But for large definitional bodies such information can be very helpful. Note that guard-debug can be specified not only in verify-guards events but also in xargs declare forms of defun events.
We now describe the guard-debug utility in some detail.
(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
(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
All rules (see rune) associated with
It remains to explain the notion of a
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.