a table used to validate meta rules
Major Section:  EVENTS

(table term-table t '((binary-+ x y) '3 'nil (car x)))

See table for a general discussion of tables and the table event used to manipulate tables.

The ``term-table'' is used at the time a meta rule is checked for syntactic correctness. Each proposed metafunction is run on each term in this table, and the result in each case is checked to make sure that it is a termp in the current world. In each case where this test fails, a warning is printed.

Whenever a metafunction is run in support of the application of a meta rule, the result must be a term in the current world. When the result is not a term, a hard error arises. The term-table is simply a means for providing feedback to the user at the time a meta rule is submitted, warning of the definite possibility that such a hard error will occur at some point in the future.

The key used in term-table is arbitrary. The top-most value is always the one that is used; it is the entire list of terms to be considered. Each must be a termp in the current ACL2 world.


user-specified invariants on theories
Major Section:  EVENTS

(theory-invariant (not (and (member-equal '(:rewrite left-to-right)
                            (member-equal '(:rewrite right-to-left)

General Forms: (theory-invariant term) ; conjoin a new invariant term or (theory-invariant term key) ; change an existing invariant term

where term is a term that uses no variables other than theory and world, and key is an arbitrary ``name'' for this invariant. If key is omitted, an integer is generated and used. Theory-invariant is an event that adds to or modifies the table of user-supplied theory invariants that are checked each time a theory expression is evaluated.

The theory invariant mechanism is provided via a table (see table) named theory-invariant-table. In fact, the theory-invariant ``event'' is just a macro that expands into a use of the table event. More general access to the theory-invariant table is provided by table itself. For example, the table can be inspected or cleared (setting the invariant to t) with table.

Theory-invariant-table maps arbitrary keys to terms mentioning, at most, the variables theory and world. Every time an alleged theory expression is evaluated, e.g., in the in-theory event or :in-theory hint, each of the terms in theory-invariant-table is evaluated with theory bound to the runic theory (see theories) obtained from the theory expression and world bound to the current ACL2 world (see world). If the result is nil, a warning message is printed. Thus, the table can be thought of as a list of conjuncts. Each term in the table has a ``name,'' which is just the key under which the term is stored. When a theory violates the restrictions specified by some term, both the name and the term are printed. By calling theory-invariant with a new term but the same name, you can overwrite that conjunct of the theory invariant.

Theory invariants are particularly useful in the context of large rule sets intended for re-use. Such sets often contain conflicting rules, e.g., rules that are to be enabled when certain function symbols are disabled, rules that rewrite in opposite directions and thus loop if simultaneously enabled, groups of rules which should be enabled in concert, etc. The developer of such rule sets understands these restrictions and probably documents them. The theory invariant mechanism allows the developer to codify his restrictions so that when they are violated the user is warned.

Since theory invariants are arbitrary terms, macros may be used to express commonly used restrictions. Because theory invariants are a new idea in ACL2, we have only defined one such macro for illustrative purposes. Executing the event

(theory-invariant (incompatible (:rewrite left-to-right)
                                (:rewrite right-to-left)))
would subsequently cause a warning message any time the current theory contained both of the two runes shown. Of course, incompatible is just defined as a macro. Its definition may be inspected with :pe incompatible.

Note: If the table event is used directly to :put a term into the theory invariant table, be aware that the term must be in translated form. This is enforced by the value invariant for theory-invariant-table. But the upshot of this is that you will be unable to use macros in theory invariants stored directly with the :put table event.


verify the guards of a function
Major Section:  EVENTS

(verify-guards flatten)
(verify-guards flatten
               :hints (("Goal" :use (:instance assoc-of-app)))
               :otf-flg t
               :doc "string")

General Form: (verify-guards name :hints hints :otf-flg otf-flg :doc doc-string)

See guard for a general discussion of guards. In the General Form above, name is the name of a :logic function (see defun-mode) or of a theorem or axiom. In the most common case name is the name of a function that has not yet had its guards verified, each subroutine of which has had its guards verified. hints and otf-flg are as described in the corresponding :doc entries; and doc-string, if supplied, is a string not beginning with ``:Doc-Section''. The three keyword arguments above are all optional. Verify-guards will attempt to prove that the guard on the named function implies the guards of all of the subroutines called in the body of the function. If successful, name is considered to have had its guards verified.

If name is one of several functions in a mutually recursive clique, verify-guards will attempt to verify the guards of all of the functions.

If name is a theorem or axiom name, verify-guards verifies the guards of the associated formula. When a theorem has had its guards verified then you know that the theorem will evaluate to non-nil in all Common Lisps, without causing a runtime error (other than possibly a resource error). In particular, you know that the theorem's validity does not depend upon ACL2's arbitrary completion of the domains of partial Common Lisp functions.

For example, if app is defined as

(defun app (x y)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      (cons (car x) (app (cdr x) y))))
then we can verify the guards of app and we can prove the theorem:
(defthm assoc-of-app
  (equal (app (app a b) c) (app a (app b c))))
However, if you go into almost any Common Lisp in which app is defined as shown and evaluate
(equal (app (app 1 2) 3) (app 1 (app 2 3)))
we get an error or, perhaps, something worse like nil! How can this happen since the formula is an instance of a theorem? It is supposed to be true!

It happens because the theorem exploits the fact that ACL2 has completed the domains of the partially defined Common Lisp functions like car and cdr, defining them to be nil on all non-conses. The formula above violates the guards on app. It is therefore ``unreasonable'' to expect it to be valid in Common Lisp.

But the following formula is valid in Common Lisp:

(if (and (true-listp a)
         (true-listp b))
    (equal (app (app a b) c) (app a (app b c)))
That is, no matter what the values of a, b and c the formula above evaluates to t in all Common Lisps (unless the Lisp engine runs out of memory or stack computing it). Furthermore the above formula is a theorem:
(defthm guarded-assoc-of-app
  (if (and (true-listp a)
           (true-listp b))
      (equal (app (app a b) c) (app a (app b c)))
This formula, guarded-assoc-of-app, is very easy to prove from assoc-of-app. So why prove it? The interesting thing about guarded-assoc-of-app is that we can verify the guards of the formula. That is, (verify-guards guarded-assoc-of-app) succeeds. Note that it has to prove that if a and b are true lists then so is (app a b) to establish that the guard on the outermost app on the left is satisfied. By verifying the guards of the theorem we know it will evaluate to true in all Common Lisps. Put another way, we know that the validity of the formula does not depend on ACL2's completion of the partial functions or that the formula is ``well-typed.''

One last complication: The careful reader might have thought we could state guarded-assoc-of-app as

(implies (and (true-listp a)
              (true-listp b))
         (equal (app (app a b) c)
                (app a (app b c))))
rather than using the if form of the theorem. We cannot! The reason is technical: implies is defined as a function in ACL2. When it is called, both arguments are evaluated and then the obvious truth table is checked. That is, implies is not ``lazy.'' Hence, when we write the guarded theorem in the implies form we have to prove the guards on the conclusion without knowing that the hypothesis is true. It would have been better had we defined implies as a macro that expanded to the if form, making it lazy. But we did not and after we introduced guards we did not want to make such a basic change.

Recall however that verify-guards is almost always used to verify the guards on a function definition rather than a theorem. We now return to that discussion.

Because name is not uniquely associated with the verify-guards event (it necessarily names a previously defined function) the documentation string, doc-string, is not stored in the documentation data base. Thus, we actually prohibit doc-string from having the form of an ACL2 documentation string; see doc-string.

Verify-guards must often be used when the value of a recursive call of a defined function is given as an argument to a subroutine that is guarded. An example of such a situation is given below. Suppose app (read ``append'') has a guard requiring its first argument to be a true-listp. Consider

(defun rev (x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) nil)
        (t (app (rev (cdr x)) (list (car x))))))
Observe that the value of a recursive call of rev is being passed into a guarded subroutine, app. In order to verify the guards of this definition we must show that (rev (cdr x)) produces a true-listp, since that is what the guard of app requires. How do we know that (rev (cdr x)) is a true-listp? The most elegant argument is a two-step one, appealing to the following two lemmas: (1) When x is a true-listp, (cdr x) is a true-listp. (2) When z is a true-listp, (rev z) is a true-listp. But the second lemma is a generalized property of rev, the function we are defining. This property could not be stated before rev is defined and so is not known to the theorem prover when rev is defined.

Therefore, we might break the admission of rev into three steps: define rev without addressing its guard verification, prove some general properties about rev, and then verify the guards. This can be done as follows:

(defun rev (x)
  (declare (xargs :guard (true-listp x)
                  :verify-guards nil))    ; Note this additional xarg.
  (cond ((endp x) nil)
        (t (app (rev (cdr x)) (list (car x))))))

(defthm true-listp-rev (implies (true-listp x2) (true-listp (rev x2))))

(verify-guards rev)

The ACL2 system can actually admit the original definition of rev, verifying the guards as part of the defun event. The reason is that, in this particular case, the system's heuristics just happen to hit upon the lemma true-listp-rev. But in many more complicated functions it is necessary for the user to formulate the inductively provable properties before guard verification is attempted.


convert a function from :program mode to :logic mode
Major Section:  EVENTS

(verify-termination fact)
 (declare (xargs :guard (and (integerp x) (>= x 0)))))

General Forms: (verify-termination fn dcl ... dcl) (verify-termination (fn1 dcl ... dcl) (fn2 dcl ... dcl) ...)

where fn and the fni are function symbols having :program mode (see defun-mode) and all of the dcls are either declare forms or documentation strings. The first form above is an abbreviation for
(verify-termination (fn dcl ... dcl))
so we limit our discussion to the second form. Each of the fni must be in the same clique of mutually recursively defined functions, but not every function in the clique need be among the fni.

Verify-termination attempts to establish the admissibility of the fni. Verify-termination retrieves their definitions, creates modified definitions using the dcls supplied above, and resubmits these definitions. You could avoid using verify-termination by typing the new definitions yourself. So in that sense, verify-termination adds no new functionality. But if you have prototyped your system in :program mode and tested it, you can use verify-termination to resubmit your definitions and change their defun-modes to :logic, addings hints without having to retype or recopy the code. You can also add or modify guards at this time.

The defun command executed by verify-termination is obtained by retrieving the defun (or mutual-recursion) command that introduced the clique in question and then possibly modifying each definition as follows. Consider a function, fn, in the clique. If fn is not among the fni above, its definition is left unmodified. Otherwise, fn is some fni and we modify its definition by inserting into it the corresponding dcls listed with fni in the arguments to verify-termination. In addition, we throw out from the old declarations in fn the :mode specification and anything that is specified in the new dcls.

For example, suppose that fact was introduced with:

(defun fact (n)
  (declare (type integer n)
           (xargs :mode :program))
  (if (zp n) 1 (* n (fact (1- n))))).
Suppose later we do (verify-termination fact). Then the following definition is submitted.
(defun fact (n)
  (declare (type integer n))
  (if (zp n) 1 (* n (fact (1- n))))).
Observe that this is the same definition as the original one, except the old specification of the :mode has been deleted so that the defun-mode now defaults to :logic. Although the termination proof succeeds, ACL2 also tries to verify the guard, because we have (implicitly) provided a guard, namely (integerp n), for this function. (See guard for a general discussion of guards, and see type-spec for a discussion of how type declarations are used in guards.) Unfortunately, the guard verification fails, because the subterm (zp n) requires that n be nonnegative, as can be seen by invoking :args zp. (For a discussion of termination issues relating to recursion on the naturals, see zero-test-idioms.) So we might want to submit
 (declare (xargs :guard (and (integerp n) (<= 0 n)))))
which will submit the definition
(defun fact (n)
  (declare (xargs :guard (and (integerp n) (<= 0 n))))
  (if (zp n) 1 (* n (fact (1- n))))).
Observe that the declaration in the verify-termination command has been inserted into the definition. In fact, this command succeeds.