		Search-engine friendly clone of the ACL2 documentation.

Note-8-5-books

Release notes for the ACL2 Community Books for ACL2 8.5

The following is a brief summary of changes made to the community-books between the releases of ACL2 8.4 and 8.5.

See also note-8-5 for the changes made to ACL2 itself. For additional details, you may also see the raw commit log.

New Libraries

Algebra

A new library for abstract algebra has been started (kestrel/algebra/). It contains a formalization of groups, including proofs of a few very simple properties in a calculational style.

Big Data Library

A preliminary new library (kestrel/big-data/) has been started for analyzing the ACL2 Community Books as an object of scientific study. Currently the focus is just on identifying name clashes, so that packages, functions, and theorems can be given unambiguous identifiers.

Clause Processors Library

A new library (kestrel/clause-processors/) includes several clause-processors (substitute, flatten literals, perform a simple subsumption), many of which are verified. These are intended as building blocks for building more complex clause-processors.

Evaluators Library

A new library (kestrel/evaluators/) collects some simple evaluators for verifying clause-processors and meta-functions.

A new tool, defevaluator+, improves open defevaluator (better defaults, more and better theorems, support for lifting results to richer evaluators).

Proof Helpers Library

A new library (kestrel/helpers/) had been added for help developing books, including very preliminary tools to find hints, prove return type theorems, and improve existing books.

A new utility has been added for processing dependency information.

Syntheto

Syntheto is a surface language for ACL2 and APT, aimed at a wider range of users than typical ACL2 and APT experts. Our implementation of Syntheto consists of a front-end (in a separate repository) and a back-end (in kestrel/syntheto/). See the Syntheto documentation in kestrel/syntheto/ for details.

Changes to Existing Libraries

ABNF Library

Some preliminary parsing generation tools have been added.

ACL2 Arrays Library (kestrel/acl2-arrays/)

Def-typed-acl2-array now generates additional rules.

Other rules have been added/improved.

Alists Light Library (kestrel/alists-light/)

Rules have been added and improved.

A book about rassoc-equal has been started.

Modularity has been improved.

`Apply$` and `loop$` libraries

projects/apply/ has changed significantly. In previous versions of ACL2 there was one user-level book on that directory, top.lisp.

Now there are three: apply.lisp, loop.lisp, and top.lisp. The first is most appropriate if you are using apply$ but not loop$. The second is most appropriate if you are using loop$. Since loop$ uses apply$, the second book includes the first. The new top.lisp includes both apply.lisp and loop.lisp and thus is equivalent to loop.lisp.

The old top.lisp included many books that were not explicitly concerned with apply$ or loop$, including

ordinals/lexicographic-ordering-without-arithmetic.lisp,
sorting/perm.lisp,
sorting/term-ordered-perms.lisp,
sorting/convert-perm-to-how-many.lisp, and
sorting/merge-sort-term-order.lisp.

Furthermore, these books were included non-locally so that their rules were added when top.lisp was included. Now they are local to top.lisp and loop.lisp. This means that user books dependent on the old top.lisp might mention or depend on rules that are no longer available when the new top.lisp is included.

Finally, the new loop.lisp defines three theory constants that may be of use. See the comment in loop.lisp.

APT Library

A new transformation, copy-function, has been added to serve as a model for creating new transformations (it transforms a function without really changing anything except function names).

A new transformation, drop-irrelevant-params, has been added for dropping unused parameters from functions. Parameters can become unused due to the application of other transformations.

A new transformation, finite-difference, has been added for incrementalization (efficiently maintaining some value that depends on other values as those values change).

A new transformation, rename-calls, has been added to rename called functions (this is still somewhat in-progress)

A new transformation, rename-params, has been added for renaming parameters of functions.

A new transformation, wrap-output, has been added for applying a wrapper computation to every if-branch of a function (e.g., to change its return type).

The apt::simplify transformation now does a better job of preserving mbt calls.

The apt::restrict transformation now accepts :guard as a special value for its restriction input, to specify the guard of the target function.

The apt::isodata transformation now generates new-to-old and old-to-new theorems of a more general and useful form.

Small improvements have been made to deftransformation, a tool for generating transformations.

A new utility, def-equality-transformation, has been added for easily creating simple APT transformations that make equality-preserving changes to functions.

A new utility, verify-guards-for-defun, has been added that uses a clause-processor to greatly speed up guard proofs (by 50,000x on one example).

Other improvements have been made to supporting utilities and to make proofs more robust.

Arithmetic Library (arithmetic/)

The amount of extra material included along with arithmetic books has been reduced.

Arithmetic-light Library (kestrel/arithmetic-light/)

Many new rules have been added, and many rules have been improved.

A new book on evenp has been added.

The guard of the function lg has been strengthened to exclude 0.

A new book, log2.lisp, on base-2 logarithms has been added. This deals with taking the (floor of) the base 2 logarithm of any positive rational.

Axe

Many improvements, optimizations, additions, and fixes have been made to Axe.

In the Tactic Prover, before stp is called, rewriting is done to replace constructs unhandled by either STP or the translation to STP (for example, shift operations). Also, the tactic :rewrite-with-precise-contexts has been added.

Various rule lists used by Axe have been improved.

Handling of assumptions and ifs has been optimized.

New options (controlling XOR handling, memoization, and hit counting) have been added to some tools.

Boolean reasoning has been improved.

The generated rewriters have been improved (better handling of boolif and bvif, using stobjs more, optional XOR normalization, more auto-generated functions).

Rewriting of calls of not has been improved: Now the argument is looked up in the node-replacement-array to see whether it is non-nil. Several additional tests now work.

A new tool, def-simplified-dag, has been added.

Debugging of failed proofs has been improved.

Pruning has been improved.

Counterexample handling has been improved (check that values have the expected types, allow an error to be returned when fixing up a counterexample, show that the node numbers in a counterexample are bounded).

Dependence on non-lightweight libraries has been reduced.

Some runtime checks have been dropped, after proving they never fail.

More tests have been added.

Test case creation has been improved.

The events generated by some tools are now local by default (prevents storing huge DAGs in .cert files).

Printing, documentation, memoization, and the Axe Evaluators have been improved.

Unroll-spec-basic can now often automatically determine all functions that need to be opened/unrolled.

Dependence on skip-proofs has been reduced (more code in :logic mode and guard-verified).

Some invariant-risk is now avoided.

Generated Axe provers now support :use hints.

A new code query tool can determine whether terms (over bit-vectors and arrays) are satisfiable and produce satisfying instances.

The Axe Equivalence Checker has been added.

A tool to unroll a function by a constant factor has been added.

An alternative implementation of the Axe Rewriter has been added.

Axe JVM toolkit (kestrel/axe/jvm/)

The lifters / unrollers have been improved in various ways. Method signatures and output types are now inferred. Results of lifting are made local by default, to keep certificates small. XORs are no longer normalized by default.

Axe x86 toolkit (kestrel/axe/x86/)

A very preliminary lifter for simple x86 code with loops has been added.

Additional options (e.g., for pruning branches) have been added to the x86 unroller.

An Axe proof of an x86 binary population-count program has been added.

Bitcoin Library

Executable specifications of Bech32 and Bech32 address encoding have been added.

Booleans Library (kestrel/booleans/)

Rules have been added and library organization has been improved.

BV Library (kestrel/bv/)

Definitions have been simplified.

Many rules have been added, improved, simplified, or renamed.

Library organization has been improved and dependencies reduced.

Rules for splitting shifts into cases have been improved.

BV Lists Library (kestrel/bv-lists/)

New rules have been added, and the library's organization has been improved.

Material on bit-vector packing has been added.

New bv-array conversion utilities have been added.

C Library

ATC, the C Code Generator for ACL2

ATC has been extended to cover a larger subset of C. See the user documentation of ATC for more details.

Cryptography Library

A formal specification of the Salsa20 hash function has been added.

Elliptic Curve Library

Several theorems have been added.

A refinement of pfield-squarep has been added.

Event Macros Library

The make-event-terse utility has been extended to handle the recently added new kind of ACL2 comment output.

File-Io-Light Library

Various simplifications have been made, including removing checks for bad channels (after proving that they cannot occur).

Rules have been added or improved dealing with read-object, channels, print-object$, read-char$, etc.

Utilities have been added to read objects from a file (using guard-verified :logic mode code) and to read a file into a stobj array of characters.

Fixtype Definition Library

A new macro fty::defresult has been added to define flat unions of a fixtype of errors with any fixtype that is disjoint from those errors. This is accompanied by b* binders to check and propagate errors.

Several fixtypes have been added, under kestrel/fty/.

Consing has been reduced in recognizers for defprod, etc.

Isar Library

This library has undergone some improvements.

Java Library

ATJ, the Java Code Generator for ACL2

An option has been added to check that no AIJ types are referenced by the generated Java code, i.e. that the generated Java code exclusively manipulates Java primitive values and arrays. If that is the case, the environment class is not generated, and the main class is much smaller than without this option.

If a Java package name is specified, the generated Java code is saved in a subdirectory of the output directory that corresponds to the typical Java convention.

JVM Model (kestrel/jvm/)

The formalization of class tables has been improved.

The modify macro has been redone (for clarity and better checking).

Work has been done to standardize normal forms and enforce abstractions better.

New rules have been added and duplicate rules removed.

Organization has been improved.

More functions are now in the JVM package.

The computation of default values of floats and doubles has been simplified.

The handling of LDC and related instructions in .class file has been improved. Now all of the constants are tagged, so we no longer require floats to be represented differently than ints.

Work has been started to define an accurate floating point model to support the JVM model (still in progress). This formalizes notions of representable numbers, floating point data (including encoding and decoding of bit-vectors), normal and subnormal numbers, infinities, NaNs, and floating point comparisons. Some proofs connect these notions to similar notions in the RTL library.

Kestrel Utilities Library

Special handling of mbt by directed-untranslate has been removed, as it is no longer necessary or appropriate because of the change to the apt::simplify transformation for mbt noted above.

The new utilities checkpoint-list and checkpoint-list-pretty and related (perhaps less useful) new utilities checkpoint-info-list and show-checkpoint-list provide programmatic interfaces to key checkpoint information.

The new utility book-runes-alist returns an alist associating book full pathnames with a list of the runes introduced .

New or improved rules deal with explode-nonnegative-integer, explode-atom, state, channels, worlds, intern-in-package-of-symbol, fresh names, supporting functions, constant names, nat-to-string and binary-pack.

Printing done by submit-event has been improved.

A new utility, defstobj+, is a drop-in replacement for defstobj that disables the stobj-related functions and proves many rules about them, such as read-over-write properties. Currently only scalar and array fields are supported.

A new tool, with-local-stobjs, extends with-local-stobj to support multiple stobjs.

Utilities for making lists of symbols have been added.

Organization has been improved and dependencies reduced.

New books have been added about assoc-keyword, theory-invariants, chk-length-and-keys, member-symbol-name, arities, negation, logic-termp, messages, hints, reconstructing macro calls, defun and mutual-recursion forms, macro arguments, explode-nonnegative-integer, intern-in-package-of-symbol, and digit-to-char.

Defopeners has been improved.

Utilities have been added or improved about :program mode, prove$, declares, ignores, translation (tolerating ignored variables), tables, symbol creation, disjoin, defmacrodoc, and verifying guards.

A new tool, defcalculation, has been added to support proofs that chain together equalities.

A draft tool, specialize-calls-in-theorems, to specialize theorems has been added.

The new utility book-of-event has been added, to determine which book introduced a name.

My-make-flag has been improved (use unnormalized bodies, speed up some proofs by 100x using a custom clause-processor).

The utility directed-untranslate$ has been added.

Utilities have been added for manipulating conjuncts and disjuncts.

The utility add-not-normalized-suffixes has been added.

The Linter has been improved (to look for contradictory guards, to look for hypotheses that are unneeded or stronger than necessary, and to suggest generalizations). Various issues found by the Linter in Community Books have been fixed.

The :ubi tool has been improved. It now sees through with-output wrappers on commands. It also no longer considers xdoc to be a keeper command.

Kestrel x86 Library (kestrel/x86/)

Rules have been added, improved, and given better names.

Error messages in the Mach-O parser have been improved.

Lists Light Library (kestrel/lists-light/)

New books have been added about make-list-ac, resize-list, functions that treat lists like sets, and replace-item.

Many rules have been added and improved.

Library organization has been improved.

Perm now has true-listp guards and calls more standard sub-functions.

Number Theory Library

Dependencies have been reduced to avoid name clashes.

Primep is now disabled.

Prime Fields Library

Rules have been added, improved, and renamed.

The behavior of the inversion function on 0 has been changed.

PFCS (Prime Field Constraint System) Library

This library has undergone several improvements, including the addition of some initial support for verifying properties of PFCS instances.

Quicklisp Library

The quicklisp library is now ignored for regressions of ACL2 built on LispWorks, due to an asdf version incompatibility with the asdf.lisp provided by LispWorks Version 8.0. That problem may become a problem for future versions of other host Lisps, as they too update their asdf versions. Perhaps this will be fixed by someone in the ACL2 community; see GitHub Issue #1332.

The quicklisp libraries have been updated to recent versions (as of 7/7/2022; previous versions were as of 2020). This fixes library version errors with Mac OS X on M1 machines and with recent versions of Ubuntu (e.g., 22.04).

Random Library (kestrel/random/)

Improvements have been made to :forward-chaining rules.

R1CS Library

verify-r1cs and related tools now support :use hints.

A verified NAND gadget generator has been added.

A verified range-check gadget generator has been added.

Documentation has been added.

Sequences Library (kestrel/sequences/)

Defforall has been improved, including reducing the number of included books from 42 to 27.

Standard Basic Library

A fixer maybe-string-fix for maybe-stringp has been added.

Standard Strings Library

The names of several functions, and associated theorems, have been made more uniform and descriptive.

Standard System Library

Some theorems about fsublis-var and fsublis-var-lst have been added.

A fixer for pseudo-event-formp has been added.

Standard Typed Alists Library

A book of theorems about symbol-alistp has been added.

A definition of alists from strings to symbols has been added.

Standard Utilities Library

The defret utility could malfunction when including an uncertified book. This has been fixed by tweaking a defsection utility to set the ``most recent function'' non-locally. This fixes GitHub Issue #1302.

defmapping, along with its wrappers defiso, definj, and defsurj, has been extended with a :thm-enable option to control whether the generated theorems are enabled or not. They are disabled by default. See the documentation of defmapping for details.

Defines has been improved to suppress return-value theorems in :program mode.

Strings Light Library (kestrel/strings-light/)

New books have been added about reversing, string length, and checking whether a string ends with some other string.

New lightweight utilities have been added for parsing characters as digits.

Terms Light Library (kestrel/terms-light/)

Utilities have been added to reconstruct lets, serialize lambdas, rename variables, find duplicate lambda arguments, add parameters to calls, find and count occurrences of subterms, lambda-bind arguments of function calls, replace terms, substitute unnecessary lambda vars, make lambda applications, reconstruct mv-lets, wrap patterns around terms, find let vars, recognize unary lambdas, manipulate conjuncts, and create, combine, and count ifs.

Some theorem names have been improved, and new rules have been added.

Some utilities have had their correctness verified.

A new utility, sublis-var-and-magic-eval, has been added to apply a substitution to a term while evaluating ground terms.

Tools (tools/)

When the tool prove$ is interrupted (with Control-C), control now returns to the top level. Formerly, that `abort' merely caused prove$ to return (mv nil nil state). Also if the given term and (if supplied) hints have illegal syntax, an error now occurs.

New keyword options :ignore-ok and :prover-error-output-off are now available for prove$.

Evaluation of (prover-steps-counted state) returns the prover steps counted for the most recently completed event.

Fixed with-supporters to work when including an uncertified book.

Defthm-flag has been improved. When defthm-flag is called with no arguments, it creates a template form for the user to fill out. That form includes placeholder hypotheses for each template theorem. Previously these were always literally (AND HYP1 HYP2), with the user expected to replace the meaningless HYP1 and HYP2 with meaningful hyps (or delete them). Now, for a function with a non-trivial guard, that guard is used for the hyp instead, since it is fairly likely to be needed in theorems about the function. The user is still welcome to edit the hyps, of course. Also, computed hints are supported better (a hint can now be simply the name of a computed hint function).

Typed Lists Light Library

Rules have been added and library organization improved.

Books about true-list-listp and pseudo-term-list-listp have been started.

Untranslated Terms Library (kestrel/untranslated-terms/)

Rename-functions has been improved in various ways.

Utilities for manipulating conjuncts have been improved.

VL Library

The dependencies of vl/util/namedb have been reduced. This change prevents vl/util/namedb from including vl/util/defs. Various include-books had to be added in namedb.lisp and other files to compensate, but the net effect is to greatly reduce what is included by namedb and tools that include it, including defrstobj and the x86isa model.

X86ISA

The dependency of CPUID features on the x86 state has been removed. Now the CPUID features are arbitrary but fixed in the model. See the documentation in the x86isa::cpuid topic for details.

Support has been added for the MOVD and MOVQ instruction variants that move data from/to the XMM registers.

Xdoc Library

Some functions have been put into :logic mode (with verified guards).

Defpointer has been improved to tolerate symbols with unusual names.

Dependencies have been reduced.

Yul Library

This library now contains a complete formalization of generic Yul, and a partial formalization of the EVM dialect of Yul. It also contains formalizations and correctness proofs of some of the Yul transformations performed in the Solidity compiler.

Zcash Library

This library has been extended with several theorems and with a formalization of several gadgets.

Proofs of various R1CS gadgets / gadget generators have been added.

A new tool, zcash::verify-zcash-r1cs, has been added (a specialization of r1cs::verify-r1cs.

Documentation has been added.

Licensing Changes

Build System Updates

Default Build Target, `basic', Avoids Quicklisp Dependency

The default `make' target for certifying the community-books, which is still `basic', now certifies slightly fewer books so that it does not depend on Quicklisp.

Hons Always Enabled

As discussed in topic note-8-5, essentially all support for building ACL2 without the hons-enabled features has been removed. The build system has been similarly updated, in particular by eliminating the hons-only value for cert_param and the exported variable ACL2_HAS_HONS.

Useless Runes Updates

The cert.pl perl script by default now makes use of useless-runes files when they are available. It does that by binding the environment variable ACL2_USELESS_RUNES=-25 unless the environment variable is already defined, in which case it heeds the existing value.

This behavior is now the same as using make to certify community books. Previously there was an unexpected slowdown when using cert.pl to certify a needed subset of books prerequisite to a particular book of interest, when those prerequisite books had precomputed *@useless-runes.lsp files. Note that the default behavior of certify-book in ACL2 has not changed, just the default behavior of cert.pl.

To turn off the use of useless runes, you can set that environment variable to the empty string, e.g.:

ACL2_USELESS_RUNES=  cert.pl ..

The above change does not apply to ACL2(r).

In ACL2(r), the useless runes files that were precomputed for ACL2 could cause certification errors if someone tried to use them, using either certify-book or cert.pl. Now the useless runes feature has been turned off for ACL2(r).

The precomputed useless-runes files continue to be ignored by ACL2(p), so the previous code that ignored useless runes when using make has been removed.

Book Dependencies in S-expression Form

The cert.pl perl script generally writes book dependency information in Makefile format to the file Makefile-tmp, or if specified, to the file named after the flag -o.

Now cert.pl has a new flag, --smakefile, that causes cert.pl to write book dependency information in S-expression format as well, to a file named xxx.lsp, where xxx is where the Makefile format dependency information is being written.

When you invoke the make command to build the community books, one of the things build/GNUmakefile does is to scan the community books for dependency information, using cert.pl. Now the default is for that call to include the --smakefile flag, causing the dependency information to also be written in a format that is easy to read by ACL2. The new file is about 4 MB, as compared with a freshly cloned ACL2 repo of about 1800 MB. If you wish to turn off this feature, you can set the environment variable ACL2_INHIBIT_DEPS_LSP to any nonempty string prior to invoking make. For example:

ACL2_INHIBIT_DEPS_LSP=1 make -j12 regression

Build colors

The roles of green and bold green in build output have been swapped. Now, for books that take 20 seconds or less, the bold green books are the slower books (10-20s) and the regular green books are the faster books (0-10s). The rationale is that bold is more prominent and we want to draw attention to slower books. This also matches how bold works for yellow and red.

Testing

Miscellaneous

The following warning is now printed when broken xdoc links are encountered: ``Please note the following broken topic link name[s]: ...''. This warning is printed to the terminal after the topic is printed by :doc, unless of course the warning is inhibited (see set-inhibit-warnings and set-inhibit-output-lst).

For the utility make-flag, the previous release (see note-8-4-books) deprecated the use of a list of cons pairs (old . new) for the value of the keyword argument, :flag-mapping. That list must now be a list of doublets, (old new).

The book doc/top-slow.lisp is now top.lisp. It is now only used to detect conflicts between books.