intro.tex

The meta rule and clause processor facilities
of the ACL2 theorem proving system~\cite{acl2:home}
are designed to allow
users to write custom proof routines which, once proven
correct, can be called by the ACL2 prover\footnote{
  Clause processors may alternatively be ``trusted'' --- used without
  proof --- but at the
  cost of a {\em trust tag} marking this use as a source of potential
  unsoundness.~\cite{trusted-cl-proc}}.
These facilities descend from the meta reasoning capability
provided by earlier Boyer-Moore provers~\cite{meta}.  Relevant
background can be found in earlier ACL2 papers on meta
reasoning~\cite{meta-05} and clause processors~\cite{trusted-cl-proc},
along with ACL2 documentation~\cite{acl2:doc}.

Such meta-level proof routines have historically been limited in their use of
ACL2's database of stored facts and its built-in prover functions.
For example, a metafunction could call the ACL2 rewriter, but when
proving this metafunction correct, the result of calling the rewriter
could not be assumed to be equivalent to the input --- that is, the
rewriter could not be assumed to be correct.  Similarly,
metafunctions and clause processors could both examine the ACL2 world
(the logical state of the prover, including the database of stored
facts), but in proving the correctness of these functions, facts
extracted from the world could not be assumed to be correct.

Meta-extract is an ACL2 feature first introduced in Version 6.0
(December, 2012).  It allows for certain facts stored in the ACL2
world and certain ACL2 prover routines to be assumed
correct when proving the correctness of metafunctions and clause
% processors.  In particular, additional \textit{meta-extract hypotheses}
% which imply the correctness of these routines and facts are allowed to
% be present in these correctness theorems. These additional hypotheses
%%% Reviewer 1:
%%% meta-extract hypotheses which imply the correctness
%%% =>
%%% meta-extract hypotheses which are implied by the correctness
%%% (These hypotheses are weaker than the full correctness of the ACL2 facts and
%%% routines. NIL does imply the full correctness, but it cannot be a meta-extract
%%% hypothesis.)
processors.  In particular, additional \textit{meta-extract hypotheses}
that capture the correctness of such routines and facts are allowed to
be present in these correctness theorems. These additional hypotheses
preserve the soundness of metareasoning in ACL2 because they encode
assumptions that we are already
making --- that the facts stored in the ACL2 logical world are true
and that ACL2's prover routines are sound.

Note that meta-extract hypotheses can be used to help {\em prove}
theorems to be stored as meta rules or as clause-processor rules, but
they have no effect on how those rules are {\em applied} during
subsequent proofs.  For that, we refer readers to existing papers
\cite{meta-05,trusted-cl-proc} as well as
documentation~\cite{acl2:doc} topics including
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_META}{\underline{META}},
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_CLAUSE-PROCESSOR}{\underline{CLAUSE-PROCESSOR}},
and
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_EXTENDED-METAFUNCTIONS}{\underline{EXTENDED-METAFUNCTIONS}}.
Also see the topic
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_META-EXTRACT}{\underline{META-EXTRACT}}
for additional user-level documentation.  Note that references to
documentation topics, such as those above, are underlined to denote
hyperlinks to topics in the online
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html}{\underline{documentation}}~\cite{acl2:doc}
for ACL2 and its books.

% The changes just below address the following question from Reviewer
% 3:
%%% (In reference to clause processors) "global facts are available
%%% but not contextual ones".  Why?
This paper primarily addresses metafunctions rather than always
referring to both metafunctions and clause processors.  The
correctness arguments are analogous.  The meta-extract functionality
available for clause processors is a subset of the functionality available for
metafunctions: the {\em global facts} discussed below
  are available for both, but {\em contextual facts} need contexts
  that are only available below the clause level.

% Sol: I changed the title just below because if the subsection looks
% like it's only about correctness, some might skip it, even though it
% contains important stuff (including the notion of pseudo-evaluator).
\subsection{Meta-extract Hypotheses}
\label{sec:intuitive}

We next introduce the various meta-extract hypotheses and
explain informally why it is sound to include them.
See the {\em Essay on Correctness of Meta Reasoning} in
the ACL2 source code for a rigorous mathematical argument.

Correctness theorems for metafunctions are stated using a
function that we will call a \textit{pseudo-evaluator}, typically
defined via the
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_DEFEVALUATOR}{\underline{\tt defevaluator}}
macro.  (Elsewhere in the ACL2
literature this is simply referred to as an evaluator; however, we
want to emphasize the difference between a pseudo-evaluator and a real
% \href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_TERM}{\underline{term}}
term
evaluator.)  A pseudo-evaluator is a constrained function about
which only certain facts are known; these facts are ones that would
also be true of a ``real'' evaluator capable of fully interpreting any
ACL2 term.  The intention is for these facts to suffice for
proving a metafunction correct, without the need for
a real term evaluator\footnote{
  It would be unsound to define what we are calling a real evaluator
  in ACL2 --- in particular, one that could evaluate terms containing
  calls of the evaluator itself, or functions that call the evaluator.
  In order to fix our handwavy argument, you could instead think of
  introducing an evaluator that can interpret all functions that are
  defined at the point when the metafunction is being applied.
}.
To prove a metafunction correct
the user must show that the pseudo-evaluation of the term output by
the metafunction is equal (or equivalent) to the pseudo-evaluation of
the input term.  Intuitively, if this can be proved of a
pseudo-evaluator, and the only facts known about the pseudo-evaluator
are ones that are also true of the real evaluator of ACL2 terms, then
this must also be true of the real evaluator: that is, the evaluations
of the input and output terms of the metafunction are equivalent, and
thus the metafunction is correct.

The meta-extract feature allows certain additional hypotheses in the
statement of the correctness theorem of a metafunction.  These meta-extract
hypotheses are applications of the pseudo-evaluator to calls of either the
function \texttt{meta\-/extract\-/global\-/fact+}, its less general
version \texttt{meta\-/extract\-/global\-/fact}, or the function
\texttt{meta\-/extract\-/contextual\-/fact}.
These functions produce various
sorts of terms by extracting facts from the ACL2 world and calling
ACL2 prover subroutines, constructed so that if ACL2 and its logical
state are sound, the terms produced should always be true.  For
example, these functions can produce:
\begin{itemize}
\item the body of a previously proven theorem;
\item the definitional equation of a previously defined function;
\item a term equating a call of a function on quoted constants to the
  quoted value of that call;
\item a term equating some term $a$ to the result of rewriting $a$
  using \href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_MFC-RW}{\underline{\tt mfc-rw}}; or
\item a term describing the type of $a$, according to ACL2's
  \href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_TYPE-SET}{\underline{type-set}}
  reasoning.
\end{itemize}
When we use such facts in our metafunction, meta-extract hypotheses
allow us to assume that they are true according to the
pseudo-evaluator while doing the correctness proof.

Intuitively, adding meta-extract hypotheses to a metafunction's
correctness theorem is allowable because we expect the (real)
evaluation of any term produced by one of the meta-extract functions
to return true.  If we prove the pseudo-evaluator theorem with
meta-extract hypotheses and, as before, reason that since the theorem
is true of the pseudo-evaluator, it is also true of the real
evaluator, then the final step is to observe that meta-extract
hypotheses are true using the real evaluator (or else ACL2 is already
unsound).  Therefore, even with meta-extract hypotheses, we can still
conclude that the evaluations of the metafunction's output and input
terms are equivalent.

Why not somehow axiomatize the idea that the contents of the ACL2
world are correct?  Simply put, we don't see how to do that, and ideas
we have heard along those lines have been unsound.  At the least, one
would seem to need to formalize the complex notion of a valid world.

\subsection{Organization of This Paper}

In Section~\ref{sec:meta-extract} we provide examples of meta-extract
hypotheses and summary documentation of their various forms.
Section~\ref{sec:user} presents a community book that
% Reviewer 3 wanted us to change "We then" to "We" on the next line,
% but I think some word is needed there.  I've changed "We then" to
% "Next we", but please feel free to change this however you like.
provides a convenient way to use the meta-extract facility.  Next we
present applications in Section~\ref{sec:applications} and finally, we
conclude with Section~\ref{sec:conclusion}.