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

A related utility can cause a function call to be evaluated using an
alternate, provably equal function. See memoize, option

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

See community book

We begin with a short log illustrating the use of

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 !>

The log above shows that the event

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

Below we explain `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 `defaxiom` events, though as explained below, no
function symbol that syntactically supports a

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 *guard keywords*,
and keywords at the top level, shown above as *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 ofgi tofi . They have their usual values and meanings, as when used (for example) in`defthm``events`. The value of each:attach keyword is eithert ornil . 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

The argument `program` mode functions and
the skipping of semantic checks. Also permitted is

The argument `defattach-system`, which has the same syntax as
`local` call
of

The first General Form above is simply an abbreviation for the form

We start with a brief introduction to the first General Form in the case
that `defconst` and `defpkg` terms, evaluation during `table`
events, some stobj operations including all `prog2$` and, more
generally, the next-to-last (i.e., second) argument of `return-last`
when its first argument is not of the form

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

For the case that

We focus henceforth on the second General Form. There must be at least one
attachment, i.e., `encapsulate` events (or macros such as `defstub` that
generate `encapsulate` events). Each non-`logic`-mode function symbol that has had its guards verified,
with the same signature as

Proof obligations must be checked before making attachments. For this
discussion we assume that each

(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

We consider a function symbol

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.

We anticipate three uses of

- 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 oftoo-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) thatg satisfies the constraint onf . Yet more informally speaking,g is ``more defined'' thanf ; we can think ofg 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.

We conclude with remarks on some details.

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

For an attachment pair

`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

We next discuss a restriction based on a notion of a function symbol
syntactically supporting an event. Function symbol *ancestral*
in event `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

(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

Next we discuss the

(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

(defattach (f acl2-numberp) (h acl2-numberp))

Such an attempt fails, because the following constraint is generated but is
not a theorem:

(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 `encapsulate` (it was introduced with `defun`). So we specify

(defattach (f acl2-numberp) (h acl2-numberp) (g acl2-numberp :attach nil))

Finally, we can check that

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

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

- 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