Release notes for the ACL2 Community Books for ACL2 8.3

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

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

A new library,

A new library,

A directory has been started to contain the implementation of
Kestrel's Axe tool. This will be populated over time as we open source Axe.
See the directory

A new library,

A new library,

A new library,

The

This is a simple proof of concept of a hierarchical deterministic wallet for cryptocurrencies, which makes use of the cryptographic, Bitcoin, and Ethereum libraries.

A new library,

A new library,

A new library,

A new library,

A new library for standard system utilities has been started.
This is currently mostly under the Kestrel books,
but it will be gradually moved directly under

A new library for standard testing utilities has been started. The
contents of the files

A new library has been added, to collect recognizers and theorems for typed alists, i.e. alists whose keys and values have specified types. This is analogous to Std/typed-lists.

Some functions have been improved slightly.

Some theorems have been added.

Added

The proof of lemma

A new transformation, `apt::casesplit`,
has been added to rephrase a function by cases.

A new transformation, `apt::isodata`,
has been added to transform data between isomorphic representations.

`apt::parteval` now provides better support
for recursive functions whose static arguments
do not change across recursive calls.
`apt::parteval` has also been extended to support untranslate specifiers.

`apt::restrict` now supports reflexive functions,
i.e. functions that occur in their termination theorem.

An input has been added to `apt::tailrec` to control whether
the wrapper function is generated or not.

A table of APT defaults has been started.
See

New APT-specific XDOC constructors have been added. Some APT-specific XDOC constructors have been extended and improved.

The inclusion of

The inclusion of

Some theorems have been added.

Verified executable attachments have been added for some of the non-executable functions in the BIP 32 formalization.

A sub-library for elliptic curves has been added, which currently contains all the secp256k1 domain parameters, and fixtypes for secp256k1 field elements, points, and keys. The parameters and the fixtypes that were previously part of the elliptic curve secp256k1 interface have been removed from that interface, which now includes the domain parameters and the fixtypes from the new sub-library.

A sub-library for ECDSA (Elliptic Curve Digital Signature Algorithm) has been added, which now contains the secp256k1 signing interface, which was previously part of the elliptic curve secp256k1 interface.

A sub-library has been added that includes formal specifications for the
SHA-2 hash functions: SHA-224, SHA-256, SHA-384, and SHA-512. The new
sub-library is in

A sub-library for KECCAK / SHA-3 hash functions has been added.

A sub-library has been added that includes formal specifications for
HMAC-SHA-256 and HMAC-SHA-512, i.e., for the HMAC keyed-hash message
authentication code, using either SHA-256 or SHA-512 as the underlying hash
function. The new sub-library is in

A sub-library for Password-Based Key Derivation Function 2 (PBKDF2)
as specified by RFC 8018, and specialized to use HMAC SHA-512,
has been added.
See `kdf::pbkdf2-hmac-sha-512`.

A sub-library has been added that includes formal specifications for
several common padding operations used in cryptography. The new
sub-library is in

A macro `crypto::definterface-hash` has been added
to introduce interfaces of hash functions.

A macro `crypto::definterface-hmac` has been added
to introduce interfaces of HMAC functions.

A macro `crypto::definterface-pbkdf2` has been added
to introduce interfaces of PBKDF2 functions.

A macro `crypto::definterface-encrypt-block` has been added
to introduce interfaces of block encryption/decryption functions.

A macro `crypto::definterface-encrypt-init` has been added
to introduce interfaces of encryption/decryption functions
that use initialization vectors
(as in certain block cipher modes of operation).

Interfaces have been introduced (via `crypto::definterface-hash`)
for the hash functions
Keccak-256, Keccak-512, RIPEMD-160, SHA-256, and SHA-512.
These supersede the previously existing placeholders
for Keccak-256, RIPEMD-160, and SHA-256, which have been removed.

Interfaces have been introduced (via `crypto::definterface-hmac`)
for the HMAC functions HMAC-SHA-256 and HMAC-SHA-512.
These supersede the previously existing placeholder
for HMAC-SHA-512, which has been removed.

Interfaces have been introduced (via `crypto::definterface-pbkdf2`)
for the PBKDF2 functions HMAC-SHA-256 and PBKDF2 HMAC-SHA-512.
These supersede the previously existing placeholder
for PBKDF2 HMAC-SHA-512, which has been removed.

Interfaces have been introduced
(via `crypto::definterface-encrypt-block`)
for the AES-128, AES-192, and AES-256 block ciphers.

Interfaces have been introduced
(via `crypto::definterface-encrypt-init`)
for the AES-128 CBC PKCS7, AES-192 CBC PKCS7, and AES-256 CBC PKCS7
ciphers (CBC mode, PKCS7 padding).

The `placeholder' for elliptic curve secp256k1 has been turned into an `interface' for elliptic curve secp256k1, consistently with the changes above. There are no more cryptographic `placeholders', but `interfaces' instead. Their structure is quite similar, but the nomenclature indicates a more permanent status.

The elliptic curve secp256k1 interface has been extended with an (abstract) signing operation.

Executable attachments have been added for the Keccak-256 interface that operates on bytes, the SHA-256 interface that operates on bytes, the HMAC-SHA-512 interface, the PBKDF2 HMAC-SHA-512 interface, the secp256k1 interface, and the secp256k1 ECDSA interface.

A function to construct signed transactions has been added.

Functions to calculate an account address from a public key and from a private key (via its public key) have been added.

Utilities for applicability conditions have been added.

XDOC constructors for documenting the implementation of event macros have been added.

More XDOC constructors for documenting event macros at the user level have been added.

The `fty::defbyte` macro has been improved
to generate additional theorems.

The `fty::defbytelist` macro has been improved
to generate additional theorems.

The `fty::defset` macro has been improved
to generate additional theorems.
It has also been extended with an option `std::deflist`,
which results in some better theorems when supplied.

A new macro `fty::deffixequiv-sk` has been added
to automate the proof of `fty::deffixequiv` theorems
for `defun-sk` (including `std::define-sk`) functions.

A new macro `fty::defflatsum` has been added
to introduce ``flat'' (i.e. not tagged) sums of disjoint types.

Changed accumulated-persistence-style profiling so that it doesn't count the frames contained in nested applications of a rule multiple times toward that rule's frame count.

The implementation of ATJ has been improved to use a more general abstract syntax and pretty-printer for Java (which are currently part of the implementation of ATJ), instead of writing directly to the output channel piecewise. This provides more flexibility, and the ability to have more code in logic mode and guard-verified.

ATJ has been extended with an option to generate Java code according to a shallow embedding approach, besides the previous deep embedding approach.

ATJ has been extended with an option to generate Java code under the assumption that the guards are always satisfied. This option should be used only with guard-verified ACL2 code and with external Java code that calls the generated Java code always with values that satisfy the guards.

ATJ has been extended with the ability to generate Java code that operates on narrower types than the one for all ACL2 values. This ability is available in the shallow embedding approach, when guards are assumed satisfied.

ATJ has been extended with the ability to generate Java code that uses Java primitive values and operations. This ability is available in the shallow embedding approach, when guards are assumed satisfied.

ATJ has been extended with the ability to generate Java code that uses Java primitive arrays and operations, and to destructively update arrays. This ability is available in the shallow embedding approach, when guards are assumed satisfied.

ATJ has been extended with the ability to generate Java loops from tail-recursive ACL2 functions. This ability is available in the shallow embedding approach, when guards are assumed satisfied.

A comprehensive tutorial on ATJ has been started.
It is available at `java::atj-tutorial`.

The return types of some of the methods that provide
native Java implementation of the ACL2 primitive functions
have been made more precise than the general type `equal`
now returns

Some of the native Java implementations of the ACL2 primitive functions have been optimized.

Variant native Java implementations of the ACL2 primitive functions have been added that operate on narrower types than the one for all ACL2 values. These are used by ATJ-generated code that operates on narrower types (see release notes about ATJ).

Native Java implementations of a few more ACL2 built-in functions have been added.

The documentation of AIJ has been extended and improved. In particular, explicit preconditions have been added for public methods, and explicit invariants have been added for non-public fields and for arguments and results of non-public methods.

A number of JUnit unit tests have been added for some of the AIJ Java code. More unit tests are planned.

An ABNF grammar has been added for the whole Java language, consisting of the lexical and syntactic sub-grammars from the Java language specification. The grammar files have been parsed with the verified ABNF grammar parser, obtaining a formal representation of the grammar of Java, which can be used to formally specify. at a very high and assured level, the concrete syntax of Java. Various properties of the thus-obtained grammar representation (e.g. closure) have been proved, for validation.

A model of Java Unicode characters has been added, along with a model of their ASCII subset.

Models have been added of the null and boolean literals, of (non-restricted and restricted) keywords, and of identifiers. The consistency of these models with the grammar (see above) has been proved.

Models have been added of the decimal, hexadecimal, octal, and binary integer literals. Abstract models have been added of the floating-point literals. Models have been added of the character and string literals.

A model of the processing of Unicode escapes has been added. This is Java's first lexical translation steps.

Models have been added of all the boolean and integer operations, as well as of all the primitive conversions on integral values. Abstract models have also been added of all the floating-point operations, as well as of all the primitive conversions involving floating-point values.

A model of (opaque) pointers has been added. A model of reference values (consisting of pointers and a null reference) has been added. A model of all values, consisting of primitive and reference values, has been added.

Note that some of the books below are not as polished as they could be.
Such books contain the text

A new book,

A new book, `declare`s .

A new book,

A new book,

A new book,

A new book, `defthm` forms.

A new book, `defun` forms.

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A new book,

A theorem about `prefixp` has been added.

A theorem has been added.

Some functions have been factored out of the file

Now, `remove-hyps` succeeds when applied to a call of `thm`
whose formula is not in the form of a valid rewrite rule.

The functions `alist-map-keys` and `alist-map-vals`
have been moved to

The function `pos-fix`,
along with its accompanying theorems and XDOC topic,
has been moved from

The function `symbol-package-name-lst`
has been moved to the Std extensions in the Kestrel Books,
under

The function `symbol-package-name-non-cl`,
originally called

The functions `organize-symbols-by-name`
and `organize-symbols-by-pkg`
has been moved to the Std extensions in the Kestrel Books,
under

A variant `mbt$` of `mbt` has been introduced,
which requires the argument to be just non-

A file `union-equal`.

The theorems about range equivalences in

A new book

A variant `str::strtok!` of `str::strtok` has been added,
which does not treat contiguous delimiters as one.
This is under the Std extensions in the Kestrel Books.

A file for lists of strings and symbols has been added.
The recognizer has been factored out of

A new book

Defret now substitutes the list of return value names for
symbols named

A new macro `defarbrec` (for `define arbitrary recursion')
has been added, to introduce recursive functions
without having to prove termination right away.
There exist similar macros in the community books,
but the specifics of this new macro are motivated for use with APT. See the `Related Tools' section
of the documentation of `defarbrec` for more information.
This macro is currently in the Std/util extensions in the Kestrel Books,
but could be moved to

A new macro `std::deffixer` has been added
that automates the definition of fixing functions,
and the generation of theorems about them,
according to a common pattern.
The macro can be extended to cover variations in the pattern if needed.
This can be used as a building block
for extending `fty::deffixtype` to generate
not only the equivalence, but also the fixer for the fixtype.
This macro is currently in the Std/util extensions in the Kestrel Books,
but could be moved to

A new macro `defiso` has been added,
to establish isomorphic mappings by verification.

A new macro `defmax-nat` has been added,
to introduce functions to return maxima of sets of natural numbers.

The tool `remove-hyps` no longer causes an error when the number of
prover steps exceeds the value of `Remove-hyps` also avoids skipping proofs, which can lead to false
``theorems''. Thanks to Stephen Westfold for reporting this issue.

Warnings have been eliminated when creating the file

The following instructions have been added to the model:

MOV moffs8, AL MOV moffs16, AX MOV moffs32, EAX MOV moffs64, RAX SHLD r/m16, r16, imm8 SHLD r/m32, r32, imm8 SHLD r/m64, r64, imm8 SHLD r/m16, r16, CL SHLD r/m32, r32, CL SHLD r/m64, r64, CL SHRD r/m16, r16, imm8 SHRD r/m32, r32, imm8 SHRD r/m64, r64, imm8 SHRD r/m16, r16, CL SHRD r/m32, r32, CL SHRD r/m64, r64, CL

The

A new generic composite constructor has been added,
namely `xdoc::ahref`.

The generic composite constructor `xdoc::seetopic`.
The previous name is still temporarily available as a synonym,
for compatibility with existing uses.

The ``defun$` or
`defwarrant`.

Modified custom makefiles

Some xdoc string processing has been made a bit more efficient.

It was possible for some web-based xdoc manual pages to be mysteriously empty due to control characters in the source documentation. It is now checked before saving a web-based manual that the :short and :long strings, when supplied, consist solely of standard characters (see standard-char-p), except that tabs are also permitted.

Supporting materials for ACL2 Workshop 2020 have been added. They are in
directory