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 (see below) 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. This guarantee is a consequence
of a more general guarantee: an ACL2 logical world exists in
which (loosely speaking) the attachment equation for (defattach f g), as
(defun f (...) (g ...)), takes the place of the original defining event
for f, for each defattach event. This more general guarantee holds
even if there are defaxiom events, though as explained below, no
function symbol that syntactically supports a defaxiom formula is allowed
to get an attachment. A deeper discussion of the logical issues is
available (but not intended to be read by most users) in a long 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. We discuss the :ATTACH keyword later in this
documentation topic. 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 immediate 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 this 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.
We next discuss a restriction based on a notion of a function symbol
syntactically supporting an event. Function symbol f is ancestral
in event E if either f occurs in E, or (recursively) f occurs
in an event E' that introduces some function symbol g that is
ancestral in E. We require that no function symbol ancestral in the
formula of a defaxiom event may have an attachment. Theoretical
reasons are discussed in comments in the ACL2 source code, but here we give a
little example showing the need for some such restriction: without it, we
show how to prove nil!
(defn g1 () 1)
(defn g2 () 2)
(defstub f1 () t)
(defstub f2 () t)
(defund p (x)
(declare (ignore x))
t)
(defevaluator evl evl-list
((p x)))
(defaxiom f1-is-f2
(equal (f1) (f2)))
(defun meta-fn (x)
(cond ((equal (f1) (f2))
x)
(t *nil*)))
(defthm bad-meta-rule
(equal (evl x a)
(evl (meta-fn x) a))
:rule-classes ((:meta :trigger-fns (p))))
(defattach f1 g1)
(defattach f2 g2)
(defthm contradiction
nil
:hints (("Goal" :use ((:instance (:theorem (not (p x)))
(x t)))))
:rule-classes nil)
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.)
Next we discuss the :ATTACH keyword. There is rarely if ever a reason to
specify :ATTACH T, but the following (admittedly contrived) example shows
why it may be necessary to specify :ATTACH NIL. First we introduce three
new function symbols.
(defstub f (x) t)
(defun g (x)
(f x))
(encapsulate ((h (x) t))
(local (defun h (x) (g x)))
(defthm h-prop
(equal (h x) (g x))))
Now suppose we want to attach the function acl2-numberp to both f
and h.
(defattach (f acl2-numberp) (h acl2-numberp))Such an attempt fails, because the following constraint is generated but is not a theorem:
(EQUAL (ACL2-NUMBERP X) (G X)). Clearly we also need to
attach to g as well.
(defattach (f acl2-numberp) (h acl2-numberp) (g acl2-numberp))But this fails for a different reason, as explained by the error message:
ACL2 Error in ( DEFATTACH (F ACL2-NUMBERP) ...): It is illegal to attach to function symbol G, because it was introduced with DEFUN. See :DOC defattach.That is: logically, we need to attach
acl2-numberp to g, but we
cannot actually attach to g because it was introduced with defun,
not with encapsulate. So we specify :ATTACH NIL for the attachment
to g, saying that no actual attachment should be made to the code for
g, even though for logical purposes we should consider that g has
been given the indicated attachment.
(defattach (f acl2-numberp) (h acl2-numberp) (g acl2-numberp :attach nil))Finally, we can check that
f, g, and h execute as expected.
ACL2 !>(assert-event (and (f 3)
(not (f t))
(g 3)
(not (g t))
(h 3)
(not (h t))))
:PASSED
ACL2 !>
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.
