Release notes for the ACL2 Community Books for ACL2 8.6

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

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

This is a work in progress for solving Ax = b, for sparse matrices A.

Added seven books to

Added support and testing for generation of *__acl2data.out files for
machine learning. The idea is to break proofs systematically and record
resulting information, including checkpoints. See

The library has been refactored to organize its constituents more clearly. Some parts of the documentation have also been improved and extended in the process of doing this refactoring.

The parsing generation tools have been significantly extended and improved.

New tools have been added to read grammars from files into formal ACL2 representations, to prove properties of the grammars, and to generate functions and theorems about the grammars.

Some fixtype names have been improved and made more consistent.

The `apt::simplify` transformation no longer breaks when certain default-hints or override-hints are present.

The `apt::simplify` transformation uses the new

The `apt::simplify` transformation, when called with option
`let` bindings and `let*` bindings that formerly remained.

The `apt::restrict` transformation has been improved
to generate more robust proofs,
which get around certain ACL2 heuristics.

The language formalization has been simplified and moved out of ATC and into the C formalization proper, i.e. into the deep embedding of C in ACL2, which is now independent from the shallow embedding of C in ACL2.

Support has been added for external object definitions (i.e. global variables) of array types.

Support has been added for structures with flexible array members.

An initial simple model of preprocessing has been added, along with support for file sets consisting of headers and source files.

An ABNF grammar for a subset of C has been added.

A new sub-library has been added, which contains an abstract syntax, and accompanying concrete syntax formulation, intended for use by tools like code generators and transformers.

Support has been added for
external object definitions (i.e. global variables) of array types,
via a new `c::defobject` event macro.

The user documentation of `c::defstruct`
has been extended and improved.

The event macro `c::defstruct` has been extended
to support flexible array members.
This macro has also been extended to generate
struct constructors as well as whole-array-member readers and writers.

Support has been added to represent and generate code that handles structures by value, in addition to code that handles structures by pointer.

An option to generate header files has been added. The previous keyed option to specify the output file path has been replaced with two keyed options to specify the output directory path and the file name without the extension.

A new proof generation approach has been started, where smaller, more modular proofs are generated for each generated C construct. This new approach will co-exist with the current one, until the former will replace the latter.

See directory `include-raw` and `partial-encapsulate`.

Several theorems have been added.

The `defdigits` tool has been extended
to generate additional theorems.

In the library of result types, some names have been improved.

A fixtype `pos-set` for sets of positive integers has been added,
along with some operations on these sets.

Added utility `show-books`, which returns a tree representing the
books included in the current ACL2 session.

The utility `checkpoint-list` and related utilities now show
top-level checkpoints even in the case of reverting to prove the original
goal by induction, and label them accordingly.

The library

Renamed `obag::emptyp`.

Added some theorems.

Disabled some rules.

Improved documentation and organization.

Renamed `omap::emptyp`.

Renamed `omap::assoc`.

The library has been moved
from

A concrete syntax for PFCSes, in the form of an ABNF grammar, has been defined.

The abstract syntax has been improved by using strings instead of symbols for names of relations and variables. This is more consistent with the concrete syntax.

Convenience constructors for the abstract syntax have been added.

Utilities have been added to build indexed names, useful for defining families of PFCS gadgets. The utilities are accompanied by theorems, useful to prove certain properties about the gadget families.

The formal notion of system (in the PFCS sense) has been improved, to be more in line with the general notion of constraint system.

Some arguments of semantic functions have been put into a more natural order.

Some theorems have been added and other theorems have been improved.

The documentation has been extended and improved.

A translator from R1CSes to PFCSes has been added, along with a checker for PFCSes that are in the R1CS subset, and along with a notion of structured R1CSes.

General rules have been added to support reasoning about PFCSes in a compositional way, and without having to deal explicitly with the proof trees used to define the PFCS semantics. See pfcs::proof-support for details.

A proof-generating lifter from deeply to shallowly embedded PFCSes has been added, so that one can more easily reason about the shallowly embedded form and mechanically transfer the reasoning to the deeply embedded form.

`Read-string` and

A new utility `untranslate$` has been added,
which is a logic-mode guard-verified version of `untranslate`.
See the documentation for details,
including functional differences with `untranslate`.

A new utility `genvar$` has been added,
which is a logic-mode guard-verified version of `genvar`.
See the documentation for details,
including functional differences with `genvar`.

A new utility `one-way-unify$` has been added,
which is a logic-mode guard-verified version
of the built-in

A new utility `termination-theorem$` has been added,
which is a logic-mode guard-verified version
of the built-in

A new utility `guard-theorem-no-simplify` has been added,
which is based on the built-in `guard-theorem`
but does no simplification and does not take a state argument.
See the documentation for details, and for why it may be useful.

A new utility `guard-theorem-no-simplify$` has been added,
which is a logic-mode guard-verified version
of the built-in `guard-theorem-no-simplify`.
See the documentation for details,
including functional differences with `guard-theorem-no-simplify`.

Theorems about the built-in `fsubcor-var` have been added.

The `set::emptyp`.

A variant without backchain limit
of the `set::double-containment` rule
has been added, disabled by default.

Some theorems have been added.

The `b*` has been extended with
an option

New utilities for error-value tuples have been added, to facilitate the generation, propagation, and catching of errors in statically strongly typed code that implements tools.

A new event macro `defirrelevant` has been added,
which automates some of the boilerplate related to
defining an irrelevant value of a given type
(usable as a dummy value, but of appropriate type).
Typically useful for irrelevant values of structured fixtypes.

The tool, `with-supporters`, has been substantially enhanced.

The tool, `prove$`, now treats hard errors as ordinary failures by
default, just as for soft errors. It also now suppresses time-limit and theory-invariant error printing as it does for
step-limit error printing.

The time-tracker capability is now turned off by the `run-script` tool, to avoid output that differs from what is expected (say,
due to running on a slow machine, or with many threads when few are
available).

Tools `functions-after` and `macros-after` return names of
functions and macros, respectively, that were introduced after a given
name.

`Make-flag` now causes a user-friendly error when the formal
parameters list is changed by an alternative definition specified by the

Support has been added for the following VEX instructions:

- SHL, SHRX, SARX
- VMOVUPS
- VZEROUPPER
- VANDPD, VANDPS, VANDNPD, VANDNPS, VORPD, VORPS, VXORPD, VXORPS, VPAND, VPANDN, VPOR, VPXOR
- VPADDB, VPADDW, VPADDD, VPADDQ (VEX versions)
- VPSUBB, VPSUBW, VPSUBD, VPSUBQ (VEX versions)

Some memory accessing functions for larger sizes have been added.

There is now XDOC support for Greek letters and more mathematical symbols. See xdoc::entities.

The utilities `install-not-normalized` and `install-not-normalized-event` have been tweaked to use the so-called
*unnormalized* body, which can avoid errors for functions that call
`wormhole-eval`.

The utilities `er-soft-logic` and `er-soft+` are unchanged.
But one might consider avoiding those two utilities now that `logic` mode (however, at the cost of
generating guard proof obligations).

The book

The behavior of function