NOTE-2-8-BUG-FIXES

Major Section:  NOTE-2-8

We have fixed a soundness bug in the tautology checker's handling of expressions of the form (not (not x)). This bug has gone back at least as far as Version_2.4. All of the regression tests passed after the fix, without modification. So we hope that this bug has rarely bitten anyone. Thanks to Qiang Zhang for sending us a proof of nil that led us to this fix: (thm (equal (and p q) (not (or (not p) (not q))))). And thanks to Matyas Sustik for an observation that led to an improvement of our initial fix.

The preceding version (2.7) introduced a soundness bug in handling of ACL2 arrays, in which functions compress1 and compress2 were returning the input alist rather than compressing it appropriately. Here is a proof of nil that no longer succeeds, based on a bug report from Warren Hunt, who we thank for bringing this problem to our atttention.

(defthm bad
  (not (let* ((ar2 (aset1 'my-array ar1 3 10))
              (ar3 (compress1 'my-array ar2))
              (ar4 (reverse (reverse ar2)))
              (ar5 (compress1 'my-array ar4)))
         (and (equal ar2 ar4)
              (not (equal ar3 ar5)))))
  :rule-classes nil)
(defthm contradiction
  nil
  :rule-classes nil
  :hints (("Goal" :use
           ((:instance bad
                       (ar1 (compress1 'my-array
                                       '((3 . 5)
                                         (:HEADER :DIMENSIONS (5)
                                                  :MAXIMUM-LENGTH 6
                                                  :DEFAULT 0
                                                  :NAME MY-ARRAY)))))))))

Previous versions have had two soundness bugs that can occur when using the proof-checker:

o The first bug pertains to the expand command, and hence x and x-dumb commands (which call expand); see proof-checker-commands. The bug can occur when applying the above commands when the current term is a call of a constrained function symbol for which there is a :definition rule. Now, the expand command will succeed only when the function symbol of the current term is a defined function symbol, in which case the original definition is always used, in analogy to how the :expand hint works in the prover; see hints. Thanks to John Erickson for sending an example that led us to wonder if there might be a soundness problem.

o The second bug pertains to the s command (and commands that call it, e.g., s-prop). The proof-checker forms a context out of the top-level hypotheses and the if-terms governing the current term. If there is a contradiction in the top-level hypotheses, the proof-checker can appropriately consider the goal to be proved, and it does so. But formerly, the criterion was weaker: the contradiction could involve the combination of the top-level hypotheses and if-term governors. Thanks to Rob Sumners for noticing this bug.

A soundness bug could be provoked in some Lisps by applying defpkg to the empty string. This has been disallowed.

We fixed a soundness bug related to packages caused by a failure to track axioms introduced locally on behalf of defpkg events. See hidden-death-package.

We fixed a soundness bug caused by a failure to check that a :type-prescription rule can be processed when proofs are skipped or under a defequiv event. The former case can occur when processing an encapsulate or include-book event, where the rule could depend on a local :compound-recognizer rule preceding the proposed :type-prescription rule under the same encapsulate or include-book event. See local-incompatibility for such an example.

We fixed a potential soundness bug relating to reclassifying a :program mode function to :logic mode (as done by verify-termination or the submission of an appropriate ``redundant'' definition) without adequate checking that stobj usage was identical. Allegedly redundant definitions must now preserve the stobjs declaration as well as the formals, body, guard and type declarations. We thank Vernon Austel for pointing out this problem.

It was possible to get a raw Lisp error by introducing a locally defined function with guard verification inhibited and then subsequently introducing the same definition non-locally without that inhibition. The following example will clarify.

(encapsulate nil
  (local
    (defun foo (x) (declare (xargs :guard t :verify-guards nil)) (car x)))
  (defun foo (x) (declare (xargs :guard t)) (car x)))
; The following causes a raw lisp error because ACL2 runs the Common Lisp
; definition of foo, because it thinks that foo's guard of t was verified.
(thm (equal (foo 3) xxx))

The sort of error message shown below can legitimately occur when certifying a book in a certification world where there was an include-book command with a relative pathname (see pathname). However, it was occurring more often than necessary. This has been fixed.

ACL2 Error in (CERTIFY-BOOK "foo" ...): The certification world has include-book commands for book "bar" that correspond to different full pathnames, namely "/u/dir1/bar" and "/u/dir2/bar". ACL2 cannot currently certify a book in such a world. To work around this problem, use an absolute pathname for at least one of these books (see :DOC pathname).

Bugs were fixed in with-output, in particular related to the use of values :all. Also, documentation for with-output has been improved. Thanks to Vernon Austel for pointing out the bugs.

Fixed a lisp error occurring when bash proof-checker command was given illegal syntax, e.g., (bash (("Goal" :in-theory (enable binary-append)))) instead of (bash ("Goal" :in-theory (enable binary-append))).

We added an appropriate guard to find-rules-of-rune, which will avoid hard lisp errors when this function is called on non-rune arguments. Thanks to Eric Smith for pointing out this issue.

It was possible for a redundant include-book form (see redundant-events) to leave a command in the ACL2 logical world and to cause (re-)loading of a compiled file. These behaviors have been fixed. In particular, if book1 has already been included in the current ACL2 world and (include-book "book1") occurs in book2, then the compiled file for book1 will not be loaded again when book2 is included. Thanks to Dave Greve for bringing our attention to these problems, and to Eric Smith for bringing up a special case earlier (where "//" occurred in the book name).

The summary printed at the end of a proof had not listed :induction rules used in a proof. This has been corrected.

The use of proof trees in emacs redefined `control-c control-c' in such a way that in telnet mode, the telnet session was interrupted and perhaps could not be continued. This has been fixed.

Source function load-theory-into-enabled-structure contained a guard-violating call of compress1. Thanks to Vernon Austel for bringing this problem to our attention; even though this bug was benign (as he pointed out), we like keeping the source code free of guard violations.

A number of proof-checker atomic macros caused a hard error when all goals have already been proved. This has been fixed. Thanks to John Erickson for sending an example of the issue.

A bug has been fixed in add-match-free-override. Formerly, a table guard violation occurred when calling add-match-free-override more than once with first argument other than :clear.

Defininitions of functions involving large constants could cause stack overflows. This has been fixed, at least in some of the most egregious cases (by making a source function fn-count-evg tail-recursive). Thanks to Jared Davis for bringing this problem to our attention.

Evaluation of computed hints could cause stack overflows. This has been fixed. Thanks to Eric Smith for bringing this problem to our attention.

Evaluation of :monitor on :definition runes is now fast even if the specified function is part of a very large mutual-recursion nest. Thanks to Eric Smith for sending an example showing that this wasn't always the case.

Fixed a bug in books/bdd/cbf.lisp that was causing certification of distributed bdd books to fail when the connected book directory (see cbd) differs from the current working directory. Thanks to Scott Guthery for bringing this bug to our attention and supplying a helpful log.

Duplicate rule names have been eliminated from warnings generated upon the use of enabled :rewrite or :definition rules. Thanks to Eric Smith for pointing out this problem.

The trace utilities (see trace), as modified for GCL and Allegro Common Lisp, had failed to show more than the first return value for so-called ``*1*'' functions (essentially, executable-counterpart functions) when they were returning multiple values (via mv). This has been fixed. Thanks to Erik Reeber for pointing out this problem. Also, it is now possible to refer to arglist in trace$ forms when ACL2 is built on GCL, not just when ACL2 is built on Allegro Common Lisp.

Uses of hide introduced during proofs by failed attempts to evaluate constrained functions (see hide) are now tracked, so that the rune (:DEFINITION HIDE) will show up in the summary.

The following bug, introduced back in Version 2.7, has been fixed. The bug applied only to GCL and may well not have affected anyone. But the function proclamation computed by ACL2 for compilation usually had an output type of nil where it should have been t.

The macro gc$ had a bug exhibited when it was supplied one or more arguments. This has been fixed.

The macro defabbrev broke when supplied a string and no documentation, e.g., (defabbrev foo () ""). Thanks to Rob Sumners for noticing this problem and providing a fix, which we have incorporated.

For ACL2 executables built on Allegro Common Lisp, a Lisp error occurred when trace$ was called on other than a defined function symbol. Now ACL2 prints a more useful error message.

The proof-checker no longer accepts a (verify) command when some function symbol in the original goal no longer exists in the current ACL2 logical world. Thanks to John Erickson for bringing this issue to our attention.

The function ld-redefinition-action may now be called by the user. Thanks to Vernon Austel for suggesting that we remove this symbol from the list of so-called untouchables.

The handling of free variables in hypotheses (see free-variables) of rewrite and linear rules had a bug that prevented some proofs from going through. Here is a simple example, essentially provided by Diana Moisuc, who we thank for bringing this issue to our attention. The proof of the thm below had failed, but now will succeed. This particular bug prevented, for example, the :all behavior from occurring when the first hypothesis of the rule does not have free variables. NOTE: Now that this bug has been fixed, you may find some proofs running much more slowly than before. You can use accumulated-persistence to locate rules that are slowing down your proofs because of excessive attention to free variables, and then execute add-match-free-override for those rules (or, just change the rules themselves to specify :once in the :rule-classes).

(defstub foo1 (* ) => *)
(skip-proofs
 (defthm aux-foo1
   (implies (and (integerp a)
                 (integerp i)
                 (equal (foo1 0)  (list 0 i)))
            (equal (foo1 a) (list 0 (+ a i))))
   :rule-classes ((:rewrite :match-free :all))))
(thm
 (implies (and (integerp i) 
               (integerp a) 
               (equal (foo1 0) (list 0 i)))
          (equal (foo1 a) (list 0 (+ a i)))))

Formerly, creation of large arrays could cause an error in the underlying Common Lisp implementation without helpful messages for the user. Now, we check Common Lisp restrictions on arrays and print a helpful error message if they are violated, namely: each dimension must be less than the value of Common Lisp constant array-dimension-limit, and the product of the dimensions must be less than the value of Common Lisp constant array-total-size-limit. Thanks to Warren Hunt for bringing this issue to our attention. Note: this change also removes a former restriction of stobj array fields to size smaller than 2^28-1, provided the underlying Lisp can support larger arrays.

The default-hints in the current logical world were ignored by verify-guards. This has been fixed. Thanks to Jared Davis for pointing out this bug and sending a helpful example.

The brr mechanism has been cleaned up in order to avoid hard errors and infinite loops that can arrive when typing interrupts (control-c) or end-of-files (control-d) inside the brr loop. Thanks to Dave Greve, Olga Matlin, Eric Smith, and Serita Van Groningen for bringing this issue to our attention. As a byproduct, if you type control-d (or if inside emacs, control-c control-d), you may now quit entirely out of ACL2 and lisp (see good-bye) in some cases where you formerly would not have, for example when sitting at the ACL2 prompt (which formerly, in Allegro Common Lisp for example, would merely take you into raw Lisp rather than quitting everything).

We have eliminated structural flaws in the HTML documentation pages that could make them unreadable in some browsers. Thanks to Bill Young for bringing this issue to our attention and to Joe Hendrix for diagnosing the problem.

The proof-checker could run very slowly after many instructions in a given session. This has been fixed; thanks to Art Flatau for bringing this problem to our attention. (Implementation detail: We now keep tag-trees duplicate-free when we accumulate them into state. This change could have minor speed advantages for some top-level proofs too, not just in the proof-checker.)

The printing of accesses to stobjs using nth or update-nth has been done using symbolic constants since ACL2 Version_2.6. However, there was a bug that prevented this feature from working for update-nth except at a top-level call. This has been fixed. Thanks to Julien Schmaltz for bringing this problem to our attention. For example, consider these events:

(defstobj st field0 field1)
(thm (equal (nth 1 (update-nth 0 17 st)) (car (cons xxx yyy)))
     :hints (("Goal" :in-theory (disable nth update-nth))))

(NTH 1 (UPDATE-NTH *FIELD0* 17 ST))

(NTH *FIELD1* (UPDATE-NTH *FIELD0* 17 ST))

It is now possible to certify and subsequently include books that require guard-checking to be off. For example, the book can contain the form (defconst *silly* (car 3)) even though 3 fails to satisfy the guard of car. Formerly, it was necessary to execute :set-guard-checking nil before a certify-book or include-book in order for such a form to be handled without error. Thanks to Hanbing Liu for bringing this problem to our attention.

Fixed a proof-checker bug that could cause probably cause strange error, ``Attempt to access the plist field''. Thanks to Bill Young for bringing this problem to our attention.

Fixed a proof-checker bug that was failing to record applications of rewrite rules using the proof-checker's :rewrite command, causing the proof summary to omit mention of that rule (for example, when using the proof-checker's :exit command to generate an :instructions hint). Thanks to Bill Young for pointing out this bug.

Modernized some of the proof-tree emacs and infix printing stuff, thanks to suggestions made by Camm Maguire.