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.
Formal specification and correctness proofs of AleoBFT, a Byzantine-fault-tolerant consensus protocol, used in the Aleo blockchain.
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
This added a proof of the Schroder-Berstein theorem. 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
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. This sub-library also includes a parser from the concrete to the abstract syntax, a printer from the abstract syntax to the concrete syntax, and other tools to operate on this syntax.
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.
A new sub-library has been added, which contains tools to perform C-to-C transformations.
A soundness issue was fixed in tshell-call, which was modified to take and return state. To accomodate users who do not wish to refactor to this new stateful variant, the old version was retained and moved to a new book under the name tshell-call-unsound.
Improvements to decomposition proof methodology in VL/SVTV framework. New support for reasoning about FSMs based on SVTV symbolic simulations. New efficient method for equivalence checking two different evaluations of the same SVEX. Improvements to SVTV-CHASE debugging tool including mode for comparing two runs.
Improved AIGNET transforms -- new BDD parametrization transform, updates to allow AIG pointer arguments to transformation configs
Add exhaustive AIG simulation as a SAT checking option in FGL
Clean up and add various improvements to def-bounds tool
See directory
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.
A few new example proof files were added to
A new subdirectory,
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
Moved from
Added some theorems.
Disabled some rules.
Improved documentation and organization.
Renamed
Renamed
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.
The Std/basic books extensions in
Read-string and
The recognizers of digit characters in various bases
have been renamed to have the suffix
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
A variant without backchain limit of the set::double-containment rule has been added, disabled by default.
Some theorems have been added.
The
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 defines macro was extended to allow the
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:
Support has been added for the following instructions:
Some memory accessing functions for larger sizes have been added.
A number of improvements were made to the model in support of booting a slightly modified Linux kernel on it. These include various instruction bug fixes, a handful of new instructions, a translation lookaside buffer (TLB), and support for exception/interrupt handling, a timer peripheral, and a TTY peripheral. Additionally, there is a new validation mechanism that uses co-simulation with a virtual machine running in KVM to find bugs in the model. All these changes, along with instructions on how to boot Linux on the model are documented in the x86isa documentation.
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
The book
The behavior of function
For textual rendering of documentation, added blank lines between list
items within