Note-8-0-books
Release notes for the ACL2 Community Books for ACL2 8.0
The following is a brief summary of changes made to the community-books between the releases of ACL2 7.4 and 8.0.
See also note-8-0 for the changes made to ACL2 itself. For
additional details, you may also see the raw commit log.
New Libraries
Supporting materials for the 2017 ACL2 Workshop
See the new directory, workshops/2017/ — specifically, its
README file.
SAT proof-checker for cube-and-conquer
The new directory is projects/sat/lrat/cube/. See file README in
that directory.
SAT proof-checker from 2011
An early SAT proof-checker based on resolution may be found in directory
books/projects/sat/zz-resolution-checker/; see the README in that
directory. It was sufficiently efficient to get limited use in industry, but
ultimately was superseded by much more efficient clause-based
proof-checking (see directory books/projects/sat/lrat/).
EDIF conversion
See projects/async/tools/convert-edif.lisp for tools to convert
between EDIF format and corresponding convenient s-expressions.
try-gl-concls
See try-gl-concls for a small but convenient utility to
find all the true conclusions (if any) from a user-provided list of
possible conclusions using gl.
GLMC
GLMC (in directory centaur/glmc) is a connection from ACL2 to
AIG-based hardware model checkers, via gl; this can be used to
prove safety properties without finding an inductive invariant. See gl::glmc for details.
Truth
Directory centaur/truth contains a library for using integers as a
representation for Boolean functions with small (single-digit) numbers of
variables, expressing the functions as truth tables. Truth tables for 5 or
fewer variables are especially efficient since the formulas are represented as
fixnums (at least in 64-bit lisps).
Ipasir
The ipasir::ipasir library (in directory centaur/ipasir)
contains an axiomatized interface for using incremental SAT solver libraries in
ACL2. A solver object is represented as an abstract stobj, and actual solver
functions from a suitable shared library can be called as the implementation.
Integration with aignet is also provided in the book
centaur/aignet/ipasir.
ABNF
The ABNF (Augmented Backus-Naur Form)
library provides (1) a formalization of the syntax and semantics of the
ABNF notation, (2) a verified parser that turns ABNF grammar text (e.g. from
the HTTP RFC) into a formal representation suitable for formal
specification (e.g. for HTTP parsing), and (3) executable operations on ABNF
grammars, e.g. to check their well-formedness and to compose them.
APT
The APT (Automated Program Transformations)
library provides tools to transform programs and program specifications
with automated support.
Changes to Existing Libraries
The std/io library now contains lemmas to help users prove
that opened input and output channels remain open until closed, to
aid guard theorem proofs. See open-channel-lemmas.
Miscellaneous std changes
The why and why-explain convenience macros in
std/std-customization.lsp now support rule classes other than
:rewrite.
The rule sets-are-true-lists has been split into three rules with the
same formula: a disabled rewrite rule of that name, a compound-recognizer rule sets-are-true-lists-compound-recognizer, and a
rewrite rule sets-are-true-lists-cheap whose backchain-limit is
1.
A new utility def-updater-independence-thm for proving stobj (and
stobj-style) accessors independent of updaters has been added to
std/stobjs/updater-independence.lisp.
Kestrel Utilities
The Kestrel Utilities have
undergone several improvements and extensions.
Improved an error message for verify-guards-program (thanks to Eric
Smith for feedback); see
kestrel/utilities/verify-guards-program.lisp.
Added utilities trans-eval-state and trans-eval-error-triple, which provide convenient interfaces to the ACL2
evaluator, trans-eval.
Improved the utility, directed-untranslate, especially for handling
let and mv-let expressions (and lambda expressions) and
towards ensuring executability of its results.
Improved the utility, copy-def, to avoid failures for some functions
defined by mutual-recursion. Thanks to Eric Smith for a helpful bug
report.
Added utility er-soft+ for producing soft errors with :logic mode code, returning a specified error-triple. The new utility
er-soft-logic is similar but a bit simpler, for use when the only
property needed of the returned error-triple is that its error
component is not nil.
Added utility manage-screen-output which is an improved version of
control-screen-output (which may eventually be removed). Added
utilities make-event-terse, restore-output, restore-output?, fail-event, and try-event to fine-tune
screen output in event-generating macros. Moved obsolete utility
control-screen-output-and-maybe-replay to Workshop supporting materials,
where the only remaining use of this utility was.
The new utility orelse arranges to evaluate an event and, if that
fails, then to evaluate a second event.
The applicability condition utilities have been replaced with the named formula utilities, which are
slightly more general and include a few improvements.
New paired name utilities have been
added, to construct names consisting of two names separated by a global
customizable separator.
A new add-const-to-untranslate-preprocess utility has been added
that extend untranslate-preprocess to keep a constant unexpanded in
output.
New error-checking utilities have been added that check conditions
on data (e.g. user input) and provide informative and consistent error
messages. These utilities include a macro def-error-checker to
concisely define error-checking functions.
A new macro defbyte has been added that introduces fixtypes for signed or unsigned bytes of specified sizes. Several
instances of applications of this macro for common sizes of both signed and
unsigned bytes is also provided.
Utilities doublets-to-alist and keyword-value-list-to-alist
have been added that convert lists of doublets and keyword-value lists to
corresponding alists.
A utility assert? has been added that is a variant of assert$ with customizable context and message.
The integers-from-to utility now has a logical definition that is
easier to reason about than its tail-recursive definition for execution (which
has not changed).
The Kestrel world query utilities, term utilities, string utilities, and character utilities
(kestrel/utilities/characters.lisp) have undergone several
improvements and extensions.
A few theorems about world-related functions and theorems about lists (in
kestrel/utilities/list-theorems.lisp) have been added.
A new logic-mode utility, magic-macroexpand, performs
macroexpansion when all macros to be expanded are in logic mode.
There is a new Kestrel symbol utilities book (initially with a single
function, symbol-package-name-safe).
The apply books
Updated books pertaining to apply$; see projects/apply-model/ and
projects/apply/.
SAT proof-checker
Additions and improvements have been made to the SAT proof-checker
directories, under projects/sat/lrat/. In particular, the proof was
completed for the incremental checker (subdirectory incremental/ with an
improved soundness theorem; a new directory was added (cube/, as
mentioned above); and renamed subdirectory main/ to sorted/. The
key subdirectory is incremental/; a new top-level book top.lisp
includes the top-level book in that subdirectory.
Aignet library
A few new verified
combinational logic transforms have been
added to aignet, most notably fraiging,
DAG-aware rewriting, and
DAG-aware and-tree balancing.
These can be used as preprocessors for SAT solving with GL via gl::gl-simplify-satlink-mode.
VL/SV libraries
- SystemVerilog unique case and unique0 case can now optionally be
treated differently from regular case statements: either a constraint may
be generated off to the side expressing the one-hot constraint, or logic may be
added that assigns X instead of the stated values when the one-hot constraint
is violated.
- Somewhat similarly, enum type variables may optionally either
generate constraints stating that they take proper enum values, or may generate
extra logic that forces them to X when assigned an improper value.
- When composing together 0-delay update functions, if bit-level
combinational loops are present, these are composed together to a fixpoint.
- vl::vl-lint has yet another use-set check, vl::vl-design-sv-use-set,
which uses SV's interpretation of SystemVerilog semantics to more exactly
analyze the usage and updates of module variables. The previous vl::lucid
use-set check is still useful since sv-use-set only checks variables, not
parameters, functions, types, etc., and also does not analyze variables local
to procedural code blocks.
SOFT
The SOFT (Second-Order Functions and
Theorems) library has been improved in several ways. The :thm-name
option is now fully supported for second-order quantifier functions and their
instances. The treatment of user inputs is more robust. The user interface is
more terse. The implementation is more streamlined. A more comprehensive test
suite now exists.
X86ISA
- The X86ISA has been slightly extended with
infrastructure to support 32-bit mode of operation; in particular, the
64-bit-modep predicate is no longer always true. Some documentation
topics and some comments have been expanded and clarified. Some exceptions are
now being added to the fault field of the x86 state rather than the
model-specific field. A complete model of segment address translation has been
added.
- Codewalker can now be used to reason about 64-bit user-level x86
programs --- see
books/projects/x86isa/proofs/codewalker-examples for demos.
- Memory functions do not traffic in lists anymore. Instead of a
list of canonical addresses, a contiguous linear memory region is now
specified by: <n, lin-addr>, where n is the number of bytes
to be read or written and lin-addr is the first address of the
memory region.
- In the programmer-level mode, disjointness of memory regions can
be conveniently expressed using a function called separate. All
the proofs in the programmer-level mode have been updated to use this
paradigm.
AVR ISA
Julien Schmaltz and Peter Schwabes' AVR ISA model has been contributed in book
projects/avr-isa.
Miscellaneous Books
The book clause-processors/use-by-hint now contains an additional
utility, use-termhint, that helps structure hints in a way that
coincides with the structure of a proof and allows hints to contain terms that
have been simplified along with the goal.
A new book tools/symlet introduces a macro let-syms and b*
binder symlet that simply replace occurrences of some symbols with some
corresponding terms in the enclosed term. Like Common Lisp's
symbol-macrolet but much less smart.
Fixed misc/profiling.lisp for newer distributions of CCL (Clozure
Common Lisp), both from SVN and from GitHub.
The macro defconsts now provides a better error message when given
a symbol that does not have the syntax of a constant.
The macro must-fail has a new keyword option, :expected, to
indicate the kind of error that is expected. New macros ensure-soft-error, ensure-hard-error, and ensure-error
provide nice interfaces to must-fail with the legal values of this new
option. See must-fail. Thanks to Eric Smith for discussions leading
to these changes.
Modified removable-runes to allow a multiplier greater than 1.
Modified output accordingly. Also, the multiplier m now provides
non-strict bounds (floor (* m steps) 1) rather than the previous
strict bound (1- (ceiling (* m steps) 1)). Moreover, a related new utility,
minimal-runes, returns a list of runes to enable that is sufficient
for admitting the event.
Licensing Changes
Build System Updates
Improved books cleaning slightly, in books/GNUmakefile.
By default, the 'make' targets for certifying books now include the
books that depend on quicklisp, except when the host Lisp is GCL. Specify
USE_QUICKLISP=0 if that is not what you want.
Improved books/GNUmakefile so that by default, it reports an error
when the bash shell is missing. (Note that a version of sh on a
FreeBSD machine caused an error.)
Also see note-8-0, specifically the section on ``Changes at the
System Level''.
Testing
The documentation topics for testing have been reorganized, with
introduction of a new topic, kestrel-testing-utilities, as a parent of
the testing utilities that are part of the kestrel-books, so that now
the topic testing-utilities is the top-level topic for the testing
utilities.
The Kestrel Testing Utilities have been integrated with similar testing
utilities under misc. The utilities in
kestrel/utilities/testing.lisp have been added to misc/eval.lisp and
misc/assert.lisp, and the tests in
kestrel/utilities/testing-tests.lisp have been moved into two new files
misc/eval-test.lisp and misc/assert-tests.lisp.
The utility run-script supports testing of evaluation of the forms
in a given file, to check that the output is as expected. So far, several
existing scripts have been adapted to take advantage of this utility:
- books/demos/mini-proveall-input.lsp — a long-standing, small
basic test of ACL2
- books/demos/marktoberdorf-08/ — based on material originally
presented by J Moore in 2008 at the Marktoberdorf Summer School; see the
README file in that directory
- books/demos/big-proof-talks/ — based on material about ACL2
presented by J Moore on July 6 and 7, 2017, at the Big Proof workshop; see the
README file in that directory
- books/projects/paco/books/proveall-input.lsp, formerly named
proveall.lsp
Miscellaneous
Added file system/to-do.txt to list some potential developer
tasks.
Fixed a bug in the package redefinition utility in community book
books/misc/redef-pkg.lisp.
Defined a constant *ACL2-system-exports* that extends *ACL2-exports* for system programmers.
