Release notes for the ACL2 Community Books for ACL2 8.2

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

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

Added an operation `remove-assocs`, which generalizes `remove-assoc` from single keys to lists of keys.

Started a library with placeholders for cryptographic functions that will be eventually replaced with complete specifications of those functions.

Added a macro `defmax-nat` to declaratively define the maximum of a
set of natural numbers.

Started a library of concepts and utilities to develop event macros (i.e. macros at the event level) more quickly and consistently.

This library includes some XDOC constructor utilities for the reference documentation of event macros.

This library also includes functions to process inputs common to multiple event macros.

Added a book

Formalized an instant run-off voting scheme and proved that it meets certain fairness criteria.

A library for integer arithmetic has been added at

Added a library for Java-related formalizations and tools, including:

AIJ ( **A**CL2**I**n**J**ava), a deep embedding in Java of an executable, side-effect-free, non-stobj-accessing subset of the ACL2 language without guards.ATJ ( **A**CL2**T**o**J**ava), a simple Java code generator that turns ACL2 functions into AIJ representations that are evaluated by the AIJ interpreter.- A
formalization in ACL2 of some aspects of the Java language.

Added a library for omaps (ordered maps), analogous to Std/osets.

Improved the aignet::constprop transform so that it canonicalizes inputs known to be equivalent or opposite to each other, not just to constants. Added aignet::obs-constprop that combines this with the existing observability transform, which works better than running the two transforms separately.

Slightly extended the applicability of the `apt::tailrec`
transformation, by relaxing a requirement on the function to be
transformed.

Improved and extended some documentation.

Added some XDOC constructor utilities tailored to APT transformations.

Replaced uses of `ubyte8` and `ubyte8-list` with `byte`
and `byte-list`.

Moved the previous placeholders for cryptographic functions into

Added a formalization of BIPs (Bitcoin Improvement Proposal) 32, 39, 43, and 44 for hierarchical deterministic wallets.

Improved the existing documentation.

Added fixers `unsigned-byte-fix`, `signed-byte-fix`, `unsigned-byte-list-fix`, and `signed-byte-list-fix` for `unsigned-byte-p`, `signed-byte-p`, `unsigned-byte-listp`, and
`signed-byte-listp`.

Added support for configuration objects that can be used to specify some
extended options. Also added support for

Added support for defining universal accessor and updater functions.

The files

Some theorems have been added.

Added operations to group digits in a smaller base into digits in a larger base, and vice versa, in both big-endian and little-endian.

The macro to generate additional return types for conversions from natural numbers to digits has been generalized and renamed.

A macro `defdigits` has been added, to generate specialized versions
of the conversion operations, and some theorems about them, for specific bases
and specific recognizers and fixers of (lists of) digits. Used this macro for
some library fixtypes (e.g. bits and bytes as digits in base 2 and 256
respectively).

A macro `defdigit-grouping` has been added, to generate specialized
versions of the digit grouping functions, and some theorems about them, for
specific pair of bases such that the larger base is a positive power, greater
than 1, of the smaller base. Used this macro for some library fixtypes
(e.g. to convert between bits and bytes).

Added more error-checking functions.

The files

Replaced uses of `ubyte8`, `ubyte8-list`, `ubyte4`, and
`ubyte4-list` with `byte`, `byte-list`, `nibble`, and
`nibble-list`.

Modified the formalizations of RLP encoding and decoding to return an explicit error flag. Added theorems showing that RLP encodings are decodable: RLP encoding is injective, and no valid encoding is a strict prefix of another one. Added executable RLP decoders and proved them correct with respect to the ones declaratively defined as inverses of the RLP encoders. Added the RLP tests from the Ethereum Wiki's page on RLP.

Added a formalization of hex-prefix decoding, declaratively defined as the inverse of hex-prefix encoding.

Added a formalization of Modified Merkle Patricia trees.

Added a formalization of the database that underlies Modified Merkle Patricia trees. This database is a finite map from Keccak-256 hashes (i.e. byte arrays of length 32) to byte arrays.

Added a formalization of the format of transactions and of their RLP encoding and decoding.

Added several other theorems. Improved some existing theorems.

Improved some documentation.

Moved the previous placeholders for cryptographic functions into

The filesystem books *Formalising Filesystems in the ACL2 Theorem
Prover: an Application to FAT32*, to appear in the proceedings of
ACL2-2018.

Recent improvements to the filesystem books include proofs of correctness of filesystem representation transformations in terms of invertibility, and an expanded set of POSIX system calls verified through refinement.

Added an option

Added a book

Added a book

Collected several

- A new macro
`fty::deflist-of-len`that generates fixtypes for lists of specified lengths, based on existing fixtypes of lists of arbitrary lenghts (introduced via`fty::deflist`). - A new macro
`fty::defset`that generates fixtypes for Std/osets with elements of specified fixtypes. This is analogous to`fty::deflist`and`fty::defalist`. - A new macro
`fty::defomap`that generates fixtypes foromaps with keys and values of specified fixtypes. This is analogous to `fty::deflist`and`fty::defalist`. - The
acl2::defbyte macro, which generated fixtypes and additional theorems for both bytes and lists of bytes, has been split into two macros`fty::defbyte`, which generates a fixtype and some additional theorems for bytes, and`fty::defbytelist`, which generates a fixtype and some additional theorems for lists of byte. - A new macro
`fty::deffixtype-alias`to introduce an ``alias'' of an existing fixtype, as well as of its recognizer, fixer, and equivalence. - An existing fixtype
`omap::map`foromaps with keys and values of any types. - An existing fixtype
`set::set`for Std/osets with elements of any types. - An existing fixtype
`nati`for natural numbers and infinity. - New fixtypes
`byte`,`byte-list`,`byte-list20`,`byte-list32`, and`byte-list64`for (unsigned 8-bit) bytes, true lists of bytes, and true lists of 20, 32, and 64 bytes. - New fixtypes
`nibble`and`nibble-list`for (unsigned 4-bit) nibbles and true lists of nibbles. - A new fixtype
`bit-list`for true lists of bits. - Existing fixtypes
ubyteN ,sbyteN ,ubyteN-list , andsbyteN-list for standard(ly named) fixtypes for unsigned or signed (true lists of) bytes of various sizes.

Used new ACL2 system features to fix the remaining known soundness bug and remove a trust tag.

Added some theorems about functions on lists.

Attempts to run `profile-ACL2` or `profile-all` had failed, for
ACL2 built on SBCL, with an obscure SBCL error message. Now, the error
message gives instructions for how to avoid the error by rebuilding SBCL from
sources after doing a specified edit. Thanks to Stas Boukarev for pointing to
the appropriate SBCL source code line.

In

Minor modifications of

A number of new lemmas have been added to

The `soft::defun2`, `soft::defchoose2`, `soft::defun-sk2`, and `soft::defun-inst` macros no longer include an
explicit list of function parameters. The function is implicitly
parameterized over the function variables that it depends on.

Added a function `remove-assocs`, moved from

Added some theorems about `remove-assoc-equal`, moved from

Added a recognizer `bytep` for ``standard'' (i.e. unsigned 8-bit)
bytes, moved from Std/io.

Added a recognizer `nibblep` for ``standard'' (i.e. unsigned 4-bit)
nibbles, moved from

Added new lemmas to the

Factored out the `bytep` predicate into a new file under Std/basic.

The definition of function list-fix from

The built-in function `take` has been redefined exactly along the
lines suggested by the theorem

Added macros `std::defthm-natp`, `std::defthm-unsigned-byte-p`,
and `std::defthm-signed-byte-p`, from the X86ISA model.

Added new lemmas and generalized and improved some existing lemmas.

Redefined more compactly the predicates in
`str::defcharset`. Added a new predicate.

Added functions `hexchars=>ubyte8` and `ubyte8=>hexchars` to
convert between single bytes and pairs of hexadecimal digit characters;
rephrased `ubyte8s=>hexchars` in terms of `ubyte8=>hexchars`.
Added functions `hexchars=>ubyte8s` and `hexstring=>ubyte8s`,
inverses of `ubyte8s=>hexchars` and `ubyte8s=>hexstring`.

The new utility `sublis-expr+` replaces terms by variables even
inside

Several files

The utility, `directed-untranslate`, has been improved in several
ways, including more complete handling of `mv-let`, `let*`, `b*`, `progn$`, `er`, `cw`, and `mbe`.

For the event macro `orelse*`, the default for the `orelse`.

Added utilities `macro-keyword-args` and `macro-keyword-args+`
to retrieve an alist of the keyword arguments of a macro, associated to their
default values.

The file `std::deflist` is now no longer brought in, so

The

Added a new utility, function-termhint, for creating termhints from existing function definitions containing hintcontext annotations.

Refactored the old file

Added a recognizer `bit-listp` for true lists of bits, and associated
theorems.

Finished adding support for 32-bit application-level execution for all the instructions, including the floating-point ones, supported by the model.

Added support for enabling/disabling machine features that depend on CPUID flags.

Detection of many decode-time exceptions is now done during opcode dispatch, as opposed to inside the instruction semantic functions. This not only lets us catch exceptions early, but also allows us to specify them even if the semantic functions themselves are missing.

Improved incrementing and decrementing of the stack pointer to be modular: 64, 32, or 16 bits, based on the current mode and on the SS.B bit of the current stack segment.

Modified the logical definitions of the x86 state (i.e., the abstract stobj). Now, the x86 state accessor functions unconditionally return well-formed values and the x86 state updater functions return a well-formed state, provided that the initial state was well-formed; thus, constraints on the index (in case of array fields) and value being written have been eliminated.

Improved the

Extended top-level memory reading functions to take into account the R bit of code segment descriptors, when they access for reading (not execution) a code segment in 32-bit mode: in this case, if R = 0, the code segment is execute-only and thus reading data from it is not allowed. Extended top-level memory functions to take into account the W bit of data segment descriptors, in 32-bit mode: if W = 0, the data segment is read-only and thus writing data to it is not allowed; writing to a code segment is not allowed either.

Opcode maps are now represented using fty::defprods, which makes it easier to operate on them in order to automatically generate dispatch functions and documentation, and to precompute some kinds of decoding information.

Extended effective-to-linear address translation to check that the visible part of the DS, ES, FS, and GS segment registers does not contain a null segment selector. A similar check on CS and SS is not needed because a null segment selector cannot be loaded into these two segment registers.

Improved the `PUSH segment register' instruction to handle a 32-bit operand size as in modern processors: instead of zero-extending the 16-bit content of the segment register to 32 bits, now the model writes the low 16 bits, leaving the high 16 bits unchanged.

Extended `x86isa::select-operand-size` to accommodate instructions
that do not follow the ``normal'' rules. The extended function has additional
parameters, whose different values trigger the use of the non-``normal''
rules. Now many more instructions use this function, avoiding repeated blocks
of identical codes in their semantic functions.

Improved and extended some documentation.

Improved the

Introduced several additional constructors.

Extended the documentation of the constructors.

Moved the constructors to

Added a feature to

Added utilities ifdef-define and ifdef-undefine in

Cleaned up the Perl scripts implementing

We now avoid causing an error when building the manual in the case that the