BIBLIOGRAPHY

Major Section:  MISCELLANEOUS

For a list of notes and reports about ACL2, see

http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html.

Below is a list of notes and reports pertaining to ACL2.

BREAKS

Major Section:  MISCELLANEOUS

Example:
Broken at PROVE.  Type :H for Help.
>>:Q


ACL2 !>

If a break occurs, e.g. because of a bug in ACL2 or a user interrupt, the break will run a Common Lisp read-eval-print loop, not an ACL2 read-eval-print loop. This may not be obvious if the prompts in the two loops are similar. Because you are typing to a Common Lisp evaluator, you must be careful. It is possible to damage your ACL2 state in irreparable ways by executing non-ACL2 Common Lisp. It is even possible to disrupt and render inaccurate the interrupted evaluation of a simple ACL2 expression.

Quitting from the break (as with :q in GCL, :reset in Allegro CL, and q in CMU CL) will return to the innermost ACL2 read-eval-print loop. Before the loop is continued, any pending cleanup forms from acl2-unwind-protects are evaluated (unless acl2::*acl2-panic-exit-flg* is non-nil, in which case no cleanup is done).

If you submit the token #. to raw lisp break, an abort is generally executed. (Some underlying Lisp systems, however, reset the read table (*readtable*), in which case you should type a number after #. and then follow the directions in the preceding paragraph.) Control is passed to the outermost ACL2 read-eval-print loop (lp). Again, unwind-protection cleanup forms are executed first.

CASE-SPLIT

Major Section:  MISCELLANEOUS

When a hypothesis of a conditional rule has the form (case-split hyp) it is logically equivalent to hyp but has the pragmatic effect of splitting the main goal into two cases, one in which (the required instance of) hyp is true and one in which (the required instance of) hyp is false.

Unlike force, case-split does not delay the ``false case'' to a forcing round but tackles it more or less immediately.

When in the proof checker, case-split behaves like force.

CHECK-SUM

Major Section:  MISCELLANEOUS

A ``check sum'' is an integer in some fixed range computed from the printed representation of an object, e.g., the sum, modulo 2**32, of the ascii codes of all the characters in the printed representation.

Ideally, you would like the check sum of an object to be uniquely associated with that object, like a fingerprint. It could then be used as a convenient way to recognize the object in the future: you could remember the check sum (which is relatively small) and when an object is presented to you and alleged to be the special one you could compute its check sum and see if indeed it was. Alas, there are many more objects than check sums (after all, each check sum is an object, and then there's t). So you try to design a check sum algorithm that maps similar looking objects far apart, in the hopes that corruptions and counterfeits -- which appear to be similar to the object -- have different check sums. Nevertheless, the best you can do is a many-to-one map. If an object with a different check sum is presented, you can be positive it is not the special object. But if an object with the same check sum is presented, you have no grounds for positive identification.

The basic check sum algorithm in ACL2 is called check-sum-obj, which computes the check sum of an ACL2 object. Roughly speaking, we scan the print representation of the object and, for each character encountered, we multiply the ascii code of the character times its position in the stream (modulo a certain prime) and then add (modulo a certain prime) that into the running sum. This is inaccurate in many senses (for example, we don't always use the ascii code and we see numbers as though they were printed in base 127) but indicates the basic idea.

ACL2 uses check sums to increase security in the books mechanism; see certificate.

CLAUSE-IDENTIFIER

Major Section:  MISCELLANEOUS

To each goal-spec, str, there corresponds a clause-identifier produced by (parse-clause-id str). For example,

(parse-clause-id "[2]Subgoal *4.5.6/7.8.9'''")

The function string-for-tilde-@-clause-id-phrase inverts parse-clause-id in the sense that given a clause identifier it returns the corresponding goal-spec.

As noted in the documentation for goal-spec, each clause printed in the theorem prover's proof attempt is identified by a name. When these names are represented as strings they are called ``goal specs.'' Such strings are used to specify where in the proof attempt a given hint is to be applied. The function parse-clause-id converts goal-specs into clause identifiers, which are cons-trees containing natural numbers.

Examples of goal-specs and their corresponding clause identifiers are shown below.

             parse-clause-id
                   -->


"Goal"                       ((0) NIL . 0)
"Subgoal 3.2.1'"             ((0) (3 2 1) . 1)
"[2]Subgoal *4.5.6/7.8.9'''" ((2 4 5 6) (7 8 9) . 3)


                   <--
      string-for-tilde-@-clause-id-phrase

The caar of a clause id specifies the forcing round, the cdar specifies the goal being proved by induction, the cadr specifies the particular subgoal, and the cddr is the number of primes in that subgoal.

Internally, the system maintains clause ids, not goal-specs. The system prints clause ids in the form shown by goal-specs. When a goal-spec is used in a hint, it is parsed (before the proof attempt begins) into a clause id. During the proof attempt, the system watches for the clause id and uses the corresponding hint when the id arises. (Because of the expense of creating and garbage collecting a lot of strings, this design is more efficient than the alternative.)

COMMAND

Major Section:  MISCELLANEOUS

...the word ``command'' usually refers to a top-level form whose evaluation produces a new logical world.

Typical commands are:
(defun foo (x) (cons x x))
(defthm consp-foo (consp (foo x)))
(defrec pair (hd . tl) nil)

Both events and commands leave landmarks on the world that enable us to determine how the given world was created from the previous one. Most of your interactions will occur at the command level, i.e., you type commands, you print previous commands, and you undo back through commands. Commands are denoted by command descriptors. See command-descriptor.

COMMAND-DESCRIPTOR

Major Section:  MISCELLANEOUS

Examples:


:max      ; the command most recently typed by the user
:x        ; synonymous with :max
(:x -1)   ; the command before the most recent one
(:x -2)   ; the command before that
:x-2      ; synonymous with (:x -2)
5         ; the fifth command typed by the user
1         ; the first command typed by the user
0         ; the last command of the system initialization
-1        ; the next-to-last initialization command
:min      ; the first command of the initialization
fn        ; the command that introduced the logical name fn
(:search (defmacro foo-bar))
          ; the first command encountered in a search from :max to
          ; 0 that either contains defmacro and foo-bar in the 
          ; command form or contains defmacro and foo-bar in some 
          ; event within its block.

The recorded history of your interactions with the top-level ACL2 command loop is marked by the commands you typed that changed the logical world. Each such command generated one or more events, since the only way for you to change the logical world is to execute an event function. See command and see events. We divide history into ``command blocks,'' grouping together each world changing command and its events. A ``command descriptor'' is an object that can be used to describe a particular command in the history of the ongoing session.

Each command is assigned a unique integer called its ``command number'' which indicates the command's position in the chronological ordering of all of the commands ever executed in this session (including those executed to initialize the system). We assign the number 1 to the first command you type to ACL2. We assign 2 to the second and so on. The non-positive integers are assigned to ``prehistoric'' commands, i.e., the commands used to initialize the ACL2 system: 0 is the last command of the initialization, -1 is the one before that, etc.

The legal command descriptors are described below. We use n to denote any integer, sym to denote any logical name (see logical-name), and cd to denote, recursively, any command descriptor.

 command                   command
descriptor                described


:max   -- the most recently executed command (i.e., the one with
          the largest command number)
:x     -- synonymous with :max
:x-k   -- synonymous with (:x -k), if k is an integer and k>0
:min   -- the earliest command (i.e., the one with the smallest
          command number and hence the first command of the system
          initialization)
n      -- command number n  (If n is not in the
          range :min<=n<=:max, n is replaced by the nearest of :min
          and :max.)
sym    -- the command that introduced the logical name sym
(cd n) -- the command whose number is n plus the command number of
          the command described by cd
(:search pat cd1 cd2)
          In this command descriptor, pat must be either an atom or
          a true list of atoms and cd1 and cd2 must be command
          descriptors.  We search the interval from cd1 through cd2
          for the first command that matches pat.  Note that if cd1
          occurs chronologically after cd2, the search is
          ``backwards'' through history while if cd1 occurs
          chronologically before cd2, the search is ``forwards''.  A
          backwards search will find the most recent match; a
          forward search will find the chronologically earliest
          match.  A command matches pat if either the command form
          itself or one of the events in the block contains pat (or
          all of the atoms in pat if pat is a list).
(:search pat)
          the command found by (:search pat :max 0), i.e., the most
          recent command matching pat that was part of the user's
          session, not part of the system initialization.

COMPUTED-HINTS

Major Section:  MISCELLANEOUS

General Form of :hints:
(hint1 hint2 ... hintk)

A common hint is of the form

(goal-spec :key1 val1 ... :keyn valn)

where goal-spec is as specified in goal-spec and each :keyi and vali is as specified in hints.

A computed hint is either a function symbol, fn, of three arguments or is a term involving, at most, the three free variables ID, CLAUSE and WORLD. The function symbol case is treated as an abbreviation of the term (fn ID CLAUSE WORLD). (Note that this tells you which argument is which.) In the discussion below we assume all computed hints are of the term form.

The evaluation of the term (in a context in which its variables are bound as described below) should be either nil, indicating that the hint is not applicable to the clause in question, or else the value is an alternating list of :keyi vali ``pairs'' as specified in hints. The first applicable hint, if any, is used and deleted from the list of hints available to the descendants of the clause (see below).

The evaluation of a hint term is done with guard checking turned off (see set-guard-checking); e.g., the form (car 23) in a computed hint returns nil as per the axioms.

When a non-nil value is returned it is treated just as though it had been typed as part of the original input. That is, your job as the programmer of computed hints is to generate the form you would have typed had you supplied a common hint at that point. (In particular, any theory expressions in it are evaluated with respect to the global current-theory, not whatever theory is active on the subgoal in question.) If the generated list of keywords and values is illegal, an error will be signaled and the proof attempt will be aborted.

It remains only to describe the bindings of the three variables. Suppose the theorem prover is working on some clause, clause, named by some goal-spec, e.g., "Subgoal *1/2'''" in some logical world, world. Corresponding to the printed goal-spec is an internal data structure called a ``clause identifier'' id. See clause-identifier.

In the case of a common hint, the hint applies if the goal-spec of the hint is the same as the goal-spec of the clause in question.

In the case of a computed hint, the variable ID is bound to the clause id, the variable CLAUSE is bound to the (translated form of the) clause, and the variable WORLD is bound to the current ACL2 world.

When a computed hint applies, it is removed from the list of hints available to the children of the clause to which it applied. This prevents it from being reapplied (often infinitely). The goals produced by induction and the top-level goals of forcing rounds are not considered children; all original hints are available to them. Insert n copies of a computed hint into the :hints to allow the hint to be used ``repeatedly'' at n different levels.

For some instruction about how to use computed hints, see using-computed-hints.

CONSTRAINT

Major Section:  MISCELLANEOUS

Suppose that a given theorem, thm, is to be functionally instantiated using a given functional substitution, alist, as described in :DOC lemma-instance. What is the set of proof obligations generated? It is the set of all terms, tm, such that (a) tm mentions some function symbol in the domain of alist, and (b) either tm arises from the ``constraint'' on a function symbol ancestral in thm or some defaxiom or (ii) tm is the body of a defaxiom. Here, a function symbol is ``ancestral'' in thm if either it occurs in thm, or it occurs in the definition of some function symbol that occurs in thm, and so on.

The remainder of this note explains what we mean by ``constraint'' in the words above.

In a certain sense, function symbols are introduced in essentially two ways. The most common way is to use defun (or when there is mutual recursion, mutual-recursion or defuns). There is also a mechanism for introducing ``witness functions''; see defchoose. The documentation for these events describes the axioms they introduce, which we will call here their ``definitional axioms.'' These definitional axioms are generally the constraints on the function symbols that these axioms introduce.

However, when a function symbol is introduced in the scope of an encapsulate event, its constraints may differ from the definitional axioms introduced for it. For example, suppose that a function's definition is local to the encapsulate; that is, suppose the function is introduced in the signature of the encapsulate. Then its constraints include, at the least, those non-local theorems and definitions in the encapsulate that mention the function symbol.

Actually, it will follow from the discussion below that if the signature is empty for an encapsulate, then the constraint on each of its new function symbols is exactly the definitional axiom introduced for it. Intuitively, we view such encapsulates just as we view include-book events. But the general case, where the signature is not empty, is more complicated.

In the discussion that follows we describe in detail exactly which constraints are associated with which function symbols that are introduced in the scope of an encapsulate event. In order to simplify the exposition we make two cuts at it. In the first cut we present an over-simplified explanation that nevertheless captures the main ideas. In the second cut we complete our explanation by explaining how we view certain events as being ``lifted'' out of the encapsulate, resulting in a possibly smaller encapsulate, which becomes the target of the algorithm described in the first cut.

At the end of this note we present an example showing why a more naive approach is unsound.

Finally, before we start our ``first cut,'' we note that constrained functions always have guards of T. This makes sense when one considers that a constrained function's ``guard'' only appears in the context of a local defun, which is skipped. Note also that any information you want ``exported'' outside an encapsulate event must be there as an explicit definition or theorem. For example, even if a function foo has output type (mv t t) in its signature, the system will not know (true-listp (foo x)) merely on account of this information. Thus, if you are using functions like foo (constrained mv functions) in a context where you are verifying guards, then you should probably provide a :type-prescription rule for the constrained function, for example, the :type-prescription rule (true-listp (foo x)).

First cut at constraint-assigning algorithm. Quite simply, the formulas introduced in the scope of an encapsulate are conjoined, and each function symbol introduced by the encapsulate is assigned that conjunction as its constraint.

Clearly this is a rather severe algorithm. Let us consider two possible optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below. The function before1 does not refer at all, even indirectly, to the locally-introduced function sig-fn, so it is unfortunate to saddle it with constraints about sig-fn.

(encapsulate
 (((sig-fn *) => *))


 (defun before1 (x)
   (if (consp x)
       (before1 (cdr x))
     x))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))
 )

(defun before1 (x)
  (if (consp x)
      (before1 (cdr x))
    x))


(encapsulate
 (((sig-fn *) => *))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))
 )

More generally, suppose an event in an encapsulate event does not mention any function symbol in the signature of the encapsulate, nor any function symbol that mentions any such function symbol, and so on. (We might say that no function symbol from the signature is an ``ancestor'' of any function symbol occurring in the event.) Then we imagine moving the event, so that it appears in front of the encapsulate. We don't actually move it, but we pretend we do when it comes time to assign constraints. Thus, such definitions only introduce definitional axioms as the constraints on the function symbols being defined, and such theorems introduce no constraints.

Once this first optimization is performed, we have in mind a set of ``constrained functions.'' These are the functions introduced in the encapsulate that would remain after moving some of them out, as indicated above. Consider the collection of all formulas introduced by the encapsulate, except the definitional axioms, that mention these constrained functions. So for example, in the event below, no such formula mentions the function symbol after1.

(encapsulate
 (((sig-fn *) => *))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))


 (defun after1 (x)
   (sig-fn x))
 )

Many subtle aspects of this rearrangement process have been omitted. For example, suppose the function fn uses sig-fn, the latter being a function in the signature of the encapsulation. Suppose a formula about fn is proved in the encapsulation. Then from the discussion above fn is among the constrained functions of the encapsulate: it cannot be moved before the encapsulate and it cannot be moved after the encapsulation. But why is fn constrained? The reason is that the theorem proved about fn may impose or express constraints on sig-fn. That is, the theorem proved about fn may depend upon properties of the witness used for sig-fn. Here is a simple example:

(encapsulate
 (((sig-fn *) => *))


 (local (defun sig-fn (x) (declare (ignore x)) 0))


 (defun fn (lst)
   (if (endp lst)
       t
       (and (integerp (sig-fn (car lst)))
            (fn (cdr lst)))))


 (defthm fn-always-true
   (fn lst)))

This is a pathological example that illustrate a trap into which one may easily fall: rather than identify the key properties of the constrained function the user has foreshadowed its intended application and constrained those notions. Clearly, the user wishing to introduce the sig-fn above would be well-advised to use the following instead:

(encapsulate
 (((sig-fn *) => *))
 (local (defun sig-fn (x) (declare (ignore x)) 0))
 (defthm integerp-sig-fn
   (integerp (sig-fn x))))

(defun fn (lst)
  (if (endp lst)
      t
    (and (integerp (sig-fn (car lst)))
         (fn (cdr lst)))))

(defthm fn-always-true
   (fn lst)))

Sometimes it is necessary to introduce a function such as fn within the encapsulate merely to state the key properties of the undefined function sig-fn. But that is unusual and the user should understand that both functions are being constrained.

Another subtle aspect of encapsulation that has been brushed over so far has to do with exactly how functions defined within the encapsulation use the signature functions. For example, above we say ``Consider the collection of all formulas introduced by the encapsulate, except the definitional axioms, that mention these constrained functions.'' We seem to suggest that a definitional axiom which mentions a constrained function can be moved out of the encapsulation and considered part of the ``post-encapsulation'' extension of the logic, if the defined function is not used in any non-definitional formula proved in the encapsulation. For example, in the encapsulation above that constrained sig-fn and introduced fn within the encapsulation, fn was constrained because we proved the formula fn-always-true within the encapsulation. Had we not proved fn-always-true within the encapsulation, fn could have been moved after the encapsulation. But this suggests an unsound rule because whether such a function can be moved after the encapsulate depend on whether its admission used properties of the witnesses! In particular, we say a function is ``subversive'' if any of its governing tests or the actuals in any recursive call involve a function in which the signature functions are ancestral.

Another aspect we have not discussed is what happens to nested encapsulations when each introduces constrained functions. We say an encapsulate event is ``trivial'' if it introduces no constrained functions, i.e., if its signatures is nil. Trivial encapsulations are just a way to wrap up a collection of events into a single event.

From the foregoing discussion we see we are interested in exactly how we can ``rearrange'' the events in a non-trivial encapsulation -- moving some ``before'' the encapsulation and others ``after'' the encapsulation. We are also interested in which functions introduced by the encapsulation are ``constrained'' and what the ``constraints'' on each are. We may summarize the observations above as follows, after which we conclude with a more elaborate example.

Second cut at constraint-assigning algorithm. First, we focus only on non-trivial encapsulations that neither contain nor are contained in non-trivial encapsulations. (Nested non-trivial encapsulations are not rearranged at all: do not put anything in such a nest unless you mean for it to become part of the constraints generated.) Second, in what follows we only consider the non-local events of such an encapsulate, assuming that they satisfy the restriction of using no locally defined function symbols other than the signature functions. Given such an encapsulate event, move, to just in front of it and in the same order, all definitions and theorems for which none of the signature functions is ancestral. Now collect up all formulas (theorems) introduced in the encapsulate other than definitional axioms. Add to this set any of those definitional equations that is either subversive or defines a function used in a formula in the set. The conjunction of the resulting set of formulas is called the ``constraint'' and the set of all the signature functions of the encapsulate together with all function symbols defined in the encapsulate and mentioned in the constraint is called the ``constrained functions.'' Assign the constraint to each of the constrained functions. Move, to just after the encapsulate, the definitions of all function symbols defined in the encapsulate that have been omitted from the constraint.

Implementation note. In the implementation we do not actually move events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm. It builds on the preceding examples.

(encapsulate
 (((sig-fn *) => *))


 (defun before1 (x)
   (if (consp x)
       (before1 (cdr x))
     x))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))


 (defun during (x)
   (if (consp x)
       x
     (cons (car (sig-fn x))
           17)))


 (defun before2 (x)
   (before1 x))


 (defthm before2-prop
   (atom (before2 x)))


 (defthm during-prop
   (implies (and (atom x)
                 (before2 x))
            (equal (car (during x))
                   (car (sig-fn x)))))


 (defun after1 (x)
   (sig-fn x))


 (defchoose after2 (x) (u)
   (and (< u x) (during x)))
 )

(SIG-FN X) is axiomatized to return one result.


In addition, we export AFTER2, AFTER1, DURING-PROP, BEFORE2-PROP, BEFORE2,
DURING, SIG-FN-PROP and BEFORE1.


The following constraint is associated with both of the functions DURING
and SIG-FN:


(AND (EQUAL (DURING X)
            (IF (CONSP X)
                X (CONS (CAR (SIG-FN X)) 17)))
     (CONSP (DURING X))
     (CONSP (SIG-FN X))
     (IMPLIES (AND (ATOM X) (BEFORE2 X))
              (EQUAL (CAR (DURING X))
                     (CAR (SIG-FN X)))))

We conclude by asking (and to a certain extent, answering) the following question: Isn't there an approach to assigning constraints that avoids over-constraining more simply than our ``second cut'' above? Perhaps it seems that given an encapsulate, we should simply assign to each locally defined function the theorems exported about that function. If we adopted that simple approach the events below would be admissible.

(encapsulate
 (((foo *) => *))
 (local (defun foo (x) x))
 (defun bar (x)
   (foo x))
 (defthm bar-prop
   (equal (bar x) x)
   :rule-classes nil))


(defthm foo-id
  (equal (foo x) x)
  :hints (("Goal" :use bar-prop)))


; The following event is not admissible in ACL2.


(defthm ouch!
  nil
  :rule-classes nil
  :hints
  (("Goal" :use
    ((:functional-instance foo-id
                           (foo (lambda (x) (cons x x))))))))

It's tempting to think we can fix this by including definitions, not just theorems, in constraints. But consider the following slightly more elaborate example. The problem is that we need to include as a constraint on foo not only the definition of bar, which mentions foo explicitly, but also abc, which has foo as an ancestor.

(encapsulate
 (((foo *) => *))
 (local (defun foo (x) x))
 (local (defthm foo-prop
          (equal (foo x) x)))
 (defun bar (x)
   (foo x))
 (defun abc (x)
   (bar x))
 (defthm abc-prop
   (equal (abc x) x)
   :rule-classes nil))


(defthm foo-id
  (equal (foo x) x)
  :hints (("Goal" :use abc-prop)))


; The following event is not admissible in ACL2.


(defthm ouch!
  nil
  :rule-classes nil
  :hints
  (("Goal" :use
    ((:functional-instance foo-id
                           (foo (lambda (x) (cons x x)))
                           (bar (lambda (x) (cons x x))))))))