|
|
|---|
|
|
|
|---|
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:
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
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
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
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
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
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