Define-trusted-clause-processor
Define a trusted (unverified) goal-level simplifier
This documentation assumes familiarity with
:clause-processor rules; see clause-processor. Briefly put, a
clause-processor is a user-defined function that takes as input the
ACL2 representation of a goal — a clause — and returns a
list of goals (i.e., a list of clauses). A :clause-processor rule is a
way to inform ACL2 that a clause-processor has been proved correct and now may
be specified in :clause-processor hints.
Here we describe a utility, define-trusted-clause-processor, that
provides another way to inform ACL2 that a function is to be considered a
clause-processor that can be specified in a :clause-processor hint. You
can find examples of correct and incorrect use of this utility in community
book books/clause-processors/basic-examples.
Consider the simple example already presented for :clause-processor
rules (again, see clause-processor), for a simple clause-processor
named note-fact-clause-processor. Instead of introducing an evaluator
and proving a correctness theorem with :rule-classes :clause-processor,
we can simply inform ACL2 that we trust the function
note-fact-clause-processor to serve as a clause-processor.
(define-trusted-clause-processor
note-fact-clause-processor
nil
:ttag my-ttag)
A non-nil :ttag argument generates a defttag event in order to
acknowledge the dependence of the ACL2 session on the (unproved) correctness
of this clause-processor. That argument can be omitted if there is currently
an active trust tag. Note that the extra defttag event will be local to the define-trusted-clause-processor event; that is, its effect
will disappear after the define-trusted-clause-processor event completes.
This point becomes clear if one understands that a call of
define-trusted-clause-processor expands to a call of encapsulate,
and a defttag event is essentially local within any encapsulate event, as is any event that sets the ACL2-defaults-table.
See defttag. Because we are trusting this clause-processor, rather
than having proved it correct, we refer to it as a ``trusted''
clause-processor to contrast with a proved-correct, or ``verified'',
clause-processor.
Now that the event displayed above has established
note-fact-clause-processor as a (trusted) clause-processor, we can use it
in a :clause-processor hint, for example as follows. Notice that the
output is identical to that for the corresponding example presented for the
verified case (see clause-processor), except that the word ``verified''
has been replaced by the word ``trusted''.
ACL2 !>(thm (equal (car (cons x y))
x)
:hints
(("Goal"
:clause-processor
(note-fact-clause-processor clause '(equal a a)))))
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
We now apply the trusted :CLAUSE-PROCESSOR function NOTE-FACT-CLAUSE-
PROCESSOR to produce two new subgoals.
Subgoal 2
(IMPLIES (EQUAL A A)
(EQUAL (CAR (CONS X Y)) X)).
But we reduce the conjecture to T, by the :executable-counterpart of
IF and the simple :rewrite rule CAR-CONS.
Subgoal 1
(EQUAL A A).
But we reduce the conjecture to T, by primitive type reasoning.
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Proof succeeded.
ACL2 !>
Indeed, if one runs this example first and subsequently verifies the
clause-processor, one will see the word ``trusted'' change to
``verified''.
The general form is as follows.
(define-trusted-clause-processor
cl-proc ;;; clause-processor function
supporters ;;; see below
&key
label ;;; optional; cl-proc$label by default
ttag ;;; discussed above
partial-theory ;;; optional encapsulate event
)
We discussed the :ttag argument above, and we will discuss the
supporters and :partial-theory arguments later below. Let us turn
our attention to the label argument and its ramifications for undoing and
redundancy.
As mentioned above, a successful define-trusted-clause-processor event
results in an encapsulate event. If the :label argument is
supplied with a non-nil value L, or if :label is omitted and
L is the result of adding the suffix "$LABEL" to cl-proc,
then the event (deflabel L) will be included under the resulting
encapsulate form. Thus, you will be able to undo this
define-trusted-clause-processor with :ubt L. Also,
because of the criteria for redundant encapsulate events (see redundant-encapsulate), the entire form is considered redundant (skipped) if
it is identical to one already executed in the current ACL2 world, with
one exception: if :partial-theory is nil or omitted, and also
:label nil is supplied explicitly, then the event will not be redundant.
If the event is not redundant, then cl-proc must not already be
designated as a trusted clause-processor.
Note that cl-proc may be defined either in :program-mode or
:logic-mode.
The supporters argument should be a true list of function symbols in
the current ACL2 world. It is important that this list include user-defined
functions whose definitions support the correctness of the clause-processor
function. Otherwise, local definitions of those missing supporters
can render the use of this clause-processor unsound, as discussed in the paper
referenced at the end of the clause-processor documentation topic.
Below we discuss an additional reason that supporters is critical for
soundness, in the case of dependent clause-processors.
(Remark. There could have been two notions of supporters: one for
functions whose definitions support the correctness of the clause-processor
function, and, in the case of dependent clause-processors, one for supporters
of the ``promised encapsulate'' discussed below. But for simplicity, a single
supporters argument serves both purposes.)
Dependent clause-processors and promised encapsulates: The
:partial-theory argument
Suppose you want to introduce a clause-processor to reason about a complex
hardware simulator that is implemented outside ACL2. Sawada and Reeber had
just such a problem, as reported in their FMCAD 2006 paper. Indeed, they used
sys-call to implement a :program-mode function in ACL2
that can invoke that simulator. (This has been changed to sys-call*
since sys-call cannot invoke the OS during proofs; see sys-call.)
In principle one could code the simulator directly in ACL2; but it would be a
tremendous amount of work that has no practical purpose, given the interface
to the external simulator. So: In what sense can we have a clause-processor
that proves properties about a simulator when that simulator is not fully
axiomatized in ACL2? Our answer, in a nutshell, is this: The above
:partial-theory argument provides a way to write merely some of the constraints on the external tool (or even no constraints at all), with the
understanding that such constraints are present implicitly in a stronger
``promised'' encapsulate, for example by exporting the full
definition.
If a trusted clause-processor is introduced with a non-nil
:partial-theory argument, we call it a ``dependent'' clause-processor,
because its correctness is dependent on the constraints implicitly introduced
by the :partial-theory encapsulate form. The implicit constraints
should logically imply the constraints actually introduced by the explicit
encapsulate, but they should also be sufficient to justify every possible
invocation of the clause-processor in a :clause-processor hint. The user
of a define-trusted-clause-processor form is making a guarantee —
or, is relying on a guarantee provided by the writer of that form — that
in principle, there exists a so-called ``promised encapsulate'': an
encapsulate form with the same signature as the
:partial-theory encapsulate form associated with the trusted
clause-processor, but whose constraints introduced are the aforementioned
implicit constraints.
There are several additional requirements on a :partial-theory
argument. First, it must be an encapsulate event with non-empty signature. Moreover, the functions introduced by that event must be exactly
those specified in the signature, and no more. And further still, the
define-trusted-clause-processor form cannot be executed inside any encapsulate form with non-empty signature; we can think of this
situation as attempting to associate more than one encapsulate with the
functions introduced in the inner encapsulate.
Moreover, soundness depends on inclusion of enough function symbols in the
supporters argument, as follows. Let S be the set of specified
supporters augmented by the set of function symbols either introduced by,
or in a property exported by, the :partial-theory argument, which we call
the ``promised encapsulate''. Then every function symbol constrained by the
promised encapsulate is in S.
The :partial-theory event will (in essence) be executed as part of the
evaluation of the define-trusted-clause-processor form. Again, a
critical obligation rests on the user who provides a :partial-theory:
there must exist (in principle at least) a corresponding promised encapsulate
form with the same signature that could logically be admitted, whenever
the above define-trusted-clause-processor form is evaluated successfully,
that justifies the designation of cl-proc as a clause-processor. See
also the paper mentioned above for more about promised encapsulates. A key
consequence is that the constraints are unknown for the functions
introduced in (the signature of) a :partial-theory encapsulate
form. Thus, functional instantiation (see functional-instantiation-example) is disabled for function in the signature
of a :partial-theory form.
A remark on the underlying implementation
You can see all of the current trusted clause-processors by issuing the
command (table trusted-cl-proc-table). The resulting alist associates
each trusted clause-processor with its supporters.
Note that define-trusted-clause-processor is actually a macro that
generates (among other things) a table event for extending
trusted-cl-proc-table. You are invited to use :trans1 to
see expansions of calls of this macro. In particular, you can see that the
:partial-theory argument results in an encapsulate event that
includes a call of the form (set-unknown-constraints-supporters f1
... fk), which in effect makes that call of encapsulate into a call of
partial-encapsulate with supporters (f1 ... fk). See partial-encapsulate.
A technique for using raw Lisp to define a trusted
clause-processor
The following code is intended to give an idea for how one might define the
``guts'' of a trusted clause-processor in raw Lisp. The idea is to stub out
functions, such as acl2-my-prove below, that you want to define in raw
Lisp; and then, load a raw Lisp file to overwrite any such function with the
real code. But then we make any such overwritten function untouchable. (This
last step is important because otherwise, one can prove nil using a
:functional-instance :use hint, by exploiting the fact that this
function has executable code for which there is no corresponding definitional
axiom.) Note: The point here is only to illustrate the use of raw Lisp, so we
do not bother to define or explain functions hint-to-termlist or
disjoin-clause-segments-to-clause, which this example assumes are defined
elsewhere; their meanings are not important for this example.
(defstub acl2-my-prove (term hint) t)
(program)
(defttag :my-cl-proc)
(progn
; We wrap everything here in a single progn, so that the entire form is
; atomic. That's important because we want the use of push-untouchable to
; prevent anything besides my-clause-processor from calling acl2-my-prove.
(progn!
(set-raw-mode-on state)
(load "my-hint-raw.lsp") ; defines my-prove in raw Lisp
(defun acl2-my-prove (term hint)
(my-prove term hint)))
(defun my-clause-processor (cl hint)
(declare (xargs :guard (pseudo-term-listp cl)
:mode :program))
(if (acl2-my-prove (disjoin cl) hint)
(disjoin-clause-segments-to-clause
(pairlis$ (hint-to-termlist hint) nil)
cl)
(prog2$ (cw "~|~%NOTE: Unable to prove goal with ~
my-clause-processor and indicated hint.~|")
(list cl))))
(push-untouchable acl2-my-prove t)
)
