DEFPROXY

define a non-executable :program-mode function for attachment 
Major Section:  EVENTS

This event is provided for those who want to experiment with defattach using :program mode functions, and without proof obligations or constraints on cycles in the extended ancestors graph; see defattach. If you merely want to define a stub or a non-executable function, see defstub or see defun-nx, respectively.

See community book books/misc/defproxy-test.lisp for an extended (but simple) example.

Example Forms:
(defproxy subr1 (* *) => *)
(defproxy add-hash (* * hashtable) => (mv * hashtable))

General Form:
(defproxy name args-sig => output-sig)
where name is a new function symbol and (name . args-sig) => output-sig) is a signature; see signature.

The macro defproxy provides a convenient way to introduce a ``proxy'': a :program mode function that can be given attachments for execution (see defattach), assuming that there is an active trust tag (see defttag). Thus, a defproxy calls expands to a defun form with the following xargs declare form: :non-executable :program. Note that verify-termination is not permitted for such a function. However, it is permitted to put the proxy function into :logic mode by use of an encapsulate event; indeed, this is the way to ``upgrade'' an attachment so that the normal checks are performed and no trust tag is necessary.

In order to take advantage of a defproxy form, one provides a subsequent defattach form to attach an executable function to the defproxy-introduced function. When :skip-checks t is provided in a defattach form, the usual checks for defattach events are skipped, including proof obligations and the check that the extended ancestor relation has no cycles (see defattach). There must be an active trust tag (see defttag) in order to use :skip-checks t. In that case the use of :skip-checks t is permitted; but note that its use is in fact required if a :program mode function is involved, and even if a :logic mode function is involved that has not been guard-verified.

The following log shows a simple use of defproxy.

ACL2 !>(defproxy foo-stub (*) => *)

Summary
Form:  ( DEFUN FOO-STUB ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 FOO-STUB
ACL2 !>(foo-stub '(3 4 5))


ACL2 Error in TOP-LEVEL:  ACL2 cannot ev the call of undefined function
FOO-STUB on argument list:

((3 4 5))

To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>(defun foo-impl (x)
         (declare (xargs :mode :program
                         :guard (or (consp x) (eq x nil))))
         (car x))

Summary
Form:  ( DEFUN FOO-IMPL ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FOO-IMPL
ACL2 !>(defttag t)

TTAG NOTE: Adding ttag :T from the top level loop.
 T
ACL2 !>(defattach (foo-stub foo-impl) :skip-checks t)

Summary
Form:  ( DEFATTACH (FOO-STUB FOO-IMPL) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 :ATTACHMENTS-RECORDED
ACL2 !>(foo-stub '(3 4 5))
3
ACL2 !>

One can replace this attachment with one that uses :logic mode functions and does not skip checks. The idea is to reintroduce the proxy function using an encapsulate form, which does not require redefinition (see ld-redefinition-action) to be enabled, and either to put the attachment into :logic mode with the guard verified, as we do in the example below, or else to attach to a different guard-verified :logic mode function.

ACL2 !>(defattach (foo-stub nil) :skip-checks t) ; remove attachment

Summary
Form:  ( DEFATTACH (FOO-STUB NIL) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 :ATTACHMENTS-RECORDED
ACL2 !>(encapsulate
        ((foo-stub (x) t :guard (true-listp x)))
        (local (defun foo-stub (x) (cdr x)))
        (defthm foo-stub-reduces-acl2-count
          (implies (consp x)
                   (< (acl2-count (foo-stub x))
                      (acl2-count x)))))

[[ ... output omitted here ... ]]

The following constraint is associated with the function FOO-STUB:

(IMPLIES (CONSP X) (< (ACL2-COUNT (FOO-STUB X)) (ACL2-COUNT X)))

Summary
Form:  ( ENCAPSULATE ((FOO-STUB ...) ...) ...)
Rules: NIL
Warnings:  Non-rec
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
 T
ACL2 !>(verify-termination foo-impl)

Since FOO-IMPL is non-recursive, its admission is trivial.  We could
deduce no constraints on the type of FOO-IMPL.

Computing the guard conjecture for FOO-IMPL....

The guard conjecture for FOO-IMPL is trivial to prove.  FOO-IMPL is
compliant with Common Lisp.

Summary
Form:  ( DEFUN FOO-IMPL ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (VERIFY-TERMINATION-FN ...))
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 FOO-IMPL
ACL2 !>(defttag nil) ; optional
 NIL
ACL2 !>(defattach (foo-stub foo-impl))

The guard proof obligation is

(IMPLIES (TRUE-LISTP X)
         (OR (CONSP X) (EQ X NIL))).

But we reduce the conjecture to T, by primitive type reasoning.

Q.E.D.

This concludes the guard proof.


We now prove that the attachment satisfies the required constraint.
The goal to prove is

(IMPLIES (CONSP X)
         (< (ACL2-COUNT (FOO-IMPL X))
            (ACL2-COUNT X))).

[[ ... output omitted here ... ]]

Q.E.D.

Summary
Form:  ( DEFATTACH (FOO-STUB FOO-IMPL))
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION FOO-IMPL)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
 :ATTACHMENTS-RECORDED
ACL2 !>

We close with some remarks on the checking of guards in the case that defattach has been called with keyword argument :skip-checks t. We illustrate with examples, where we assume an attachment pair (f . g) created by an event (defattach ... (f g) ... :skip-checks t ...). A good model for the treatment of :skip-checks t is dependent on whether f was introduced with defproxy or with encapsulate: for defproxy, the normal guard-related checks are treated as skipped, while for encapsulate, they are assumed to hold.

First suppose that f was introduced using defproxy, and consider the following example. 

(defproxy f (*) => *)
(defun g (x) (car x)) ; not guard-verified; implicit guard of t is too weak
(defttag t) ; trust tag needed for :skip-checks t
(defattach (f g) :skip-checks t)
If we try to evaluate the form (f 3) in ACL2, then the top-level so-called ``executable counterpart'' (i.e., the logically-defined funcction, also known as the ``*1*'' function) of f is invoked. It calls the executable counterpart of g, which calls the executable counterpart of car, which in turn checks the guard of car and causes a guard violation error (unless we first turn off guard-checking; see set-guard-checking). 
ACL2 !>(trace$ f g)
 ((F) (G))
ACL2 !>(f 3)
1> (ACL2_*1*_ACL2::F 3)
  2> (ACL2_*1*_ACL2::G 3)


ACL2 Error in TOP-LEVEL:  The guard for the function call (CAR X),
which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
in the call (CAR 3).  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.  See :DOC set-guard-checking for information about suppressing
this check with (set-guard-checking :none), as recommended for new
users.

ACL2 !>

Little changes if we modify the example above by strengtheing the guard of g. 

(defproxy f (*) => *)
(defun g (x)
  (declare (xargs :guard (consp x)))
  (car x))
(defttag t) ; trust tag needed for :skip-checks t
(defattach (f g) :skip-checks t)
The result of evaluating (f 3) is as before, except that this time the guard violation occurs at the time that g is called. 
ACL2 !>(trace$ f g)
 ((F) (G))
ACL2 !>(f 3)
1> (ACL2_*1*_ACL2::F 3)
  2> (ACL2_*1*_ACL2::G 3)


ACL2 Error in TOP-LEVEL:  The guard for the function call (G X), which
is (CONSP X), is violated by the arguments in the call (G 3).  To debug
see :DOC print-gv, see :DOC trace, and see :DOC wet.  See :DOC set-
guard-checking for information about suppressing this check with (set-
guard-checking :none), as recommended for new users.

ACL2 !>

Now consider a slight variation of the example just above, in which f is introduced using encapsulate instead of using defproxy. 

(encapsulate ( ((f *) => *) )
             (local (defun f (x) x)))
(defun g (x)
  (declare (xargs :guard (consp x)))
  (car x))
(defttag t) ; trust tag needed for :skip-checks t
(defattach (f g) :skip-checks t)
Since f was introduced by encapsulate instead of by defproxy, ACL2 assumes that the usual guard properties hold. In particular, it assumes that (informally speaking) the guard of f implies the guard of g; see defattach for details. So in this case, ACL2 proceeds under that assumption even though it's actually false, and the result is a raw Lisp error.

ACL2 !>(trace$ f g)
 ((F) (G))
ACL2 !>(f 3)
1> (ACL2_*1*_ACL2::F 3)
  2> (G 3)

***********************************************
************ ABORTING from raw Lisp ***********
Error:  Attempt to take the car of 3 which is not listp.
***********************************************

If you didn't cause an explicit interrupt (Control-C),
then the root cause may be call of a :program mode
function that has the wrong guard specified, or even no
guard specified (i.e., an implicit guard of t).
See :DOC guards.

To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)
ACL2 !>

If you replace g by its definition in the first example of this series, i.e. with a guard (implicitly) of t, you will see the same error, this time because the defattach event assumed that g was guard-verified.