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).
The primitive for intcar, which returns the least-significant bit of
(ifix x) as a Boolean value, is defined in primitives.lisp as
(def-fgl-primitive intcar (x)
:g-concrete (mv t (and (integerp x.val)
: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)
: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
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.
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
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
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.
(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))
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.