VERIFY-TERMINATION

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

Example:
(verify-termination fact)

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.

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 other than to add (declare (xargs :mode :logic)). 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, as well as (declare (xargs :mode :logic)). 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 be tempted to submit the following:
(verify-termination
 fact
 (declare (xargs :guard (and (integerp n) (<= 0 n))))).
However, this is considered a changing of the guard (from (integerp n)), which is illegal. If we instead change the guard in the earlier defun after undoing that earlier definition with :ubt fact, then (verify-termination fact) will succeed.

Remark on system functions. There may be times when you want to apply verify-termination (and also, perhaps, verify-guards) to functions that are predefined in ACL2. It may be necessary in such cases to modify the system code first. See http://www.cs.utexas.edu/users/moore/acl2/open-architecture/ for a discussion of the process for contributing updates to the system code and books with such verify-termination or verify-guards events. To see which built-in :program mode functions have already received such treatment, see directory books/system; for example, use the Unix utility `grep' to search:

grep '(verify-' books/system/*.lisp

Note that if fn1 is already in :logic mode, then the verify-termination call has no effect. It is generally considered to be redundant, in the sense that it returns without error; but if the fn1 is a constrained function (i.e., introduced in the signature of an encapsulate, or by defchoose), then an error occurs. This error is intended to highlight unintended uses of verify-termination; but if you do not want to see an error in this case, you can write and use your own macro in place of verify-termination. The following explanation of the implementation of verify-termination may help with such a task.

We conclude with a discussion of the use of make-event to implement verify-termination. This discussion can be skipped; we include it only for those who want to create variants of verify-termination, or who are interested in seeing an application of make-event.

Consider the following proof of nil, which succeeded up through Version_3.4 of ACL2.

(encapsulate
 ()
 (defun foo (x y)
   (declare (xargs :mode :program))
   (if (or (zp x) (zp y))
       (list x y)
     (foo (1+ x) (1- y))))
 (local (defun foo (x y)
          (declare (xargs :measure (acl2-count y)))
          (if (or (zp x) (zp y))
              (list x y)
            (foo (1+ x) (1- y)))))
 (verify-termination foo))

(defthm bad-lemma
  (zp x)
  :hints (("Goal" :induct (foo x 1)))
  :rule-classes nil)
How did this work? In the first pass of the encapsulate, the second defun of foo promoted foo from :program to :logic mode, with y as the unique measured variable. The following call to verify-termination was then redundant. However, on the second pass of the encapsulate, the second (local) definition of foo was skipped, and the verify-termination event then used the first definition of foo to guess the measure, based (as with all guesses of measures) on a purely syntactic criterion. ACL2 incorrectly chose (acl2-count x) as the measure, installing x as the unique measured variable, which in turn led to an unsound induction scheme subsequently used to prove nil (lemma bad-lemma, above)

Now, verify-termination is a macro whose calls expand to make-event calls. So in the first pass above, the verify-termination call generated a defun event identical to the local defun of foo, which was correctly identified as redundant. That expansion was recorded, and on the second pass of the encapsulate, the expansion was recalled and used in place of the verify-termination call (that is how make-event works). So instead of a measure being guessed for the verify-termination call on the second pass, the same measure was used as was used on the first pass, and a sound induction scheme was stored. The attempt to prove nil (lemma bad-lemma) then failed.