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 session.

- The built-in axioms describe properties of the ACL2 data types, such as
the following.
ACL2 !>:pe car-cons -8139 (DEFAXIOM CAR-CONS (EQUAL (CAR (CONS X Y)) X)) ACL2 !>

- A key extension principle is the Principle of Definition, which, for a
definition
(defun <fn> <args> <body>) , introduces an axiom equating<body> with application of<fn> to<args> . This principle permits recursion, and even mutual-recursion, provided a suitable*measure conjecture*is provable. - Other events come with extension principles too, including
`encapsulate`,`defchoose`,`defpkg`, and`include-book`. Note that from a logical perspective,`defstobj`and`defabsstobj`just provide definitional extensions. - Each ACL2 theory is
*closed under induction*: that is, every instance of induction (in the language of the theory) below the ordinalepsilon-0 (see ordinals) is also in the theory. In practical terms, this is what allows ACL2 to prove theorems by induction.

For more about the ACL2 logic see the following publications by Matt Kaufmann and J Moore.

- “A Precise Description of the ACL2 Logic” (April, 1998).
- “Structured
Theory Development for a Mechanized Logic”,
*Journal of Automated Reasoning*26, no. 2 (2001) 161-203.

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
`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.)

Here are examples illustrating the last point above, regarding use of a single Lisp.

; True in SBCL 2.4.2, about the character it calls #MICRO_SIGN, ; but false in LispWorks 8.0.1: (alpha-char-p (code-char 181)) ; False in SBCL 2.4.2, about the character it calls #CENT_SIGN, ; but true in Allegro CL 10.1: (alpha-char-p (code-char 162))

Here is another example illustrating the requirement on a single Lisp. In ACL2 built on most host Lisp implementations, one can admit the following event. (See df for background on floating-point computations with ACL2.)

(defthm usual-sin-2pi (equal (df-sin (df* 2 *df-pi*)) #d-2.4492935982947064E-16))

But in ACL2 built on LispWorks, one can instead admit the following.

(defthm lispworks-sin-2pi (equal (df-sin (df* 2 *df-pi*)) #d-2.4492127076447545E-16))

Clearly one could prove

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-of-the-top-level-loop
- Guarantees provided by top-level evaluation