DEFINE-TRUSTED-CLAUSE-PROCESSOR

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)

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 !>

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
  )

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.

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.)

(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)
  )