Defattach
Execute constrained functions using corresponding attached functions
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 in
the list (:hints :instructions
:otf-flg :attach
:skip-checks :system-ok). More details are in the ``Syntax and
Semantics'' section below.
A related utility can cause a function call to be evaluated using an
alternate, provably equal function. See memoize, option
:INVOKE.
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. It may also be helpful to see evaluation.
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-a.lisp.
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 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 :kwd11 val11 ...)
...
(fk gk :kwdk1 valk1 ...)
:kwd1 val1 ...)
where each indicated keyword-value pair is optional and each keyword is in
the list (:hints :instructions
:otf-flg :attach
:skip-checks :system-ok). We distinguish between keywords
within the (fi gi :kwdi1 vali1 ...), which we call guard keywords,
and keywords at the top level, shown above as :kwd1 val1 ..., which we
call top-level keywords.
- The guard keywords are in the list (:hints :instructions :otf-flg :attach). The
:hints, :instructions, and :otf-flg
keywords in (fi gi ...) are used in the proofs of the guard proof
obligation for the attachment of gi to fi. They have their usual
values and meanings, as when used (for example) in defthm events. The value of each :attach keyword is either t or nil.
We discuss the :attach keyword later in this documentation
topic.
- The top-level keywords :hints, :instructions, and :otf-flg
are used in the constraint proof obligations just as described above for the
guard proof obligations. When :attach is used as a top-level keyword,
its value serves as a default for entries (fi gi ...) that do not specify
:attach. :Skip-checks and :system-ok are described below.
No keyword may occur twice in the same context: that is, neither twice as a
guard keyword in the same (fi gi ...) entry, nor twice as a top-level
keyword. Moreover, :instructions may not occur in the same context with
:hints or :otf-flg.
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 (defined below) and hence the check for cycles in
this relation (which is discussed below). We do not make any logical claims
when the value of :skip-checks is non-nil; indeed, a trust tag is
then required (see defttag). Note that 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.
The argument :system-ok t allows attachment to system functions.
Without this argument, the defattach event will fail if any fi is a
built-in ACL2 function. Rather than supplying this argument directly, it is
recommended to use defattach-system, which has the same syntax as
defattach with two exceptions: it adds :system-ok t automatically,
that is, :system-ok is implicit; and it expands to a local call
of defattach. The latter is important so that the attachment does not
affect system behavior outside a book containing the defattach event. Of
course, if it is truly intended to affect such behavior, the argument
:system-ok t may be given directly to defattach, without a
surrounding use of local.
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. We also consider g to be an extended
immediate ancestor of f if there are function symbols f' and g'
that are introduced in the same events as f and g,
respectively (such as the same mutual-recursion or the same encapsulate with non-empty signatures), such that g' is an extended
immediate ancestor of f' in the sense above. For a proposed
defattach event, we check that the graph defined by 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:
- Constrained function execution
- Sound modification of the ACL2 system
- Program refinement
We discuss these in turn.
- The example at the beginning of this documentation illustrates
constrained function execution.
- ACL2 is written essentially in itself. Thus, there is an opportunity to
attach 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. See system-attachments. 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.
- 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 through 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. Another example is that a meta function or clause-processor
function can call functions that have attachments, with a restriction that
those attached functions must not also be ancestral in a corresponding
evaluator. See evaluator-restrictions for a discussion of that
restriction, and see transparent-functions for a device that can relax
the restriction (while imposing additional requirements on attachments).
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.
(Of interest only to users of apply$.) Special handling is applied
when attempting to attach to a so-called warrant, which is produced by
an application of defwarrant (or defun$). In that case it is
legal to attach the function true-apply$-warrant to the warrant, without
any proof obligation. This attachment is actually performed automatically by
defwarrant, so users (even users of apply$) need not deal
explicitly with such attachments. However, these attachments make warrants
executable in the loop; for example, after (defwarrant foo), (warrant
foo) will evaluate to t in the loop.
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)
The form (all-attachments (w state)) evaluates to the list of all
attachments except in two cases: warrants, and attachments introduced
with a non-nil value of :skip-checks. To obtain the attachment to a
function symbol FN, without the above restrictions and with value
nil if there is no attachment to FN: (cdr (attachment-pair 'FN (w
state))).
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 not introduced with encapsulate (it was introduced with defun). 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 !>
The advanced feature, with-global-stobj, imposes certain
restrictions on a defattach event. You can probably ignore this point
unless you get an error pertaining to with-global-stobj. For relevant
documentation see with-global-stobj, specifically the section on
``Constrained Functions and Defattach''.
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 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.
Subtopics
- System-attachments
- System-level algorithms that users can modify with attachments
- Ignored-attachment
- Why attachments are sometimes not used
- Defattach-system
- Attach to built-in, system-level, constrained functions
