\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../data}
\usepackage{../graphics}
\usepackage{soul}
\usepackage{proof}

% beamer stuff
\renewcommand{\slidecaption}{CFL, King's College London}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       

\newcommand\grid[1]{%
	\begin{tikzpicture}[baseline=(char.base)]
	\path[use as bounding box]
	(0,0) rectangle (1em,1em);
	\draw[red!50, fill=red!20]
	(0,0) rectangle (1em,1em);
	\node[inner sep=1pt,anchor=base west]
	(char) at (0em,\gridraiseamount) {#1};
	\end{tikzpicture}}
\newcommand\gridraiseamount{0.12em}

\makeatletter
\newcommand\Grid[1]{%
	\@tfor\z:=#1\do{\grid{\z}}}
\makeatother	

\newcommand\Vspace[1][.3em]{%
	\mbox{\kern.06em\vrule height.3ex}%
	\vbox{\hrule width#1}%
	\hbox{\vrule height.3ex}}

\def\VS{\Vspace[0.6em]}


\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[-3mm]
  \LARGE Compilers and \\[-2mm] 
  \LARGE Formal Languages\\[3mm] 
  \end{tabular}}

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Office: & N7.07 (North Wing, Bush House)\\
  Slides: & KEATS (also home work is there)\\
  \end{tabular}
  \end{center}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Compilers \& Boeings 777}

First flight in 1994. They want to achieve triple redundancy in hardware
faults.\bigskip

They compile 1 Ada program to\medskip

\begin{itemize}
\item Intel 80486
\item Motorola 68040 (old Macintosh's)
\item AMD 29050 (RISC chips used often in laser printers)
\end{itemize}\medskip

using 3 independent compilers.\bigskip\pause

\small Airbus uses C and static analysers. Recently started using CompCert.

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{seL4 / Isabelle}

\begin{itemize}
\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip
\item US DoD has competitions to hack into drones; they found that the
  isolation guarantees of seL4 hold up\bigskip
\item CompCert and seL4 sell their code  
\end{itemize}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{POSIX Matchers}

\begin{itemize}
\item Longest match rule (``maximal munch rule''): The 
longest initial substring matched by any regular expression 
is taken as the next token.

\begin{center}
\bl{$\texttt{\Grid{iffoo\VS bla}}$}
\end{center}\medskip

\item Rule priority:
For a particular longest initial substring, the first regular
expression that can match determines the token.

\begin{center}
\bl{$\texttt{\Grid{if\VS bla}}$}
\end{center}
\end{itemize}\bigskip\pause

\small
\hfill Kuklewicz: most POSIX matchers are buggy\\
\footnotesize
\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\mbox{}\\[-14mm]\mbox{}
\small
\bl{
\begin{center}
\begin{tabular}{lcl}
$\textit{der}\;c\;(\ZERO)$ & $\dn$ & $\ZERO$\\
$\textit{der}\;c\;(\ONE)$  & $\dn$ & $\ZERO$\\
$\textit{der}\;c\;(d)$     & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;\ONE \; \textit{else} \;\ZERO$\\
$\textit{der}\;c\;(r_1 + r_2)$ & $\dn$ & $(\textit{der}\;c\;r_1) + (\textit{der}\;c\;r_2)$\\
$\textit{der}\;c\;(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\
      & & $\textit{then}\;((\textit{der}\;c\;r_1)\cdot r_2) + (\textit{der}\;c\;r_2)$\\
      & & $\textit{else}\;(\textit{der}\;c\;r_1)\cdot r_2$\\
$\textit{der}\;c\;(r^*)$ & $\dn$ & $(\textit{der}\;c\;r)\cdot (r^*)$\\
  $\textit{der}\;c\;(r^{\{n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\
  & & \textit{else if} $\textit{nullable}(r)$ \textit{then} $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\
  & & \textit{else} $(\textit{der}\;c\;r)\cdot (r^{\{n-1\}})$\\
  $\textit{der}\;c\;(r^{\{\uparrow n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\
  & & \textit{else}
  $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\
\end{tabular}
\end{center}}
  
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Proofs about Rexps}

Remember their inductive definition:

  \begin{center}
  \begin{tabular}{@ {}rrl}
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
         & \bl{$\mid$} & \bl{$\ONE$}     \\
         & \bl{$\mid$} & \bl{$c$}            \\
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\
         & \bl{$\mid$} & \bl{$r^*$}          \\
         & \bl{$\mid$} & \bl{$r^{\{n\}}$}     \\
         & \bl{$\mid$} & \bl{$r^{\{\uparrow n\}}$}     \\
  \end{tabular}
  \end{center}

If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Rexp (2)}

\begin{itemize}
\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
  holds for \bl{$r$}.
\item \ldots
\end{itemize}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Strings}

If we want to prove something, say a property \bl{$P(s)$}, for all
strings \bl{$s$} then \ldots\bigskip

\begin{itemize}
\item \bl{$P$} holds for the empty string, and\medskip
\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
already holds for \bl{$s$}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{frame}[c]
%
%\bl{\begin{center}
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
%$zeroable(\varnothing)$      & $\dn$ & \textit{true}\\
%$zeroable(\epsilon)$         & $\dn$ &  \textit{false}\\
%$zeroable (c)$               & $\dn$ &  \textit{false}\\
%$zeroable (r_1 + r_2)$       & $\dn$ &  $zeroable(r_1) \wedge zeroable(r_2)$ \\ 
%$zeroable (r_1 \cdot r_2)$   & $\dn$ &  $zeroable(r_1) \vee zeroable(r_2)$ \\
%$zeroable (r^*)$             & $\dn$ & \textit{false}\\
%\end{tabular}
%\end{center}}

%\begin{center}
%\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
%\end{center}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Correctness of the Matcher}

\begin{itemize}
\item We want to prove\medskip
\begin{center}
\bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$}
\end{center}\bigskip

where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$}
\bigskip\pause

\item We can do this, if we know\medskip
\begin{center}
\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}
\end{center}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Some Lemmas}

\begin{itemize}
\item \bl{$Der\;c\;(A\cup B) = 
(Der\;c\;A)\cup(Der\;c\;B)$}\bigskip
\item If \bl{$[] \in A$} then
\begin{center}
\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$}
\end{center}\bigskip
\item If \bl{$[] \not\in A$} then
\begin{center}
\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$}
\end{center}\bigskip
\item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\
\small\mbox{}\hfill (interesting case)\\
\end{itemize}

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Why?}

Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold?
\bigskip


\begin{center}
\begin{tabular}{lcl}
\bl{$Der\;c\;(A^*)$} & \bl{$=$} &  \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\
& \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\
& \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\
& \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\
\end{tabular}
\end{center}\bigskip\bigskip

\small
using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\
\mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{POSIX Spec}

\begin{center}
\bl{\infer{[] \in \ONE \to Empty}{}}\hspace{15mm}
\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip

\bl{\infer{s \in r_1 + r_2 \to Left(v)}
          {s \in r_1 \to v}}\hspace{10mm}
\bl{\infer{s \in r_1 + r_2 \to Right(v)}
          {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip

\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}
          {\small\begin{array}{l}
           s_1 \in r_1 \to v_1 \\
           s_2 \in r_2 \to v_2 \\
           \neg(\exists s_3\,s_4.\; s_3 \not= []
           \wedge s_3 @ s_4 = s_2 \wedge
           s_1 @ s_3 \in L(r_1) \wedge
           s_4 \in L(r_2))
           \end{array}}}
           
\bl{\ldots}           
\end{center}


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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t,squeeze]
\frametitle{Sulzmann \& Lu Paper}

\begin{itemize}
\item I have no doubt the algorithm is correct --- 
  the problem is I do not believe their proof.

  \begin{center}
  \begin{bubble}[10cm]\small
  ``How could I miss this? Well, I was rather careless when 
  stating this Lemma :)\smallskip
 
  Great example how formal machine checked proofs (and 
  proof assistants) can help to spot flawed reasoning steps.''
  \end{bubble}
  \end{center}\pause
  
  %\begin{center}
  %\begin{bubble}[10cm]\small
  %``Well, I don't think there's any flaw. The issue is how to 
  %come up with a mechanical proof. In my world mathematical 
  %proof $=$ mechanical proof doesn't necessarily hold.''
  %\end{bubble}
  %\end{center}\pause
  
\end{itemize}

  \only<3>{%
  \begin{textblock}{11}(1,4.4)
  \begin{center}
  \begin{bubble}[10.9cm]\small\centering
  \includegraphics[scale=0.37]{msbug.png}
  \end{bubble}
  \end{center}
  \end{textblock}}
  

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

\end{document}

%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{2nd CW}

Remember we showed that\\

\begin{center}
\bl{$der\;c\;(r^+) = (der\;c\;r)\cdot r^*$}
\end{center}\bigskip\pause


Does the same hold for \bl{$r^{\{n\}}$} with \bl{$n > 0$}

\begin{center}
\bl{$der\;c\;(r^{\{n\}}) = (der\;c\;r)\cdot r^{\{n-1\}}$} ?
\end{center}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{2nd CW}

\begin{itemize}
\item \bl{$der$}

\begin{center}
\bl{$der\;c\;(r^{\{n\}}) \dn 
\begin{cases}
\varnothing & \text{\textcolor{black}{if}}\; n = 0\\
der\;c\;(r\cdot r^{\{n-1\}}) & \text{\textcolor{black}{o'wise}}
\end{cases}$} 
\end{center}

\item \bl{$mkeps$}

\begin{center}
\bl{$mkeps(r^{\{n\}}) \dn
[\underbrace{mkeps(r),\ldots,mkeps(r)}_{n\;times}]$} 
\end{center}

\item \bl{$inj$}

\begin{center}
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
\bl{$inj\;r^{\{n\}}\;c\;(v_1, [vs])$}     & \bl{$\dn$} &
\bl{$[inj\;r\;c\;v_1::vs]$}\\
\bl{$inj\;r^{\{n\}}\;c\;Left(v_1, [vs])$} & \bl{$\dn$} &
\bl{$[inj\;r\;c\;v_1::vs]$}\\
\bl{$inj\;r^{\{n\}}\;c\;Right([v::vs])$}  & \bl{$\dn$} &
\bl{$[mkeps(r)::inj\;r\;c\;v::vs]$}\\
\end{tabular}
\end{center}

\end{itemize}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Induction over Strings}

\begin{itemize}
\item case \bl{$[]$}:\bigskip

We need to prove 

\begin{center}
  \bl{$\forall r.\;\;nullable(ders\;[]\;r) \;\Leftrightarrow\; [] \in L(r)$}
\end{center}\bigskip  
  
\begin{center}
  \bl{$nullable(ders\;[]\;r) \;\dn\; nullable\;r \;\Leftrightarrow\ldots$}
\end{center} 
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Induction over Strings}

\begin{itemize}
\item case \bl{$c::s$}\bigskip

We need to prove 

\begin{center}
  \bl{$\forall r.\;\;nullable(ders\;(c::s)\;r) \;\Leftrightarrow\; (c::s) \in L(r)$}
\end{center} 

We have by IH

\begin{center}
  \bl{$\forall r.\;\;nullable(ders\;s\;r) \;\Leftrightarrow\; s \in L(r)$}
\end{center}\bigskip 

\begin{center}
\bl{$ders\;(c::s)\;r \dn ders\;s\;(der\;c\;r)$}
\end{center}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Induction over Regexps}

\begin{itemize}
\item The proof hinges on the fact that we can prove\bigskip

\begin{center}
  \Large\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}
\end{center} 
\end{itemize}

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