Correctness property claimed for ACL2
What can we conclude when we use ACL2 to prove a formula or to
compute the value of an expression? This topic provides a high-level sketch
of an answer.
Any notion of correctness of ACL2 necessarily depends on the logic that it
is intended to implement. At its core, the ACL2 logic is just classical
first-order logic. The first-order theory for a given ACL2 session, which we
may call the “prover's theory”, is the result of extending its set
of built-in axioms according to events that have been executed in the
For more about the ACL2 logic see the following publications by Matt
Kaufmann and J Moore.
The following soundness property is key for a given ACL2 session.
- The theorem prover proves only formulas that are theorems in the
corresponding prover's theory in that session.
Note that the theorem prover uses evaluation during proofs. The soundness
property thus encompasses the following: when such evaluation of a term
tm produces a value v, then (equal tm 'v) is provable from the
context of that evaluation. Evaluation in the top-level loop has such a
property as well, but because of attachments (see defattach) and apply$, provability is with respect to a larger “evaluation
theory”; see guarantees-of-the-top-level-loop.
Here is a list of general restrictions on the soundness guarantee.
- The prover's theory of a session includes all axioms introduced by hidden
defpkg events. See hidden-death-package.
- There is no soundness guarantee for a session in which there is raw Lisp
evaluation with side effects. (ACL2 normally avoids putting the user into raw
Lisp, but this can happen with an interrupt, the use of break$, or
explicitly leaving the top-level loop with :q.) “Side
effects” should be interpreted as generously as possible: this certainly
includes redefining a function or assigning to a variable, but not merely
evaluating an arithmetic expression, for example.
- There is no soundness guarantee for a session in which any trust tag has
been installed (see defttag). The absence of trust tags is guaranteed
by the absence of “TTAG NOTE” being printed to standard
output (that is, to *standard-co*).
- The soundness guarantee only applies when a set of books is certified from
scratch, including community-books, in a single environment — in
particular, with the same Lisp implementation and operating system. (In
practice this is often not an issue.)
This topic has discussed the soundness guarantee from the user perspective.
Those interested in exploring deeper theoretical and implementation issues are
welcome to read the extensive relevant comments in the ACL2 source code,
including the comments labeled as follows (listed in order of appearance as of
this writing, not to indicate the order in which to read them).
- Essay on Admitting a Model for Apply$ and the Functions that Use It
- Essay on Hidden Packages
- Essay on Soundness Threats
- Essay on a Total Order of the ACL2 Universe
- Essay on Illegal-states
- Essay on Evaluation in ACL2
- Essay on the Logical Basis for Linear Arithmetic
- Essay on the Correctness of Abstract Stobjs
- Essay on Memoization with Partial Functions (Memoize-partial)
- Essay on Correctness of Evaluation with Stobjs
- Essay on Correctness of Meta Reasoning
- Guarantees provided by top-level evaluation