Release notes for the ACL2 Community Books for ACL2 8.1

The following is a brief summary of changes made to the community-books between the releases of ACL2 8.0 and 8.1.

See also note-8-1 for the changes made to ACL2 itself. For additional details, you may also see the raw commit log.

A new regular expression library, acre::acre, is available in

Added PLTP(A), The Pure Lisp Theorem Prover, reimplemented in ACL2. An
ACL2 reconstruction of the 1973 Pure Lisp Theorem Prover (PLTP), the original
``Boyer-Moore theorem prover'' after which both NQTHM and ACL2 were modeled,
is available in

A new directory,

Added utility include-book-paths to list paths via `include-book` down to a given book, which may be useful for reducing book
dependencies.

Added utility apply-fn-if-known to apply a function that might not exist; even the package for the function symbol might not exist.

Added a fixer `integer-range-fix` for `integer-range-p`, as
well as a recognizer `integer-range-listp` and and a fixer `integer-range-list-fix` for true lists of `integer-range-p`, all with
accompanying theorems.

Added a

Added a new utility, `skip-in-book`, that wraps around a form to
prevent its evaluation during book certification or inclusion.

The new utility `defthm<w` will attempt to prove a theorem directly
from previously-proved theorems. It does this by generating suitable hints using the new utility, previous-subsumer-hints.

Added some utilities for building XDOC documentation. The `defxdoc+` extends `defxdoc` with additional conveniences.

A new event, `defunt`, is a variant of `defun` that uses
termination theorems from a large set of community-books —
namely, all books included in `termination-theorem` lemma-instances that reference `fms!-lst`, which
writes a list to a character output channel; `injections`, which lists
all maps from a domain to a range; `strict-merge-sort-<`, which sorts without
duplicates; and `subsetp-eq-linear`, which is a linear-time subset test
for sorted lists of symbols.

Added a new macro `unsigned-byte-p` and `signed-byte-p` and to the
library binary predicates `unsigned-byte-listp` and `signed-byte-listp`.

Started a new library for Ethereum.

Started a new library for Bitcoin.

A new book,

The behavior and code for the expander (see defthm?) have been improved in a few ways (some of them technical), as follows.

- A bug has been fixed that was preventing hints from being passed to
the forcing round (if any). An example may be found in the new book,
misc/expander-tests.lisp . - The deprecated
`fmt`directives~p and~q have been replaced by~x and~y , respectively. - Error messages have been improved for the function
simplify-hyps when there is a contradiction. - The state globals
tool2-result andtool2-error are no longer set. (They appear to have been unused.) - The functions
tool2-fn ,tool2-fn-lst , andsimplify-hyps now have a new final argument,ctx . Also, the macrotool2 now has a:ctx keyword argument.

Updated the ACL2+books manual to accommodate the replacement of David Russinoff's online rtl manual by his upcoming Springer book.

Improved `install-not-normalized` to handle cases in which
recursively-defined functions have non-recursive normalized definitions.

The

The `ensure-error`, `ensure-soft-error`, `ensure-hard-error`, `thm?`, and `not-thm?` have been renamed to `must-fail-with-error`, `must-fail-with-soft-error`, `must-fail-with-hard-error`, `must-prove`, and `must-not-prove`. The old names are still available as
deprecated synonyms, which will be removed in one of the next releases.

The old directory *Modeling Algorithms in SystemC* now makes even
less sense than it did; the best we could come up with as a replacement is
*Restricted Algorithmic C*.

The utility `make-flag` has a new keyword argument,

Extended and simplified the `defun-sk`
function (whose fields can then be accessed); instead, now the utilities
retrieve the various pieces of information directly.

Extended the `defchoose`
functions.

Made several improvements to `directed-untranslate`, including: avoid
assertion errors that could occur when using `declare` forms with `let`, `let*`, or `mv-let` expressions: enhance insertion of
appropriate `mv` calls; extend dropping of unused `let` bindings;
avoid an assertion error with `b*`.

Removed the `evens` utility.

Extended the

Extended the Kestrel world query utilities with functions to collect the names of all the known packages in the ACL2 world and to check if a function is primitive.

Extended the

Extended the Kestrel term utilities with operations to substitute function symbols without performing simplification, to construct terms that are functions applications of certain forms, to collect all the lambda expressions in terms, and to collect all the package names in (symbols in) terms.

The utility `install-not-normalized-event` now includes option
`install-not-normalized` event. The new
utility, `install-not-normalized-event-lst`, can thus handle `mutual-recursion` nicely, e.g.: `install-not-normalized$` to submit the event generated by `install-not-normalized-event`.

Extended the

Added some

Added a theorem about lists of strings.

Merged the utilities in

Extended the Kestrel symbol utilities with a utility that lifts `symbol-package-name` to lists.

Moved `maybe-msgp` under newly created

Moved `msg-downcase-first` and `msg-upcase-first` from the

A new book, `ACL2-pc::when-not-proved`), for
skipping instructions when all goals have been proved. It also defines two
(more complex) macros, `ACL2-pc::prove-guard`) and
`ACL2-pc::prove-termination`), for
(respectively) using previously-proved guard or termination theorems
efficiently, as well as a more general macro, `ACL2-pc::fancy-use`, for
using lemma instances (via

Improved the `mutual-recursion`, and improved it to work better with an

Fixed the utility, `orelse`, so that

Fixed a few books that broke due to the change in `defevaluator` (see
note-8-1 for details).

Added a

Improved user input validation.

Added support for the new `defun-sk`. This
option is now supported by SOFT's `soft::defun-sk2` and `soft::defun-inst` macros.

Most of the model has been extended to 32-bit mode. The only instructions that remain to be extended to 32-bit mode are JMP far and the floating-point instructions. The 32-bit-only instructions PUSHA, POPA, INC with opcodes 40h-47h, DEC with opcodes 48h-4Fh, and PUSH CS/SS/DS/ES have been added to the model. Support for the kinds of paging in 32-bit mode is still missing, but this is only needed for the system view of the model, not the application view.

Some of the XDOC documentation and some of the comments have been slightly expanded.

The notion of programmer-level mode and system-level mode have been renamed
to `application-level view' and `system-level view', to avoid overloading the
word `mode', which in the x86 has a more specific meaning. Similarly, the
notion of page structure marking mode has been renamed `marking view'. This
involved renaming the

The instruction decoder has been extended to detect VEX- and EVEX-encoded (AVX, AVX2, AVX512) instructions, in both 64- and 32-bit modes of operation. However, semantic functions of many of these instructions are still unimplemented.

Annotated opcode maps are now used to generate opcode dispatch functions and instruction coverage information.

Improved documentation.

Improved options to control the screen output.

Improved `apt::tailrec` transformation with an option to attempt to
automatically infer the domain for some of the transformation's applicability
conditions.

Improved `apt::restrict` transformation to wrap the restriction test
with `mbt`; added an applicability condition to ensure that the
restriction test is boolean-valued.

Imported more symbols from the

Added the bitops::sparseint library, which represents large integers as balanced binary trees, which can save memory by sharing structure among many such objects.

Improved scalability of several SV utilities when large variables are present by recoding several functions that previously used Lisp bignums to use a bitops::sparseint based encoding.

Added optional accumulated-persistence-style profiling of attempted rule
applications, available with keyword argument

Changed the representation of symbolic objects, removing the

Added option to bind some variables that can be used by the nextstate, property, constraint, and initstate terms. These bindings will be symbolically evaluated once, which can perhaps improve performance by not requiring them to be repeated.

Added a utility, xdoc::archive-xdoc, that saves the documentation generated by a series of local events, partially preprocessing it to avoid references to definitions that might only be locally available.

The `defpointer` utility for xdoc now accepts names that have
special characters such as

The

The build system now has support for ifdef and ifndef, which
are make-event-supported macros defined in

A BibTeX file has been added to the community books, containing reference
information for papers published at the ACL2 Workshops. This may be useful to
you if you wish to cite such a paper in a LaTeX document. It is available at

A Developer's Guide (see developers-guide) has been added, to assist those who may wish to become ACL2 Developers. It replaces the much smaller ``system-development'' topic.

The download button now works in the web-based manual.

When the `include-raw` utility with option `comp`, it was possible for that subsequent
compilation to overwrite intended raw Lisp definitions, for a host Lisp that
does not compile on-the-fly (i.e., for a host Lisp other than CCL or SBCL).
The way to prevent such overwrites is to extend state globals