Major Section: RELEASE-NOTES
Important changes:
Versions of ACL2 preceding this one contain a subtle soundness bug! We found a flaw in our detection of subversive-recursions. The bug allowed some subversive recursions to slip through undetected.
We believe it would have been difficult to have exploited this flaw
inadvertently. In particular, the following five conditions are
necessary.
(1) Introduce a constrained function, say f, via an encapsulate.
(2) In the same encapsulation, define a clique of mutually
recursive functions. This clique must be non-local and in
:logic mode.
(3) In that mutually recursive clique, use the constrained function
f (perhaps indirectly) so that the termination argument for the
clique depends on properties of the witness for f. Thus,
f or some other function dependent upon f, must be used in
an argument in a recursive call or in a term governing a recursive
call. Furthermore, the use of f must be such that the
termination proof cannot be done without exploiting properties of
the witness for f. Other uses of the constrained functions in
the clique are ok.
(4) Fail to include the exploited properties of f among the
constraints of the encapsulation.
(5) Later, outside the encapsulation, explicitly use a functional
instantiation in which f is replaced by a function not enjoying
the crucial properties.
See subversive-recursions for details.
Less important notes:
We have begun to write some introductory tutorial material for those who wish to learn to program in ACL2. Most of this material is HTML-based. See the Hyper-Card on the ACL2 home page.
The documentation of verify-guards was improved to explain why
one might wish to verify the ``guards'' of a defthm event. The
missing documentation was noticed by John Cowles.
A bug was fixed in cross fertilization. The bug caused the system to report that it had substituted one term for another when in fact no substitution occurred. The bug was noticed by Bill McCune.
