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 constraints on the soundness guarantee.

- The prover's theory of a session is construed to include 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.)

Next, we provide examples illustrating the last point above, restricting to the use of a single Lisp.

**Example 1: Divergences involving character and string
operations.**

Consider the following log in raw Lisp using SBCL, which introduces
versions of characters “

* (code-char 193) #LATIN_CAPITAL_LETTER_A_WITH_ACUTE * (code-char 225) #LATIN_SMALL_LETTER_A_WITH_ACUTE *

While most Lisps that host ACL2 consider these two characters to be alphabetic characters with case (upper and lower, respectively), GCL does not (at least, a version available as of this writing).

(alpha-char-p (code-char 193)) ; T except NIL in GCL (alpha-char-p (code-char 225)) ; T except NIL in GCL (upper-case-p (code-char 193)) ; T except NIL in GCL (lower-case-p (code-char 225)) ; T except NIL in GCL (char-code (char-downcase (code-char 193))) ; 225 except 193 in GCL (char-code (char-upcase (code-char 225))) ; 193 except 225 in GCL (let ((s (string-downcase (string (code-char 193))))) (char-code (char s 0))) ; 225 except 193 in GCL (let ((s (string-upcase (string (code-char 225))))) (char-code (char s 0))) ; 193 except 225 in GCL

**Example 2: Another divergence for alpha-char-p.**

; 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))

**Example 3: A divergence involving a floating-point computation.**

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