Attach a terminating executable function to a definition

Suppose you define a function

(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

(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

Fortunately,

(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 `defun` form above, but to
cause execution 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

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)) :ruler-extenders :basic :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) :ruler-extenders :basic :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) :RULER-EXTENDERS :BASIC :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)) :RULER-EXTENDERS :BASIC :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 `xargs` of the

CAVEAT: Termination is not considered for calls of `mbe` under the
top-level call. Moreover, the `mbe` call under
the

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 `declare` form) must
specify a `keyword-value-listp` each of whose keys is one of `xargs` keys of

The above General Form's macroexpansion is of the form `declare` form, and is the result of
evaluating the given

; 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 `declare`
form are the result of adding

; 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 `mbe` in