(*<*)
theory Slides1
imports "../thys/UTM" "../thys/Abacus_Defs"
begin
declare [[show_question_marks = false]]
hide_const (open) s
abbreviation
"update2 p a \<equiv> update a p"
notation (latex output)
Cons ("_::_" [48,47] 48) and
Oc ("0") and
Bk ("1") and
exponent ("_\<^bsup>_\<^esup>") and
inv_begin0 ("I\<^sub>0") and
inv_begin1 ("I\<^sub>1") and
inv_begin2 ("I\<^sub>2") and
inv_begin3 ("I\<^sub>3") and
inv_begin4 ("I\<^sub>4") and
inv_begin ("I\<^bsub>cbegin\<^esub>") and
inv_loop1 ("J\<^sub>1") and
inv_loop0 ("J\<^sub>0") and
inv_end1 ("K\<^sub>1") and
inv_end0 ("K\<^sub>0")
lemma inv_begin_print:
shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
"s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and
"s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and
"s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and
"s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
"s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
apply(case_tac [!] tp)
by (auto)
lemma inv1:
shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
unfolding Turing_Hoare.assert_imp_def
unfolding inv_loop1.simps inv_begin0.simps
apply(auto)
apply(rule_tac x="1" in exI)
apply(auto simp add: replicate.simps)
done
lemma inv2:
shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
apply(rule ext)
apply(case_tac x)
apply(simp add: inv_end1.simps)
done
lemma measure_begin_print:
shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
"s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
"s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and
"s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
by (simp_all)
lemma inv_begin01:
assumes "n > 1"
shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
using assms by auto
lemma inv_begin02:
assumes "n = 1"
shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
using assms by auto
(*>*)
text_raw {*
\renewcommand{\slidecaption}{SMAL, 16 July 2013}
\newcommand{\bl}[1]{#1}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\\[-3mm]
\Large Reasoning about Turing Machines\\[-1mm]
\Large and Low-Level Code\\[-3mm]
\end{tabular}}
\begin{center}
Christian Urban\\[1mm]
%%\small King's College London
\end{center}\bigskip
\begin{center}
in cooperation with Jian Xu and Xingyuan Zhang
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{A Trend in Verification}%
\begin{itemize}
\item in the past:\\
\begin{quote}
model a problem mathematically and proof properties about the
model
\end{quote}\bigskip
\item needs elegance, is still very hard\bigskip\pause
\item does not help with ensuring the correctness of running programs
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{A Trend in Verification}%
\begin{itemize}
\item make the specification executable (e.g.~Compcert)\bigskip\pause
you would expect the trend would be to for example model C, implement
your programs in C and verify the programs written in C (e.g.~seL4)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{A Trend in Verification}%
\begin{itemize}
\item but actually people start to verify machine code directly
(e.g.~bignum arithmetic implemented in x86-64 -- 700 instructions)
\item CPU models exists, but the strategy is to use a small subset
which you use in your programs
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Why Turing Machines}%
\begin{itemize}
\item at the beginning it was just a nice student project
about computability
\begin{center}
\includegraphics[scale=0.3]{boolos.jpg}
\end{center}
\item found an inconsistency in the definition of halting computations
(Chap.~3 vs Chap.~8)
\pause
\item \small Norrish formalised computability via lambda-calculus (and nominal);
Asperti and Riccioti formalised TMs but didn't get proper UTM
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Turing Machines}%
\begin{itemize}
\item tapes contain 0 or 1 only
\begin{center}
\begin{tikzpicture}[scale=1]
\draw[very thick] (-3.0,0) -- ( 3.0,0);
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
\draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
\draw[fill] (-1.65,0.1) rectangle (-1.35,0.4);
\draw (-0.25,0.8) -- (-0.25,-0.8);
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
\node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};
\node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};
\node [anchor=base] at (0.1,0.7) {\small \;\;head};
\node [anchor=base] at (-2.2,0.2) {\ldots};
\node [anchor=base] at ( 2.3,0.2) {\ldots};
\end{tikzpicture}
\end{center}
\item steps function
\begin{quote}
What does the tape look like after the TM has executed n steps?
\end{quote}\pause
designate the 0-state as halting state and remain there forever
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Copy Turing Machines}%
\begin{itemize}
\item TM that copies a number on the input tape
\begin{center}
\begin{tikzpicture}[scale=0.7]
\node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
\node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
\node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
\node [anchor=base] at (2.2,-0.8) {\small$\overbrace{\text{cbegin}}^{}$};
\node [anchor=base] at (5.6,-0.8) {\small$\overbrace{\text{cloop}}^{}$};
\node [anchor=base] at (10.5,-0.8) {\small$\overbrace{\text{cend}}^{}$};
\begin{scope}[shift={(0.5,0)}]
\draw[very thick] (-0.25,0) -- ( 1.25,0);
\draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\end{scope}
\begin{scope}[shift={(2.9,0)}]
\draw[very thick] (-0.25,0) -- ( 2.25,0);
\draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\end{scope}
\begin{scope}[shift={(6.8,0)}]
\draw[very thick] (-0.75,0) -- ( 3.25,0);
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\end{scope}
\begin{scope}[shift={(11.7,0)}]
\draw[very thick] (-0.75,0) -- ( 3.25,0);
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\end{scope}
\end{tikzpicture}
\end{center}\bigskip
\footnotesize
\begin{center}
\begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
\begin{tabular}[t]{@ {}l@ {}}
@{text cbegin} @{text "\<equiv>"}\\
\hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
\end{tabular}
&
\begin{tabular}[t]{@ {}l@ {}}
@{text cloop} @{text "\<equiv>"}\\
\hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"}
\end{tabular}
&
\begin{tabular}[t]{@ {}l@ {}}
@{text cend} @{text "\<equiv>"}\\
\hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
\end{tabular}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
\definecolor{mygrey}{rgb}{.80,.80,.80}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Hoare Logic for TMs}%
\begin{itemize}
\item Hoare-triples and Hoare-pairs:
\small
\begin{center}
\begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}
\begin{tabular}[t]{@ {}l@ {}}
\colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
\hspace{7mm}if @{term "P tp"} holds then\\
\hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
\hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
\hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
\end{tabular} &
\begin{tabular}[t]{@ {}l@ {}}
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
\hspace{7mm}if @{term "P tp"} holds then\\
\hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
\end{tabular}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
\definecolor{mygrey}{rgb}{.80,.80,.80}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Hoare Reasoning}%
\begin{itemize}
\item reasoning is still quite difficult---invariants
\footnotesize
\begin{center}
\begin{tabular}{@ {\hspace{-4mm}}lcl@ {\hspace{-0.9cm}}l@ {}}
\hline
@{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
@{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
@{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
@{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
@{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
& & @{thm (rhs) inv_begin02}\smallskip \\
\hline
@{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
& & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
@{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
\hline
@{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
@{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
\hline
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Register Machines}%
\begin{itemize}
\item instructions
\begin{center}
\begin{tabular}{rcl@ {\hspace{10mm}}l}
@{text "I"} & $::=$ & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
& $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\
& & & then decrement it by one\\
& & & otherwise jump to instruction @{text L}\\
& $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Recursive Functions}%
\begin{itemize}
\item addition, multiplication, \ldots
\item logical operations, quantifiers\ldots
\item coding of numbers (Cantor encoding)
\item UF\pause\bigskip
\item Recursive Functions $\Rightarrow$ Register Machines
\item Register Machines $\Rightarrow$ Turing Machines
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Sizes}%
\begin{itemize}
\item UF (size: 140843)
\item Register Machine (size: 2 Mio instructions)
\item UTM (size: 38 Mio states)
\end{itemize}\bigskip\bigskip
\small
old version: RM (12 Mio) UTM (112 Mio)
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\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 looks awfully like ``real'' assembly code\pause
\item Conclusion: we have a playing ground for reasoning about low-level
code; we work on automation
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)