Two proposals for attaching executable functions to logic definitions
                                 Matt Kaufmann
                             ACL2 Seminar 1/15/03
                      Jointly developed with Rob Sumners
                with useful feedback including a key idea from
                                 Vernon Austel

============================================================

Emails from Dave Greve, Jose-Luis Ruiz, and probably others have pointed out a
problem with obtaining efficient execution.  Suppose you want to define a
function such as the following.

  (defun foo (x)
    (declare (xargs :guard (good-arg x)))
    (if (test x)
        (foo (destr x))
      (base x)))

Perhaps, however, (test x) isn't enough to conclude that (destr x) is smaller
than x, specifically:

  (implies (test x)
           (e0-ord-< (acl2-count (destr x))
                     (acl2-count x)))

But suppose we can prove the following:

  (implies (and (good-arg x)
                (test x))
           (e0-ord-< (acl2-count (destr x))
                     (acl2-count x)))

So, we instead define foo as follows:

  (defun foo (x)
    (declare (xargs :guard (good-arg x)))
    (if (and (good-arg x)
             (test x))
        (foo (destr x))
      (base x)))

Unfortunately, if good-arg is an expensive function to run, foo could be
needlessly slow, especially if the original definition of foo is one for which
the guards can be verified:

  (implies (and (good-arg x) (test x))
           (good-arg (destr x)))

Below are two proposals for solving this problem.  The first one is based on a
suggestion from Vernon Austel.  The second is included because it may provide a
more natural solution in some cases.  But I'm leaning towards the first
proposal, both because it is probably much simpler to implement and because it
is probably easier to use in most cases.  At the end we'll see how the first
proposal is general enough to "implement" the second proposal.

============================================================
PROPOSAL #1 [based on an idea of Vernon Austel]
============================================================

Consider the following function, where "mbt" is mnemonic for "must be true".

(defun mbt (x)
  (declare (xargs :guard (eq x t)))
  x)

But suppose we can define mbt under the hood, in Common Lisp, as follows:

(defmacro mbt (x)
  (declare (ignore x))
  t)

We can then deal with the example above by wrapping mbt around the guard:

  (defun foo (x)
    (declare (xargs :guard (good-arg x)))
    (if (and (MBT (good-arg x))
             (test x))
        (foo (destr x))
      (base x)))

Until the guards are verified, we get the slow code, where (good-arg x) is
evaluated.  But after verify-guards, calls of (foo x) for which (good-arg x) is
true are evaluated in raw Lisp.  The raw Lisp code avoids evaluating (good-arg
x), by definition of the macro mbt.  This is logically sound because we have
verified the guard of mbt on the call (mbt (good-arg x)), which ensures that
the evaluation of (good-arg x) in the body would return t anyhow.

Another example.

The mbt idea handles a similar sort of problem related to termination.
Consider the following example, where (destr x) cannot be proven smaller than x
under the (test x) assumption, perhaps because (destr x) is really of the form
(.... (foo (d x)) ....).

  (defun foo (x)
    (declare (xargs :guard (good-arg x)))
    (if (and (test x)
             (mbt (< (acl2-count (destr x)) (acl2-count x))))
        (foo (destr x))
      (base x)))

In the usual case like this, one can prove the following after admitting foo.

  (implies (test x)
           (< (acl2-count (destr x)) (acl2-count x)))

In fact, part of the proof obligation generated by (verify-guards foo) will be:

  (implies (and (good-arg x)
                (test x))
           (< (acl2-count (destr x)) (acl2-count x)))

Once (verify-guards foo) succeeds, calls of foo will lead (when the guard is
met) to calls of the Common Lisp function foo, in which the mbt call has been
replaced by t.

============================================================
PROPOSAL #2
============================================================

The following proposal solves the fast evaluation problem by allowing the user
to define two functions: function foo, to be used in the logic, and function
foo-exec (say), to be executed.  Here are events to be submitted.

  (defbody foo (x)
    foo-exec
    (declare (xargs :guard (good-arg x)))
    (if (and (good-arg x) (test x))
        (foo (destr x))
      (base x)))

  (defun foo-exec (x)
    (declare (xargs :guard (good-arg x) :mode :program))
    (if (test x)
        (foo-exec (destr x))
      (base x)))

  (set-exec ((foo foo-exec)))

The (defbody foo ...) form is treated just like a defun in the logic.  But
under the hood, its Common Lisp function and its so-called
executable-counterpart (also called "*1*") function are set up to call foo-exec
once the set-exec has been executed.  Some details are below, but the basic
idea is to replace the original body of foo by (if xxx (foo-exec x)
<original-body>), where xxx is true after the set-exec has been executed.

The above three forms could be generated by a single call:

  (defexec foo (x)
    (foo-exec (if (test x)
                  (foo-exec (destr x))
                (base x)))
    (declare (xargs :guard (good-arg x)))
    (if (and (good-arg x)
             (test x))
        (foo (destr x))
      (base x)))

Here is Example 2 from the preceding section (Proposal #1), done using defexec.

  (defexec foo (x)
    (foo-exec (if (test x)
                  (foo-exec (destr x))
                (base x)))
    (declare (xargs :guard (good-arg x)))
    (if (and (test x)
             (< (acl2-count (destr x)) (acl2-count x)))
        (foo (destr x))
      (base x)))

By the way, this proposal gives a way to execute encapsulated functions.  Given
for example (encapsulate ((fn-abs (x) t)...) ...), we can define

   (defbody fn (x) 
     fn-exec
     (declare (xargs :guard ...))
     (fn-abs x))

and then defun fn-exec and execute (set-exec ((fn fn-exec))).  Then we can use
fn everywhere in our work rather than fn-abs. If fn-abs is too constrained to
be able to prove the theorem required for the set-exec, but you want to install
fn-exec anyhow, you can use (skip-proofs (set-exec ((fn fn-exec)))).

============================================================

New event:

     (defbody fn (var1 ... varn)
        fn-exec
        doc-string dcl ... dcl body)

The :mode is considered :logic; it is an error to specify :program in the dcls.

Effect:

Logically, this is the same as replacing defbody by defun and omitting fn-exec.

In raw Lisp, this expands to the following, where XXX is (global-symbol fn).

     (defun fn (var1 ... varn) doc-string dcl ... dcl
        (if (get 'XXX 'exec)
            (fn-exec var1 ... varn)
          body))

The definition of *1*fn is as it was before, but instead of calling raw Lisp fn
when the guard is true, it calls raw Lisp fn-exec when both (get 'XXX 'exec)
and the guard are true, and calls raw Lisp fn only when the guard is true but
(get 'XXX 'exec) is false.

Technical points.

(1) If fn is recursive, then instead we use the following.

     (defun fn (var1 ... varn) doc-string dcl ... dcl
        (if (get 'XXX 'exec)
            (fn-exec var1 ... varn)
          (labels ((fn (var1 ... varn) body))
             body)))

It may be useful to modify trace to warn about recursive calls or about
the existence of execution function fn-exec.

(2) An attempt will be made to turn off compiler warnings about undefined
functions (because fn-exec need not yet be defined).

(3) The above call (fn-exec var1 ... varn) requires IGNORE declarations to be
stripped out of declare forms when macroexpanding defbody to defun in raw Lisp.

(4) Fn-exec is normally a name, but it can be of the form (exec-name
exec-body).  In that case, we normally require that exec-name has already been
defined, and we replace (fn-exec var1 ... varn) above by exec-body.  (Without
the requirement that exec-name has been defined, the compiler could perhaps be
confused if there are calls of as-yet-undefined macros in that body.  But see
the defexec proposal below.)  In this case we go ahead and leave ignore
declarations in place (skipping (3) just above).  But note that one might need
to use set-ignore-ok in case some vari is ignored in fn but not in fn-exec,
since in that case, Common Lisp may require us to avoid using (declare (ignore
vari)) -- or alternatively, the user could replace the body of fn with (prog2$
var-i body).

============================================================

New event:

     (set-exec fn-exec-alist)

Fn-exec-alist is a true list with elements of the form (fn fn-exec), where fn
is associated with the name fn-exec in some previous defbody.

For each such (fn fn-exec) pair, the formals of fn and fn-exec must be
identical, as must be the guards.  Also, all such fn must be in
:logic mode.  Let fs be the functional substitution associating each such
fn-exec with fn.  Now for each such pair (fn fn-exec), let fnbody be the result
of functionally substituting fs into the body of fn-exec.  Fnbody must be in
:logic mode, and we must prove the following, where g-fn is the common guard of
fn and fn-exec.

     (implies g-fn (equal (fn var1 ... varn) fnbody))

Also, we must apply guard verification to each fnbody.  More precisely, we
apply guard verification as though the sequence of definitions has been
modified as shown here for fn:

     (defun fn (declare (xargs :guard g-fn)) (var1 ... varn) fnbody)

The result of this event is to (setf (get (global-symbol fn) 'exec) t) and also
to mark fn as having had its guards verified: (eq (symbol-class fn (w state))
:common-lisp-compliant).  The undo-stack is maintained appropriately.

============================================================

Let us see how the defexec example above expands in the logic and in raw Lisp.
Again, the example is:

  (defexec foo (x)
    (foo-exec (if (test x) (foo-exec (destr x)) (base x)))
    (declare (xargs :guard (good-arg x)))
    (if (and (good-arg x)
             (test x))
        (foo (destr x))
      (base x)))

This macro call expands to:

  (defbody foo (x)
    (foo-exec (if (test x) (foo-exec (destr x)) (base x)))
    (declare (xargs :set-exec t))
    (declare (xargs :guard (good-arg x)))
    (if (and (good-arg x) (test x))
        (foo (destr x))
      (base x)))

The form (declare (xargs :set-exec t)) requires that foo-exec has *not* yet
been defined, and then to define it in program mode using the indicated body
and the same formals and guard.  Moreover, it (essentially) calls (set-exec
((foo foo-exec))).  If any of this fails, the defexec fails.

In the logic, the above form expands to the following.

  (progn
    (defun foo-exec (x)
      (declare (xargs :mode :program))
      (declare (xargs :guard (good-arg x)))
      (if (test x) (foo-exec (destr x)) (base x)))
    (defbody foo (x)
      (foo-exec (if (test x) (foo-exec (destr x)) (base x)))
      (declare (xargs :guard (good-arg x)))
      (if (and (good-arg x) (test x))
          (foo (destr x))
        (base x)))
    (set-exec ((foo foo-exec))))

However, in raw Lisp the expansion is as follows.  Notice that now we have no
efficiency hit at all.

  (progn
    (defun foo-exec (x)
      (declare (xargs :guard (good-arg x)))
      (if (test x)
          (foo-exec (destr x))
        (base x)))
    (defun foo (x)
      (declare (xargs :set-exec t))
      (declare (xargs :guard (good-arg x)))
      ;; body of foo-exec follows:
      (if (test x)
          (foo-exec (destr x))
        (base x))))

============================================================

Other considerations:

Mutual-recursion would be modified to allow all defbody forms, each without
:set-exec declarations.  (With some thought we might be able to remove that
restriction.)

Do we want to allow a :program mode function to be "upgraded" to :logic mode
using defbody?  For simplicity, let's not.

I need to convince myself that local events cannot cause a problem.  For
example, I need to think about (local (defbody ...)) inside an encapsulate.

============================================================

How defbody generates a *1* function, by way of example.

(defbody foo (x)
  foo-exec
  (declare (xargs :guard (integer-listp x) :verify-guards nil))
  (if (consp x)
      (+ (car x) (foo (cdr x)))
    0))

This would produce the following.  What is shown is actually what is currently
produces for the corresponding (defun foo (x) ...), except for the 2 new lines
shown in lower case (and the extra parenthesis below them).  This is of course
a silly example, since it's difficult to see how we could define foo-exec to be
more efficient than foo!

(DEFUN ACL2_*1*_ACL2::FOO (X)
  (LABELS ((ACL2_*1*_ACL2::FOO
            (X)
            (IF (CONSP X)
                (ACL2_*1*_ACL2::BINARY-+
                 (ACL2_*1*_COMMON-LISP::CAR X)
                 (ACL2_*1*_ACL2::FOO
                  (ACL2_*1*_COMMON-LISP::CDR X)))
                '0)))
          (LET ((ACL2_*1*_ACL2::FOO (SYMBOL-CLASS 'FOO (W *THE-LIVE-STATE*))))
               (COND
                ((EQ ACL2_*1*_ACL2::FOO :COMMON-LISP-COMPLIANT)
                 (COND
                  ((INTEGER-LISTP X)
                   (RETURN-FROM ACL2_*1*_ACL2::FOO
                                (if (get ACL2_*1*_ACL2::FOO 'exec)
                                    (foo-exec x)
                                  (FOO X))))
                  ((F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*)
                   (THROW-RAW-EV-FNCALL
                    (LIST 'EV-FNCALL-GUARD-ER 'FOO (LIST X)
                          '(INTEGER-LISTP X) '(NIL))))))
                ((AND (F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*)
                      (NOT (ACL2_*1*_ACL2::INTEGER-LISTP X)))
                 (THROW-RAW-EV-FNCALL
                  (LIST 'EV-FNCALL-GUARD-ER 'FOO (LIST X) '(INTEGER-LISTP X)
                        '(NIL)))))
               (ACL2_*1*_ACL2::FOO X))))

Without the ":verify-guards nil", the first COND would be replaced by the
second COND, for both defbody and (as is now done already) defun.

Technical note: Perhaps it would be more efficient for defpkg to create a new
package, much as it currently creates global and *1* packages (see end of
definition of defpkg-raw in the ACL2 sources).  Then we could just use (boundp
'new-package::FOO) in place of (get 'ACL2_*1*_ACL2::FOO 'exec) above.

Note:  If the defbody form came with (declare (xargs :set-exec t)), then we
would replace these lines

                                (if (get ACL2_*1*_ACL2::FOO 'exec)
                                    (foo-exec x)
                                  (FOO X))

with the body of foo-exec.  Moreover, since the guards were verified, we could
eliminate the outer COND.  So we would obtain:

(DEFUN ACL2_*1*_ACL2::FOO (X)
  (LABELS ((ACL2_*1*_ACL2::FOO
            (X)
            (IF (CONSP X)
                (ACL2_*1*_ACL2::BINARY-+
                 (ACL2_*1*_COMMON-LISP::CAR X)
                 (ACL2_*1*_ACL2::FOO
                  (ACL2_*1*_COMMON-LISP::CDR X)))
                '0)))
          (LET ((ACL2_*1*_ACL2::FOO (SYMBOL-CLASS 'FOO (W *THE-LIVE-STATE*))))
               (COND
                ((INTEGER-LISTP X)
                 (RETURN-FROM ACL2_*1*_ACL2::FOO
                              <body_of_foo-exec>))
                ((F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*)
                 (THROW-RAW-EV-FNCALL
                  (LIST 'EV-FNCALL-GUARD-ER 'FOO (LIST X)
                        '(INTEGER-LISTP X) '(NIL)))))
               (ACL2_*1*_ACL2::FOO X))))

============================================================
COMPARING PROPOSAL #1 WITH PROPOSAL #2
============================================================

Proposal #2 allows you to define your -exec functions in a separate file.  You
could, for example, certify a "slow" book of defbody functions, and then
certify an "efficient" book that includes the "slow" book and contains set-exec
forms along with efficient implementations via -exec functions.  One could try
a variety of different such "efficient" books.  However, the order of the books
could be reversed, where the "efficient" book is included in the "slow" book.
The price of this reversal would be relatively minor:  Each time the
"efficient" book is changed, the "slow" book would have to be recertified.

Proposal #1 allows some of this same functionality, albeit in a slightly more
cumbersome manner, and where the -exec function definitions cannot be deferred.
Suppose for example we have:

  (defexec foo (x)
    (foo-exec <fast-body>)
    (declare (xargs :guard <guard>))
    <slow-body>)

The proof obligations generated by the set-exec implicit in defexec are as
follows, where <fast-body'> is the result of replacing calls of foo-exec by
calls of foo in <fast-body>.

  (implies <guard>
           (equal <fast-body'> <slow-body>))

  (implies <guard>
           <guard-proof-obligations-from-fast-body'>)

We can get the same effect using mbt as follows.

  (defun foo (x)
    (declare (xargs :guard <guard>))
    (if (and (mbt <guard>)
             (equal <fast-body'> <slow-body>))
        <fast-body'>
      <slow-body>))

The proof obligations generated by guard verification would be as follows.

  (implies <guard> <guard>)

  (implies <guard>
           (equal <fast-body'> <slow-body>))

  (implies (and <guard> (mbt <guard>) (equal <fast-body'> <slow-body>))
           <guard-proof-obligations-from-fast-body'>)

  (implies (and <guard>
                (not (and (mbt <guard>) (equal <fast-body'> <slow-body>))))
           <guard-proof-obligations-from-fast-body'>)

The first and fourth of these are trivial, and the second and third together
are equivalent to the two proof obligations generated by the earlier defexec.