• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-8-7
            • Note-8-7-books
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Release-notes-books
          • Note-3-6-1
          • Note-1-2
          • Note-2-4
          • Note-2-6
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Note-8-7
• Release-notes-books

Note-8-7-books

Release notes for the ACL2 Community Books for ACL2 8.7

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

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

New Libraries

Aleo Library

Formalizations and proofs about the Aleo blockchain and ecosystem.

The existing AleoBFT library is now a sub-library of this broader Aleo library.

We have added an ABNF grammar of the Leo language, along with ACL2 code to parse the grammar into an ACL2 representation and prove some properties of the grammar.

HOL-ACL2 Link Support

See projects/hol-acl2/README-acl2. That directory provides modifications of the HOL-ACL2 link from a HOL4 distribution, updating ACL2 aspects of that link to work with the latest versions of ACL2.

RISC-V ISA Model

A preliminary model of RISC-V ISA has been added, which covers unprivileged RV32IM and RV64IM (except for FENCE, HINT, ECALL, and EBREAK), little endian memory access, fully readable and writable address space, and no alignment checks.

Set Theory Library

This work in progress supports the use of ACL2 to reason both about first-order set theory and about “higher-order” notions (without involving apply$).

Changes to Existing Libraries

C Library

Tool-Oriented C Syntax

We have added a tool, c$::defpred, to concisely define predicates over the abstract syntax.

FTY Library

A manual page explaining general folds for fixtypes has been added.

A new event macro fty::deffold-reduce has been added, to generate reducing folds, according to the nomenclature explained in the page on general folds.

Some utilities have been added to operate on the FTY database: see fty::database. The data structures for the FTY database have been put into guard-verified logic mode.

Schroeder-Bernstein Library

This library has moved from [books]/projects/schroder-bernstein to [books]/projects/schroeder-bernstein in order to reflect the prevailing German convention of printing an "o" with umlaut as "oe" when umlaut letters are unavailable.

Standard Typed Alists Library

A theorem has been added.

Standard Utilities Library

A macro binder for b* has been added. This binder closely resembles the fun binder, but expands to a macrolet instead of an flet.

Tools Library

The "defthm-macro" generated by make-flag has been fixed to handle theorems over trivial mutual-recursion cliques consisting of just one function.

Documentation

Licensing Changes

Build System Updates

Testing

Miscellaneous

Books based on run-script now certify even when gag-mode has been set in advance, say, by an ACL2-customization file.

Tests run by certifying kestrel/acl2data/gather/tests/run-tests.lisp would fail when environment variable ACL2_CUSTOMIZATION was set. That bug has been fixed.

The new directory demos/attach-stobj/ illustrates the use of attach-stobj. See file README.txt in that directory. Additional tests of attach-stobj may be found in the directory system/tests/attachable-stobjs/

The new book demos/fp.lisp (with associated files fp.acl2 and fp-raw.lsp in the same directory) illustrates the power of partial-encapsulate, showing how it is used in the implementation of floating-point operations in ACL2. Note that an extensive test suite for floating-point operations may be found in demos/floating-point-input.lsp, with associated output file demos/floating-point-log.txt, with associated output file