Well-formedness-guarantee
Guarantee that a metafunction or clause-processor returns a
well-formed answer
A :well-formedness-guarantee is a keyword attribute available
in the :meta and :clause-processor :rule-classes. By default, when a metafunction or clause processor is
applied, ACL2 checks that the output is well-formed (and does not contain
certain ``forbidden'' functions; see set-skip-meta-termp-checks). By
providing a :well-formedness-guarantee when you store a :meta or
:clause-processor rule, you can cause ACL2 to skip these runtime
checks.
This is considered an advanced feature that requires that you prove certain
theorems; this is probably only worthwhile if your metafunctions or clause
processors produce very large terms. Henceforth, we assume you are familiar
with metafunctions and clause processors.
This topic first exhibits a simple example of a well-formedness guarantee
for a metafunction. This example is really an outline; a self-contained,
runnable example may be found in the community-books in file
books/demos/meta-wf-guarantee-example.lisp. Then we describe the
acceptable values of the :well-formedness-guarantee keyword of both the
:meta and :clause-processor rule-classes. Next we show the forms of
the theorems you must prove to provide such guarantees. Finally, we discuss
the runtime effects of providing such guarantees.
Example
Suppose that fn is a vanilla metafunction that rewrites terms with top
function symbol TARGET, of arity 1. The event storing fn as
a metafunction would normally be something like this:
(defthm fn-is-correct
(implies (and (pseudo-termp x)
(alistp a))
(equal (evl x a)
(evl (fn x) a)))
:rule-classes
((:meta :trigger-fns (TARGET))))
where
evl is an evaluator for all the function symbols known to
fn.
Suppose that to prove this theorem,
evl must be able to interpret the
symbols
TARGET,
CONS, and
IF. While the metatheorem for
fn establishes that
fn returns something with the same
``meaning'' (under
evl) as its input, it does not answer the question:
does
fn return a well-formed term, all of whose function symbols are in
:logic mode? Given the above
:rule-class, whenever the
simplifier fires the
:meta rule
fn-is-correct by applying
fn to
a term, it checks that the value,
val, is well-formed, by evaluating
(logic-termp val (w state)). The function
logic-termp checks
that its argument is a
term all of whose function symbols are in
:logic mode.
Function: logic-termp
(defun logic-termp (x wrld)
(declare (xargs :guard (plist-worldp-with-formals wrld)))
(and (termp x wrld)
(logic-fnsp x wrld)))
The logic-termp check can be avoided if, before you store the rule
fn-is-correct, you prove:
(defthm fn-is-well-formed
(implies (and (logic-termp x w)
(arities-okp '((TARGET . 1)
(CONS . 2)
(IF . 3))
w))
(logic-termp (fn x) w))
:rule-classes nil)
and then you store
fn-is-correct this way:
(defthm fn-is-correct
(implies (and (pseudo-termp x)
(alistp a))
(equal (evl x a)
(evl (fn x) a)))
:rule-classes
((:meta :trigger-fns (TARGET)
:well-formedness-guarantee fn-is-well-formed)))
Acceptable Values
Now we describe the values you may provide with the
:well-founded-guarantee keyword of the :meta and the
:clause-processor rule-classes.
General Forms:
:well-formedness-guarantee thm-name1
:well-formedness-guarantee (thm-name1)
:well-formedness-guarantee (thm-name1 thm-name2)
where both
thm-name1 and
thm-name2 are the names of previously
proved ``well-formedness theorems'' (see the next section); furthermore,
thm-name1 must be about the metafunction or clause processor being
introduced, and
thm-name2 must be about the hypothesis metafunction (if
any) associated with the metafunction. For
:meta rules, all three forms
are accepted, but the last form is required if the
:meta rule involves a
hypothesis metafunction. That is, to provide a
:well-formedness-guarantee for a metatheorem with a hypothesis
metafunction, you must supply both
thm-name1 and
thm-name2. For
:clause-processor rules, you must use the first form.
Each well-formedness theorem provides an ``arity alist'' that specifies the
assumed arities of the function symbols known to the metafunction or clause
processor. The arities shown for the function symbols listed in that alist
must be the same as the arities of those functions in the actual ACL2 logical
world current at the time the :meta or :clause-processor is
stored. Moreover, the function symbols in that alist must all be in
:logic mode.
Furthermore, none of the function symbols in the arity alists should be
``forbidden'' function symbols as explained in set-skip-meta-termp-checks.
When the :meta or :clause-processor rule is stored, notes are
made that will prevent the function symbols on the arity alists from becoming
untouchable (and thus forbidden). See push-untouchable.
The only way a function's arity or forbidden status can change, or that a
function can transition out of :logic mode, is if the user has engaged in
redefinition or activated a trust tag to add or remove untouchables. Thus,
the restrictions above are unimportant to most users.
Well-Formedness Theorems
Theorems must be proved to establish that metafunctions and clause
processors return well-formed results. These are called ``well-formedness
theorems.'' Note: To say a theorem is a ``well-formedness theorem'' is a
remark about the shape of the formula, not its rule-class. There is no
:well-formedness-theorem rule-class and a well-formedness theorem may be
stored with any :rule-classes that accept the syntax of the
formula or as :rule-classes nil. Indeed, if one of your
metafunctions uses another function to produce a subterm of the metafunction's
answer, you might need to prove a well-formedness theorem for the sub-function
and make it a :rewrite rule.
Well-formedness theorems for metafunctions and clause processors are
similar but slightly different. We deal with metafunctions and their
corresponding hypothesis metafunctions (if any) first. The shapes of the
well-formedness theorems for a metafunction and hypothesis metafunction are
identical, but remember that you must prove a well-formedness theorem for both
the metafunction and the associated hypothesis metafunction. So suppose
fn is a metafunction or a hypothesis metafunction and let (fn x ...)
be a legal call on distinct variable symbols. (Recall that extended
metafunctions and their hypothesis functions can take three arguments.) Then
the general form a well-formedness theorem for fn states that fn
returns a termp when given one, provided the arities of certain
function symbols are as expected:
General Form of Well-Formedness Theorem for a Metafunction:
(implies (and (logic-termp x w)
(arities-okp '<alist> w))
(logic-termp (fn x ...) w))
where
<alist> is an alist pairing function symbols with their assumed
arities as illustrated in the opening example. Note that the first argument
of
arities-okp in the theorem is a quoted constant. You may omit or
reorder the hypotheses above and you may use different variable symbols in
place of
x and
w, but they must be distinct and different from the
variables in the ``
....''
An example of <alist> is ((TARGET . 1) (CONS . 2) (IF . 3)).
Generally, the <alist> you provide should assign arities to every symbol
known to fn, i.e., every function symbol known to the evaluator used in
your correctness theorem. If you inspect the definition of termp you
will see that it uses w to obtain arities of the function symbols in
x. The arities-okp hypothesis restricts w to worlds where
the function symbols known to fn have the arities you expect and are in
:logic-mode. For example, given the (arities-okp '<alist>
w) hypothesis for the <alist> above, the theorem prover will rewrite
(arity 'IF w) to 3. By default arity and arities-okp are
disabled; and the following rewrite rules, which are part of ACL2's initial
world, will take care of calls like (arity 'IF w) and (logicp
fn w).
Theorem: arities-okp-implies-arity
(defthm arities-okp-implies-arity
(implies (and (arities-okp user-table w)
(assoc fn user-table))
(equal (arity fn w)
(cdr (assoc fn user-table)))))
Theorem: arities-okp-implies-logicp
(defthm arities-okp-implies-logicp
(implies (and (arities-okp user-table w)
(assoc fn user-table))
(logicp fn w)))
Now we turn to the well-formedness theorem for a clause processor,
cl-proc. Let (cl-proc x ...) be a legal call on distinct variable
symbols. The theorem establishes that cl-proc returns a list of clauses
when given a clause, provided certain functions have the expected arities.
But the recognizer for a clause is the function logic-term-listp and
the recognizer for a list of clauses is logic-term-list-listp:
General Forms of Well-Formedness Theorem for a Clause Processor
(implies (and (logic-term-listp x w)
(arities-okp '<alist> w))
(logic-term-list-listp (cl-proc x ...) w))
(implies (and (logic-term-listp x w)
(arities-okp '<alist> w))
(logic-term-list-listp (clauses-result (cl-proc x ...)) w))
The first form above is for a cl-proc that returns a single value and
the second form is for a cl-proc that returns multiple values.
The discussion about metafunctions, above, applies here as well.
<Alist> is an alist pairing function symbols with their assumed arities.
You may omit or reorder the hypotheses and you may use different variable
symbols in place of x and w, but they must be distinct and different
from the variables in the ``....''
Runtime Effects
In the absence of a :well-formedness-guarantee, if a metafunction or
clause processor is applied during a proof and produces val, then certain
checks are made on val before it is used in the proof attempt. In the
case of a metafunction, (logic-termp val (w state)) is checked and
val is scanned to ensure that it contains no forbidden function symbols.
In the case of a clause processor, (logic-term-list-listp val (w state))
is checked and val is scanned to ensure that it contains no forbidden
function symbols.
If val is large (e.g., because the input is large), these checks can
take more time than the metafunction or clause processor did to produce
val! It is for this reason that we provide for
:well-formedness-guarantees.
When a :well-formedness-guarantee is provided no checks are made on
val. However, ACL2 will check that the arity alist(s) involved in the
guarantee still correctly shows the arities of the function symbols listed.
Because those function symbols were not forbidden when the guarantee was made
and are prohibited from being forbidden thereafter, no check is necessary to
ensure that no forbidden symbols are introduced into the proof.
