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

New metafunctions can be defined with the form

The primitive for

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

To install the primitives listed in

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,

As a very simple example,

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

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

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

This introduces a function

(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

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.