--- a/Slides/Slides2.thy Tue Jul 23 15:18:15 2013 +0200
+++ b/Slides/Slides2.thy Tue Jul 23 23:46:08 2013 +0200
@@ -195,8 +195,8 @@
\item Asperti and Ricciotti formalised TMs in Matita\smallskip
\begin{itemize}
- \item \textcolor{gray}{no undecidability $\Rightarrow$ interest in complexity}
- \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates.}
+ \item \textcolor{gray}{no undecidability result $\Rightarrow$ interest in complexity}
+ \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates}
\begin{quote}
\textcolor{gray}{"In particular, the fact that the universal machine operates with a different
alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}
@@ -632,11 +632,11 @@
\only<3>{
\begin{itemize}
\item Suppose @{text H} decides @{text contra} called with code
- of @{text contra} does \emph{not} halt, then\smallskip
+ of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}
\begin{center}\small
\begin{tabular}{@ {}l@ {}}
- \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
+ \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}
@{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
@{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
@{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
@@ -710,17 +710,17 @@
\begin{itemize}
\item feels awfully like reasoning about machine code
- \item compositional constructions / reasoning not frictionless
+ \item compositional constructions / reasoning not at all frictionless
\item sizes
\begin{center}
\begin{tabular}{ll}
& sizes:\smallskip\\
UF & 140843 constructors\\
- Reg.~Mach.~ & @{text 2} Mio instructions\\
+ URM & @{text 2} Mio instructions\\
UTM & @{text 38} Mio states\\
\end{tabular}
- \end{center}\pause
+ \end{center}\smallskip\pause
\item an observation: our treatment of recursive functions is a mini-version
of the work by\\ Myreen \& Owens about deeply embedding HOL
@@ -730,7 +730,7 @@
\begin{textblock}{4}(2,13.9)
\begin{tikzpicture}
\draw (0,0) node {\small\begin{tabular}{l}$^\star$old version:
- RM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
+ URM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
\end{tikzpicture}
\end{textblock}}
@@ -738,6 +738,109 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\begin{tabular}{@ {}c@ {}}Stealing From Other Works\end{tabular}}%
+
+ \begin{itemize}
+ \item Jensen, Benton, Kennedy ({\bf 2013}),
+ {\it High-Level Separation Logic for Low-Level Code}\medskip\\
+
+ \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},
+ PhD thesis\medskip
+
+ \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}
+
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Better Composability}%
+
+ \begin{itemize}
+ \item an idea from Jensen, Benton, Kennedy who looked at X86
+ assembly programs and macros\bigskip
+
+ \item assembly for TMs:\medskip
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "move_one_left"} @{text "\<equiv>"}\\
+ \hspace{13mm} @{text "\<Lambda> exit."}\\
+ \hspace{16mm} @{text "Inst (L, exit) (L, exit)"} @{text ";"}\\
+ \hspace{16mm} @{text "Label exit"}\\
+ \end{tabular}
+ \end{center}\bigskip\bigskip
+
+ \begin{tabular}{l}
+ $\Rightarrow$ represent "state" labels as functions\\
+ \phantom{$\Rightarrow$} (with bound variables $\Rightarrow$ locality)
+ \end{tabular}
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Better Composability}%
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-10mm}}l}
+ @{text "move_left_until_zero"} @{text "\<equiv>"} \\
+ \hspace{31mm} @{text "\<Lambda> start exit."}\\
+ \hspace{36mm} @{text "Label start"} @{text ";"}\\
+ \hspace{36mm} @{text "if_zero exit"} @{text ";"}\\
+ \hspace{36mm} @{text "move_left"} @{text ";"}\\
+ \hspace{36mm} @{text "jmp start"} @{text ";"}\\
+ \hspace{36mm} @{text "Label exit"}\\
+ \end{tabular}
+ \end{center}
+
+ \small
+ \begin{tabular}{l}
+ @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^isub>0, e), (W\<^isub>1, exit); Label exit"}\\
+ \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^isub>0, e), (W\<^isub>1, e)"}
+ \end{tabular}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{{\large The Trouble With Hoare-Triples}}%
+
+ \begin{itemize}
+ \item Whenever we wanted to prove
+
+ \begin{center}
+ \large @{text "{P} p {Q}"}
+ \end{center}\bigskip\medskip
+
+ \item[@{text "(1)"}] we had to find a termination order proving that @{text p} terminates
+ \textcolor{gray}{(not easy)}
+
+ \item[@{text "(2)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy either)}
+ \end{itemize}\pause
+
+ \begin{center}
+ \alert{very little opportunity for automation}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -746,20 +849,93 @@
\frametitle{Separation Algebra}%
\begin{itemize}
- \item introduced a separation algebra framework for register machines and TMs
- \item we can semi-automate the reasoning for our small TMs
- \item we can assemble bigger programs out of smaller components\bigskip
+ \item use some infrastructure introduced by Klein et al in Isabelle/HOL
+ \item and an idea by Myreen\bigskip\bigskip
- \item looks awfully like ``real'' assembly code\pause
- \item Conclusion: we have a playing ground for reasoning about low-level
- code; we work on automation
+ \begin{center}
+ \large @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"}\bigskip\bigskip
+ \end{center}
+
+ \item[] @{text "p, c, q"} will be assertions in a separation logic\pause
+
+ \begin{center}
+ e.g.~~@{text "\<lbrace>st i \<star> hd n \<star> ones u v \<star> zero (v + 1)\<rbrace>"}
+ \end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Separation Triples}%
+ \Large
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{-10mm}}l}
+ @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\
+ & @{text "\<forall> cf r."}\\
+ & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\
+ & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (run k cf)"}
+ \end{tabular}
+ \end{center}\bigskip\bigskip
+ \normalsize
+ @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Automation}%
+
+ \begin{itemize}
+ \item we introduced some tactics for handling sequential programs\bigskip
+
+ \begin{center}
+ @{text "\<lbrace>p\<rbrace> i:[c\<^isub>1 ; ... ; c\<^isub>n]:j \<lbrace>q\<rbrace>"}
+ \end{center}\bigskip\bigskip
+
+ \item for loops we often only have to do inductions on the length
+ of the input (e.g.~how many @{text "1"}s are on the tape)\pause
+
+ \item these macros allow us to completely get rid of register machines
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Conclusion}%
+
+ \begin{itemize}
+ \item What started out as a student project, turned out to be much more
+ fun than first thought.\bigskip
+
+ \item Where can you claim that you proved the correctness of
+ a @{text "38"} Mio instruction program.
+ (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
+ \bigskip
+
+ \item We learned a lot about current verification technology for low-level code.
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
(*<*)
end