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 distributed 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 distributed 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`

.