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 !>