|
|
|---|
|
|
|
|---|
Release notes for the ACL2 Community Books for ACL2 8.4
The following is a brief summary of changes made to the community-books between the releases of ACL2 8.3 and 8.4.
See also note-8-4 for the changes made to ACL2 itself. For additional details, you may also see the raw commit log.
A library to support reasoning about programs that use ACL2
arrays (e.g., those satisfying array1p). Includes operations that make
such arrays exapandable. Includes a tool for defining typed ACL2 arrays. See
This is a library about the ACL2 programming language. It includes a formalization of its evaluation semantics. (This is just the work of this library's author, not an official semantics of the ACL2 programming language; see evaluation for an official description of the ACL2 evaluation semantics.)
A library has been started to collect algorithm schemes, starting
with a scheme for a generic tail recursive function. See
A formalization of two-dimensional arrays as lists of lists (both
with arbitrary elements and with elements that are known to be bit-
vectors). See
A library that defines a
This is a library about the C language. It contains a formalization of (some aspects of) the C language and ATC (`ACL2 To C'), a C code generator for ACL2.
This is a proof-generating C code generator for ACL2. Besides the C code, it also generates proofs (i.e. ACL2 theorems) asserting the correctness of the C code.
This currently covers a relatively limited subset of ACL2 and C. The coverage is being extended.
This currently covers just character sets, bytes, and keywords. The coverage is being extended.
A preliminary formalization of the static and dynamic semantics of a subset of C can be found as part of ATC. Some of that material may be moved here in the future.
This is a library to support proofs in the style of Isabelle's Isar (Intelligent Semi-Automated Reasoning) language. It is just a small step in that direction for now.
This is a library about JSON.
It currently contains an initial abstract syntax of JSON,
consisting of fixtypes;
it also contains some initial operations on this abstract syntax,
as well as a translator from the output of the parser at
A JSON parser implemented in ACL2, including Unicode support. See
Kestrel's model of the Java Virtual Machine, including support for
code proofs and lifting. Works with Kestrel's Axe toolkit. Also includes a
class file parser. See
A library about number theory, dealing with notions like
primality, divisibility, quadratic residues, etc. Includes the defprime and
defprime-alias tools to introduce standard reasoning machinery about
primes. Includes a proof of the Tonelli-Shanks Modular Square Root Algorithm.
See
This is a library that represents bags (a.k.a. multisets) as non-strictly-ordered lists. Thus, they capture (up to isomorphism) the mathematical notion of bag; in particular, bag equality is equal.
This is analogous to the library of ordered sets and to the library of ordered maps.
This is a library that formally specifies and implements the Minimal Multiplicative Complexity (MiMC) hash function as used by Ethereum's Semaphore. This is currently under the cryptographic library.
This is a library that introduces and formalizes the notion of PFCS (Prime Field Constraint Systems), which generalize R1CS and possibly other constraint systems for zero-knowledge proofs. This is currently under the cryptographic library.
A lightweight library containing some simple random number
generators. See
This library can be used to read in sections of ELF/Mach-O files into ACL2. An older version of these books used to live in the x86isa library.
A library for defining higher-order operations over lists (defforall,
defexists, defmap, and deffilter). See
This is a library about a simple programming language, called Imp, found (with small variations) in a variety of didactic resources. This library formalizes syntax and semantics of this language, and provides a program-mode interpreter of Imp programs. This library may be extended with examples of formal verification of Imp programs in ACL2.
This is a library about the Solidity language for Ethereum smart contracts. It includes a formalization of some aspects of the language. There are plans to extend this to cover more aspects.
A lightweight library about strings, including changing case,
splitting strings and character lists, etc. See
A lightweight library of operations on terms (e.g., finding free
and bound vars and applying variable substitutions). See
A lightweight library dealing with lists of objects of particular
types (rather than lists in general). For example, lists of integers, of
symbols, of pseudo-terms, etc. See
A lightweight library about Unicode, dealing with UTF-8 encoding and
UTF-16 surrogate code points. See
A new library for manipulating untranslated terms, which allows
structure to be maintained that would be lost by translation. See
This library contains Kestrel's x86 proof machinery, which complements the
X86ISA model. This library focuses on readability of proof terms and
supporting the lifting of x86 code into logic with the Axe toolkit. It also
includes parsers for PE and Mach-O executables. See
This is a library about the Yul intermediate language, currently used in the Ethereum Solidity compiler but designed for more general use. This library includes a formalization of some aspects of the language. There are plans to extend this to cover more aspects.
This is a library about the Zcash blockchain, which is based on zero-knowledge proofs.
The proofs of correctness of the grammar parser have been moved to a separate file, so that including the parser does not necessarily also includes the proofs, and so that book certification can be faster.
A new file and XDOC topic has been started to collect parsing primitives, i.e. parsing functions from the ABNF grammar parser that are more generally useful than that parser. These parsing primitives may be useful to write parsers for other languages specified by ABNF grammars (besides ABNF itself, which is what the grammar parser does).
New rules and books have been added, including books on
An APT defaults table has been added, analogous to the ACL2 defaults table but specific to APT. Utilities to set and retrieve a number of defaults have also been added.
Some XDOC constructors have been added, and others have been improved. See xdoc::apt-constructors.
Some input processors have been added, and others have been improved. See apt::input-processors.
A new transformation has been added: apt::schemalg, the `schematic algorithm transformation'. This transformation applies algorithm schemas to non-executable specifications: given a functional specification (e.g. consisting of an input/output relation, possibly as a precondition and postcondition), this transformation partially determines the solution and generates sub-specifications that, once recursively solve, provide a solution to the initial specification. In particular, divide-and-conquer algorithm schemas are supported: the schema is a recursive function that decompose the input, solve the sub-input(s), and composes the sub-output(s) to obtain an output. This schematic algorithm transformation is currently realized using SOFT to represent specifications and algorithm schemas, with specifications as second-order functions and refinement as backward implication, as described in the ACL2-2015 Workshop paper on SOFT. In the future, this transformation may be extended to represent specifications and algorithm schemas via the built-in apply$.
A new transformation has been added: apt::solve, the `solving transformation'. This attempts to directly solve a program synthesis problem, expressed as a constraint problem, via inference methods like rewriting, SMT solving, SAT solving, etc. Currently two rewriting methods are supported, along with a manual method in which the solution is supplied (which still automates some event and proof generation); support for more methods will be added.
A new transformation has been added: apt::expdata, the `expanded data transformation'. This can realize data type refinements where each instance of the old data may be represented by multiple instances of the new data, according to a surjective mapping from the new to the old data. These are more general data type refinements than apt::isodata, but the transformation is not inherently reversible (e.g. for raising the level of abstraction in program analysis).
The apt::propagate-iso transformation has been added.
A new transformation has been added: apt::simplify, the `simplification transformation'. It transforms a given definition or term using ACL2 reasoning, in particular by applying the currently (or specified) enabled rewrite rules. The result is generally simpler than the input but logically equivalent to it.
The apt::isodata transformation has been improved as follows:
The apt::restrict transformation has been improved as follows:
The apt::tailrec transformation has been improved as follows:
A file
New design notes about specifications and refinements have been added, along with a manual page that describes various forms of specifications.
A variety of APT-related utilities have been added, including
Many new rules and books have been added, including books on
Major additions have been made to the open-source Axe toolkit,
which now includes most of Axe. The library now includes Axe's connection
to the STP solver as well as machinery to make customized Axe rewriters and
provers. A basic (general-purpose) prover and rewriter are included, as are
a legacy prover and rewriter. Utilities to unroll specifications through
rewriting are included, as is the Axe Tactic Prover. Many rules that have
been useful in Axe proofs are also included. See
A toolkit for using Axe to reason about JVM code has been added.
It includes utilities to lift JVM code into logic. A Formal Unit Tester
tool is also included, to support small solver-backed proofs about bounded
executions of programs. See
A toolkit for using Axe to reason about x86 code has been added.
It includes utilities to lift x86 code into logic. See
A toolkit for using Axe to reason about R1CSes has been added. It
includes utilities to lift R1CSes into logic and verify them. See
New rules and defcongs have been added. See
Extensive additions have been made, including over 1000 new rules. Books
have been added covering many more BV operations, including subtraction,
arithmetic negation, multiplicaton, shifts, bitwise
Many new rules and books have been added. New books
include ones about
Formal specifications of the BLAKE2s, BLAKE2s-extended, and
BLAKE-256 hash functions have been added. See
The formalization of short Weierstrass curves has been extended and improved.
A formalization of twisted Edwards curves has been added.
A formalization of Montgomery curves has been added.
A formalization of the birational equivalence between Montgomery and twisted Edwards curves has been added.
The file
A formalization of the Edwards BLS12 elliptic curve has been added.
A formal semantics for rank-1 constraint systems (R1CSes) has been added. These are often used by zero-knowledge proofs. Extensive reasoning support for reasoning about R1CSes has also been added, including verified R1CS gadgets and support for applying the Axe toolkit.
This library is being moved
from
Some theorems about hex-prefix encoding have been added.
A sub-library for the Semaphore gadget has been added. This includes various specifications and proofs of Semaphore-related R1CSes, including a mixing function from BLAKE2s and 3 variants of the MiMC hash function. It also includes Semaphore-specialized Axe tools to lift R1CSes into logic and verify them.
The utilities
cw-event,
fail-event,
make-event-terse, and
try-event
have been moved here
from
The XDOC constructor
The XDOC constructor xdoc::evmac-topic-event-generation has been extended with an additional option.
New XDOC constructors have been added and some XDOC constructors have been improve.
A utility evmac-prepare-proofs has been added, to improve the robustness of proofs generated by event macros.
Utilities have been added to generate various kinds of event forms from attributes of the event forms.
Some general XDOC topics about event macros have been added, which can be referenced by the user documentation of event macros.
ELF reader now gets the contents of all the sections listed in
the headers of a given ELF binary. Also, the package name has been
changed from
Various lightweight utilities have been added to read and write files (of
bytes, characters, and objects). These include a utility to read the bytes
of a file into a stobj array. Reasoning support has also been added for
various built-in I/O functions. Related utilities have been added, such as
to check whether a file exists or is newer than a given date. See
A new macro fty::defbyte-ihs-theorems has been added
to generate theorems about fixtypes introduced via fty::defbyte
and functions in the IHS library.
This macro has been used to generate, and make available,
these theorems for some of the
More
The macro fty::defset has been improved to generate additional theorems.
The macro fty::defomap has been improved to generate additional theorems.
A fixtype nat-set of osets of natural numbers has been added.
fty::deflist has been extended to generate a theorem about the list fixer applied to repeat.
A macro fty::defsubtype has been added.
A macro fty::defunit has been added.
More JUnit unit tests have been added, integrated with the IntelliJ IDEA project.
The Java implementations of some natively implemented ACL2 functions have been optimized.
Variant Java implementations of some natively implemented ACL2 functions have been added, in support of the automatic mapping, in the shallow embedding with guards, of ACL2 booleans and characters to Java booleans and characters.
A native implementation has been added of the char ACL2 built-in function. As with other native implementations, this consists of a few variants for different input and output types. This native Java implementation is faster than the Java code obtained from the unnormalized body of char, which converts the string to a list of characters and then calls nth; the native Java implementation accesses the string directly.
The model of Java primitive arrays has been extended with functions to convert between arrays and corresponding ACL2 lists. The model has been made much more compact by defining and using a macro that captures the structure common to the eight Java primitive array types.
Support has been added to recognize ACL2 functions that convert between Java primitive arrays and ACL2 lists, and translate them to Java code that converts between arrays and lists. This applies to the shallow embedding with guards.
In the shallow embedding with guards,
now ACL2 booleans are mapped to Java booleans when possible.
The generated Java code takes care of converting, as needed,
between the Java booleans
and the
In the shallow embedding with guards,
now ACL2 characters are mapped to Java characters when possible.
The generated Java code takes care of converting, as needed,
between the Java characters
and the
In the shallow embedding with guards,
now ACL2 strings are mapped to Java strings when possible.
The generated Java code takes care of converting, as needed,
between the Java strings (i.e.
Some of the generated Java code in the shallow embedding with guards
has been made more idiomatic.
Calls of the Java method corresponding to not
are now avoided in favor of using Java's
A new post-translation step has been added to ``inline'' (in a suitable sense) the calls of the array write methods that are generated by the translation step. This makes the generated Java code more idiomatic. This applies to the shallow embedding with guards.
A new post-translation step has been added to simplify generated Java conditional expressions whose test is a boolean literal.
The Java code to build the ACL2 environment is now generated
in a separate Java class in a separate Java file.
This class's name is obtained by adding
The Java abstract syntax used by the code generator is now more precise, in the sense that it captures more syntactic aspects of Java.
ATJ function types have been verified and recorded for more built-in functions, thus avoiding certain type casts and other conversions in the generated Java code. ATJ function types have also been verified and recorded for certain library functions, for the same reason; these files can be included as needed.
The macros java::atj-main-function-type and java::atj-other-function-type have been extended with an option to provide hints for the theorems they prove internally.
An option
Some functions and theorems related to integer literals have been added. These are part of the formalized abstract syntax of Java.
Some theorems about the Java primitive operations have been added.
More aspects of the Java syntax have been formalized, including: the ISO 8851-1 subset of Unicode characters; type identifiers; unqualified method identifiers; package names; reference types; and all types.
The formalization, including the ABNF grammar,
have been updated to Java 14.
In particular, this involved updating of the ABNF grammar with
A library wrapper for
Many rules, congruences, and new books have been added. New books cover
the functions
Added an operation to create an omap from a list of keys and a corresponding list of values.
Many new rules have been added, and existing rules have been improved.
These include many rules for recogizing R1CS gadgets. The library is more
organized, and some proofs have been made faster.
Add support for defining fields based off child stobjs.
A new macro soft::defsoft has been added, to record a function as second-order after the function has been introduced via a non-SOFT event. The SOFT macros soft::defun2, soft::defchoose2, and soft::defun-sk2 have been simplified to be abbreviations of defun, defchoose, and defun-sk followed by soft::defsoft.
New macros
A new macro soft::defequal, to define second-order equalities between functions and provide some reasoning support for them.
An option
An option
A new utility good-valuep has been added, which checks whether a value is either a good atom or a cons pair whose components are recursively good values. That is, the value must not be a bad arom or contains (directly or indirectly) bad atoms.
A new utility good-pseudo-termp has been added, which checks whether a pseudo-term only contains good values (see good-valuep) in its quoted constants.
Modified the raw-Lisp implementation of read-string to catch errors successfully, as intended. This could fail in SBCL 2.0.5 (implementation note: because the error message referenced a string stream that was already closed).
A new utility check-if-call has been added, to check if a term is a call of if and to return its three arguments if that is the case.
A new utility check-and-call has been added, to check if a term is a (translated) call of and and to return its two conjuncts if that is the case.
A new utility check-or-call has been added, to check if a term is a (translated) call of or and to return its two disjuncts if that is the case.
A new utility check-mbt-call has been added, to check if a term is a (translated) call of mbt and to return its argument if that is the case.
A new utility check-mbt$-call has been added, to check if a term is a (translated) call of mbt$ and to return its argument if that is the case.
A theorem about the built-in
A new utility fresh-name-listp-msg-weak has been added, which lifts fresh-namep-msg-weak to lists.
The utility check-mv-let-call has been generalized to check for the presence of hide wrappers introduced when mv-let has ignore declarations, and to return information about their presence or absence.
The utilities install-not-normalized-event and install-not-normalized-event-lst have been improved to return an additional result, namely the updated list of names to avoid. This helps making the calling code more concise and less error-prone.
The utility install-not-normalized now uses the untranslated version of the original body in the generated definition.
A new utility if-tree-leaf-terms has been added, to collect the leaf sub-terms of a term according to the if tree structure of the term.
The utility
New utilities irrelevant-formals-info and chk-irrelevant-formals-ok have been added, to perform an irrelevant-formals check on a given definition or list of definitions.
New utilities have been added to find the sources of invariant-risk
for given functions. See
The contents of the file
The relocation stub
The event macros assert! and assert!-stobj no longer invoke make-event, but rather, create direct calls of assert-event.
A type symbol-symbollist-alistp has been added for alists from symbols to true lists of symbols.
A new event macro defund-sk has been added,
which is like defun-sk but it disables
(1) the function definition (if
A new event macro defmacro+ has been added, with is like defmacro but with XDOCintegration.
Like defun-nx, now define also disables the executable counterpart of a non-executable function.
A new event macro defmapping has been added, to verify and record mappings that must be (based on supplied options) injective, surjective, or bijective.
The defiso event macro is now a specialization of defmapping, implemented as a thin wrapper of defmapping.
A new event macro definj has been added to verify and record injective mappings. It is a specialization of defmapping, implemented as a thin wrapper of defmapping.
A new event macro defsurj has been added to verify and record surjective mappings. It is a specialization of defmapping, implemented as a thin wrapper of defmapping.
A new event macro defthm-commutative has been added, to generate commutativity theorems for binary operations more concisely.
Support for
Support for defun-sk's option
A macro std::tuple has been added, to mimic the mv return specifier notation for tuple (i.e. list) results, useful inside error triples.
The macro std::define-sk has been moved
from
A new event macro add-io-pairs has been added, to speed up a function using verified input-output pairs. Related utilities include add-io-pair, remove-io-pairs, show-io-pairs, and get-io-pairs.
A new event macro defmin-int has been added, to declarative define the minimum of a (possibly infinite) set of integers. This is similar to defmax-nat.
A large number of utilities have been added, covering a wide range of
topics. These include dealing with event forms, making fresh names,
manipulating hints, dealing with untranslated terms, building simple list
structures, dealing with quoted entities, building strings, checking
whether a symbol has properties, dealing with runes, parsing options,
processing keyword args, and recognizing legal variable names.
New utilities also deal with importing and legal variable names, format
strings, printing, translation, manipulating terms, invariant risk,
submitting events to ACL2, creating temp dirs, process IDs, usernames,
calling scripts, macroexpansion and translation, asserts,
untranslated-terms, redundant events, guard-holders, ruler-extenders,
lets/lambdas, fake worlds, clause identifiers,
Various improvements have been made to
New utilities support computing a constant using
A new ACL2 Lint tool can detect common ACL2 errors.
Reasoning about I/O channels has been improved.
A new tool,
A new data structure, string trees, can efficiently represent a sequence of strings (e.g., for writing to a file).
A new tool supports polarity-based rewriting, whereby a term can be either strengthened or weakened depending on whether it is an assumption or a conclusion.
Sorting utilities have been added, including
Various xdoc-related utilities have been added, including new xdoc
constructors (such as one that creates paragraphs from blocks of text
separated by blank lines). A new tool,
See
The web-based manual now includes a clickable link to GitHub at the top of each documentation topic from the Community Books. The link lets you view the contents of the source file that introduced that topic.
The file
By default,
One line of file
Building of the combined ACL2+Books manual (by certifying
The line containing
The book
See rewrite$ for a flexible, convenient interface to the ACL2 rewriter that can be called programmatically. See rewrite$-hyps for a related utility that rewrites a list of hypotheses.
See open-trace-file! for a variant of open-trace-file suitable for use within make-event.
There are some changes in the utility make-flag (descibed in more
detail in its documentation). (1) The value for keyword argument
The utility install-not-normalized now takes an additional keyword
argument,