Major Section: EVENTS
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
distributed 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. 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)))))Indeed, if one runs this example first and subsequently verifies the clause-processor, one will see the word ``trusted'' change to ``verified''.[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 !>
The general form is as follows.
(define-trusted-clause-processor cl-proc ;;; clause-processor function supporters ;;; see below &key label ;;; optional, but required if doc is non-nil doc ;;; optional ttag ;;; discussed above partial-theory ;;; optional encapsulate event )If a
:label
LAB
is supplied, then a subsidiary deflabel
event
will be generated with name LAB
, which will enable you to to undo this
define-trusted-clause-processor
event using: :
ubt
LAB
. If
you supply a :label
then you may supply a :doc
argument to use with
that generated deflabel
event. We discussed the :ttag
argument
above. The entire form is considered redundant (skipped) if it is identical
to one already executed in the current ACL2 world; but if it is not
redundant, then cl-proc
must not already have been similarly designated
as a trusted clause-processor.
Note that cl-proc
may be defined either in :program
-mode or
:logic
-mode.
The :supporters
argument will often be nil
. In general, it is a true
list of symbols, all of which must be function symbols in the current ACL2
world at the time the define-trusted-clause-processor
form is evaluated.
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.
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. 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 :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
.
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-clause-processor-table)
. Those that are dependent
clause-processors will be associated in the resulting association list with a
pair whose car
is the list of supporters and whose cdr
is t
,
i.e., with (supporters . t)
; the others will be associated just with
(supporters)
.
Thus, define-trusted-clause-processor
is actually a macro that generates
(among other things) a table
event for a table named
trusted-clause-processor-table
; see table. You are invited to use
:
trans1
to see expansions of calls of this macro.