Some Issues with Guards and Evaluation in ACL2 Matt Kaufmann ACL2 seminar, 8/4/04 Part 1: A weakness in the current guard-checking mechanism recently noticed by David Rager, and a proposal for a fix. Below is a log (slightly edited as shown) of a demo illustrating guards and evaluation in ACL2, including the above-mentioned weakness. The focus is on so-called "*1* functions" ("executable counterparts") that compute results in the ACL2 logic. A patch to their generation is discussed below. There is a small problem with that patch as it currently stands, as evidenced by the final trace below of oneify-cltl-code; I'll discuss this in the seminar. As we'll see, the problem is that guards are not checked in recursive calls of :logic mode functions whose guards have not been verified. The solution is to provide two new values for :set-guard-checking, namely :ALL and :NOWARN. :set-guard-checking T ; as before, warn for skipped guard-checking :set-guard-checking NIL ; as before, namely, skip all guard-checking :set-guard-checking :NOWARN ; same as T, but do not warn :set-guard-checking :ALL ; check guards even on recursive calls =============================================================================== sundance:~/talks/seminar-8-4-04> acl2l # in-development copy of ACL2 2.9 << elided >> ACL2 !>(value-triple "Introductory example of user-defined guards and guard-checking") "Introductory example of user-defined guards and guard-checking" ACL2 !>(defun foo (x) (declare (xargs :guard (true-listp x))) (car x)) Since FOO is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO. The guard conjecture for FOO is trivial to prove. FOO is compliant with Common Lisp. Summary Form: ( DEFUN FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(foo '(a b c)) A ACL2 !>(trace$ foo) NIL ACL2 !>(foo '(a b c)) 1> (ACL2_*1*_ACL2::FOO (A B C)) 2> (FOO (A B C)) <2 (FOO A) <1 (ACL2_*1*_ACL2::FOO A) A ACL2 !>(foo (cons 3 4)) ; i.e., (foo '(3 . 4)) 1> (ACL2_*1*_ACL2::FOO (3 . 4)) ACL2 Error in TOP-LEVEL: The guard for the function symbol FOO, which is (TRUE-LISTP X), is violated by the arguments in the call (FOO '(3 . 4)). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>:set-guard-checking nil ; turn off guard-checking Turning guard checking off. That is, results will be given in the ACL2 logic. This raises a question: how should :program functions be evaluated? They have no logical definitions. Our decision is that calls of :program functions at the top level will continue to be evaluable but will continue to check their guards and signal errors when their guards are not satisfied. As with :logic functions, when a guard has been satisfied no subsidiary guard checking will be done. A few :logic functions that take STATE, including for example PRINC$, will also be treated this way. ACL2 >(foo (cons 3 4)) ; i.e., (foo '(3 . 4)) 1> (ACL2_*1*_ACL2::FOO (3 . 4)) <1 (ACL2_*1*_ACL2::FOO 3) 3 ACL2 >:set-guard-checking t ; turn guard-checking back on Turning guard checking on. ACL2 !>:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(defun foo (x) (declare (xargs :guard t :verify-guards nil)) (car x)) Since FOO is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO. Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(foo '(a b c)) ; note that *1*foo does not call (raw-lisp function) foo 1> (ACL2_*1*_ACL2::FOO (A B C)) <1 (ACL2_*1*_ACL2::FOO A) A ACL2 !>(foo 3) ; guard violation underneath foo 1> (ACL2_*1*_ACL2::FOO 3) ACL2 Error in TOP-LEVEL: The guard for the function symbol CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>(untrace$) ; turn off tracing of all functions (including foo) NIL ACL2 !>(value-triple "A weakness in guard checking. Although this was deliberate, for efficiency, David Rager recently pointed out potential confusion for the user.") "A weakness in guard checking. Although this was deliberate, for efficiency, David Rager recently pointed out potential confusion for the user." ACL2 !>; Oneify-cltl-code returns the definition of the *1* function (without ; the leading DEFUN). We will ignore trace output at first, but will ; return to it later. ; *** Comments, in lower-case, have been added on lines with ***. (trace$ oneify-cltl-code) NIL ACL2 !>(defun my-test1 (expr) ; @@@ original *1* code is in output below (declare (xargs :guard (true-listp expr) :verify-guards nil)) (if (atom expr) expr (cons (my-test1 (car expr)) (my-test1 (cdr expr))))) The admission of MY-TEST1 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 EXPR). We could deduce no constraints on the type of MY-TEST1. However, in normalizing the definition we used primitive type reasoning. 1> (ONEIFY-CLTL-CODE :LOGIC NIL (MY-TEST1 (EXPR) (DECLARE (XARGS :GUARD (TRUE-LISTP EXPR) :VERIFY-GUARDS NIL)) (IF (ATOM EXPR) EXPR (CONS (MY-TEST1 (CAR EXPR)) (MY-TEST1 (CDR EXPR))))) NIL |current-acl2-world|) <1 (ONEIFY-CLTL-CODE (ACL2_*1*_ACL2::MY-TEST1 (EXPR) ; *** We bind ACL2_*1*_ACL2::MY-TEST1 locally using LABELS, which accounts for ; *** recursion. Below we comment on where this is used. (LABELS ((ACL2_*1*_ACL2::MY-TEST1 (EXPR) (IF (ATOM EXPR) EXPR (CONS (ACL2_*1*_ACL2::MY-TEST1 (ACL2_*1*_COMMON-LISP::CAR EXPR)) (ACL2_*1*_ACL2::MY-TEST1 (ACL2_*1*_COMMON-LISP::CDR EXPR)))))) (LET ((ACL2_*1*_ACL2::MY-TEST1 (SYMBOL-CLASS 'MY-TEST1 (W *THE-LIVE-STATE*)))) ; *** The above binding of the name ACL2_*1*_ACL2::MY-TEST1 is perhaps ; *** confusing, since we already use that name for a function. But it's a ; *** handy symbol, which we know is not used elsewhere. There is also a role ; *** in avoiding recursive calls in mutual-recursion, which we do not discuss ; *** here. (COND ((EQ ACL2_*1*_ACL2::MY-TEST1 :COMMON-LISP-COMPLIANT) ; *** Guards have been verified, so we can execute in raw Lisp if the ; *** guard-check passes. (COND ((TRUE-LISTP EXPR) (RETURN-FROM ACL2_*1*_ACL2::MY-TEST1 (MY-TEST1 EXPR))) ((F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*) ; *** The (TRUE-LISTP EXPR) guard check has failed, so we get an error. (THROW-RAW-EV-FNCALL (LIST 'EV-FNCALL-GUARD-ER 'MY-TEST1 (LIST EXPR) '(TRUE-LISTP EXPR) '(NIL)))))) ((AND (F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*) ; *** Guards have not been verified (previous case), but guard-checking is on, ; *** so we check the guard and cause an error if it fails. (NOT (ACL2_*1*_ACL2::TRUE-LISTP EXPR))) (THROW-RAW-EV-FNCALL (LIST 'EV-FNCALL-GUARD-ER 'MY-TEST1 (LIST EXPR) '(TRUE-LISTP EXPR) '(NIL))))) ; *** If none of the cases above applies, then we fall through and execute in ; *** the logic. The LABELS binding above defines the function being called ; *** here. (ACL2_*1*_ACL2::MY-TEST1 EXPR))))) Summary Form: ( DEFUN MY-TEST1 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) MY-TEST1 ACL2 !>(untrace$) NIL ACL2 !>(my-test1 '(a b c)) ; "should" see a guard violation (A B C) ACL2 !>(my-test1 'a) ; note the guard violatino ACL2 Error in TOP-LEVEL: The guard for the function symbol MY-TEST1, which is (TRUE-LISTP EXPR), is violated by the arguments in the call (MY-TEST1 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>; Turn guard-checking off, so that evaluation is done in the ACL2 logic, ; without regard to guards. :set-guard-checking nil Turning guard checking off. That is, results will be given in the << elided >> ACL2 >(my-test1 'a) A ACL2 >; Turn guard-checking back on. :set-guard-checking t Turning guard checking on. ACL2 !>(defun my-test2 (expr) (declare (xargs :guard (true-listp expr) :verify-guards nil)) (if (endp expr) expr (cons (my-test2 (car expr)) (my-test2 (cdr expr))))) << elided >> MY-TEST2 ACL2 !>(my-test2 '(a b c)) ; Why doesn't true-listp guard the endp call? ACL2 Error in TOP-LEVEL: The guard for the function symbol ENDP, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (ENDP 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>; Note that my-test1 and my-test2 agree in the logic. :set-guard-checking nil Turning guard checking off. That is, results will be given in the << elided >> ACL2 >(my-test2 '(a b c)) (A B C) ACL2 >; Turn guard-checking back on. :set-guard-checking t Turning guard checking on. ACL2 !>:ubt! 1 ; go back to the beginning 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>:q ; go into raw Lisp Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2(1): (LP!) ; developer hack for ignoring #-acl2-loop-only code << elided >> ACL2 !>:redef! ; go to :program mode and allow redefinition of system functions T ACL2 p!>; We want redefinition of the macro set-guard-checking in the ACL2 loop, so ; it's not enough to load the patch into raw Lisp. (ld "patch-guards.lisp") << elided >> ACL2 p!>:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2(2): ; We want redefinition of the #-acl2-loop-only definitions, so it's not enough ; to load (ld) the patch into the ACL2 loop. (load "patch-guards.lisp") ; Loading << elided >> T ACL2(3): (lp) << elided >> ACL2 p!>:logic ACL2 !>(trace$ oneify-cltl-code) NIL ACL2 !>(defun my-test1 (expr) ; @@@ new *1* code is in output below (declare (xargs :guard (true-listp expr) :verify-guards nil)) (if (atom expr) expr (cons (my-test1 (car expr)) (my-test1 (cdr expr))))) The admission of MY-TEST1 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 EXPR). We could deduce no constraints on the type of MY-TEST1. However, in normalizing the definition we used primitive type reasoning. 8520232 bytes have been tenured, next gc will be global. See the documentation for variable EXCL:*GLOBAL-GC-BEHAVIOR* for more information. 1> (ONEIFY-CLTL-CODE :LOGIC NIL (MY-TEST1 (EXPR) (DECLARE (XARGS :GUARD (TRUE-LISTP EXPR) :VERIFY-GUARDS NIL)) (IF (ATOM EXPR) EXPR (CONS (MY-TEST1 (CAR EXPR)) (MY-TEST1 (CDR EXPR))))) NIL |current-acl2-world|) <1 (ONEIFY-CLTL-CODE (ACL2_*1*_ACL2::MY-TEST1 (EXPR) ; *** The following MACROLET form binds *1*BODY to a zero-ary macro that ; *** macroexpands to the indicated IF expression. That way, we don't have to ; *** lay down the IF expression twice in the code that follows (this is ; *** probably minor). (MACROLET ((*1*BODY NIL '(IF (ATOM EXPR) EXPR (CONS (ACL2_*1*_ACL2::MY-TEST1 (ACL2_*1*_COMMON-LISP::CAR EXPR)) (ACL2_*1*_ACL2::MY-TEST1 (ACL2_*1*_COMMON-LISP::CDR EXPR)))))) ; *** The following MACROLET form binds *1*LABELS-MACRO to a zero-ary macro ; *** that macroexpands to the indicated LABELS expression. Again, this is for ; *** brevity (expression sharing). The point is that unlike the earlier code, ; *** this time we cannot do the LABELS binding at the top, because we want to ; *** be able to make a true recursive call of the top-level function being ; *** defined. (MACROLET ((*1*LABELS-MACRO NIL '(LABELS ((ACL2_*1*_ACL2::MY-TEST1 (EXPR) (*1*BODY))) (ACL2_*1*_ACL2::MY-TEST1 EXPR)))) (LET ((ACL2_*1*_ACL2::MY-TEST1 (SYMBOL-CLASS 'MY-TEST1 (W *THE-LIVE-STATE*)))) ; *** This time there is no fall-through; the COND expression returns the ; *** result. (COND ((EQ ACL2_*1*_ACL2::MY-TEST1 :COMMON-LISP-COMPLIANT) (COND ((TRUE-LISTP EXPR) (MY-TEST1 EXPR)) ((F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*) (THROW-RAW-EV-FNCALL (LIST 'EV-FNCALL-GUARD-ER 'MY-TEST1 (LIST EXPR) '(TRUE-LISTP EXPR) '(NIL)))) ; *** We know that guard-checking-on is NIL, so we simply execute in the ; *** logic, skipping further guard evaluation. (T (*1*LABELS-MACRO)))) ((AND (F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*) (NOT (ACL2_*1*_ACL2::TRUE-LISTP EXPR))) (THROW-RAW-EV-FNCALL (LIST 'EV-FNCALL-GUARD-ER 'MY-TEST1 (LIST EXPR) '(TRUE-LISTP EXPR) '(NIL)))) ((EQ (F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*) :ALL) ; *** Do not call the LABELS function! Instead, recursively call the top-level ; *** *1* function that we are defining. (*1*BODY)) (T (MAYBE-WARN-FOR-GUARD MY-TEST1) ; *** Since guard-checking-on is not :ALL, we go ahead and execute in the ; *** logic, skipping further guard evaluation. But first we warn if ; *** guard-checking-on is T rather than :NOWARN. (*1*LABELS-MACRO)))))))) Summary Form: ( DEFUN MY-TEST1 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) MY-TEST1 ACL2 !>(untrace$) NIL ACL2 !>(my-test1 '(a b c)) ACL2 Warning [Guard-checking] in TOP-LEVEL: Guard-checking will be inhibited on recursive calls of the executable counterpart (i.e., in the ACL2 logic) of MY-TEST1. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn) (A B C) ACL2 !>(set-guard-checking :all) Leaving guard checking on, but changing value to :ALL. ACL2 !>(my-test1 '(a b c)) ACL2 Error in TOP-LEVEL: The guard for the function symbol MY-TEST1, which is (TRUE-LISTP EXPR), is violated by the arguments in the call (MY-TEST1 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>(wet (my-test1 '(a b c))) ACL2 Error in WITH-ERROR-TRACE: The guard for the function symbol MY-TEST1, which is (TRUE-LISTP EXPR), is violated by the arguments in the call (MY-TEST1 'A). See :DOC wet for how you might be able to get an error backtrace. 1> (ACL2_*1*_ACL2::MY-TEST1 (A B C)) 2> (ACL2_*1*_ACL2::MY-TEST1 A) ACL2 !>(set-guard-checking :nowarn) Leaving guard checking on, but changing value to :NOWARN. ACL2 !>(my-test1 '(a b c)) (A B C) ACL2 !>(defun my-test2 (expr) (declare (xargs :guard (true-listp expr) :verify-guards nil)) (if (endp expr) expr (cons (my-test2 (car expr)) (my-test2 (cdr expr))))) << elided >> MY-TEST2 ACL2 !>:set-guard-checking t Leaving guard checking on, but changing value to T. ACL2 !>(my-test2 '(a b c)) ; as before, we get mysterious endp guard violation ACL2 Warning [Guard-checking] in TOP-LEVEL: Guard-checking will be inhibited on recursive calls of the executable counterpart (i.e., in the ACL2 logic) of MY-TEST2. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn) ACL2 Error in TOP-LEVEL: The guard for the function symbol ENDP, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (ENDP 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>(set-guard-checking :all) Leaving guard checking on, but changing value to :ALL. ACL2 !>(my-test2 '(a b c)) ; now the violation comes earlier, on (my-test2 'a) ACL2 Error in TOP-LEVEL: The guard for the function symbol MY-TEST2, which is (TRUE-LISTP EXPR), is violated by the arguments in the call (MY-TEST2 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>(set-guard-checking :nowarn) ;should go back to "bad" behavior, no warning Leaving guard checking on, but changing value to :NOWARN. ACL2 !>(my-test2 '(a b c)) ACL2 Error in TOP-LEVEL: The guard for the function symbol ENDP, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (ENDP 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>:set-guard-checking nil ; check that we can still evaluate in the logic Turning guard checking off. That is, results will be given in the << elided >> ACL2 >(my-test2 '(a b c)) (A B C) ACL2 >(value-triple "Let us compare the *1* code before and after the patch. Search backward for @@@.") "Let us compare the *1* code before and after the patch. Search backward for @@@." ACL2 >(trace$ my-test1) NIL ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>; Notice below that the recursive calls of the *1* function are missing, since ; they are made by the local (LABELS) function. (my-test1 '(a b c)) 1> (ACL2_*1*_ACL2::MY-TEST1 (A B C)) ACL2 Warning [Guard-checking] in TOP-LEVEL: Guard-checking will be inhibited on recursive calls of the executable counterpart (i.e., in the ACL2 logic) of MY-TEST1. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn) <1 (ACL2_*1*_ACL2::MY-TEST1 (A B C)) (A B C) ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(my-test1 '(a b c)) 1> (ACL2_*1*_ACL2::MY-TEST1 (A B C)) 2> (ACL2_*1*_ACL2::MY-TEST1 A) ACL2 Error in TOP-LEVEL: The guard for the function symbol MY-TEST1, which is (TRUE-LISTP EXPR), is violated by the arguments in the call (MY-TEST1 'A). See :DOC wet for how you might be able to get an error backtrace. ACL2 !>