|
|
|---|
|
|
|
|---|
A brief transcript illustrating guards in ACL2
This note addresses the question: what is the use of guards in ACL2? Although we recommend that beginners try to avoid guards for a while, we hope that the summary here is reasonably self-contained and will provide a helpful introduction to guards in ACL2. For a more systematic discussion, see guard. For a summary of that topic, see guard-quick-reference.
Before we get into the issue of guards, let us note that there are two important “modes”:
defun-mode — “Does this defun add an axiom (‘logic mode’) or not (`:program mode')?” (See defun-mode.) Only logic mode functions can have their “guards verified” via mechanized proof; see verify-guards.
set-guard-checking — “Should runtime guard violations signal an error (
:all , and usually witht or:nowarn ) or go undetected (nil ,:none )? The question relates to the use of Common Lisp to evaluate expressions; see set-guard-checking.
Here are some examples of the relation between the ACL2 prompt and
the “modes” discussed above. Also see default-print-prompt. The first examples all have ld-skip-proofsp
equal to
ACL2 !> ; logic mode with guard checking on ACL2 > ; logic mode with guard checking off ACL2 p!> ; program mode with guard checking on ACL2 p> ; program mode with guard checking off
Here are some examples with default-defun-mode equal to
ACL2 > ; guard checking off, ld-skip-proofsp nil ACL2 s> ; guard checking off, ld-skip-proofsp t ACL2 !> ; guard checking on, ld-skip-proofsp nil ACL2 !s> ; guard checking on, ld-skip-proofsp t
ACL2 !>(+ 'abc 3) ACL2 Error [Evaluation] in TOP-LEVEL: The guard for the function call (BINARY-+ X Y), which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)), is violated by the arguments in the call (BINARY-+ 'ABC 3). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>:set-guard-checking nil [[.. output elided ..]] ACL2 >(+ 'abc 3) 3 ACL2 >(< 'abc 3) T ACL2 >(< 3 'abc) NIL ACL2 >(< -3 'abc) T ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(defun sum-list (x) (declare (xargs :guard (integer-listp x) :verify-guards nil)) (cond ((endp x) 0) (t (+ (car x) (sum-list (cdr x)))))) The admission of SUM-LIST is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of SUM-LIST is described by the theorem (ACL2-NUMBERP (SUM-LIST X)). We used primitive type reasoning. Summary Form: ( DEFUN SUM-LIST ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.03) SUM-LIST ACL2 !>(sum-list '(1 2 3)) ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited for some recursive calls, including SUM-LIST; see :DOC guard-checking- inhibited. 6 ACL2 !>(sum-list '(1 2 abc 3)) ACL2 Error [Evaluation] in TOP-LEVEL: The guard for the function call (SUM-LIST X), which is (INTEGER-LISTP X), is violated by the arguments in the call (SUM-LIST '(1 2 ABC 3)). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>:set-guard-checking nil [[.. output elided ..]] ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >(defthm sum-list-append (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. [[.. output elided ..]] *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM SUM-LIST-APPEND ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) [[.. output elided ..]] (:TYPE-PRESCRIPTION SUM-LIST)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 470 SUM-LIST-APPEND
See declare, and xargs, and verify-guards for related background, though we intend what follows to be self-explanatory.
Declare Form Guards Verified? (declare (xargs :mode :program ...)) no (declare (xargs :guard g)) yes (declare (xargs :guard g :verify-guards nil)) no (declare (xargs ...<no :guard>...)) no ACL2 >:pe sum-list L 1 (DEFUN SUM-LIST (X) (DECLARE (XARGS :GUARD (INTEGER-LISTP X) :VERIFY-GUARDS NIL)) (COND ((ENDP X) 0) (T (+ (CAR X) (SUM-LIST (CDR X)))))) ACL2 >(verify-guards sum-list) Computing the guard conjecture for SUM-LIST.... The non-trivial part of the guard conjecture for SUM-LIST, given the [[.. output elided ..]] Q.E.D. That completes the proof of the guard theorem for SUM-LIST. SUM-LIST is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS SUM-LIST) Rules: ((:DEFINITION ENDP) [[.. output elided ..]] (:TYPE-PRESCRIPTION SUM-LIST)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 115 SUM-LIST ACL2 >:pe sum-list LV 1 (DEFUN SUM-LIST (X) (DECLARE (XARGS :GUARD (INTEGER-LISTP X) :VERIFY-GUARDS NIL)) (COND ((ENDP X) 0) (T (+ (CAR X) (SUM-LIST (CDR X)))))) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(sum-list '(1 2 abc 3)) ACL2 Error [Evaluation] in TOP-LEVEL: The guard for the function call (SUM-LIST X), which is (INTEGER-LISTP X), is violated by the arguments in the call (SUM-LIST '(1 2 ABC 3)). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>:set-guard-checking nil [[.. output elided ..]] ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >
We continue this demo by tracing
ACL2 >(trace$ sum-list) ((SUM-LIST)) ACL2 >(sum-list '(1 2 abc 3)) 1> (ACL2_*1*_ACL2::SUM-LIST (1 2 ABC 3)) 2> (ACL2_*1*_ACL2::SUM-LIST (2 ABC 3)) 3> (ACL2_*1*_ACL2::SUM-LIST (ABC 3)) 4> (ACL2_*1*_ACL2::SUM-LIST (3)) 5> (SUM-LIST (3)) 6> (SUM-LIST NIL) <6 (SUM-LIST 0) <5 (SUM-LIST 3) <4 (ACL2_*1*_ACL2::SUM-LIST 3) <3 (ACL2_*1*_ACL2::SUM-LIST 3) <2 (ACL2_*1*_ACL2::SUM-LIST 5) <1 (ACL2_*1*_ACL2::SUM-LIST 6) 6 ACL2 >
For a theorem to be guard-verified, its statement should be executable
without error in Common Lisp. The following is thus not guard-verifiable,
since its evaluation can cause an error if
ACL2 >:pe sum-list-append
2 (DEFTHM SUM-LIST-APPEND
(EQUAL (SUM-LIST (APPEND A B))
(+ (SUM-LIST A) (SUM-LIST B))))
ACL2 >(verify-guards sum-list-append)
Computing the guard conjecture for SUM-LIST-APPEND....
The non-trivial part of the guard conjecture for
SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST,
is
Goal
(AND (TRUE-LISTP A)
(INTEGER-LISTP A)
(INTEGER-LISTP (APPEND A B))
(INTEGER-LISTP B)).
******** FAILED ********
ACL2 >
Perhaps surprisingly, a defthm event with statement
(implies (and (integer-listp a) (integer-listp b)) (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b))))
is still not guard-verifiable. The reason is that implies is a
function, so its arguments are both always evaluated — in particular,
its second argument is evaluated even if its first argument evaluates to
ACL2 >(defthm common-lisp-sum-list-append (if (and (integer-listp a) (integer-listp b)) (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b))) t) :rule-classes nil) Q.E.D. Summary Form: ( DEFTHM COMMON-LISP-SUM-LIST-APPEND ...) Rules: ((:REWRITE SUM-LIST-APPEND)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 23 COMMON-LISP-SUM-LIST-APPEND ACL2 >(verify-guards common-lisp-sum-list-append) Computing the guard conjecture for COMMON-LISP-SUM-LIST-APPEND.... The non-trivial part of the guard conjecture for COMMON-LISP-SUM-LIST-APPEND, given the :forward-chaining rules ACL2-NUMBER-LISTP-FORWARD-TO-TRUE-LISTP, INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP and RATIONAL-LISTP-FORWARD-TO-ACL2-NUMBER-LISTP and the :type-prescription rules ACL2-NUMBER-LISTP, INTEGER-LISTP, RATIONAL-LISTP and SUM-LIST, is Goal (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (INTEGER-LISTP (APPEND A B))). [[.. output elided ..]] Q.E.D. That completes the proof of the guard theorem for COMMON-LISP-SUM-LIST-APPEND. COMMON-LISP-SUM-LIST-APPEND is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS COMMON-LISP-SUM-LIST-APPEND) Rules: ((:DEFINITION BINARY-APPEND) [[.. output elided ..]] (:TYPE-PRESCRIPTION SUM-LIST)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 565 COMMON-LISP-SUM-LIST-APPEND ACL2 >
Guard verification fails when the theorem is for “code” that cannot even be parsed (or “translated”; see term) as executable code.
ACL2 >(defthm foo (consp (mv x y))) Q.E.D. The storage of FOO depends upon primitive type reasoning. Summary Form: ( DEFTHM FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 >(verify-guards foo) ACL2 Error in ( VERIFY-GUARDS FOO): The guards for FOO cannot be verified because its formula has the wrong syntactic form for evaluation, perhaps due to multiple-value or stobj restrictions. See :DOC verify-guards. Summary Form: ( VERIFY-GUARDS FOO) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error [Failure] in ( VERIFY-GUARDS FOO): See :DOC failure. ******** FAILED ******** ACL2 >