applications.tex

% \begin{comment}
% [Old comment] SOL will write this (perhaps including an application
%   from Centaur)
% --- Sol, is this done now?
% \end{comment}

% Since we used upper-case for subsections in intro.tex, for
% consistency let's use them in this file, too.  (But we could use
% lower-case in both; fine with me either way.)

% \begin{comment}
%   I was thinking of this as some examples readers could look at to
%   show how meta-extract is used in practice, but now that we have the
%   examples from the previous section maybe that shouldn't be the
%   focus.  Instead, maybe we really want to say what the most important
%   uses of it so far have been, and just show that it really is useful
%   in building sophisticated tools.  So, de-emphasize the just-expand
%   utility and spend a bit more time on GL?

%   [Matt, replacing what I wrote in my 12/28 email] I'm probably not
%   understanding your point, since to me, ``how meta-extract is used in
%   practice'' and ``most important uses of it so far'' are almost the
%   same.  Maybe your point was that it's better to focus on the most
%   {\em important} uses than it is to focus on the practicality of a
%   wide {\em range} of uses.  If so, I guess I sort of agree if I had
%   to choose; but I think both are really good.  And really, the
%   section already fleshes out the range of uses while mentioning some
%   important ones, notably GL.  Anyhow, I'll probably be happy with
%   whatever you'd like to do here.  In particular, if you care to
%   provide a bit more detail about how meta-extract supports GL, that
%   would be fine; but I can live with what we already have, too.  Oh,
%   and it looks like you might be concerned about overlap between this
%   section and the previous two sections, but I think each section
%   makes its own contribution: Section~\ref{sec:meta-extract} shows how
%   meta-extract works, Section~\ref{sec:user} shows your
%   bad-guy-based tools, and this section shows wide applicability,
%   sometimes providing important capabilities.

%   [Sol] What I said wasn't clear, but I think I meant that we don't
%   need examples that just show how to use meta-extract, tutorial-like,
%   but rather examples that show how useful it is.  So I'm going to
%   demote the just-expand utility to Others and spend a little more
%   time on GL.
% \end{comment}

\subsection{GL Symbolic Interpreter}

The
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_GL}{\underline{GL}}
framework for bit-level symbolic execution~\cite{gl-diss,
  bit-blasting-GL} is an important tool for hardware verification
efforts at Centaur Technology \cite{centaur-framework}.  To prove a
theorem, GL attempts to symbolically interpret the conclusion and
render it into a Boolean formula which can be proved via a
satisfiability check.  Given a bit-level representation of each
variable, the symbolic interpreter recursively computes a bit-level representation
of each subterm.  It expands function definitions as needed, down to
certain primitive functions for which support is built in.  Recent
versions can also apply rewrite rules.  It is implemented as a clause
processor and uses meta-extract to look up function definitions and
rewrite rules from the world and to evaluate ground terms using
\texttt{magic-ev-fncall}.

GL was originally written before meta-extract, and used two tricks to
replace its functionality.  The complexity of these tricks reflects
the utility of meta-extract, since it allows GL to now avoid these
desperate measures.
\begin{itemize}
\item In order to justify the correctness of function definitions, GL
  would keep track of all definitions that were used, and return each
  definitional equation as an additional proof obligation from the
  clause processor.  GL proof hints were orchestrated so as to use
  \texttt{:by} hints to attempt to cheaply discharge these
  obligations.  GL did not yet use rewrite rules, but they could have
  been handled similarly.
\item In order to apply functions to concrete arguments, each GL
  clause processor had an apply function that could call a fixed set
  of functions by name using a \texttt{case} statement.  GL provided
  automation for defining new such clause processors so that users
  could build in their own set of functions.
\end{itemize}


\subsection{Rewrite-bounds}

The community book ``centaur/misc/bound-rewriter.lisp'' provides a
tool for solving certain inequalities: it replaces subterms of an
inequality with known bounds if those subterms are in monotonic
positions.  For example, the term $a-b$ monotonically decreases as $b$
increases, so if we wish to prove $c<a-b$ and we know $B \geq b$, then
it suffices to prove $c<a-B$.  While this example would be easily
handled by ACL2's linear arithmetic solver, there are problems that
the bound rewriter can handle easily that overwhelm ACL2's nonlinear
solver and cannot be solved with linear arithmetic -- e.g.,
\begin{verbatim}
(implies (and (rationalp a) (rationalp b) (rationalp c)
              (<= 0 a) (<= 0 b) (<= 1 c)
              (<= a 10) (<= b 20) (<= c 30))
         (<= (+ (* a b c) (* a b) (* b c) (* a c))
             (+ (* 10 20 30) (* 10 20) (* 20 30) (* 10 30))))
\end{verbatim}
% Reviewer 3 say:
%%% Some discussion as to *why* "normal" linear or non-linear
%%% arithmetic in ACL2 can't solve this problem is in order here.
% I've tried to address that somewhat below, but I don't think it's
% the job of this paper to debug the nonlinear package.
This formula can't be solved with linear arithmetic, because it is not a
linear problem.  (If each product of variables is replaced by a fresh
variable, the result is clearly not a theorem.)
Moreover, the hint \texttt{:nonlinearp t} causes ACL2 to hang indefinitely.
However, the hint
\begin{verbatim}
(rewrite-bounds ((<= a 10)
                 (<= b 20)
                 (<= c 30)))
\end{verbatim}
solves it instantaneously by replacing upper-boundable occurrences of
\texttt{a} by 10, \texttt{b} by 20, and \texttt{c} by 30.  The same
results are obtained --- a quick proof using {\tt rewrite-bounds} but
an indefinite hang using nonlinear arithmetic --- if the arithmetic
expression on the last line of the theorem is replaced by its value,
7100.

The bound rewriter tool is implemented as a meta rule and uses
meta-extract extensively.  To determine which subterms are in
monotonic positions, it uses type-set reasoning to determine the signs
of subterms.  For example, $a \cdot b$ increases as $b$ increases if
$a$ is nonnegative and decreases as $b$ increases if $a$ is
nonpositive; if we can't (weakly) determine the sign of $a$, then we
can't replace $b$ or any subterm with a bound.  To determine whether a
proposed bound of a subterm is (contextually) true, it uses
\texttt{mfc-relieve-hyp} to show it by rewriting, and if that fails,
\texttt{mfc-ap} to show it by linear arithmetic reasoning.  The
correctness of these uses of ACL2 reasoning utilities are justified by
meta-extract-contextual-fact hypotheses.

\subsection{Context-rw}

A meta rule for context-sensitive rewriting, accomplishing something
similar to Greve's ``Nary'' framework \cite{greve06}, is defined in
``centaur/misc/context-rw.lisp'' (see
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_CONTEXTUAL-REWRITING}{\underline{contextual-rewriting}}).
Like Nary, it supports an analogue of congruence reasoning using
contexts that are more general than equivalence relations.  An example
of its use is to allow, e.g.,
\begin{verbatim}
(logbitp 4 (logand (logior a b c (logapp 6 d e)) f g))
\end{verbatim}
\noindent to be simplified to
\begin{verbatim}
(logbitp 4 (logand (logior a b c d) f g))
\end{verbatim}
without defining a rewrite rule specifically for that case. The
context rewriter uses certain theorems to justify rewriting subterms
under new contexts, that is, with new calls wrapped around them.  In
this case we might have a rule that says that \texttt{(logbitp 4 ...)}
induces a \texttt{(logand 16 ...)} context; this context can then be
propagated through the \texttt{logand} and \texttt{logior} down to the
\texttt{logapp} call, which simplifies under that context to just
\texttt{d}, using a traditional rewrite rule such as the following:
\begin{verbatim}
(implies (and (syntaxp (and (quotep n) (quotep m)))
              (equal (logtail m n) 0))
         (equal (logand n (logapp m a b))
                (logand n a)))
\end{verbatim}
% Sol: I added explanation here, even though you explain "roles
% ... reversed" later, since otherwise I think the rule is kind of
% confusing to read.  But if you want to delete my change, that's fine.
\noindent When interpreted as a context rule, the following says that
\texttt{logbitp} induces a \texttt{logand} context, by directing
replacement of an instance of the right-hand side of the equality by
the corresponding instance of the left-hand side.
\begin{verbatim}
(implies (syntaxp (quotep n))
         (equal (logbitp n (logand (ash 1 (nfix n)) m))
                (logbitp n m)))
\end{verbatim}
\noindent And the following rule says that \texttt{logior} propagates such a
\texttt{logand} context onto its second argument:
\begin{verbatim}
(implies (syntaxp (quotep n))
         (equal (logand n (logior a (logand n b)))
                (logand n (logior a b))))
\end{verbatim}
\noindent A syntactic requirement for context rules is that the left-
and right-hand sides must be identical except that some subterm of the
LHS is replaced by a variable in the RHS (in this case \texttt{b}),
and that is the only occurrence of that variable in the RHS.  That
variable corresponds to the subterm onto which the context will be
propagated, and the corresponding subterm of the LHS reflects the
context that will be propagated onto it.  So the rule immediately above says:
\begin{quote}
When \texttt{logior} occurs under a \texttt{(logand n ...)} context where
\texttt{n} is a constant, propagate the \texttt{(logand n ...)} context
onto the second argument of the \texttt{logior}.
\end{quote}
\noindent Experienced ACL2 users might note that the roles of the
left- and right-hand sides are essentially reversed in this usage;
this is because often the reverse of a good context-propagation rule
is also a good rewrite rule.

The context rewriter uses meta-extract in order to trust rewrite rules
extracted from the world and results from \texttt{mfc-rw+} and
\texttt{mfc-relieve-hyp}, which it uses, respectively, to simplify
subterms under new contexts and to discharge hypotheses necessary for
applying the context rules.

\subsection{Others}

A few other utilities from the community books use
meta-extract solely to be able to extract a formula from the world
(using \texttt{meta-extract-formula}) and assume it to be true.  For
example, ``clause-processors/witness-cp.lisp'' provides a framework
for reasoning about quantification (see
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_WITNESS-CP}{\underline{witness-cp}});
it uses \texttt{meta-extract-formula} to look up a stored fact showing
that a term representing a universal quantification implies any
instance of the quantified formula.  A second,
``clause-processors/just-expand.lisp'', provides a clause processor
and meta rule that force expansion of certain terms, somewhat similar
to the \texttt{:expand} hint.  A third,
``clause-processors/replace-equalities.lisp'', provides a tool for
replacing known equalities in ways that the
rewriter can't, e.g., replacing a variable with a term.  For example, the
following is not a valid rewrite rule because its left-hand side is a
variable, but it could be a good replace-equalities rule:
\begin{verbatim}
 (implies (matches pattern x)
          (equal x
                 (patternsubst pattern (sigma pattern x))))
\end{verbatim}

% \begin{comment}
% [Matt] Above, ``subsitute'' looks like a typo.

% [Sol] Yes, I appear to have misspelled it in a few places.  I mostly
% meant the form above to be evocative rather than an actual example of
% anything; I've changed it for now to use fewer functions that exist,
% but if you prefer we could make it a real example that exists in the
% books somewhere.
% \end{comment}