		Search-engine friendly clone of the ACL2 documentation.

Fgl-primitive-and-meta-rules

Adding fast-executing primitive routines to FGL.

FGL is geared toward doing most reasoning via rewrite rules. But sometimes rewrite rules aren't fast enough or are otherwise inadequate for something we want to do. For these cases, FGL supports two kinds of custom reasoning procedures, "metafunctions" and "primitives". Metafunctions are more general than primitives and we will mostly discuss them here. A metafunction takes a function and argument list as input and produces a term and binding alist as output. A primitive is a specialization of a metafunction that produces a symbolic object as output rather than a term and binding alist. When applying a metafunction, the term returned is symbolically interpreted under the returned bindings, whereas when applying a primitive the symbolic object is returned directly.

A metafunction is a function that takes a function name f, argument list (symbolic objects), interpreter state, and state, and returns (mv successp rhs-term bindings interp-st state), where successp is a flag indicating whether the answer is valid. If so, rhs-term must evaluate under the evaluation of bindings to f of the evaluations of the arguments. The returned interp-st must satisfy several constraints showing that it was not invalidly modified; usually, all a primitive should do with the interp-st is build new gates onto the aignet of its logicman (see fgl-interpreter-state). Primitives take the same inputs but return (mv successp obj interp-st state), where the evaluation of obj must equal f of the evaluations of the arguments.

New metafunctions can be defined with the form def-fgl-meta and new primitives with def-fgl-primitive. However, before the newly defined metafunctions/primitives may be used, they must be installed into the current metafunction and primitive dispatcher function using install-fgl-metafns. This creates a new function that wraps all existing metafunctions into a case statement, and attaches it to the stub fgl-meta-fncall-stub. It also creates a similar dispatcher function for primitives and another one for binder meta rules (see binder).

Example

The primitive for intcar, which returns the least-significant bit of (ifix x) as a Boolean value, is defined in primitives.lisp as follows:

(def-fgl-primitive intcar (x)
  (fgl-object-case x
    :g-concrete (mv t (and (integerp x.val)
                           (intcar x.val))
                    interp-st)
    :g-integer (mv t (mk-g-boolean (car x.bits)) interp-st)
    :g-boolean (mv t nil interp-st)
    :g-cons (mv t nil interp-st)
    :g-map (mv t (and (integerp x.alist)
                      (intcar x.alist))
               interp-st)
    :otherwise (mv nil nil interp-st)))

Def-fgl-primitive sets up the correct signature and guards for the primitive function, extracts the named formals (in this case x) from the argument list, and proves the necessary theorems to ensure it can be installed as a primitive. It stores the association between intcar and the new primitive function, named fgl-intcar-primitive, in the table fgl-primitives.

To install the primitives listed in fgl-primitives, use (install-fgl-metafns name), which defines a new function name-primitive-fncall that takes a function symbol, argument list, interp-st, and state, and dispatches based on the function symbol to that function's primitive, if any (if not, it returns unsuccessful). This function is then attached to fgl-primitive-fncall-stub, which is called by the FGL interpreter to run primitives.

Formula Checks

FGL requires that primitives return results that evaluate correctly with respect to the FGL evaluator, fgl-object-eval -- that is, the result object must evaluate to the same thing as the evaluation of the input function symbol applied to the argument list. However, fgl-object-eval is based on an ACL2 evaluator fgl-ev which only understands a limited set of function symbols. Naively, this would prevent us from proving that the primitives evaluate correctly. However, we are allowed to assume the correctness of facts we extract from the ACL2 state with respect to fgl-ev -- see meta-extract for details. In many cases we can show that when some set of theorems are stored in the state in the expected form, and the evaluator is assumed to always evaluate these theorems to non-NIL values, the evaluator then correctly understands some new function.

As a very simple example, (ifix x) is not understood by fgl-ev, but it is defined as (if (integerp x) x 0). All of the functions in its definition -- if, integerp -- are understood by fgl-ev. So we can show that fgl-ev understands ifix if we check that the definition of ifix stored in the state is the one we expect, and also assume that facts stored in the state are correct with respect to fgl-ev.

We can build up to arbitrarily complex functions, in this way, as long as they are defined rather than constrained. For example, if we check that the definitional formulas for =, ZIP, FIX, and EXPT are present in the world, then we can show that fgl-ev understands expt terms.

In order to define primitives that need to check formulas in order to show they are correct, we first define a "formula check" function, an executable function that checks that a list of facts are correctly present in the state. We show that if this formula check function returns true, then the primitive evaluates correctly. When installing a new set of primitives, we define a new formula check function that checks all the facts checked by the formula check functions depended on by the primitives, and show that it implies each of them. Then, when running the FGL clause processor, we run that formula check function to check that all the definitions that primitives depend on are present: doing this once ahead of time is fast and allows primitives to proceed without checking any of these facts.

We offer some automation for proving formula check theorems. For example, in bitops-primitives.lisp, we use the form

(def-formula-checks bitops-formula-checks
  (logapp
   acl2::logmask$inline
   acl2::logtail$inline
   acl2::loghead$inline
   logbitp
   integer-length))

This introduces a function bitops-formula-checks which checks all of the facts necessary to ensure that the listed functions operate as expected. Then, when defining a primitive that depends on this, we simply add :formula-check bitops-formula-checks within the def-fgl-primitive form. For example:

(def-fgl-primitive acl2::logtail$inline (n x)
  (b* (((unless (fgl-object-case n :g-concrete))
        (mv nil nil interp-st))
       ((mv ok x) (gobj-syntactic-integer-fix x))
       ((unless ok) (mv nil nil interp-st))
       (x-bits (gobj-syntactic-integer->bits x)))
    (mv t (mk-g-integer (tail-bits (nfix (g-concrete->val n)) x-bits))
        interp-st))
  :formula-check bitops-formula-checks)

The def-formula-checks automation currently only supports single recursion and only uses the base definitions of functions. However, it would be possible to extend it to support custom definitions, thereby supporting mutual recursion using definitions of those functions that equate them to calls of a flag function.

Constrained functions, and functions that depend on constrained functions, pose more of a challenge. But recall that what we're trying to prove is that if the primitive call succeeds, then its result is equivalent to the input function call. If we are to introduce a primitive for a constrained function, or a function that depends on a constrained function, we must be able to prove that equal to something in some cases. It would then suffice to check formulas that show that in the cases we care about, the evaluation of the function reduces to some other form.