Guarantees provided by top-level evaluation

We often refer to the ``top-level loop,'' or just ``the loop'' when
the context is understood. The loop is the interactive read-eval-print loop
with which the user interacts to issue commands, query the ACL2 logical
world, test functions, conjectures, and systems, etc. This documentation
topic mainly addresses the logical guarantees of the loop. For practical
advice about interacting with and configuring the loop see `ld`.
`state`-using function with many parameters which may be set by the
user).

But here we are concerned with what it means, logically, when a term
*tm* evaluates without error to a value *v* in the loop.

We do not formalize macroexpansion here, but rather, we deal with
so-called “translated” terms, where macros and constants
have been expanded away. We also do not discuss here how ACL2 evaluates
expressions; see evaluation for such discussion.
(Those interested in implementation issues may also read the long comment in
ACL2 source file

See soundness for a more general discussion of soundness-related issues (including, for example, interrupts and trust tags).

One might like to think that for any term, *tm*, a non-erroneous
interaction like

ACL2 !>tmv

means that the formula

(equaltm'v)

is a theorem and can be proved by the prover.

For example, let `rfix`) the argument to be a rational, but those aspects of

(defun sq (x) (declare (xargs :guard t :verify-guards t)) (let ((x (rfix x))) (* x x)))

then the evaluation

ACL2 !>(sq 3) 9

suggests that

But the situation is quite subtle and deserves further discussion. That is what this topic is about.

**Spoiler Alert**: We will not give logical semantics to every
non-erroneous evaluation in this discussion. We only hint at how it can be
done for many terms. Furthermore, even for those terms whose evaluations do
correspond to theorems, the logical theory in which those theorems can be
proved is not the theory supported by the ACL2 prover but an extension of it.
We ultimately describe below the so-called *evaluation theory* which is
an extension of ACL2's *proof theory*. So this documentation topic
discusses two logical theories. Because any theory in which proofs are done
might be called the ``proof theory'' and in this section we need to clearly
distinguish between the two theories being discussed, we'll refer to the
theory supported by the ACL2 theorem prover as the *prover's
theory*.

Suppose `program` mode function
that squares its argument. Then the top-level evaluation

ACL2 !>(prog-sq 3) 9

clearly should not suggest

(equal (prog-sq 3) 9)

is a theorem. `defun` and `defthm`. But it is also a convenience
that allows ACL2 to be used as a programming language (e.g., to
prototype a system one might eventually admit to the logic and prove theorems
about).

Therefore, when attempting to define the logical meaning of top-level
evaluations we might restrict our attention to `logic` mode terms
only. But this is not sufficient for several reasons.

Evaluation of terms involving single-threaded objects or ``stobjs''
raise problems, even if the terms involved are in

ACL2 !>(defstobj st fld) ... ST ACL2 !>(update-fld 3 st) <st> ACL2 !>(update-fld (sq (fld st)) st) <st> ACL2 !>(fld st) 9

but the strawman conjecture from the last evaluation,

(implies (stp st) (let* ((st (update-fld 3 st)) (st (update-fld (sq (fld st)) st))) (equal (fld st) 3)))

This reminds us that the top-level loop tracks changes to each ``live''
stobj and records them in the ACL2 `state`. Those changes must be
reflected in any suggested theorems.

`Apply$` calls `apply$-userfn` to handle the application of
user-defined function symbols. `warrant` hypotheses (see `defwarrant`). Recall
that warrants link the functions approved by `tame`ness conditions. As noted at the bottom of the
discussion of `defwarrant`, there is a model of the prover's theory in
which all warrants issued by **Lesson 12** of introduction-to-apply$).

One might wonder why we have warrants at all, aside from the local problem. The key reason is that inconsistency can result from non-terminating recursion if we had the following axiom schema

Unsound Axiom Schema: (equal (apply$ 'f(list a1 ... an)) (fa1 ... an))

for every defined function *f*. See the `defwarrant` keep the prover's theory consistent. One might then ask
``how do we get away with letting the top-level loop

To illustrate the difference between the behavior of the top-level loop
and the prover, suppose the function

(defwarrant sq)

and then consider the top-level evaluation

ACL2 !>(apply$ 'sq '(3)) 9

This is possible because the warrant for

However,

(implies (warrant sq) (equal (apply$ 'sq '(3)) '9))

where

Thus, to extend the strawman conjecture to functions in which

But

(defbadge prog-sq) (defun logic-sq (x) (declare (xargs :mode :logic)) (apply$ 'prog-sq (list x)))

Since the top-level loop can evaluate applications of

ACL2 !>(logic-sq 3) 9

Note that

(equal (logic-sq 3) '9)

nor

(implies (warrant logic-sq) (equal (logic-sq 3) '9))

is a theorem in the prover's theory because

(implies (warrant logic-sq) (equal (logic-sq 3) (apply$ 'prog-sq '(3))))

This example contradicts the suggestion, just above, that if we properly
considered warrants we could give logical meaning to evaluations of

Constrained functions raise problems if they have been given
attachments (see `defattach`). The top-level loop uses attachments to
compute values consistent with the constraints, but the prover's theory does
not. Attachments are useful for building and testing instances of models
consistent with the constraints.

For example, let

(encapsulate (((nonneg-rat *) => *)) (local (defun nonneg-rat (x) (declare (ignore x)) 0)) (defthm nonneg-rat-constraint (and (rationalp (nonneg-rat x)) (<= 0 (nonneg-rat x)))))

It is impossible to evaluate

(defattach nonneg-rat sq)

and then we can ``evaluate'' calls of

ACL2 !>(nonneg-rat 3) 9

But of course the strawman conjecture

The ACL2 logic formalizes an applicative (functional and side-effect free)
extension of a subset of Common Lisp (see common-lisp). It is
described in chapter 6 of Computer-Aided
Reasoning: An Approach, by Kaufmann, Manolios, and Moore, as an extension
of quantifier-free first-order logic with equality (section 6.1). The syntax
is that of translated terms though the user is allowed to use a more
flexible syntax which can be extended by defining constant symbols and
macros (see `defconst` and `defmacro`). To see the formal
translation of such a term use the command `trans`. In section
6.2 of the book, axioms are added to characterize the basic data objects of
numbers (integers, rationals, and complex rationals), characters, strings,
symbols, and ordered pairs. In section 6.3, the ordinals up to epsilon-0 are
constructed from ordered pairs and integers; a well-founded ``less than''
relation is also defined. But the book's construction of the ordinals is now
obsolete. A new representation was implemented after the book was published.
See ordinals. In Section 6.4, a conservative Principle of
Definition (see `defun` and `defuns` or `mutual-recursion`)
is introduced, allowing the addition of axioms defining new function symbols.
In Section 6.5, a Principle of Induction up to epsilon-0 is described.
Induction and recursion are duals: every admissible recursive function
suggests an induction and vice versa and this duality is used by the ACL2
prover to select an often appropriate induction scheme for a conjecture. See
induction and `hints` for ways to influence this selection.
Finally, in section 6.6, the book introduces `encapsulate` to introduce
constrained functions and functional instantiation (a derived rule of
inference akin to second order instantiation), and a variety of other ways of
conservatively adding new function symbols.

The ACl2 prover proves theorems in the extension of the above theory
obtained by adding the axioms introduced by events successfully
carried out in the user's session. The most common such axiom-adding events
are `defun`, `defchoose`, and `encapsulate`, which all
conservatively extend the theory by the addition of axioms about new function
symbols. But `mutual-recursion`).
`Defstobj` and `defabsstobj` add recognizers, constructors, and
accessors for single-threaded objects (aka ``stobjs'') but logically
just use `defaxiom`, but *strongly discourage its
use*. There are many other events that add axioms, e.g., `defun-nx`
and `defun-sk` but these are defined as macros that expand into the
primitives just listed. In addition, there is a facility for including files
of previously admitted events, `include-book`.

Note that an event of the form `skip-proofs` event does assume that all proof obligations introduced
by

Given a user's session, we call the above described theory the *prover's
theory*.

Now recall the strawman proposal for what evaluation in the top-level loop means, i.e., that the evaluation

ACL2 !>tmv

might mean that the formula

(equaltm'v)

is a theorem. We have illustrated with *not* necessarily a theorem of the prover's theory!

However, there is a theory in which many of these conjectures are theorems.

The *evaluation theory* is obtained from the prover's theory as
follows.

Instead of treating stobj names as variables, the evaluation theory treats them as abbreviations for the ``current value'' of the stobj, specifically, the constant obtained by composing the sequence of all updates to the stobj's fields carried out so far in the top-level loop. Thus, for example, in the evaluation theories created by this sequence of top-level evaluations

ACL2 !>(defstobj st fld) ; [1] ST ACL2 !>(update-fld 3 st) ; [2] <st> ACL2 !>(update-fld (* (fld st) (fld st)) st) ; [3] <st>

st is an abbreviation for(NIL) after evaluation [1], an abbreviation for(3) after evaluation [2], and an abbreviation for(9) after evaluation [3].Every warrant created by

defwarrant is assumed true as an axiom.For every

(defattach f g) event in the prover's theory the axiom (i.e., constraints) onf is replaced by the axiom(equal (f ...) (g ...)) in the evaluation theory. (Of course this replacement also takes place when using the more general form for`defattach`,(defattach ... (f g ...) ...) .)

Given the restrictions enforced by

Furthermore, the top-level evaluation

ACL2 !>tmv

means that

(equaltm'v)

is a theorem in the evaluation theory provided

*tm*is a:logic mode term, and- every symbol that reaches the first argument of any
apply$-userfn in the execution of*tm*is in:logic mode.

The ACL2 prover cannot generally prove these theorems, since it operates in the prover's theory. However, as noted, there are often ways to encode the conjectures into ACL2 formulas that are provable — in particular, by adding suitable warrant hypotheses — though the ACL2 system does not provide tools for doing so.

In this section we illustrate some consequences of the guarantee that for
any term, *tm*, satisfying certain restrictions, if *tm* evaluates
to a value *v*, then the term

(equaltm'v)

is a theorem of the evaluation theory.

Each command below is enumerated and after the entire sequence we make
observations about the results and implications. It might also help to read
the section **Top-Level Evaluation of Apply$** in the documentation for
`apply$`, which describes how

ACL2 !>(include-book "projects/apply/top" :dir :system) ... ACL2 !>(defun my-cons (x y) ; [1] (declare (xargs :mode :program)) (cons x y)) ... ACL2 !>(defbadge my-cons) ; [2] MY-CONS now has the badge (APPLY$-BADGE 2 1 . T) but has no warrant. T ACL2 !>(apply$ 'my-cons '(3 4)) ; [3] (3 . 4) ACL2 !>(thm (equal (my-cons 3 4) '(3 . 4))) ; [4] ... ******** FAILED ******** ACL2 !>(verify-termination my-cons) ; [5] ... ACL2 !>(apply$ 'my-cons '(3 4)) ; [6] ACL2 Error in TOP-LEVEL: The value of APPLY$-USERFN is not specified on MY-CONS because MY-CONS has not been warranted. ACL2 !>(defwarrant my-cons) ; [7] MY-CONS is now warranted by APPLY$-WARRANT-MY-CONS, with badge (APPLY$-BADGE 2 1 . T). ACL2 !>(apply$ 'my-cons '(3 4)) ; [8] (3 . 4) ACL2 !>ACL2 !>(thm (equal (my-cons 3 4) '(3 . 4))) ; [9] ... ******** FAILED ******** ACL2 !>(thm ;[10] (implies (warrant my-cons) (equal (my-cons 3 4) '(3 . 4)))) ... Q.E.D. ... Proof succeeded.

In events [1] and [2] `verify-termination` in [5] we can no longer evaluate the application
of **Lesson 12** of introduction-to-apply$ and
discussed more thoroughly in ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore.