|
|
|---|
|
|
|
|---|
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
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
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,
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 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
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
Warnings have been eliminated when creating the file
The following instructions have been added to the model:
The
A new generic composite constructor has been added, namely xdoc::ahref.
The generic composite constructor
The `
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