Some Issues with Guards and Evaluation in ACL2 Matt Kaufmann ACL2 seminar, 8/4/04 Part 2: - A newly-found soundness bug (yes, a proof of nil) related to safe-mode, and a proposed fix that may, in part, involve elimination of so-call "small images". I've proved nil in ACL2 2.8 and (the current) 2.9. I suspect that the proof would work in every ACL2 back through 1.8. The proof, consisting of three certifiable books, is included at the end, below. The basic idea is to exploit a remaining hole in the evaluation mechanism, the one that caused us to introduce "safe-mode" so that :program mode functions are evaluated in the logic during macroexpansion. From :DOC note-2-6-proofs: An obscure potential soundness hole has been fixed by redoing the way evaluation takes place in the ACL2 loop and during theorem proving. We expect that users will see no difference based on this change. (Those interested in the details can see the long comment ``Essay on Evaluation in ACL2'' in source file interface-raw.lisp.) Here is an example. ACL2 !>(trace$ oneify-cltl-code) NIL ACL2 !>(defun foo (x) (declare (xargs :mode :program)) (car x)) 1> (ONEIFY-CLTL-CODE :PROGRAM NIL (FOO (X) (DECLARE (XARGS :MODE :PROGRAM)) (CAR X)) NIL |current-acl2-world|) <1 (ONEIFY-CLTL-CODE (ACL2_*1*_ACL2::FOO (X) (LABELS ((ACL2_*1*_ACL2::FOO (X) (ACL2_*1*_COMMON-LISP::CAR X))) (WHEN (NOT (F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*)) (RETURN-FROM ACL2_*1*_ACL2::FOO (FOO X))) (ACL2_*1*_ACL2::FOO X)))) Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(untrace$) NIL ACL2 !>(trace$ foo) NIL ACL2 !>(defmacro mac (x) (foo x)) Summary Form: ( DEFMACRO MAC ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) MAC ACL2 !>(defun bar (x) (mac x)) 1> (ACL2_*1*_ACL2::FOO X) ACL2 Error in ( DEFUN BAR ...): The guard for the function symbol CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 'X). See :DOC wet for how you might be able to get an error backtrace. ACL2 Error in ( DEFUN BAR ...): In the attempt to macroexpand the form (MAC X), evaluation of the macro body caused an error. Summary Form: ( DEFUN BAR ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ******** FAILED ******** See :DOC failure ******** FAILED ******** ACL2 !>:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2(3): (defun ACL2_*1*_ACL2::FOO (X) ;; This is how we did things through v2-5. (foo x)) ACL2_*1*_ACL2::FOO ACL2(4): (lp) ACL2 Version 2.8. Level 1. Cbd "/v/filer1a/v0q046/kaufmann/talks/seminar-8-4-04/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defun bar (x) (mac x)) 1> (ACL2_*1*_ACL2::FOO X) 2> (FOO X) Error: Attempt to take the car of X which is not listp. [condition type: SIMPLE-ERROR] Restart actions (select using :continue): 0: Return to Top Level (an "abort" restart). 1: Abort entirely from this process. [1] ACL2(5): :zoom Evaluation stack: (ERROR SIMPLE-ERROR :FORMAT-CONTROL ...) ->(CAR X) (FOO X) (MULTIPLE-VALUE-LIST (APPLY EXCL::BASIC-DEFINITION EXCL:ARGLIST)) [... EXCL::%EVAL ] (LET* (#) (SETQ VALUES #:G9102)) [... EXCL::%EVAL ] (PROG (VALUES) (PROGN # #) ...) [... EXCL::EVAL-AS-PROGN ] (LET (#) (PROG # # ...)) [... EXCL::%EVAL ] ((EXCL::ENCAPSULATED FOO) X) (ACL2_*1*_ACL2::FOO X) ... more older frames ... [1] ACL2(6): The hole is that we only implemented safe-mode for user-defined functions. Specifically, we do not mess with safe mode in function oneify-cltl-code-program, as indicated by the comment there: ; This is only used on ACL2 system functions. Here we are trusting the guards ; that we have specified for those functions. But in fact some :program mode system functions do not have correct (or any) guards. Here's the one I exploited, from basis.lisp: (defun add-to-set-eq-in-alist (key val alist) (cond ((null alist) (list (list key val))) ((eq key (caar alist)) (cons (cons key (add-to-set-eq val (cdr (car alist)))) (cdr alist))) (t (cons (car alist) (add-to-set-eq-in-alist key val (cdr alist)))))) I exploited the lack of a guard on the eq call in the books below. I think the fix is to avoid calling oneify-cltl-code-program. It may simplify things to eliminate small images, since the case (eq (small-p (w state)) t) that leads to a call of oneify-cltl-code-program in add-trip (for the case that the trip's car is '*1*defuns) is only active when building a small image. At the end I include data for small vs. large images. Here is the proof of nil. We could strengthen the requirement for redundancy in defconst in order to eliminate this example, but I can easily imagine still finding other such proofs of nil with sufficient effort. ============================== bad1.lisp ============================== (in-package "ACL2") (defconst *c* '(a b)) (defconst *d* *c*) (defmacro bad-macro () (list 'quote (add-to-set-eq-in-alist *c* 3 (list (list *d* 4))))) (defthm thm1 (equal (bad-macro) '(((a b) 3 4))) :rule-classes nil) ============================== bad2.lisp ============================== (in-package "ACL2") (defconst *c* '(a b)) (defconst *d* '(a b)) (defmacro bad-macro () (list 'quote (add-to-set-eq-in-alist *c* 3 (list (list *d* 4))))) (defthm thm2 (equal (bad-macro) '(((a b) 4) ((a b) 3))) :rule-classes nil) ============================== bad.lisp ============================== (in-package "ACL2") (include-book "bad1" :load-compiled-file nil) (include-book "bad2" :load-compiled-file nil) (defthm ouch nil :hints (("Goal" :use (thm1 thm2))) :rule-classes nil) ======================================================================