DEFEXEC

attach a terminating executable function to a definition 
Major Section:  EVENTS

Suppose you define a function (fn x) with a guard of (good-input-p x), and you know that when the guard holds, the measure decreases on each recursive call. Unfortunately, the definitional principle (see defun) ignores the guard. For example, if the definition has the form 

(defun fn (x)
  (declare (xargs :guard (good-input-p x)))
  (if (not-done-yet x)
      (... (fn (destr x)) ...)
    ...))
then in order to admit this definition, ACL2 must prove the appropriate formula asserting that (destr x) is ``smaller than'' x under the assumption (not-done-yet x) but without the assumption (good-input-p x), even if (not-done-yet x) is true. In essence, it may be necessary to submit instead the following definition. 
(defun fn (x)
  (declare (xargs :guard (good-input-p x)))
  (if (good-input-p x)
      (if (not-done-yet x)
          (... (fn (destr x)) ...)
        ...)
    nil)
But it is unfortunate that when calls of fn are evaluated, for example when fn is applied to an explicit constant during a proof, then a call of good-input-p must now be evaluated on each recursive call.

Fortunately, defexec provides a way to keep the execution efficient. For the example above we could use the following form. 

(defexec fn (x)
  (declare (xargs :guard (good-input-p x)))
  (mbe :logic (if (good-input-p x)
                  (if (not-done-yet x)
                      (... (fn (destr x)) ...)
                    ...)
                nil)
       :exec  (if (not-done-yet x)
                  (... (fn (destr x)) ...)
                ...)))
Here ``mbe'' stands for ``must-be-equal'' and, roughly speaking, its call above is logically equal to the :logic form but is evaluated using the :exec form when the guard holds. See mbe. The effect is thus to define fn as shown in the defun form above, but to cause execution of fn using the :exec body. The use of defexec instead of defun in the example above causes a termination proof to be performed, in order to guarantee that evaluation always theoretically terminates, even when using the :exec form for evaluation. 
Example:


; Some of the keyword arguments in the declarations below are irrelevant or
; unnecessary, but they serve to illustrate their use.


(defexec f (x)
  (declare (xargs :measure (+ 15 (acl2-count x))
                  :hints (("Goal" :in-theory (disable nth)))
                  :guard-hints (("Goal" :in-theory (disable last)))
                  :guard (and (integerp x) (<= 0 x) (< x 25)))
           (exec-xargs
                  :test (and (integerp x) (<= 0 x))
                  :default-value 'undef ; defaults to nil
                  :measure (nfix x)
                  :well-founded-relation o<))
  (mbe :logic (if (zp x)
                  1
                (* x (f (- x 1))))
       :exec  (if (= x 0)
                  1
                (* x (f (- x 1))))))
The above example macroexpands to the following. 
(ENCAPSULATE ()
 (LOCAL
  (ENCAPSULATE ()
   (SET-IGNORE-OK T)
   (SET-IRRELEVANT-FORMALS-OK T)
   (LOCAL (DEFUN F (X)
            (DECLARE
             (XARGS :VERIFY-GUARDS NIL
                    :HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
                    :MEASURE (NFIX X)
                    :WELL-FOUNDED-RELATION O<))
            (IF (AND (INTEGERP X) (<= 0 X))
                (IF (= X 0) 1 (* X (F (- X 1))))
                'UNDEF)))
   (LOCAL (DEFTHM F-GUARD-IMPLIES-TEST
            (IMPLIES (AND (INTEGERP X) (<= 0 X) (< X 25))
                     (AND (INTEGERP X) (<= 0 X)))
            :RULE-CLASSES NIL))))
 (DEFUN F (X)
   (DECLARE (XARGS :MEASURE (+ 15 (ACL2-COUNT X))
                   :HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
                   :GUARD-HINTS (("Goal" :IN-THEORY (DISABLE LAST)))
                   :GUARD (AND (INTEGERP X) (<= 0 X) (< X 25))))
   (MBE :LOGIC
        (IF (ZP X) 1 (* X (F (- X 1))))
        :EXEC
        (IF (= X 0) 1 (* X (F (- X 1)))))))
Notice that in the example above, the :hints in the local definition of F are inherited from the :hints in the xargs of the defexec form. We discuss such inheritance below. 
General Form:
(defexec fn (var1 ... varn) doc-string dcl ... dcl
  (mbe :LOGIC logic-body
       :EXEC  exec-body))
where the syntax is identical to the syntax of defun where the body is a call of mbe, with the exceptions described below. Thus, fn is the symbol you wish to define and is a new symbolic name and (var1 ... varn) is its list of formal parameters (see name). The first exception is that at least one dcl (i.e., declare form) must specify a :guard, guard. The second exception is that one of the dcls is allowed to contain an element of the form (exec-xargs ...). The exec-xargs form, if present, must specify a non-empty keyword-value-listp each of whose keys is one of :test, :default-value, or one of the standard xargs keys of :measure, :well-founded-relation, :hints, or :stobjs. Any of these four standard xargs keys that is present in an xargs of some dcl but is not specified in the (possibly nonexistent) exec-xargs form is considered to be specified in the exec-xargs form, as illustrated in the example above for :hints. (So for example, if you want :hints in the final, non-local definition but not in the local definition, then specify the :hints in the xargs but specify :hints nil in the exec-xargs.) If :test is specified and not nil, let test be its value; otherwise let test default to guard. If :default-value is specified, let default-value be its value; else default-value is nil. Default-value should have the same signature as exec-body; otherwise the defexec form will fail to be admitted.

The above General Form's macroexpansion is of the form (PROGN encap final-def), where encap and final-def are as follows. Final-def is simply the result of removing the exec-xargs declaration (if any) from its declare form, and is the result of evaluating the given defexec form, since encap is of the following form. 

; encap
(ENCAPSULATE ()
  (set-ignore-ok t)             ; harmless for proving termination
  (set-irrelevant-formals-ok t) ; harmless for proving termination
  (local local-def)
  (local local-thm))
The purpose of encap is to ensure the the executable version of name terminates on all arguments. Thus, local-def and local-thm are as follows, where the xargs of the declare form are the result of adding :VERIFY-GUARDS NIL to the result of removing the :test and (optional) :default-value from the exec-xargs. 
; local-def
(DEFUN fn formals
  (DECLARE (XARGS :VERIFY-GUARDS NIL ...))
  (IF test
      exec-body
    default-value))


; local-thm
(DEFTHM fn-EXEC-GUARD-HOLDS
  (IMPLIES guard test)
  :RULE-CLASSES NIL)
We claim that if the above local-def and local-thm are admitted, then all evaluations of calls of fn terminate. The concern is that the use of mbe in final-def allows for the use of exec-body for a call of fn, as well as for subsequent recursive calls, when guard holds and assuming that the guards have been verified for final-def. However, by local-thm we can conclude in this case that test holds, in which case the call of fn may be viewed as a call of the version of fn defined in local-def. Moreover, since guards have been verified for final-def, then guards hold for subsequent evaluation of exec-body, and in particular for recursive calls of fn, which can thus continue to be viewed as calls using local=def.