DEFATTACH

execute constrained functions using corresponding attached functions
Major Section:  EVENTS

This documentation topic is organized into the following sections:

Introductory example.
Syntax and semantics of defattach.
Three primary uses of defattach.
Miscellaneous remarks, with discussion of possible user errors.

Please see encapsulate if you intend to use defattach but are not already familiar with the use of encapsulate to introduce constrained functions.

See community book books/misc/defattach-example.lisp for a small example. it illustrates how defattach may be used to build something like ``higher-order'' programs, in which constrained functions may be refined to different executable functions. More uses of defattach may be found in the ACL2 source code, specifically, file boot-strap-pass-2.lisp.

The argument :skip-checks t enables easy experimentation with defattach, by permitting use of :program mode functions and the skipping of semantic checks. Also permitted is :skip-checks nil (the default) and :skip-checks :cycles, which turns off only the update of the extended ancestor relation and hence the check for cycles in this relation; see below. We do not make any logical claims when the value of :skip-checks is non-nil; indeed, a trust tag is required in this case (see defttag). Remark for those who use the experimental HONS extension (see hons-and-memoization): the interaction of memoization and attachments is not tracked for attachments introduced with a non-nil value of :skip-checks. For more discussion of :skip-checks t, see defproxy; we do not discuss :skip-checks further, here.

Introductory example.

We begin with a short log illustrating the use of defattach. Notice that after evaluating the event (defattach f g), a call of the constrained function f is evaluated by instead calling g on the arguments.

ACL2 !>(encapsulate
        ((f (x) t :guard (true-listp x)))
        (local (defun f (x) x))
        (defthm f-property
          (implies (consp x) (consp (f x)))))
[... output omitted ...]
 T
ACL2 !>(defun g (x)
         (declare (xargs :guard (or (consp x) (null x))))
         (cons 17 (car x)))
[... output omitted ...]
 G
ACL2 !>(f '(3 4)) ; undefined function error


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

((3 4))

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

ACL2 !>(defattach f g)
[... output omitted ...]
 :ATTACHMENTS-RECORDED
ACL2 !>(f '(3 4)) ; f is evaluated using g
(17 . 3)
ACL2 !>(trace$ f g)
 ((F) (G))
ACL2 !>(f '(3 4)) ; f is evaluated using g
1> (ACL2_*1*_ACL2::F (3 4))
  2> (ACL2_*1*_ACL2::G (3 4))
    3> (G (3 4))
    <3 (G (17 . 3))
  <2 (ACL2_*1*_ACL2::G (17 . 3))
<1 (ACL2_*1*_ACL2::F (17 . 3))
(17 . 3)
ACL2 !>(defattach f nil) ; unattach f (remove its attachment)
[... output omitted ...]
 :ATTACHMENTS-RECORDED
ACL2 !>(f '(3 4)) ; undefined function error once again
1> (ACL2_*1*_ACL2::F (3 4))


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

((3 4))

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

ACL2 !>

Syntax and semantics of defattach.

The log above shows that the event (defattach f g) allows g to be used for evaluating calls of f. From a logical perspective, the evaluation takes place in the addition to the current session of an ``attachment equation'' axiom (universally quantified over all x) for each defattach event:

(equal (f x) (g x)) ;;; attachment equation axiom for (defattach f g)

Below we explain defattach in some detail. But it is important to keep in mind that evaluation with the attachment equations takes place in an extension of the logical theory of the session. ACL2 guarantees that this so-called ``evaluation theory'' remains consistent, assuming that the absence of defaxiom events from the user. A deeper discussion of the logical issues is available (but not intended to be read by most users) in a comment in the ACL2 source code labeled ``Essay on Defattach.''

Example Forms:
(defattach f g)   ; call g in place of calling constrained function f
(defattach (f g)) ; same as just above
(defattach (f g :hints (("Goal" :in-theory (enable foo)))))
                  ; equivalent to first form above, except with hints for the
                  ; proof that the guard of f implies the guard of g
(defattach (f g :hints (("Goal" :in-theory (enable foo)))
                :otf-flg t))
                  ; as above, except with an :otf-flg of t for the proof that
                  ; the guard of f implies the guard of g
(defattach (f g)
           :hints (("Goal" :use my-thm)))
                  ; equivalent to first form above, except with hints for the
                  ; proof that the constraints on f hold for g
(defattach (f g)
           :hints (("Goal" :use my-thm))
           :otf-flg t)
                  ; as above, except with an :otf-flg of t for the proof that
                  ; the constraints on f hold for g
(defattach (f g)
           (h j)) ; Attach g to f and attach j to h
(defattach (f g :attach nil)
           (h j)) ; Same as just above, including the same proof obligations,
                  ; except for one difference: because of :attach nil, calls
                  ; of f will not be evaluated, i.e., there will be no
                  ; executable attachment of g to f
(defattach (f nil)
           (h j)) ; Attach j to h and unattach f
(defattach (f g :hints (("Goal" :in-theory (enable foo))))
           (h j :hints (("Goal" :in-theory (enable bar))))
           :hints (("Goal" :use my-thm)))
                  ; Attach g to f and attach j to h, with hints:
                  ; - For proving that the guard of f implies the guard of g,
                  ;   enable foo;
                  ; - For proving that the guard of h implies the guard of j,
                  ;   enable bar; and
                  ; - For proving that the constraints on f and h hold for
                  ;   g and j (respectively), use theorem my-thm.


(defattach f nil)   ; remove the attachment of f, if any (e.g., g above)
(defattach (f nil)) ; same as just above

General Forms:
(defattach f g)   ; single attach or, if g is nil, unattach
(defattach (f1 g1 :kwd val ...)
           ...
           (fk gk :kwd' val' ...)
           :kwd'' val'' ...)
where each indicated keyword-value pair is optional and each keyword is one of :ATTACH, :HINTS, :OTF-FLG, or :INSTRUCTIONS. The value of each :ATTACH keyword is either t or nil, with default t except that the value of :ATTACH at the ``top level,'' after each entry (fi gi ...), is the default for each :ATTACH keyword supplied in such an entry. The associated values for the other keywords have the usual meanings for the proof obligations described below: the guard proof obligation for keywords within each (fi gi ...) entry, and the constraint proof obligation for keywords at the top level. No keyword may occur twice in the same context, i.e., within the same (fi gi ...) entry or at the top level; and :INSTRUCTIONS may not occur in the same context with :HINTS or :OTF-FLG.

The first General Form above is simply an abbreviation for the form (defattach (f g)), which is an instance of the second General Form above. For the second General Form we say that gi is ``attached to'' fi (by the defattach event) if gi is not nil, and otherwise we say that fi is ``unattached'' (by the defattach event). It is also convenient to refer to <fi,gi> as an ``attachment pair'' (of the event) if gi is not nil. We may refer to the set of fi as the ``attachment nest'' of each fi.

We start with a brief introduction to the first General Form in the case that g is not nil. This form arranges that during evaluation, with exceptions noted below, every call of the constrained function symbol f will in essence be replaced by a call of the function symbol g on the same arguments. We may then refer to g as the ``attachment of'' f, or say that ``g is attached to f.'' Notable exceptions, where we do not use attachments during evaluation, are for macroexpansion, evaluation of defconst and defpkg terms, evaluation during table events, some stobj operations including all updates, and especially evaluation of ground terms (terms without free variables) during proofs. However, even for these cases we allow the use of attachments in the first argument of prog2$ and, more generally, the next-to-last (i.e., second) argument of return-last when its first argument is not of the form 'm for some macro, m.

To see why attachments are disallowed during evaluation of ground terms during proofs (except for the prog2$ and return-last cases mentioned above), consider the following example.

(defstub f (x) t)
(defun g (x) (+ 3 x))
(defattach f g)
If the form (f 2) is submitted at the ACL2 prompt, the result will be 5 because the attachment g of f is called on the argument, 2. However, during a proof the term (f 2) will not be simplified to 5, since that would be unsound, as there are no axioms about f that would justify such a simplification.

For the case that g is nil in the first General Form above, the result is the removal of the existing attachment to f, if any. After this removal, calls of f will once again cause errors saying that ``ACL2 cannot ev the call of undefined function f ...''. In this case not only is the previous attachment to f removed; moreover, for every function symbol f' in the attachment nest of f in the defattach event that introduced the existing attachment to f, then f' is unattached. (An example near the end of this documentation topic shows why this unattachment needs to be done.) Such removal takes place before the current defattach is processed, but is restored if the new event fails to be admitted.

We focus henceforth on the second General Form. There must be at least one attachment, i.e., i must be at least 1. All keywords are optional; their role is described below. The fi must be distinct constrained function symbols, that is, function symbols all introduced in signatures of encapsulate events (or macros such as defstub that generate encapsulate events). Each non-nil gi is a :logic-mode function symbol that has had its guards verified, with the same signature as fi (though formal parameters for fi and gi may have different names). (Note: The macro defattach!, defined in community book books/misc/defattach-bang, avoids this restriction.) This event generates proof obligations and an ordering check, both described below. The effect of this event is first to remove any existing attachments for all the function symbols fi, as described above for the first General Form, and then to attach each gi to fi.

Proof obligations must be checked before making attachments. For this discussion we assume that each gi is non-nil (otherwise first remove all attachment pairs <fi,gi> for which gi is nil). Let s be the functional substitution mapping each fi to gi. For any term u, we write u\s for the result of applying s to u; that is, u\s is the ``functional instance'' obtained by replacing each fi by gi in u. Let G_fi and G_gi be the guards of fi and gi, respectively. Let G_fi' be the result of replacing each formal of fi by the corresponding formal of gi in G_fi. ACL2 first proves, for each i (in order), the formula (implies G_fi' G_gi)\s. If this sequence of proofs succeeds, then the remaining formula to prove is the functional instance C\s of the conjunction C of the constraints on the symbols fi; see constraint. This last proof obligation is thus similar to the one generated by functional instantiation (see constraint). As with functional instantiation, ACL2 stores the fact that such proofs have been done so that they are avoided in future events (see lemma-instance). Thus, you will likely avoid some proofs with the sequence

(defattach f g)
(defattach f nil)
(defattach f g)
(defattach f nil)
...
rather than the sequence:
(defattach f g)
:u
(defattach f g)
:u
...

It remains to describe an ordering check. We begin with the following motivating example.

(defstub f (x) t) ; constrained function with no constraints
(defun g (x) (declare (xargs :guard t)) (not (f x)))
(defattach f g) ; ILLEGAL!
Were the above defattach event to succeed, the evaluation theory (discussed above) would be inconsistent: (f x) equals (g x) by the new attachment equation, which in turn equals (not (f x)) by definition of g. The evaluation would therefore be meaningless. Also, from a practical perspective, there would be an infinite loop resulting from any call of f.

We consider a function symbol g to be an ``extended ancestor of'' a function symbol f if either of the following two criteria is met: (a) g occurs in the formula that introduces f (i.e., definition body or constraint) and g is introduced by an event different from (earlier than) the event introducing f; or (b) g is attached to f. For a proposed defattach event, we check that the resulting extended ancestor relation has no cycles, where for condition (b) we include all attachment pairs that would result, including those remaining from earlier defattach events.

Of course, a special case is that no function symbol may be attached to itself. Similarly, no function symbol may be attached to any of its ``siblings'' -- function symbols introduced by the same event -- as siblings are considered equivalent for purposes of the acyclicity check.

Three primary uses of defattach.

We anticipate three uses of defattach:

(1) Constrained function execution

(2) Sound modification of the ACL2 system

(3) Program refinement

We discuss these in turn.

(1) The example at the beginning of this documentation illustrates constrained function execution.

(2) ACL2 is written essentially in itself. Thus, there is an opportunity to attaching to system functions. For example, encapsulated function too-many-ifs-post-rewrite, in the ACL2 source code, receives an attachment of too-many-ifs-post-rewrite-builtin, which implements a heuristic used in the rewriter. To find all such examples, search the source code for the string `-builtin'.

Over time, we expect to continue replacing ACL2 source code in a similar manner. We invite the ACL2 community to assist in this ``open architecture'' enterprise; feel free to email the ACL2 implementors if you are interested in such activity.

(3) Recall that for an attachment pair <f,g>, a proof obligation is (speaking informally) that g satisfies the constraint on f. Yet more informally speaking, g is ``more defined'' than f; we can think of g as ``refining'' f. With these informal notions as motivation, we can view defattach as providing refinement though the following formal observation: the evaluation theory extends the theory of the ACL2 session, specifically by the addition of all attachment equations. For the logic-inclined, it may be useful to think model-theoretically: The class of models of the evaluation theory is non-empty but is a subset of the class of models of the current session theory.

Miscellaneous remarks, with discussion of possible user errors.

We conclude with remarks on some details.

A defattach event is never redundant (see redundant-events); in that sense it is analogous to in-theory.

As mentioned above, the use of attachments is disabled for evaluation of ground terms during proofs. However, attachments can be used on code during the proof process, essentially when the ``program refinement'' is on theorem prover code rather than on functions we are reasoning about. The attachment to too-many-ifs-post-rewrite described above provides one example of such attachments. Meta functions and clause-processor functions can also have attachments, with the restriction that no common ancestor with the evaluator can have an attachment; see evaluator-restrictions.

For an attachment pair <f,g>, evaluation of f never consults the guard of f. Rather, control passes to g, whose guard is checked if necessary. The proof obligation related to guards, as described above, guarantees that any legal call of f is also a legal call of g. Thus for guard-verified code that results in calls of f in raw Lisp, it is sound to replace these calls with corresponding calls of g.

Defattach events are illegal inside any encapsulate event with a non-empty signature unless they are local to the encapsulate.

To see all attachments: (all-attachments (w state)). (Note that attachments introduced with a non-nil value of :skip-checks will be omitted from this list.)

We conclude with an example promised above, showing why it is necessary in general to unattach all function symbols in an existing attachment nest when unattaching any one of those function symbols. Consider the following example.

(defstub f1 () t)
(encapsulate ((f2 () t))
  (local (defun f2 () (f1)))
  (defthm f2=f1 (equal (f2) (f1))))
(encapsulate ((f3 () t))
  (local (defun f3 () (f1)))
  (defthm f3=f1 (equal (f3) (f1))))
(defun four () (declare (xargs :guard t)) 4)
(defun five () (declare (xargs :guard t)) 5)
(defattach (f1 four) (f2 four))
(defattach (f1 five) (f3 five))
The second defattach replaces erases the existing attachment pair <f1,four> before installing the new attachment pairs <f1,five> and <f3,five>. After the second defattach, both (f1) and (f3) evaluate to 5. Now suppose that the attachment pair <f2,four> were not erased. Then we would have (f1) evaluating to 5 and (f2) evaluating to 4, contradicting the constraint f2=f1. The evaluation theory would thus be inconsistent, and at a more concrete level, the user might well be surprised by evaluation results if the code were written with the assumption specified in the constraint f2=f1.