Partial-encapsulate
Introduce functions with some constraints unspecified
See encapsulate for relevant background.
Partial-encapsulate is a variant of encapsulate for which some of
the constraints are implicit. This is an advanced capability that is useful
when one installs special-purpose code, possibly in raw Lisp, using a trust
tag (see defttag).
Introduction
The syntax for partial-encapsulate is the same as the syntax of
encapsulate, except for the addition of an argument, supporters,
which is described below.
General Form:
(partial-encapsulate (signature ... signature)
(f1 ... fk) ; supporters
ev1
...
evn)
where, as for encapsulate: each signature is a well-formed signature, each describing a different function symbol, and each evi is
an embedded event form (see embedded-event-form). The additional
argument (shown above) is a true-list of function symbols, the
supporters: it is an error if any such symbol, fi, is not a known
function symbol at the time the partial-encapsulate call is evaluated,
the exception being that fi may be introduced in one of the signatures.
A partial-encapsulate form must satisfy the following three requirements
in addition to those of the corresponding encapsulate form: it must have
at least one signature, it must not occur within any other encapsulate or
partial-encapsulate form that has at least one signature, and every
function symbol that it introduces must be specified in one of the
signatures.
A call of partial-encapsulate introduces its signature functions
together with its exported theorems, exactly as though it had been the call of
encapsulate with the same signatures and events, however with one
difference: the partial-encapsulate logically incorporates additional
constraints that are not mentioned. This is discussed further below, but for
now let us note that because of this difference, a successful evaluation of a
partial-encapsulate form results in a special ``unknown-constraints''
designation for the functions introduced by the signatures. Any attempt to
access the constraints for those functions will thus fail. Consider the
following example, which introduces f as a constrained function symbol
that is constrained not only by the property that f returns a boolean,
but also by additional, unspecified (implicit) constraints.
(partial-encapsulate
((f (x) t))
nil
(local (defun f (x) (declare (xargs :guard t)) (consp x)))
(defthm booleanp-f
(booleanp (f x))
:rule-classes :type-prescription))
(defthm symbolp-f
(symbolp (f y)))
(encapsulate
((g (x) t))
(local (defun g (x) (consp x)))
(defthm booleanp-g (booleanp (g x))))
Then the following fails, even though it would succeed if we replace
partial-encapsulate by encapsulate above. The reason is that the
partial-encapsulate form allows for constraints beyond just the property that
f is boolean. Imagine that special code had been inserted (using a trust
tag) for reasoning about f when proving a theorem like symbolp-f
that we were now trying to functionally instantiate.
; Functional instantiation FAILS because of unknown-constraints on f
(defthm symbolp-g
(symbolp (g y))
:hints (("Goal" :by (:functional-instance symbolp-f (f g)))))
Supporters and corresponding encapsulate
A partial-encapsulate represents any encapsulate form that
introduces the same function symbols, has the same signatures, and extends the
constraints introduced such that every function symbol occurring in at least
one of the additional constraints must either be mentioned in one of the
evi or be among the list of supporters, (f1 ... fk). We may refer
to such an encapsulate form as a ``corresponding encapsulate''. The user
of partial-encapsulate should keep in mind such a set of additional
constraints. The supporters should thus include all function symbols in the
theorems exported from the intended corresponding encapsulate, except that
signature functions are always included among the supporters whether specified
or not, and hence their inclusion is optional.
The list of supporters is used for generating proof obligations for a
:functional-instance lemma-instance. Specifically, the supporters
serve as the ``ancestors'' of the partial encapsulate's signature functions,
in the constraint-generation algorithm described in the documentation for
constraint. Thus, if supporters are missing that occur in the intended
corresponding encapsulate, then functional instantiation may be unsound
because some proof obligations fail to be generated. Note that in the typical
application described next, where the implicit constraints all specify
evaluation results for calls of signature functions as discussed below, the
specified list of supporters can simply be nil.
Applications
A trust tag (see defttag) is not needed for evaluation of a
partial-encapsulate form. However, for a typical application of
partial-encapsulate — redefinition of a constrained function in raw Lisp
— a trust tag is of course necessary (see defttag). In such a
case, the corresponding encapsulate may be viewed as extending the original
partial-encapsulate with all theorems of the form (equal (f a1 ... ak)
val), ranging over all computations (f a1 ... ak) ever to be
evaluated (a finite but potentially huge set) where val is the value
returned for (f a1 ... ak). It is the responsibility of the creator of
such an application to ensure that all evaluations satisfy the original
constraints of the partial-encapsulate.
Note that in this sort of application — that is, where the implicit
constraints all arise from function evaluations — the supporters
argument may soundly be nil, since only the signature functions are
involved in the implicit constraints (and those functions are automatically
included among the supporters, even when not specified by the user).
For examples of such an application, including explanatory comments, see
community-books and books/demos/partial-encapsulate.lisp and
books/demos/include-raw-examples/mem-access-sound/mem.lisp.
Partial-encapsulates are, in essence, also used in the implementation of
dependent clause-processors, where the list of supporters might well be
non-nil. See define-trusted-clause-processor.
Implementation
This section is provided as a reference for those interested, but can
probably be safely skipped by most readers.
Consider the following example.
ACL2 !>:trans1 (partial-encapsulate
((f0 (x) t))
(g0)
(local (defun f0 (x) x))
(defthm f0-prop
(implies (integerp x)
(integerp (f0 x)))))
(ENCAPSULATE ((F0 (X) T))
(LOCAL (DEFUN F0 (X) X))
(DEFTHM F0-PROP
(IMPLIES (INTEGERP X)
(INTEGERP (F0 X))))
(SET-UNKNOWN-CONSTRAINTS-SUPPORTERS G0))
ACL2 !>
This example illustrates that a partial-encapsulate call expands to a
call of encapsulate obtained by removing the supporters argument, but
with the following extra event inserted after given list of events, where
(f1 ... fk) is the specified list of supporters.
(set-unknown-constraints-supporters f1 ... fk)
The macro, set-unknown-constraints-supporters, extends a table,
unknown-constraints-table. As evaluation of the partial-encapsulate
concludes, the world is extended so that each signature function has a
'constraint-lst property indicating that its constraints are unknown, but
with supporters (``ancestors'', as discussed above) according to that table.
This macro call can thus be inserted non-locally within an encapsulate,
anywhere after the local function definitions, to make an encapsulate behave
like a partial-encapsulate.
