Note-7-2-books
Release notes for the ACL2 Community Books for ACL2 7.2 (Jan 2016)
The following is a brief summary of changes made to the community-books between the releases of ACL2 7.1 and 7.2.
See also note-7-2 for the changes made to ACL2 itself. For
additional details, you may also see the raw commit log.
New Libraries
Kestrel Institute's contributions are now available under
kestrel/ directory. This directory contains some system
utilities to complement the built-in system-utilities. It also
includes some general utilities to build and execute tests, retrieve
constituents of ACL2 events like defun-sk, etc.
Modeling Algorithms in SystemC and ACL2
David Russinoff has contributed a library, projects/masc/,
for modeling algorithms in SystemC and ACL2.
SOFT
Alessandro Coglio has contributed a tool called SOFT (Second-Order
Functions and Theorems) that mimics second-order behavior. See
tools/soft.lisp.
stateman
J Strother Moore's stateman books are located in
projects/stateman/. Stateman is a utility that uses
metafunctions to manage large terms tepresenting machine states.
SV is a new hardware verification library from Centaur Technology
that includes a vector-based expression representation, efficient
symbolic simulation integrated with gl, and support for many
SystemVerilog features. It replaces esim as a backend to vl; see sv::sv-versus-esim for a comparison.
Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann have
contributed a library, projects/x86isa/, containing the
specification of the x86 instruction set architecture and utilities
to simulate and reason about x86 machine code.
Other new books
A toy cache coherency protocol called VI and its proof of
correctness have been contributed by Ben Selfridge and David Rager
in projects/cache-coherence/. This effort takes an approach
that starts with a goal invariant and develops many helper
invariants while trying to prove this goal invariant.
David Russinoff has contributed a proof of the group axioms for
the addition operation on the elliptic curve known as
Curve25519; these books can be found in
projects/curve25519/. Another library in projects/shnf
contains a formalization of the theory of sparse Horner normal forms
for integer polynomials.
Ben Selfridge has contributed his library projects/sb-machine
that contains a formalization of the x86-TSO memory model. This model
contains a machine with multiple processors, a shared memory, and
store buffers.
The book demos/meta-wf-guarantee-example.lisp has an example
that demonstrates the use of :well-formedness-guarantee for
meta rules
The book misc/install-not-normalized.lisp installs an
unnormalized definition; see install-not-normalized.
The book hints/hint-wrapper.lisp allows you to supply hints
in the statement of a theorem; see hint-wrapper.
system/event-names.lisp defines ep and ep- to
return the list of event names (resp., excluding those events built
into ACL2) with a given case-insensitive prefix.
system/termp.lisp contains work done to verify the guards of
the ACL2 built-in function termp.
A new book tools/flag.lisp creates a flag-based induction
scheme for a mutual recursion; see make-flag.
New timing tools like oracle-time and oracle-timelimit
in tools/oracle-time.lisp provide the run time and bytes
allocated during the execution of a form.
A new book tools/removable-runes.lisp automatically computes
runes to disable in order to speed up a proof. See removable-runes.
Libraries in workshops/2015/
Supporting materials for some accepted papers in the ACL2
Workshop, 2015 can be found in the directory
workshops/2015/.
- Cuong Chau, Matt Kaufmann, and Warren Hunt contributed their
books on Fourier Series Formalization in ACL2(r) in subdirectory
chau-kaufmann-hunt/.
- David Hardin contributed his books involving reasoning about LLVM
code using Codewalker in the subdirectory hardin/.
- Panagiotis Manolios and Mitesh Jain submitted their work on
proving skipping refinement with ACL2s in the subdirectory
jain-manolios/.
- Yan Peng and Mark Greenstreet contributed their libraries to
extend ACL2 with SMT solvers using SMTLINK in the subdirectory
peng-greenstreet/.
Changes to Existing Libraries
The book acl2s/defdata/defdata-attach.lisp, which is used to
attach or modify metadata for a defdata type, now truely uses
defattach for enumerators, i.e., enumerators have constant names that
can be attached to different enumerator functions. This facility thus
deprecates enum/test and separate test-enumerators. For now, most
enumerators are in program mode and non-guard-verified, and
hence, defattaching them requires trust-tags.
The cgen books have been updated as follows:
- Support has been added for collecting statistics on which
hypotheses are failing in vacuous tests.
- First-class support (e.g., for equality) has been added for
membership relation/constraint, i.e., member/enum has the same
status as range types.
- Nested testable events like thm, defthm, etc. are not
supported anymore. This results in the simplification of the
event-stack global to just a event-ctx global, which
stores the ctx-form. This simplification also allows us to
aim for a global timeout on cgen/testing thm/defthm forms.
- Support for complex-rationals has been added in number
ranges.
The ACL2s::defunc books have been udpated as follows:
- The print-summary event prints total time taken by
defunc events. Now time is only printed twice, once for
test? and once for defunc logical events. Both these
times are computed using read-run-time ACL2 function and is
the accurate run time (not wall-clock time).
- A new timeout abort event is inserted at the beginning of the
defunc/static/non-static events set (generated by
defunc-events-with-staticp-flag function) . This event checks
if the elapsed time has exceeded the timeout limit and if it has,
then it aborts with an error and thus we fall through the outer
:OR to the next choice.
- The program-mode-p predicate function now checks the
following: Is there a program-mode sub-function in the body?
- The cgen-timeout parameter is used to restrict time spent
by all the body contract testing as a global timeout.
The syntax for FUN binders patbind-fun has been extended to
allow inline/notinline declarations on the resulting FLET
forms.
b* now requires that variables be bound to a form and it will
no longer treat nil and t as aliases for &. Error
messages produced by b* have been made more informative.
Reduction XOR related functions have been added to the
bitops library in parity. Lemmas in bitops::bitops/ihsext-basics have been cleaned up. Theorems about
unsigned-byte-p have been added for rotate-right and rotate-left.
A small book about floor has been added:
centaur/bitops/floor.lisp.
More slice and merge functions have been added in bitops::bitops/merge. Some integer-length rules in
centaur/bitops/integer-length.lisp have been changed to allow
better free variable matching.
coi
A new book for reasoning about modular arithmetic using nary
congruences has been contributed; see
coi/nary/nary-mod.lisp.
Books in coi have been updated so as to avoid name conflicts
with std books.
The fty books have been re-organized --- deftypes.lisp
has been split up into different files, and tests have been moved to
a subdirectory tests/. Performance problems with certain macros,
mostly related to reasoning about tag and kind functions, have been
fixed.
fty::deftranssum has been extended to support nested fty::defprods.
The bundled quicklisp libraries have been updated. The quicklisp
books work only for ACL2 built on CCL or SBCL.
The rtl/rel11 books have seen many updates, courtesy of
Dmitry Nadezhin.
Guards have been added to functions in
rtl/rel11/lib/. General cleanup of the rtl/rel11/ books,
like removing unnecessary hypotheses and include-books, has
also been done.
New radix-aware versions of functions in rtl/rel11/support/
directory have been added. E.g., the old function bitn has a
fixed radix of 2 and takes x and n as input arguments and
the new radix-aware version corresponding to this function is
digitn, which takes the radix b in addition to x and
n as inputs.
The books rtl/rel11/support/basic.lisp,
rtl/rel11/support/bits.lisp,
rtl/rel11/support/float.lisp,
rtl/rel11/support/reps.lisp, and
rtl/rel11/support/masc.lisp are now certifiable by ACL2(r).
Some books from rtl/rel11/rel9-rtl-pkg/lib, like
reps.lisp, rom-helpers.lisp, and
simple-loop-helpers.lisp, along with their supporters, have been
moved to rtl/rel11/support/.
Bugs in rtl/rel11/lib/excps.lisp related to divide-by-zero
exception and the ep exponent width in the function
convert-nan-to-op have been fixed.
A new macro called impliez has been added in
std/basic/defs.lisp. This macro expands to an if, so
unlike implies, guards in the consequent can be verified
assuming the antecedent.
New theorems about ACL2-count and nth have been
added to std/lists/nth.lisp.
The guards of list-equiv in std/lists/list-defuns.lisp
have been verified. The function list-fix was tweaked so that
it avoids consing if its input is indeed a true-listp. A new
function llist-fix, which is logically list-fix but is
the identity function for execution, has been also added.
A possibly better non-CCL raw Lisp implementation of bitsets::bignum-extract has been added.
A new rule pick-a-point-subset-constraint-helper was added in
std/osets to allow pick-a-point proofs to be used even when
subset is disabled.
For define, defretd has been added to go with
defret. Also, defret now allows the otf-flg
flag. :guard t declarations in define have been eliminated
if guards have already been provided. Also, information displayed by
pe of functions introduced using define has been cleaned
up using pe-table.
A new macro rule is a THM-like version of defrule. Rule and defrule produce leaner output now,
almost identical to that produced by thm and defthm.
For details about changes made to VL, see note-7-2-vl.
Topics with missing parents are now placed under a new topic xdoc::missing-parents instead of under top.
The title of xdoc manuals can be easily configured by editing
xdoc/fancy/config.js. No warning about a redefined topic is
produced when the topic is identical to the original one.
xdoc now loads acl2-doc-wrap instead of acl2-doc so
that the loaded documentation doesn't overwrite the user's
topics.
A bug in see that did not allow properly escaping the printed
name of a symbol has been fixed. The implementation of defsection had another bug that caused 'Definitions and
Theorems' section to be added to topics even when there were no
definitions or theorems in that section; this bug has been fixed as
well. Also, defsection does not explicitly turn on error
printing during event submission anymore.
The output from xdoc::save now shows more timing
information.
Legacy stuff like write-acl2-xdoc, :import option with
xdoc::save, and xdoc-verbose has been removed.
Other Libraries
A new book projects/codewalker/demo-fact-partial.lisp is a
variant of projects/codewalker/demo-fact.lisp that provides a
guide to how Codewalker might be modified so that termination proofs
can be avoided or delayed.
Multiple values and stobjs are now supported in the
coi/defung/ libraries.
Must-fail and related utilities in misc/eval.lisp
produce much less output by default. Also,
make-event/eval-check.lisp no longer duplicates code from
misc/eval.lisp. Instead, it defines ! utilities that
behave like the counterparts previously defined (without the !
suffix).
A bug in remove-hyps that occurred when no proof steps are
required in a proof has been fixed.
A new tarai-measure has been added in
coi/termination/assuming/complex.lisp, which is allows this book
to certify quickly in ACL2(r) as well. Consequently, this book was
removed from SLOW_BOOKS in books/GNUmakefile.
Some floating-point support has been added to the JVM M5 model;
see models/jvm/m5/m5.lisp.
gl now displays a more informative error message about
duplicated indices in :g-bindings.
Satlink now uses drat-trim, available at
tools/drat-trim/, instead of drup-trim.
The book tools/untranslate-for-exec.lisp has been improved to
handle nested mv-lets.
Deleted Books and Stubs
The book defexec/other-apps/records/records-bsd.lisp has been
deleted --- it was out of sync with records.lisp in the same
directory.
The book make-event/assert-check-include-1.lisp has been
deleted.
The book misc/dead-events.lisp has been moved to
tools/dead-events.lisp, and a relocation stub has been added in
the older location.
In the directory misc/, *-bsd.lisp books are now
reloc_stub books.
Books in projects/concurrent-programs/german-protocol/ have
been moved to projects/cache-coherence/german-protocol/.
The rtl/rel10 has been removed from the community
books. These books were not in use anywhere in the contributed
books.
The book system/gather-dcls.lisp has been deleted after its
contents were moved to
system/verified-termination-and-guards.lisp.
Licensing Changes
The following books now have BSD-3-Clause license.
- arithmetic-2/ and arithmetic-3/
- misc/rtl-untranslate.lisp
- M5 books models/jvm/m5/
- rtl books
- system/cantor-pairing-bijective.lisp
- tools/with-arith5-help.lisp
Build System Updates
The cert.pl documentation at build/doc.lisp has been
moved to its own BUILD package.
cert.pl now produces successful certification messages that
include times and color coding. cert.pl has also been patched
to correctly handle filenames with dollar signs. It has new options
for removing .cert.out files after successful certifications and
for sending them to a temporary directory.
A new build::cert_param for SMTLINK, uses-smtlink, has
been added so that books using it will not be certified unless
supporting software such as Z3 is installed. Another
cert_param called non-gcl has been added.
A new CERT_PL_SHOW_HOSTNAME environment variable has been
added to cert.pl that can show the hostname after each book gets
certified.
make system
The topic Books-certification gives clearer instructions on
building the books and the manual.
- make manual now just builds doc/top.cert and
system/doc/acl2-manual.cert.
- make everything now just depends on all the books it was
going to build.
- make quicklisp now just causes an error if
USE_QUICKLISP is not set.
Miscellaneous
A new tool build/memsum.pl analyzes memory usage during
regressions.
A new tool build/slowevents.pl attempts to identify the
slowest events in a book or a set of books.
Subtopics
- Note-7-2-vl
- Notes about changes to vl and sv in ACL2 7.2.
