\documentclass[t]{beamer}
\let\Tiny=\tiny

\usepackage{alltt}
\usepackage{graphicx}

\def\toolong{$\hspace{-100cm}$}

\title{(Co)verifying a compiler and a prover:\\the CakeML project}
\author{Freek Wiedijk}
\institute{Radboud University Nijmegen}
\date{2013\;10\;29}

\begin{document}

\begin{frame}[c]
\maketitle
\end{frame}

\begin{frame}[fragile]
\frametitle{factorial in HOL4}

\begingroup
\def\\{\char`\\}
\begin{alltt}
val fact_def = Define `
  (fact 0 = 1) /\\
  (fact (SUC n) = (SUC n) * fact n)
`;
\end{alltt}
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{program extraction in HOL4}

\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
val tEVAL = rhs o concl o EVAL;

val _ = set_trace "assumptions" 1;

val translate_fact = translate fact_def;

val fact_ast =
  (rand o rator o rhs o concl o definition) "fact_demo_decls_0";

val fact_string =
  tEVAL ``dec_to_sml_string ^fact_ast``;

val _ = (print (fromHOLstring fact_string); print "\\n");
\end{alltt}
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{certificate theorem}

\begingroup
\def\implies{$\Rightarrow$}
\begin{alltt}
Certificate theorem for fact:

 []
|- DeclAssum fact_demo_decls env \implies
   Eval env (Var (Short "fact")) ((NUM --> NUM) fact)
\end{alltt}
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{certificate theorem (continued)}

\begin{alltt}\footnotesize
Definition of declaration list:

 []
|- fact_demo_decls =
   [Dletrec
      [("fact","v1",
        If (App (Opb Leq) (Var (Short "v1")) (Lit (IntLit 0)))
          (Lit (IntLit 1))
          (App (Opn Times)
             (App (Opn Plus)
                (Let "k" (... ... (... ... ))
                   (... ... (... ... ) (Var (... ... ))))
                (Lit (IntLit 1)))
             (App Opapp (Var (Short "fact"))
                (Let "k"
                   (App (... ... ) (Var (... ... )) (Lit (IntLit 1)))\toolong
                   (If (... ... (... ... )) (Lit (IntLit 0))
                      (Var (Short "k")))))))]]
\end{alltt}

\end{frame}

\begin{frame}[fragile]
\frametitle{pretty-printed CakeML version of fact}

\begin{alltt}\small
fun fact v1 = 
  (if (v1 <= 0) 
  then 1 
  else ((
    let val k = (v1 - 1) 
    in 
      (if (k < 0) 
      then 0 
      else k) 
    end + 1) * (fact 
    let val k = (v1 - 1) 
    in 
      (if (k < 0) 
      then 0 
      else k) 
    end ))) ;
\end{alltt}

\end{frame}

\begin{frame}[fragile]
\frametitle{compiling to bytecode inside HOL4}

\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
val translate_fact10 = hol2deep ``fact 10``;

val fact10_ast =
  (rand o rator o concl) translate_fact10;

val bare_bc_state = tEVAL ``
  <|stack := [];
    code := PrintE++[Stop];
    pc := 0;
    refs := FEMPTY;
    handler := 0;
    clock := NONE;
    output := "";
    cons_names := [];
    inst_length := K 0 |>
``;

val initial_bc_state_no_eval = tEVAL ``
  install_code [] (SND (SND compile_primitives)) ^bare_bc_state
``;
\end{alltt}
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{compiling to bytecode inside HOL4 (continued)}

\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
val fact10_bc_state = tEVAL ``
  let (state1,_,code1) =
    compile_top (initial_repl_fun_state.rcompiler_state)
      (Tdec ^fact_ast) in
  let bc_state1 = install_code (cpam state1) code1
      ^initial_bc_state_no_eval in
  let (state2,_,code2) =
    compile_top state1 (Tdec (Dlet (Pvar "it") ^fact10_ast)) in
  let bc_state2 = install_code (cpam state2) code2 bc_state1 in
  bc_state2
``;

val fact10_bc = tEVAL ``(^fact10_bc_state).code``;

val fact10_bc_string = (print o fromHOLstring o tEVAL) ``
  FLAT (MAP (\\inst. bc_inst_to_string inst ++ "\\n")
    (code_labels (K 0) ^fact10_bc))
``;
\end{alltt}
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{bytecode for `fact 10'}

\begingroup
\def\\{\char`\\}
\def\rest{\textsf{{\dots} plus 1082 more bytecodes \dots}}
\begin{alltt}\footnotesize
printC 'r'
printC 'a'
printC 'i'
printC 's'
printC 'e'
printC ' '
print
printC '\\n'
stop
pushPtr addr 0
pushExc
jump addr 374
load 2
ref
pops 1
load 1
store 3\smallskip
\rest
\end{alltt}
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{running the bytecode outside HOL4}

\begin{alltt}\footnotesize
% /opt/src/vml/unverified/bytecode/cakeml-byte fact.bc
val + = <fn>
val - = <fn>
val * = <fn>
val div = <fn>
val mod = <fn>
val < = <fn>
val > = <fn>
val <= = <fn>
val >= = <fn>
val = = <fn>
val := = <fn>
val ~ = <fn>
val ! = <fn>
val ref = <fn>
val fact = <fn>
val it = 3628800
% 
\end{alltt}

\end{frame}

\begin{frame}[fragile]
\frametitle{CakeML source grammar}

\begingroup
\newcommand{\bnf}{::=}
\newcommand{\gramsep}{\ensuremath{\ |\ }}
\newcommand{\eg}{\textit{e.g.}}
\small
\[
\begin{array}{lcl}
\mathit{id} &\bnf& x\gramsep \mathit{Mn}\texttt{.}x\\

\mathit{cid} &\bnf& \mathit{Cn}\gramsep \mathit{Mn}\texttt{.}\mathit{Cn}\\

t & \bnf & \texttt{int} \gramsep\texttt{bool}\gramsep\texttt{unit}\gramsep
\alpha \gramsep id \gramsep t\ id \gramsep \texttt{(}t(\texttt{,}t)^*\texttt{)}id\\
&|& t\ \texttt{*}\ t\gramsep t\ \texttt{->}\ t\gramsep  t\ \texttt{ref}\gramsep \texttt{(}t\texttt{)}\\

l & \bnf & \mathbb{Z} \gramsep\texttt{true}\gramsep \texttt{false}\gramsep \texttt{()}\gramsep \texttt{[]}\\

p & \bnf & x\gramsep l\gramsep \mathit{cid} \gramsep \mathit{cid}\ p\gramsep \texttt{ref}\ p \gramsep \texttt{\_}\gramsep \texttt{(}p(\texttt{,}p)^*\texttt{)} \gramsep\texttt{[}p\,(\texttt{,}p)^*\texttt{]}\\ %
&|& p\ \texttt{::}\ p\\

e & \bnf & l \gramsep \mathit{id} \gramsep \mathit{cid} \gramsep \mathit{cid}\ e \gramsep \texttt{(}e\texttt{,}e\,(\texttt{,}e)^*\texttt{)}\gramsep\texttt{[}e\,(\texttt{,}e)^*\texttt{]}\\
&|& \texttt{raise}\ e\gramsep e\ \texttt{handle}\ p\ \texttt{=>}\ e\ (\texttt{|}\ p\ \texttt{=>}\ e)^*\\
&|& \texttt{fn}\ x\ \texttt{=>}\ e \gramsep e\ e \gramsep \texttt{(}(e\ \texttt{;})^*\ e\texttt{)}\gramsep\mathit{uop}\ e \gramsep e\ \mathit{op}\ e\\
&|& \texttt{if}\ e\ \texttt{then}\ e\ \texttt{else}\ e\gramsep\texttt{case}\ e\ \texttt{of}\ p\ \texttt{=>}\ e\ (\texttt{|}\ p\ \texttt{=>}\ e)^*\\
&|& \texttt{let}\ (\mathit{ld}|\texttt{;})^*\ \texttt{in}\ (e\ \texttt{;})^*\ e\ \texttt{end}\\

\mathit{ld} &\bnf& \texttt{val}\ x\ \texttt{=}\ e\gramsep
 \texttt{fun}\ x\ y^+\ \texttt{=}\ e\ (\texttt{and}\ x\ y^+\ \texttt{=}\ e)^*\\

\mathit{uop} &\bnf& \texttt{ref}\gramsep\texttt{!}\gramsep\verb+~+\\

\mathit{op} &\bnf& \texttt{=}\gramsep \texttt{:=} \gramsep \texttt{+}\gramsep \texttt{-}\gramsep \texttt{*}\gramsep \texttt{div}\gramsep \texttt{mod}\gramsep \texttt{<}\gramsep \texttt{<=}\gramsep \texttt{>}\gramsep \texttt{>=} \gramsep\texttt{<>}\gramsep\texttt{::}\\

&|&\texttt{before}\gramsep\texttt{andalso} \gramsep \texttt{orelse}%\\

%c & \bnf & \mathit{Cn} \gramsep \mathit{Cn}\ \texttt{of}\ t\\
%\mathit{tyd} & \bnf & \mathit{tyn}\ \texttt{=}\ c\ (\texttt{|}\ c)^*\\
%\mathit{tyn} &\bnf& \texttt{(}\alpha(\texttt{,}\alpha)^*\texttt{)}\ x\gramsep \alpha\ x\gramsep x\\
%
%d &\bnf& \texttt{datatype}\ \mathit{tyd}\ (\texttt{and}\ \mathit{tyd})^*\gramsep \texttt{val}\ p\ \texttt{=}\ e\\
%&|& \texttt{fun}\ x\ y^+\ \texttt{=}\ e\ (\texttt{and}\ x\ y^+\ \texttt{=}\ e)^*\\
%&|& \texttt{exception}\ c\\
%
%\mathit{sig} &\bnf& \texttt{:>}\ \texttt{sig}\ (\mathit{sl}\,|\texttt{;})^*\ \texttt{end}\\
%\mathit{sl} &\bnf& \texttt{val}\ x\ \texttt{:}\ t \gramsep \texttt{type}\ \mathit{tyn}\gramsep \texttt{datatype}\ \mathit{tyd}\ (\texttt{and}\ \mathit{tyd})^*\\
%
%\mathit{top} &\bnf& \texttt{structure}\ \mathit{Mn}\ \mathit{sig}^?\ \texttt{=}\ \texttt{struct}\ (d\,|\texttt{;})^*\ \texttt{end}\texttt{;}\gramsep d\texttt{;}\gramsep e\texttt{;}
%
\end{array}
\]
\endgroup

\end{frame}

\begin{frame}[fragile]
\frametitle{CakeML source grammar (continued)}

\begingroup
\newcommand{\bnf}{::=}
\newcommand{\gramsep}{\ensuremath{\ |\ }}
\newcommand{\eg}{\textit{e.g.}}
\small
\[
\begin{array}{lcl}
%\mathit{id} &\bnf& x\gramsep \mathit{Mn}\texttt{.}x\\
%
%\mathit{cid} &\bnf& \mathit{Cn}\gramsep M\texttt{.}\mathit{Cn}\\
%
%t & \bnf & \texttt{int} \gramsep\texttt{bool}\gramsep\texttt{unit}\gramsep
%\alpha \gramsep id \gramsep t\ id \gramsep \texttt{(}t(\texttt{,}t)^*\texttt{)}id\\
%&|& t\ \texttt{*}\ t\gramsep t\ \texttt{->}\ t\gramsep  t\ \texttt{ref}\gramsep \texttt{(}t\texttt{)}\\
%
%l & \bnf & \mathbb{Z} \gramsep\texttt{true}\gramsep \texttt{false}\gramsep \texttt{()}\gramsep \texttt{[]}\\
%
%p & \bnf & x\gramsep l\gramsep \mathit{cid} \gramsep \mathit{cid}\ p\gramsep \texttt{ref}\ p \gramsep \texttt{\_}\gramsep \texttt{(}p(\texttt{,}p)^*\texttt{)} \gramsep\texttt{[}p\,(\texttt{,}p)^*\texttt{]}\\ %
%&|& p\ \texttt{::}\ p\\
%
%e & \bnf & l \gramsep \mathit{id} \gramsep \mathit{cid} \gramsep \mathit{cid}\ e \gramsep \texttt{(}e\texttt{,}e\,(\texttt{,}e)^*\texttt{)}\gramsep\texttt{[}e\,(\texttt{,}e)^*\texttt{]}\\
%&|& \texttt{raise}\ e\gramsep e\ \texttt{handle}\ p\ \texttt{=>}\ e\ (\texttt{|}\ p\ \texttt{=>}\ e)^*\\
%&|& \texttt{fn}\ x\ \texttt{=>}\ e \gramsep e\ e \gramsep \texttt{(}(e\ \texttt{;})^*\ e\texttt{)}\gramsep\mathit{uop}\ e \gramsep e\ \mathit{op}\ e\\
%&|& \texttt{if}\ e\ \texttt{then}\ e\ \texttt{else}\ e\gramsep\texttt{case}\ e\ \texttt{of}\ p\ \texttt{=>}\ e\ (\texttt{|}\ p\ \texttt{=>}\ e)^*\\
%&|& \texttt{let}\ (\mathit{ld}|\texttt{;})^*\ \texttt{in}\ (e\ \texttt{;})^*\ e\ \texttt{end}\\
%
%\mathit{ld} &\bnf& \texttt{val}\ x\ \texttt{=}\ e\gramsep
% \texttt{fun}\ x\ y^+\ \texttt{=}\ e\ (\texttt{and}\ x\ y^+\ \texttt{=}\ e)^*\\
%
%\mathit{uop} &\bnf& \texttt{ref}\gramsep\texttt{!}\gramsep\verb+~+\\
%
%\mathit{op} &\bnf& \texttt{=}\gramsep \texttt{:=} \gramsep \texttt{+}\gramsep \texttt{-}\gramsep \texttt{*}\gramsep \texttt{div}\gramsep \texttt{mod}\gramsep \texttt{<}\gramsep \texttt{<=}\gramsep \texttt{>}\gramsep \texttt{>=} \gramsep\texttt{<>}\gramsep\texttt{::}\\
%
%&|&\texttt{before}\gramsep\texttt{andalso} \gramsep \texttt{orelse}\\

c & \bnf & \mathit{Cn} \gramsep \mathit{Cn}\ \texttt{of}\ t\\
\mathit{tyd} & \bnf & \mathit{tyn}\ \texttt{=}\ c\ (\texttt{|}\ c)^*\\
\mathit{tyn} &\bnf& \texttt{(}\alpha(\texttt{,}\alpha)^*\texttt{)}\ x\gramsep \alpha\ x\gramsep x\\

d &\bnf& \texttt{datatype}\ \mathit{tyd}\ (\texttt{and}\ \mathit{tyd})^*\gramsep \texttt{val}\ p\ \texttt{=}\ e\\
&|& \texttt{fun}\ x\ y^+\ \texttt{=}\ e\ (\texttt{and}\ x\ y^+\ \texttt{=}\ e)^*\\
&|& \texttt{exception}\ c\\

\mathit{sig} &\bnf& \texttt{:>}\ \texttt{sig}\ (\mathit{sl}\,|\texttt{;})^*\ \texttt{end}\\
\mathit{sl} &\bnf& \texttt{val}\ x\ \texttt{:}\ t \gramsep \texttt{type}\ \mathit{tyn}\gramsep \texttt{datatype}\ \mathit{tyd}\ (\texttt{and}\ \mathit{tyd})^*\\

\mathit{top} &\bnf& \texttt{structure}\ \mathit{Mn}\ \mathit{sig}^?\ \texttt{=}\ \texttt{struct}\ (d\,|\texttt{;})^*\ \texttt{end}\texttt{;}\gramsep d\texttt{;}\gramsep e\texttt{;}

\end{array}
\]
\endgroup

\end{frame}

\begin{frame}
\frametitle{CakeML project directories}

\begin{center}
\vspace{-.3cm}
\toolong\includegraphics[width=1.1\textwidth]{vml_visit/vml}\toolong
\end{center}

\end{frame}

\end{document}