# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374615968 -7200
# Node ID 6f71b016cbe7437cc810dd4d7bb5ecb226dbcdbc
# Parent  55dc9ff45b73eadb6d4a9771147236faef76ca55
slides

diff -r 55dc9ff45b73 -r 6f71b016cbe7 Slides/Slides2.thy
--- 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
diff -r 55dc9ff45b73 -r 6f71b016cbe7 Slides/document/smiley.jpg
Binary file Slides/document/smiley.jpg has changed
diff -r 55dc9ff45b73 -r 6f71b016cbe7 slides2.pdf
Binary file slides2.pdf has changed