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
(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
The preceding version (2.7) introduced a soundness bug in handling of ACL2
arrays, in which functions
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)))))))))On a related note, a new function
flush-compresscan be used for subtle control of under-the-hood raw Lisp support for fast array access, although we expect it to be very rare that users need this extra support.
Previous versions have had two soundness bugs that can occur when using the proof-checker:
o The first bug pertains to the
expandcommand, and hence
x-dumbcommands (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
definitionrule. Now, the
expandcommand 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
:expandhint 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
scommand (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
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
We fixed a soundness bug caused by a failure to check that a
type-prescription rule can be processed when proofs are skipped or
defequiv event. The former case can occur when processing an
include-book event, where the rule could depend
compound-recognizer rule preceding the proposed
type-prescription rule under the same
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
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))Thanks to Jared Davis for bringing this problem to our attention. We are particularly grateful to Jared because his example exploited this bug by applying it to a function defined using
mbe(introduced in this same version, 2.8), in order to prove
The sort of error message shown below can legitimately occur when certifying
a book in a certification world where there was an
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
: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))))
(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
(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
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.
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
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
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.
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
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.
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
gc$ had a bug exhibited when it was supplied one or more
arguments. This has been fixed.
defabbrev broke when supplied a string and no documentation,
(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
) 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.
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
had failed, but now will succeed. This particular bug prevented, for
: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
accumulated-persistence to locate rules that are slowing down
your proofs because of excessive attention to free variables, and then
add-match-free-override for those rules (or, just change the
rules themselves to specify
:once in the
(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.
brr mechanism has been cleaned up in order to avoid hard errors and
infinite loops that can arrive when typing interrupts (
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
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
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))))Before the fix, the proof attempt of the above silly thm printed the following.
(NTH 1 (UPDATE-NTH *FIELD0* 17 ST))After the fix, we instead see the following.
(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
car. Formerly, it was necessary to execute
nil before a
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
:exit command to generate an
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.