Major Section: EVENTS
This documentation assumes familiarity with
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
:clause-processor rule is a way to inform ACL2 that a
clause-processor has been proved correct and now may be specified in
Here we describe a utility,
provides another way to inform ACL2 that a function is to be considered a
clause-processor that can be specified in a
You can find examples of correct and incorrect use of this utility in
Consider the simple example already presented for
(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
:ttagargument generates a
defttagevent 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
: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.
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
LABis supplied, then a subsidiary
deflabelevent will be generated with name
LAB, which will enable you to to undo this
LAB. If you supply a
:labelthen you may supply a
:docargument to use with that generated
deflabelevent. We discussed the
:ttagargument 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-procmust not already have been similarly designated as a trusted clause-processor.
cl-proc may be defined either in
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.
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
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
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
argument, we call it a ``dependent'' clause-processor, because its
correctness is dependent on the constraints implicitly introduced by the
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
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
encapsulate form associated with the trusted clause-processor, but whose
constraints introduced are the aforementioned implicit constraints.
There are several additional requirements on a
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
with the functions introduced in the inner
: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
there must exist (in principle at least) a corresponding promised encapsulate
form with the same signature that could logically be admitted, whenever
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
form. Thus, functional instantiation (see functional-instantiation-example)
is disabled for function in the signature of a
A remark on the underlying implementation
You can see all of the current trusted clause-processors by issuing the
(table trusted-clause-processor-table). Those that are dependent
clause-processors will be associated in the resulting association list with a
car is the list of supporters and whose
(supporters . t); the others will be associated just with
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.
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
:use hint, by exploiting the fact that this
function has executable code for which there is no corresponding definitional
(defstub acl2-my-prove (term hint) t)
; 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.
(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) )