Trusted Extension of ACL2 System Code: Towards an Open Architecture
Matt Kaufmann
Univ. of Texas at Austin

Over its lifetime of 21 years, ACL2 has increasingly supported various
kinds of trusted extension.  J Moore will summarize such capabilities
in his invited workshop talk.

This talk will present a new ACL2 utility, defattach, that can be used
to attach executable counterparts to {\em constrained} function
symbols: those that have been introduced using ACL2's ``encapsulate''
mechanism, so that they have specified properties but do not have
runnable definitions.  It is important to note that defattach supports
more than the attachment of functionally equivalent (but presumably
more efficient) code to a function symbol; ACL2 already has a utility
(MBE, ``must-be-equal'') for that purpose.  For example, if f is
constrained to return a natural number and len is the length function,
then (defattach f len) introduces the axiom

  forall x . f(x) = len(x)

and allows us to compute f using len.  It does not however allow us to
{\em prove} that f is len; that is not a theorem of the current
theory, but rather, it is a theorem of the {\em evaluation theory},
which is defined to extend the current theory with {\em defattach
equations} like the one displayed above.

Attachments may be used for any of three purposes:

- Testing (Common Lisp evaluation to test specifications)
- Program refinement (really, theory extension)
- System code extension

The third of these supports our goal of opening up the architecture
of ACL2.

Small examples will be used to demo uses of defattach.  The talk will
also touch on the logical foundations, especially as pertaining to the
trust story.  Further demos will illustrate care that has been taken
to implement the logical foundations in terms of an evaluation theory
that is guaranteed to be consistent, and to avoid confusion of these
two theories.

The fundamental idea of defattach is that it equates pairs of function
symbols, associating constrained functions with executable functions,
in a way that guarantees consistent theory extension.  The talk will
strongly encourage questions and discussion during the talk and demos.
A question of particular interest is whether the defattach notion of
theory refinement relate to existing notions, and if so, how.