Note-8-1-books
Release notes for the ACL2 Community Books for ACL2 8.1
The following is a brief summary of changes made to the community-books between the releases of ACL2 8.0 and 8.1.
See also note-8-1 for the changes made to ACL2 itself. For
additional details, you may also see the raw commit log.
New Libraries
A new regular expression library, acre::acre, is available in
books/centaur/acre/. Compared to the implementation in
projects/regex, this version's features are less similar to GNU grep and
somewhat more similar to Perl regular expressions. However, it does not aim
to be fully compatible, but to have a well-defined set of features with clean
code that can be easily extended and behaves predictably (as much as possible,
for regular expressions).
Added PLTP(A), The Pure Lisp Theorem Prover, reimplemented in ACL2. An
ACL2 reconstruction of the 1973 Pure Lisp Theorem Prover (PLTP), the original
``Boyer-Moore theorem prover'' after which both NQTHM and ACL2 were modeled,
is available in books/projects/pltpa/pltpa.lisp. More importantly, a PLTP
archive has been set up. That archive includes much original source
material (e.g., scanned images of the 1973 POP-2 implementation of PLTP) as
well as an extensive discussion of the differences between PLTP and PLTP(A),
and an OCaml version of PLTP, named PLTA(O), by Grant Passmore.
A new directory, books/projects/arm/, contains proofs of correctness
of the Floating-point operations of addition, multiplication, fused
multiply-add, division, and square root, as implemented in the FPU of an Arm
Cortex-A class high-end processor.
Added utility include-book-paths to list paths via include-book down to a given book, which may be useful for reducing book
dependencies.
Added utility apply-fn-if-known to apply a function that might not
exist; even the package for the function symbol might not exist.
Added a fixer integer-range-fix for integer-range-p, as
well as a recognizer integer-range-listp and and a fixer integer-range-list-fix for true lists of integer-range-p, all with
accompanying theorems.
Added a library to convert
between natural numbers and their representations as lists of digits in
arbitrary bases in big-endian and little-endian order. Digits are natural
numbers below the base. There are variants for minimum-length,
non-zero-minimum-length, and specified-length lists of digits. The library
includes, among others, theorems stating that the number-to-digits and
digits-to-number conversions are mutual inverses in a suitable sense.
Added a new utility, skip-in-book, that wraps around a form to
prevent its evaluation during book certification or inclusion.
The new utility defthm<w will attempt to prove a theorem directly
from previously-proved theorems. It does this by generating suitable hints using the new utility, previous-subsumer-hints.
Added some utilities for building XDOC documentation. The XDOC constructors are utilities to
construct well-tagged XDOC strings via ACL2 function calls whose nesting
structure mirrors the nesting of the XML. defxdoc+ extends defxdoc with additional conveniences.
A new event, defunt, is a variant of defun that uses
termination theorems from a large set of community-books —
namely, all books included in books/doc/top.lisp, which is the book that
creates the ACL2+Books manual — to generate termination proofs
automatically. Those proofs use :termination-theorem lemma-instances that reference defun events in those included books.
Several new supporting utilities are documented: fms!-lst, which
writes a list to a character output channel; injections, which lists
all maps from a domain to a range; strict-merge-sort-<, which sorts without
duplicates; and subsetp-eq-linear, which is a linear-time subset test
for sorted lists of symbols.
Added a new macro defbyte for introducing fixtypes for unsigned and
signed bytes of specified sizes, as well as fixtypes of lists of such bytes,
along with theorems relating the fixtype recognizers to the built-in binary
predicates unsigned-byte-p and signed-byte-p and to the
library binary predicates unsigned-byte-listp and signed-byte-listp.
Started a new library for Ethereum.
Started a new library for Bitcoin.
A new book, clause-processors/bindinglist.lisp, supports a meta-level
structure for a list of bindings of variables to values, with functions that
convert these to and from nests of lambdas and proofs that establish these
functions' semantics with respect to an evaluator.
Changes to Existing Libraries
The behavior and code for the expander (see defthm?) have been
improved in a few ways (some of them technical), as follows.
- A bug has been fixed that was preventing hints from being passed to
the forcing round (if any). An example may be found in the new book,
misc/expander-tests.lisp.
- The deprecated fmt directives ~p and ~q have been
replaced by ~x and ~y, respectively.
- Error messages have been improved for the function simplify-hyps when
there is a contradiction.
- The state globals tool2-result and tool2-error are no
longer set. (They appear to have been unused.)
- The functions tool2-fn, tool2-fn-lst, and simplify-hyps now
have a new final argument, ctx. Also, the macro tool2 now has a
:ctx keyword argument.
Updated the ACL2+books manual to accommodate the replacement of David
Russinoff's online rtl manual by his upcoming Springer book.
Improved install-not-normalized to handle cases in which
recursively-defined functions have non-recursive normalized definitions.
The misc/assert.lisp book no longer includes misc/eval.lisp,
since tests about the misc/assert.lisp utilities are now in a separate
book misc/assert-tests.lisp.
The misc/eval.lisp utilities ensure-error, ensure-soft-error, ensure-hard-error, thm?, and not-thm? have been renamed to must-fail-with-error, must-fail-with-soft-error, must-fail-with-hard-error, must-prove, and must-not-prove. The old names are still available as
deprecated synonyms, which will be removed in one of the next releases.
The old directory books/projects/masc/ has been replaced by the bew
directorybooks/projects/rac/. The reason is that our RTL modeling
language now uses the register class templates of Algorithm C instead of those
of SystemC, so the name Modeling Algorithms in SystemC now makes even
less sense than it did; the best we could come up with as a replacement is
Restricted Algorithmic C.
The utility make-flag has a new keyword argument, :last-body,
to specify using the most recent definition rule for a function symbol
instead of its original definition.
Extended and simplified the defun-sk query utilities. The utilities now
handle the recently introduced :constrain option. The utilities no
longer build a record with all the information about the defun-sk
function (whose fields can then be accessed); instead, now the utilities
retrieve the various pieces of information directly.
Extended the defchoose query
utilities with a recognizer for symbols that name defchoose
functions.
Made several improvements to directed-untranslate, including: avoid
assertion errors that could occur when using declare forms with let, let*, or mv-let expressions: enhance insertion of
appropriate mv calls; extend dropping of unused let bindings;
avoid an assertion error with mv-let expressions; and preserve basic uses
of b*.
Removed the keywords-of-keyword-value-list utility, because it is
subsumed by the built-in evens utility.
Extended the error-checking
utilities with several error-checking functions.
Extended the Kestrel world query utilities with functions to collect the
names of all the known packages in the ACL2 world and to check if a
function is primitive.
Extended the term
function recognizers with recognizers for true lists of
(pseudo-)lambda-expressions and (pseudo-)term-functions.
Extended the Kestrel term utilities with operations to substitute function
symbols without performing simplification, to construct terms that are
functions applications of certain forms, to collect all the lambda expressions
in terms, and to collect all the package names in (symbols in) terms.
The utility install-not-normalized-event now includes option
:allp nil in the generated install-not-normalized event. The new
utility, install-not-normalized-event-lst, can thus handle mutual-recursion nicely, e.g.: (install-not-normalized-event-lst (getpropc
'f1 'recursivep nil) nil nil (w state)). Also, added new utility install-not-normalized$ to submit the event generated by install-not-normalized-event.
Extended the oset utilities
with a fixtype for osets.
Added some theorems about lists
of natural numbers.
Added a theorem about lists of strings.
Merged the utilities in kestrel/utilities/characters.lisp into
the string utilities. Extended the
combined utilities with some theorems about the pre-existing functions and
with new functions to check if (lists of) characters are all of specified
kinds, to convert a list of unsigned 8-bit bytes to a corresponding list or
string of hex digit characters. Refactored all the old and new utilities into
separate files to reduce dependencies.
Extended the Kestrel symbol utilities with a utility that lifts symbol-package-name to lists.
Moved maybe-msgp under newly created message utilities. Extended these utilities with a
recognizer of true lists of messages.
Moved msg-downcase-first and msg-upcase-first from the string utilities to the message utilities.
A new book, kestrel/utilities/proof-builder-macros.lisp, is a place to
define proof-builder macros. This book currently defines a simple
macro, when-not-proved (see ACL2-pc::when-not-proved), for
skipping instructions when all goals have been proved. It also defines two
(more complex) macros, prove-guard (see ACL2-pc::prove-guard) and
prove-termination (see ACL2-pc::prove-termination), for
(respectively) using previously-proved guard or termination theorems
efficiently, as well as a more general macro, ACL2-pc::fancy-use, for
using lemma instances (via :use) efficiently.
Improved the copy-def utility (community book
kestrel/utilities/copy-def.lisp) in several ways: added an :expand
hint in the recursive case (as is sometimes necessary), improved it to work
better with mutual-recursion, and improved it to work better with an
:equiv argument.
Fixed the utility, orelse, so that :quiet t pushes the output
stack, as per existing documentation.
Fixed a few books that broke due to the change in defevaluator (see
note-8-1 for details).
SOFT
Added a :print option to control screen output.
Improved user input validation.
Added support for the new :constrain option of defun-sk. This
option is now supported by SOFT's soft::defun-sk2 and soft::defun-inst macros.
X86ISA
Most of the model has been extended to 32-bit mode. The only instructions
that remain to be extended to 32-bit mode are JMP far and the floating-point
instructions. The 32-bit-only instructions PUSHA, POPA, INC with opcodes
40h-47h, DEC with opcodes 48h-4Fh, and PUSH CS/SS/DS/ES have been added to the
model. Support for the kinds of paging in 32-bit mode is still missing, but
this is only needed for the system view of the model, not the application
view.
Some of the XDOC documentation and some of the comments have been slightly
expanded.
The notion of programmer-level mode and system-level mode have been renamed
to `application-level view' and `system-level view', to avoid overloading the
word `mode', which in the x86 has a more specific meaning. Similarly, the
notion of page structure marking mode has been renamed `marking view'. This
involved renaming the programmer-level-mode and
page-structure-marking-mode field of the state stobj to the shorter
app-view and marking-view, and also renaming some functions and
theorems acccordingly.
The instruction decoder has been extended to detect VEX- and EVEX-encoded
(AVX, AVX2, AVX512) instructions, in both 64- and 32-bit modes of operation.
However, semantic functions of many of these instructions are still
unimplemented.
Annotated opcode maps are now used to generate opcode dispatch functions
and instruction coverage information.
APT
Improved documentation.
Improved options to control the screen output.
Improved apt::tailrec transformation with an option to attempt to
automatically infer the domain for some of the transformation's applicability
conditions.
Improved apt::restrict transformation to wrap the restriction test
with mbt; added an applicability condition to ensure that the
restriction test is boolean-valued.
Imported more symbols from the "ACL2" package into the "APT"
package.
Bitops
Added the bitops::sparseint library, which represents large integers
as balanced binary trees, which can save memory by sharing structure among many
such objects.
SV
Improved scalability of several SV utilities when large variables are present
by recoding several functions that previously used Lisp bignums to use a
bitops::sparseint based encoding.
GL
Added optional accumulated-persistence-style profiling of attempted rule
applications, available with keyword argument :prof-enabledp t.
Changed the representation of symbolic objects, removing the :g-number
form which could represent complex rationals and replacing it with a simpler
:g-integer form. (Complex rationals may still be supported using
rewriting. Also, the :g-number shape specifier is still supported for
backward compatibility, though it is restricted to only represent integers and
translates directly into :g-integer symbolic objects.) Removed some
native symbolic counterparts for functions that can be dealt with more cleanly
via rewrite rules.
GLMC
Added option to bind some variables that can be used by the nextstate, property,
constraint, and initstate terms. These bindings will be symbolically evaluated once,
which can perhaps improve performance by not requiring them to be repeated.
Xdoc
Added a utility, xdoc::archive-xdoc, that saves the documentation
generated by a series of local events, partially preprocessing it to avoid
references to definitions that might only be locally available.
The defpointer utility for xdoc now accepts names that have
special characters such as <.
STD
The std/typed-lists/unsigned-byte-listp.lisp book now includes
std/lists/take locally. As a result,
projects/x86isa/tools/execution/exec-loaders/mach-o/mach-o-reader.lisp,
std/io/take-bytes.lisp, unicode/read-utf8.lisp, and
unicode/utf8-decode.lisp also include this book locally.
Licensing Changes
Build System Updates
The build system now has support for ifdef and ifndef, which
are make-event-supported macros defined in books/build/ifdef.lisp.
In particular, this allows the community books' makefile to support building
different versions of the manual depending what external tools are
installed.
Testing
Miscellaneous
A BibTeX file has been added to the community books, containing reference
information for papers published at the ACL2 Workshops. This may be useful to
you if you wish to cite such a paper in a LaTeX document. It is available at
books/workshops/references/. That directory also contains an example
LaTeX file demonstrating how the references may be cited, as well as a README
with some more information.
A Developer's Guide (see developers-guide) has been added, to assist
those who may wish to become ACL2 Developers. It replaces the much smaller
``system-development'' topic.
The download button now works in the web-based manual.
When the include-raw utility with option :do-not-compile t was
followed by :comp, it was possible for that subsequent
compilation to overwrite intended raw Lisp definitions, for a host Lisp that
does not compile on-the-fly (i.e., for a host Lisp other than CCL or SBCL).
The way to prevent such overwrites is to extend state globals
program-fns-with-raw-code and logic-fns-with-raw-code, which however
was not always done. This is now done automatically, which fixes the
overwrite problem.
