slides-meta-extract-body.tex

% Another file will have the \documentclass and then \input this one.
% \documentclass[xcolor=x11names,compress]{beamer}

%% General document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage{lipsum}
\usepackage{ragged2e}
\usepackage{alltt}
\usepackage{rotating}
\usepackage{lscape}
\usepackage{setspace}
\usepackage{array}
\usepackage{verbatim}
\usepackage{fancyvrb}
\usepackage{color}
\usepackage{xspace}
\newcommand\codeHighlightr[1]{\textcolor[rgb]{1,0,0}{\textbf{#1}}}
\newcommand\codeHighlightg[1]{\textcolor[rgb]{0,1,0}{\textbf{#1}}}
\newcommand\codeHighlightb[1]{\textcolor[rgb]{0,0,1}{\textbf{#1}}}
\newcommand{\SmallSkip}{\vspace{0.5cm}\noindent}
\newcommand{\demo}{{\color{red} [DEMO]}}
\definecolor{darkorange}{RGB}{210,105,30}
\usepackage[english]{babel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%% Beamer Layout %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\useoutertheme[subsection=false,shadow]{miniframes}
\useinnertheme{default}
\usefonttheme{serif}
\usepackage{palatino}

\setbeamerfont{title like}{shape=\scshape}
\setbeamerfont{frametitle}{shape=\scshape}

%\setbeamercolor*{lower separation line head}{bg=DeepSkyBlue4}
\setbeamercolor*{lower separation line head}{bg=darkorange}
\setbeamercolor*{normal text}{fg=black,bg=white}
\setbeamercolor*{alerted text}{fg=red}
\setbeamercolor*{example text}{fg=black}
\setbeamercolor*{structure}{fg=black}

\setbeamercolor*{palette tertiary}{fg=black,bg=black!10}
\setbeamercolor*{palette quaternary}{fg=black,bg=black!10}

\renewcommand{\(}{\begin{columns}}
\renewcommand{\)}{\end{columns}}
\newcommand{\<}[1]{\begin{column}{#1}}
\renewcommand{\>}{\end{column}}
\setbeamertemplate{footline}{\hfill\insertframenumber/\inserttotalframenumber}
\setbeamertemplate{navigation symbols}{}

%\setbeamersize{text margin right=20pt}

% Modified from Jared (xdoc paper):
\hypersetup{%
   colorlinks=true,% hyperlinks will be black
   linkcolor=blue,% added by Matt K.
   urlcolor=blue,% added by Matt K.
   urlbordercolor=blue,% hyperlink borders will be red
   pdfborderstyle={/S/U/W 1.5}% border style will be underline of width 1pt
}

\definecolor{darkcyan}{cmyk}{1.0,0.2,0.2,0.2}

\newcommand\mydotdot{{\color{orange} ...}}

\AtBeginSection[]
{
   \begin{frame}
       \frametitle{\hspace{4mm}Outline}
       \tableofcontents[currentsection, currentsubsection]
   \end{frame}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\title{Meta-extract: Using Existing Facts in Meta-reasoning}
%\subtitle{SUBTITLE}
\author{
        Matt Kaufmann (UT Austin) \\
        Sol Swords (Centaur Technology)
}
\date{
        \vspace{1cm}
        ACL2 Workshop 2017
}
\titlepage
\end{frame}
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \begin{frame}{\hspace{4mm}Outline}
% \tableofcontents
% \end{frame}
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{\scshape Introduction}
\begin{frame}[fragile]
\frametitle{Introduction}

\begin{itemize}

\item ACL2 supports two kinds of user-defined, verified proof routines:
\begin{itemize}
\item \texttt{:meta} rule class: \texttt{term} $\rightarrow$ \texttt{term}, invoked by the rewriter, 
\item \texttt{:clause-processor} rule class: \texttt{clause} $\rightarrow$ \texttt{clauses}, invoked by hints.
\end{itemize}
% \item Must prove correctness with respect to an \textit{evaluator} which support a fixed set of functions.
\item Previously could extract facts from the world and use built-in proof tools, but could not assume them correct.
\item Now (post-2012) these facts/tools may be assumed correct via \textit{meta-extract hypotheses} when proving soundness of metafunctions.
  % from the {\em world} or the {\em context}.

  \begin{itemize}
  % \item Metafunctions can use  both; clause processors have only a world, not a context.
  % \item The facts will be \textit{extracted} at runtime, but \textit{assumed correct} when proving the metafunction.
  % \item Therefore, routines can use facts that were introduced \textit{after} they were proved correct.
  \item $\star\star\star$ At run time, a metafunction may use facts that were not available when it was proved correct! $\star\star\star$
  \end{itemize}
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{This talk}
  \begin{itemize}

  \item reviews meta reasoning

  \item gives two simple examples to illustrate meta-extract hypotheses

  \item discusses a nice shortcut

  \item summarizes some applications %; and

%  \item points to the paper and supporting materials for more information.

  \end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[\scshape Review]{\scshape Review of {\tt :Meta} Rules}
\begin{frame}[fragile]{Review of {\tt :Meta} Rules}

Canonical example of a {\tt :meta} rule:\\
\verb|cancel_plus-equal| {\small (from ``books/meta/meta-plus-equal.lisp'')}
cancels like terms from the equality of two sums.

{\footnotesize
\begin{verbatim}
ACL2 !>:trans (equal (+ x y x z) (+ x z z z))

(EQUAL (BINARY-+ X (BINARY-+ Y (BINARY-+ X Z)))
       (BINARY-+ X (BINARY-+ Z (BINARY-+ Z Z))))

=> *

ACL2 !>(cancel_plus-equal
        '(EQUAL (BINARY-+ X (BINARY-+ Y (BINARY-+ X Z)))
                (BINARY-+ X (BINARY-+ Z (BINARY-+ Z Z)))))
(EQUAL (BINARY-+ Y X) (BINARY-+ Z Z))
\end{verbatim}
}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Review of {\tt :Meta} Rules (2)}

Key events:
\begin{itemize}
\item Define an evaluator:
\begin{verbatim}
(defevaluator ev-plus-equal ...)
   (ev-plus-equal term alist) --> value
\end{verbatim}
  
\item Define the metafunction:
\begin{verbatim}
(defun cancel_plus-equal (x) ...)
\end{verbatim}

\item Prove the metafunction correct w.r.t. the evaluator:
\begin{verbatim}
(defthm cancel_plus-equal-correct
  (equal
   (ev-plus-equal x a)
   (ev-plus-equal (cancel_plus-equal x) a))
  :rule-classes ((:meta :trigger-fns (equal))))
\end{verbatim}
\end{itemize}
Let's see this rule used in a proof.

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Review of {\tt :Meta} Rules (2)}

% {\scriptsize
{\footnotesize
\begin{verbatim}
ACL2 !>(include-book "meta/meta-plus-equal" :dir :system)
....
ACL2 !>(trace$ cancel_plus-equal)
 ((CANCEL_PLUS-EQUAL))
ACL2 !>(thm (implies (and (acl2-numberp z)
                          (equal (+ x y x z) (+ x z z z)))
                     (equal z (/ (+ x y) 2)))
            :hints (("Goal" :in-theory (disable (tau-system)))))
Goal'
1> (CANCEL_PLUS-EQUAL
    (EQUAL (BINARY-+ X (BINARY-+ X (BINARY-+ Y Z)))
           (BINARY-+ X (BINARY-+ Z (BINARY-+ Z Z)))))
<1 (CANCEL_PLUS-EQUAL (EQUAL (BINARY-+ X Y) (BINARY-+ Z Z)))
....
Proof succeeded.
ACL2 !>
\end{verbatim}
}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[\scshape Example 1]{\scshape Example 1: Using Global Facts}
\begin{frame}[fragile]{Example 1: Using Global Facts}

Goal: Rewrite stobj \texttt{(accessor (updater val foo\$))} terms without either:
\begin{itemize}
\item proving $n^2$ individual rules per stobj
\item enabling accessors/updaters to expand to \texttt{nth}/\texttt{update-nth}
\end{itemize}
An approach: \texttt{nth-update-nth-ev-meta-fn} checks that
\texttt{accessor} is defined as a call of \texttt{nth} and
\texttt{updater} is defined as a call of \texttt{update-nth} and
rewrites accordingly.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Example 1: Using Global Facts}
\begin{itemize}
\item Can look up function definitons from the world.
\item But: how can we prove this correct?
\item Before meta-extract we'd need to somehow verify that the definitions found in the world were correct
  \begin{itemize}
  \item E.g., have a hypothesis metafunction that produces the corresponding assumption.
  \end{itemize}
\item Meta-extract lets you assume this while proving your metafunction correct.
\item Accessor \& updater functions don't need to be known by evaluator
\begin{itemize}
  \item Can prove it operates correctly even on functions that haven't been defined yet!
\end{itemize}
\end{itemize}
\end{frame}
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \begin{frame}[fragile]{Example 1: Using Global Facts}
%   Key: Function definitions can be retrieved from the world using
%   \texttt{meta-extract-formula} and \textit{assumed correct} using
%   a \texttt{meta-extract-global-fact} hyp.
% \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\begin{frame}[fragile]{Example 1: Using Global Facts}

\begin{verbatim}
; demos/nth-update-nth-meta-extract.lisp
(defthm nth-update-nth-meta-rule-st
  (implies
   (and (nth-update-nth-ev ; (f (update-g val st))
         (meta-extract-global-fact
          (list :formula (car term)) state)
         (meta-extract-alist term a state))
        ...)
   (equal (nth-update-nth-ev term a)
          (nth-update-nth-ev
           (nth-update-nth-meta-fn term mfc state)
           a)))
  :hints ...
  :rule-classes ((:meta :trigger-fns ...)))
\end{verbatim}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Example 1: Meta-extract Hypothesis}
  \texttt{Meta-extract-global-fact}:
\begin{itemize}
\item Returns various terms expressing known facts.
\item Only produces terms that are known true.
\item Meta rule/clause processor theorems are allowed to assume the terms it produces
  evaluate to true as a special hypothesis.
\end{itemize}
Part of the definition:
\begin{Verbatim}[formatcom=\small]
(case-match obj
  ((':formula name)
   (meta-extract-formula name st))
  ...)
\end{Verbatim}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\begin{frame}[fragile]{Meta-Extract-Global-Fact}
Supports:
\begin{itemize}
\item Theorem bodies, function definitions, and constraints (\texttt{meta-extract-formula})
\item Rewrite rules from functions' \texttt{lemmas} properties
\item Evaluation of ground function calls (\texttt{magic-ev-fncall}).
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[\scshape Example 2]{\scshape Example 2: Using Contexts}
\begin{frame}[fragile]{Example 2: Using Contexts}

Consider this metafunction:
\begin{Verbatim}[frame=none, framesep=5pt]
(defun nth-symbolp-metafn (term mfc state)
  (declare (xargs :stobjs state))
  (case-match term
    (('nth n x)
     (if (equal (mfc-ts n mfc state :forcep nil)
                *ts-symbol*)
         (list 'car x)
       term))
    (& term)))
\end{Verbatim}
Approximately: ``If term is \verb|(nth n x)| and \verb|n| is
known to be a symbol in the current context, rewrite term to
\verb|(car x)|.''

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[fragile]{Example 2: Using Contexts}
\begin{itemize}
\item How can we prove this correct?
\item Before meta-extract we'd need to somehow verify that \texttt{mfc-ts} was ``telling the truth''
  \begin{itemize}
  \item E.g., have a hypothesis metafunction that produces the corresponding assumption.
  \end{itemize}
\item Meta-extract lets you assume this while proving your metafunction correct.
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[fragile]{Example 2: Using Contexts}
Correctness theorem for \texttt{nth-symbolp-metafn}:

\begin{Verbatim}[formatcom=\small]
; workshops/2017/kaufmann-swords/support/intro.lisp
(defthm nth-symbolp-meta
  (implies
   ;; Meta-extract hypothesis:
   (nthmeta-ev (meta-extract-contextual-fact
                 `(:typeset ,(cadr term))
                 mfc 
                 state)
               a)
   ;; Standard meta rule conclusion:
   (equal (nthmeta-ev term a)
          (nthmeta-ev (nth-symbolp-metafn
                       term mfc state)
                      a)))
  :rule-classes ((:meta :trigger-fns (nth))))
\end{Verbatim}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Example 2: Meta-extract Hypothesis}
  \texttt{Meta-extract-contextual-fact}:
\begin{itemize}
\item Returns various terms expressing facts known under a given context.
\item Only produces terms that are known true.
\item Meta rule theorems are allowed to assume the terms it produces
  evaluate to true.
\end{itemize}
Part of the definition:
\begin{Verbatim}[formatcom=\small]
(case-match obj
  ((':typeset term . &) ; mfc-ts produces correct results
   `(typespec-check
     ',(mfc-ts term mfc state :forcep nil :ttreep nil)
     ,term))
\end{Verbatim}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Meta-Extract-Contextual-Fact}
Supports:
\begin{itemize}
\item Typeset reasoning (\texttt{mfc-ts})
\item Rewriting (\texttt{mfc-rw},\ \ \texttt{mfc-rw+},\ \ \texttt{mfc-relieve-hyp})
\item Linear arithmetic (\texttt{mfc-ap})
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[\scshape Shortcut]{\scshape A Nice Shortcut}
\begin{frame}[fragile] {A Nice Shortcut}
\begin{Verbatim}[fontsize=\small]
(my-evl (meta-extract-contextual-fact obj mfc state) a)
(my-evl (meta-extract-global-fact obj state) alist)
\end{Verbatim}
The above meta-extract hyps are accepted with \textit{any term} in place of \texttt{obj} and \texttt{alist}.
\begin{Verbatim}[fontsize=\small]
(defchoose my-evl-contextual-badguy (obj) (a mfc state)
  (not (my-evl (meta-extract-contextual-fact
                obj mfc state)
               a)))
\end{Verbatim}
\begin{itemize}
\item Means: ``If there is an obj such that the evaluation of the meta-extract is false, return one''
\item Using this as the \texttt{obj} implies the hyp for all \texttt{obj}.
\item $\rightarrow$ At most two meta-extract hyps cover all uses.
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\begin{frame}[fragile] {A Nice Shortcut}
Community book ``clause-processors/meta-extract-user'' defines event-generating macro
\texttt{def-meta-extract}, which produces:
\begin{itemize}
\item bad guy functions for a given evaluator
\item macros for meta-extract hyps using bad-guys
\item theorems showing how these hyps imply the correctness of various tools/facts.
\end{itemize}

E.g., 

\begin{Verbatim}[fontsize=\small]
(defthm my-evl-meta-extract-formula
   (implies (and (my-evl-meta-extract-global-facts)
                 (equal (w st) (w state)))
            (my-evl (meta-extract-formula name st) a)))
\end{Verbatim}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[\scshape Applications]{\scshape Some Applications}
\begin{frame}[fragile] {Some Applications}

\begin{itemize}

\item The GL symbolic interpreter uses meta-extract hypotheses to call
  functions, use rewrite rules, etc., without additional proof
  obligations

\item The community book {\tt centaur/misc/bound-rewriter.lisp}
  provides a tool for solving certain inequalities

\item A meta rule for context-sensitive rewriting (like Greve's
  ``nary'' framework) is defined in {\tt centaur/misc/context-rw.lisp}

\item Others....

\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{\scshape Conclusion}
\begin{frame}[fragile] {Conclusion}

Some concluding thoughts....

\begin{itemize}

\item This talk is just an introduction; meta reasoning is a bit
  complex to absorb in real time!

\item The paper develops the ideas from this talk more thoroughly,
  with more illustrative examples.

\item If you use GL then you are already taking advantage of
  meta-extract.

\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}