|
|
|---|
|
|
|
|---|
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 library contains a parser for CSV (comma separated value) files and utilities for handling parsed CSV files.
A (partial) formal specification of the Ethereum Virtual Machine (EVM) has
been added as
A new, cleanroom formalization of IEEE-754 floating point arithmetic has been
added as
Jun Sawada's 1998-1999 dissertation work, consisting of verification for
the FM9801 pipelined microprocessor design, has been added as directory
This is a work in progress for solving Ax = b, for sparse matrices A.
Added seven books to
A new library (
A new hint,
An initial ACL2 library for Leo, Provable Inc.'s language for zero-knowledge applications.
Hanbing Liu's 2006 dissertation work on a "defensive JVM" has been added
as directory
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-Bernstein theorem. See
A new library (
This library contains a simple XML parser.
A new library (
This library has been moved
from
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.
Various rules and tests have been added/improved, and library organization has been improved.
Some fixtype names have been improved and made more consistent.
Various rules have been added/improved, some new functions and books have
been added, and library organization has been improved. A few functions
have been deprecated, including
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.
Minor improvements were made to rename-params (fixed handling of ignores), finite-difference (e.g., :extra-guard option), wrap-output, drop-irrelevant-params, and rename-params.
Documentation was improved.
The
Various rules have been added/improved, proofs have been sped up, new books
have been added, and library organization has been improved. Dependence
on other libraries, such as
Many improvements have been made to the Axe toolkit. These include improvements to the legacy Axe tools (Rewriter, Prover, and Equivalence checker) as well as to the new tools (rewriters, provers, etc.) that we are creating. These new tools are generated from a template for various applications, and we sometimes refer to them as generated rewriters, generated provers, etc. Improvements specific to individual Axe variants (for x86, JVM, and R1CS reasoning) are discussed in further sections, below.
Various Axe-specific rewrite rules have been added, improved, organized, and renamed. Rule-lists have also been improved in many ways (e.g., to build in more simplifications).
Axe rewriters were improved in various ways (most of these improvements apply
to the new, generated rewriters). Handling of
When memoization is enabled, generated rewriters now do two rewrites, first with memoization and then a second one using node contexts (but no memoization, for soundness). We sometimes need to use the node contexts, but we also want memoization turned on when most of the work is being done (this can make a huge difference in the speed of large rewrites). When a rewriter does makes two passes, it now ensures the reduced rule limits from pass 1 are passed to pass 2.
Axe rules now support binding hypotheses. These must be wrapped in
calls of the identity function
Lambdas are no longer always expanded in normal hypotheses of Axe rules.
Instead, we call
Various theorems were proved about the implementation of Axe itself, and
theorems were added to justify some of Axe's operations (e.g., simplifications
it makes). Many skip-proofs in the legacy Axe tools were removed, and more
code was put into
Generated provers now support the
The dependencies of Axe were reduced, as were the rules exported when Axe is included (e.g., rules Axe uses to reason about its own implementation).
The Tactic Prover now applies a set of rewrite rules before calling STP on a
goal. These prepare the proof for STP by rewriting unsupported constructs into
supported ones (e.g., splitting rotations with non-constant rotation amounts
into cases). Also, a
At least one fix was made to the STP translation, and supporting analyses,
such as type inference, were improved and clarified. The formalization of Axe
types was improved (including some long awaited changes), and better error
checking is now done. STP calls record the time taken. The environment variable
The
A
The
Evaluation was improved to build more functions into the evaluators.
Tests and examples were added and improved (e.g., when new tool options reduce user input required). New examples include some Axe verifications of AES implementations. Documentation has also been improved.
Pruning of unreachable if branches has been improved (evaluating additional
ground terms and supporting
The implementation was optimized in various ways, e.g. by using stobjs and
fast-alists, by using
The Equivalence Checker now allows the
The
Printing was significantly improved (e.g., to print elapsed times, to print more information for failures, and to elide uninteresting output). Counterexample printing has also been improved, as has printing when monitoring rules (only printing relevant DAG nodes and suppressing printing of huge assumptions) and when printing assumptions (adding the ability to elide given function calls).
The Java Formal Unit Tester now analyzes all methods whose names start with
The R1CS variant of Axe has benefited from many of the general Axe improvements mentioned above, especially scalability improvements to generated provers. Also, more global rules have been built in.
Many improvements were made to the x86 variant of Axe, including incorporation
of improved rules and normal forms from the
The x86 Axe tools now use an Axe Rewriter variant specialized for x86 reasoning.
A new tool,
Support for parsing and lifting ELF files was added, as was a :position-independent option.
Lifting of x86 code into logic was improved in many ways, including new rules, new normal forms,
improved rule-lists, better support for floating-point operations, better
debugging, more ways to indicate which components of the final state should be
extracted, and improved generation of assumptions for lifting. The
Lifting has been optimized (e.g., by avoiding passing in unhelpful assumptions
when pruning). Also, the Lifter avoids opening
The ability to name and describe the types of inputs was added. This can help
the tools put in some assumptions automatically. If this option is used, the
Lifter puts in assumptions about the inputs being separate from the code and
the saved return address. Also, the assumptions about inputs being disjoint
from subsequent stack slots are now sensitive to the number of stack slots
specified. For an array input, variables can now be introduced for individual
elements. The scheme for introducing variable for registers has been improved,
and type assumptions are now generated for these variables. Initial support
for Lifter
The order of parameters in generated functions has been improved (to match x86
calling conventions), and the
The Axe x86 tools now always use
An executable to be lifted must now be indicated by giving its path. Passing in an entire parsed executable, as was previously done, is now deprecated.
Examples were added, including a proof of an x86 implementation of the TEA block cipher, and an example of lifting and verifying a recursive x86 factorial program.
A Formal Unit Tester for x86 binaries was added. This can be used to augment unit test suites with small proofs about binary programs.
A large number of bit-vector rules were added, collected, improved, and
renamed. One focus was on rules that introduce BV operators by rewriting
arithmetic or
Functions
New functions
The book
A typed bit-vector equality operation
The functions
Various rules have been added/improved (e.g., rules about bit packing), the
function
Various rules have been added/improved, and library organization has been improved.
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 accommodate 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
Library organization was improved and a :well-formedness-guarantee was added.
Formal specifications have been added for the AES block cipher, the TEA block cipher, and the SHA-3 hash function. Proofs have been done to connect the SHA-3 spec to the Keccak spec.
The formalization of rank-1 constraint systems (R1CSes) has been improved in
various ways (e.g., added/generalized rules, added dense form of R1CSes, imported
See directory
Several theorems have been added.
The defdigits tool has been extended to generate additional theorems.
The
Various rules have been added/improved (e.g., rules about
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.
The Helpers Library has been significantly improved.
A new Proof Advice tool has been added to help create and repair ACL2 proofs. The tool can get proof help over the web, from machine learning models running on servers. It also applies some proof search heuristics. Tools have also added to experimentally evaluate how well the Proof Advice tool performs.
A new tool, repair-book, has been added to repair failed ACL2 proofs based on information previously saved during successful proofs.
The improve-book tool has been improved. It has also been used to improve various other books and libraries.
A new utility, speed-up-book, has been added. It attempts to speed up a given book in various ways. It has been used to speed up the certification of various other books and libraries.
An ACL2 Linter tool was improved and moved to this library.
A lightweight variant of HTTP post has been added.
The parser now uses more tail recursion. Function
A few new example proof files were added to
A new subdirectory,
Various small improvements and fixes were made. The
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.
Various new utilities have been added, including
New data structures have been added, including
New books on have been created about
Various rules have been added (e.g., about
Library organization has been improved (e.g., splitting out material on
Various improvement have been made, including to
The utility
The utility
The
New utilities
The
The utility
Various rules about list functions have been added or collected (e.g., rules
about
Some experiments have been added verifying rewriter-like tools using :meta-extract.
The library
Some new symbols have been imported into the
Renamed
This library have been 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.
Some new symbols have been imported into the
Some proofs have been significantly sped up.
The tools
The Std/basic books extensions in
A lightweight version of
Some
The std::deflist utility now adds
Read-string and
The Std/strings books extensions in
The recognizers of digit characters in various bases
have been renamed to have the suffix
The Std/system books extensions in
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 Std/util books extensions in
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 std::defaggregate utility has been improved to allow its calls to be local. Also, its proofs have been made more robust.
The define utility has been prevented from turning on error output if that output was already inhibited.
New functions have been added, including
A variety of term-processing utilities have been added, improved, or collected. These involve things like free variables, substitution, getting rid of various kinds of unnecessary lambdas or lambda bindings, etc. Several of the utilities have had various properties proved, including that they preserve the meaning of terms, preserve various well-formedness properties of terms, do not introduce free variables, etc. The function pre-simplify-term (previously called simplify-lambdas) combines several helpful simplifications. New books have been added about functions such as all-fnnames1, get-conjuncts, get-hyps-and-conc, etc.
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 and ‘
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
A new
New books were added about
New functions
Library organization has been improved (legacy utilities have been moved). More
utilities on untranslated terms have been added, including ones to get conjuncts
and disjuncts and to collect free variables. Support for
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.
A large number of changes have been made to this library, including adding, improving, and organizing many rules supporting Axe's symbolic execution of x86 code, especially in 64-bit mode. These include rules about flags, branch conditions, reading and writing to memory, and floating-point computations. Also added/improved were rules for introducing alternate definitions and normal forms, for the purposes of readability, compatibility with Axe, or more efficient or more predictable symbolic execution.
Utilities for generating assumptions for symbolic execution were also improved.
A great many additions to the
Improvements were made to the ELF parser and related tools, and a new
tool,
There is now XDOC support for Greek letters and more mathematical symbols. See xdoc::entities.
A
Doc topics builtin-defthms and builtin-defaxioms have been added.
A new doc topic, 100-theorems, was added to collect ACL2 proofs of theorems from the Formalizing 100 Theorems project. Several proofs of additional theorems from the list have also been added by the ACL2 community.
Support for ‘
A new build::cert_param,
The build::cert.pl tool now checks the
`The Makefile and scripts used by the Jenkins continuous integration system
were improved (especially comments and printing). The CPU load is now limited
to the value of the
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
The SEO optimized copy of the web based XDOC manual has been updated to take the `xkey` corresponding to the current page as a query parameter instead of part of the path. This allows all the pages to be ratelimited as a single page by `mod_evasive`.
Several developments have been put into more appropriate packages,
including