--- a/ROOT Wed Jun 26 14:42:42 2013 +0100
+++ b/ROOT Wed Jul 17 10:33:19 2013 +0100
@@ -12,7 +12,17 @@
"thys/UF"
"thys/UTM"
-session ITP = UTM +
- options [document = pdf, document_output = "."]
+session ITP in Paper = UTM +
+ options [document = pdf, document_output = "..", document_variants = "paper"]
theories
- "Paper/Paper"
\ No newline at end of file
+ "Paper"
+
+session Slides1 in Slides = UTM +
+ options [document = pdf, document_output = "..", document_variants = "slides1"]
+ theories
+ "Slides1"
+
+session Slides2 in Slides = UTM +
+ options [document = pdf, document_output = "..", document_variants = "slides2"]
+ theories
+ "Slides2"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides1.thy Wed Jul 17 10:33:19 2013 +0100
@@ -0,0 +1,524 @@
+(*<*)
+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\<^isub>0") and
+ inv_begin1 ("I\<^isub>1") and
+ inv_begin2 ("I\<^isub>2") and
+ inv_begin3 ("I\<^isub>3") and
+ inv_begin4 ("I\<^isub>4") and
+ inv_begin ("I\<^bsub>cbegin\<^esub>") and
+ inv_loop1 ("J\<^isub>1") and
+ inv_loop0 ("J\<^isub>0") and
+ inv_end1 ("K\<^isub>1") and
+ inv_end0 ("K\<^isub>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
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides2.thy Wed Jul 17 10:33:19 2013 +0100
@@ -0,0 +1,524 @@
+(*<*)
+theory Slides2
+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 ("1") and
+ Bk ("0") and
+ exponent ("_\<^bsup>_\<^esup>") and
+ inv_begin0 ("I\<^isub>0") and
+ inv_begin1 ("I\<^isub>1") and
+ inv_begin2 ("I\<^isub>2") and
+ inv_begin3 ("I\<^isub>3") and
+ inv_begin4 ("I\<^isub>4") and
+ inv_begin ("I\<^bsub>cbegin\<^esub>") and
+ inv_loop1 ("J\<^isub>1") and
+ inv_loop0 ("J\<^isub>0") and
+ inv_end1 ("K\<^isub>1") and
+ inv_end0 ("K\<^isub>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}{ITP, 24 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
+(*>*)
\ No newline at end of file
Binary file paper.pdf has changed
--- a/scala/comp1.scala Wed Jun 26 14:42:42 2013 +0100
+++ b/scala/comp1.scala Wed Jul 17 10:33:19 2013 +0100
@@ -5,6 +5,7 @@
import lib._
import turing._
import abacus._
+import scala.annotation.tailrec
// TMs used in the translation
@@ -38,14 +39,18 @@
}
-// start address of the nth instruction
-def address(p: AProg, n: Int) = {
- def layout(p: AProg) = p.map(_ match {
- case Inc(n) => 2 * n + 9
- case Dec(n, _) => 2 * n + 16
- case Goto(n) => 1
- })
- layout(p).take(n).sum + 1
+// start address of the instructions
+@tailrec
+def layout(p: AProg, sum: Int, out: List[Int]) : List[Int] = p match {
+ case Nil => out.reverse
+ case Inc(n)::p => layout(p, 2 * n + 9 + sum, 2 * n + 9 + sum::out)
+ case Dec(n, _)::p => layout(p, 2 * n + 16 + sum, 2 * n + 16 + sum::out)
+ case Goto(n)::p => layout(p, 1 + sum, 1 + sum::out)
+ }
+
+def address(layout: List[Int], n: Int) = {
+ //println("calculating layout of " + n)
+ layout(n) + 1
}
def compile_Inc(s: Int, n: Int) =
@@ -56,17 +61,29 @@
def compile_Goto(s: Int) = TMGoto.shift(s - 1)
-def compile_abc(p: AProg, s: Int, i: AInst) = i match {
- case Inc(n) => compile_Inc(s, n)
- case Dec(n, e) => compile_Dec(s, n, address(p, e))
- case Goto(e) => compile_Goto(address(p, e))
+@tailrec
+def compile_abc(lay: List[Int], p: AProg, cnt: Int, out: List[TM]): List[TM] = {
+ if (cnt % 1000 == 0) println("compile counter of instructions " + cnt);
+p match {
+ case Nil => out.reverse
+ case Inc(n)::p => compile_abc(lay, p, cnt + 1, compile_Inc(address(lay, cnt), n)::out)
+ case Dec(n, e)::p => compile_abc(lay, p, cnt + 1, compile_Dec(address(lay, cnt), n, address(lay, e))::out)
+ case Goto(e)::p => compile_abc(lay, p, cnt + 1, compile_Goto(address(lay, e))::out)
+}
}
// component TMs for each instruction
-def TMs(p: AProg) =
- p.zipWithIndex.map{case (i, n) => compile_abc(p, address(p, n), i)}
+def TMs(p: AProg) = {
+ val lay = layout(p, 0, Nil)
+ println("layout calculated")
+ println("number of states (38667456): " + lay.last)
+ compile_abc(lay, p, 0, Nil)
+}
-def toTM(p: AProg) = TMs(p).reduceLeft(_ ++ _)
+def toTM(p: AProg) = {
+ println("start TM compilation")
+ TMs(p).reduceLeft(_ ++ _)
+}
}
--- a/scala/comp2.scala Wed Jun 26 14:42:42 2013 +0100
+++ b/scala/comp2.scala Wed Jul 17 10:33:19 2013 +0100
@@ -23,42 +23,49 @@
case n => ClearRegs(n - 1) :+ Abacus(Dec(n - 1, 2), Goto(0))
}
-def cn_merge_gs(x: List[(Abacus, Int, Int)], p: Int) : Abacus = x match {
+def cn_merge_gs(x: List[(Abacus, Int)], n: Int, p: Int) : Abacus = x match {
case Nil => Abacus(Nil)
- case (gprog, gpara, gn)::gs => gprog :+ MVReg(gpara, p) :+ cn_merge_gs(gs, p + 1)
+ case (gprog, gn)::gs => gprog :+ MVReg(n, p) :+ cn_merge_gs(gs, n, p + 1)
}
// translation:
// second component is the arity of the recursive function,
// third componen is the maximum of registers used
-def compile_rec(f: Rec) : (Abacus, Int, Int) = f match {
- case Z => (Abacus(Goto(1)), 1, 2)
- case S => (AbacusAdd(0, 1, 2) :+ Abacus(Inc(1)), 1, 3)
- case Id(i, j) => (AbacusAdd(j, i, i + 1), i, i + 2)
+def compile_rec(f: Rec) : (Abacus, Int) = f match {
+ case Z => (Abacus(Goto(1)), 2)
+ case S => (AbacusAdd(0, 1, 2) :+ Abacus(Inc(1)), 3)
+ case Id(i, j) => (AbacusAdd(j, i, i + 1), i + 2)
case Cn(n, f, gs) => {
val cied_gs = gs.map(compile_rec)
- val (fprog, fpara, fn) = compile_rec(f)
- val pstr = (1 + n :: fn :: (cied_gs.map(_._3))).max
- val qstr = pstr + gs.length + 1
- (cn_merge_gs(cied_gs, pstr) :+ MVRegs(0, qstr, n) :+
- MVRegs(pstr, 0, gs.length) :+ fprog :+
- MVReg(fpara, pstr) :+ ClearRegs(gs.length) :+
- MVReg(pstr, n) :+ MVRegs(qstr, 0, n), n, qstr + n)
+ val (fprog, fn) = compile_rec(f)
+ val qstr = (fn :: (cied_gs.map(_._2))).max
+ (cn_merge_gs(cied_gs, n, qstr) :+
+ MVRegs(0, qstr + gs.length, n) :+
+ MVRegs(qstr, 0, gs.length) :+
+ fprog :+
+ MVReg(f.arity, qstr + gs.length + 1) :+
+ ClearRegs(gs.length) :+
+ MVRegs(qstr + gs.length , 0, n + 1), qstr + gs.length + n + 1)
}
case Pr(n, f, g) => {
- val (fprog, fpara, fn) = compile_rec(f)
- val (gprog, gpara, gn) = compile_rec(g)
- val p = List(n + 3, fn, gn).max
+ val (fprog, fn) = compile_rec(f)
+ val (gprog, gn) = compile_rec(g)
+ val qstr = List(fn, gn).max
val e = gprog.p.length + 7
- (MVReg(n, p) :+ fprog :+ MVReg(n, n + 1) :+
- ((Abacus(Dec(p, e)) :+ gprog :+ Abacus(Inc(n), Dec(n + 1, 3), Goto(1))) ++
- Abacus(Dec(n + 2, 0), Inc (n + 1), Goto (gprog.p.length + 4))), n + 1, p + 1)
+ (MVReg(0, qstr) :+
+ MVRegs(1, 0, n) :+
+ fprog :+
+ MVReg(n, n + 1) :+
+ MVRegs(0, 2, n) :+
+ ((Abacus(Dec(qstr, e)) :+ gprog :+ Abacus(Inc(0), Dec(n + 1, 3), Goto(1))) ++
+ Abacus(Dec(n + 2, 0), Inc (1), Goto (gprog.p.length + 4))), qstr + 1)
}
case Mn(n, f) => {
- val (fprog, fpara, fn) = compile_rec(f)
+ val (fprog, fn) = compile_rec(f)
val len = fprog.p.length
- (fprog ++ Abacus(Dec(n + 1, len + 5), Dec(n + 1, len + 3), Goto(len + 1), Inc(n), Goto(0)),
- n, List(n + 1, fn).max)
+ (MVRegs(0, 1, n) :+
+ (fprog ++ Abacus(Dec(n + 1, len + 5), Dec(n + 1, len + 3), Goto(len + 1), Inc(0), Goto(0))),
+ fn)
}
}
--- a/scala/ex.scala Wed Jun 26 14:42:42 2013 +0100
+++ b/scala/ex.scala Wed Jul 17 10:33:19 2013 +0100
@@ -2,8 +2,8 @@
import turing._
import abacus._
import recs._
-//import comp1._
-//import comp2._
+import comp1._
+import comp2._
// Turing machine examples
@@ -123,18 +123,22 @@
println("Pdec2 7 -> 2: " + Pdec2.eval(7))
println("Enclen 0 .. 10: " + (0 until 10).map(Enclen.eval(_)))
-/*
+println("Size of UF -> 140843: " + UF.size)
+
+
// compilation of rec to abacus tests
def test_comp2(f: Rec, ns: Int*) = {
- val (abc_f, arity, _) = compile_rec(f)
+ val (abc_f, _) = compile_rec(f)
val abc_map = (0 until ns.length).zip(ns).toMap[Int, Int]
- val start = System.nanoTime()
- val res = (abc_f.run(abc_map))(arity)
- val end = System.nanoTime()
- val time = (end - start)/1.0e9
- ("Result: " + res + " length: " + abc_f.p.length + " time: " + "%.5f".format(time))
+ //val start = System.nanoTime()
+ //val res = (abc_f.run(abc_map))(arity)
+ //val end = System.nanoTime()
+ //val time = (end - start)/1.0e9
+ //("Result: " + res + " length: " + abc_f.p.length + " time: " + "%.5f".format(time))
+ ("Length: " + abc_f.p.length)
}
+
println("S(3) " + test_comp2(S, 3))
println("Const(1) " + test_comp2(Const(1), 0))
println("Const(10) " + test_comp2(Const(10), 0))
@@ -143,23 +147,25 @@
println("Power(3, 4) " + test_comp2(Power, 3, 4))
println("Minus(30, 4) " + test_comp2(Minus, 30, 4))
println("Fact(5) " + test_comp2(Fact, 5))
-
+//println("UF(0) " + test_comp2(UF, 0))
def test_comp1(f: Rec, ns: Int*) = {
- val (abc_f, arity, _) = compile_rec(f)
- val tm = toTM(abc_f.p) :+ TMMopup(arity)
- val start = System.nanoTime()
- val res = tm.run(Tape(ns.toList))
- val end = System.nanoTime()
- val time = (end - start)/1.0e9
- ("length: " + tm.p.length + " tape: " + arity + " time: " + "%.5f".format(time) + "\nResult: " + res)
+ val (abc_f, _) = compile_rec(f)
+ println("Abacus Length: " + abc_f.p.length)
+ val tm = toTM(abc_f.p) :+ TMMopup(f.arity)
+ //val start = System.nanoTime()
+ //val res = tm.run(Tape(ns.toList))
+ //val end = System.nanoTime()
+ //val time = (end - start)/1.0e9
+ //("length: " + tm.p.length + " tape: " + arity + " time: " + "%.5f".format(time) + "\nResult: " + res)
+ ("Length: " + abc_f.p.length + " " + tm.p.length)
}
-println("")
-println("S(3) " + test_comp1(S, 3))
-println("Const(10) " + test_comp1(Const(10), 0))
-println("Add(6, 3) " + test_comp1(Add, 6, 3))
-println("Mult(4, 5) " + test_comp1(recs.Mult, 4, 5))
-println("Fact(4) " + test_comp1(Fact, 4))
+//println("")
+//println("S(3) " + test_comp1(S, 3))
+//println("Const(10) " + test_comp1(Const(10), 0))
+//println("Add(6, 3) " + test_comp1(Add, 6, 3))
+//println("Mult(4, 5) " + test_comp1(recs.Mult, 4, 5))
+//println("Fact(4) " + test_comp1(Fact, 4))
+println("UF(0) " + test_comp1(UF, 0))
-*/
--- a/scala/recs2.scala Wed Jun 26 14:42:42 2013 +0100
+++ b/scala/recs2.scala Wed Jul 17 10:33:19 2013 +0100
@@ -12,6 +12,7 @@
def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))
def o(r: Rec, f: Rec, g: Rec, h: Rec) = Cn(r.arity, this, List(r, f, g, h))
def arity : Int
+ def size : Int
}
case object Z extends Rec {
@@ -20,6 +21,7 @@
case _ => throw new IllegalArgumentException("Z args: " + ns)
}
override def arity = 1
+ override def size = 1
}
case object S extends Rec {
@@ -27,7 +29,8 @@
case n::Nil => n + 1
case _ => throw new IllegalArgumentException("S args: " + ns)
}
- override def arity = 1
+ override def arity = 1
+ override def size = 1
}
case class Id(n: Int, m: Int) extends Rec {
@@ -38,6 +41,7 @@
else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
override def arity = n
+ override def size = 1
}
case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
@@ -62,7 +66,8 @@
}
override def arity = n
- override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
+ override def toString = f.toString + " o " + gs.map(_.toString).mkString ("(",", ", ")")
+ override def size = 1 + f.size + gs.map(_.size).sum
}
// syntactic convenience
@@ -91,6 +96,7 @@
override def arity = n + 1
override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
+ override def size = 1 + f.size + g.size
}
// syntactic convenience
@@ -107,6 +113,7 @@
else throw new IllegalArgumentException("Mn: args")
override def arity = n
+ override def size = 1 + f.size
}
object Mn {
@@ -211,6 +218,7 @@
}
override def arity = 1
+ override def size = MaxTriangle.size
}
case object TriangleFast extends Rec {
@@ -222,12 +230,13 @@
}
override def arity = 1
+ override def size = Triangle.size
}
//(0 until 200).map(MaxTriangleFast.eval(_))
-val Penc = Add o (TriangleFast o (Add o (Id(2, 0), Id(2, 1))), Id(2, 0))
+val Penc = Add o (Triangle o (Add o (Id(2, 0), Id(2, 1))), Id(2, 0))
val Pdec1 = Minus o (Id(1, 0), Triangle o (MaxTriangle o (Id(1, 0))))
val Pdec2 = Minus o (MaxTriangle o (Id(1, 0)), Pdec1 o (Id(1, 0)))
Binary file slides1.pdf has changed
Binary file slides2.pdf has changed
--- a/thys2/Translation2.thy Wed Jun 26 14:42:42 2013 +0100
+++ b/thys2/Translation2.thy Wed Jul 17 10:33:19 2013 +0100
@@ -51,20 +51,30 @@
"rec_ci (Cn n f gs) = (let cied_gs = map (\<lambda> g. rec_ci g) gs in
let cied_f = rec_ci f in
let qstr = Max (set (map snd (cied_f # cied_gs))) in
- (cn_merge_gs cied_gs n qstr; mv_boxes 0 (qstr + length gs) n;
- mv_boxes qstr 0 (length gs) ; fst cied_f; mv_box (arity f) (Suc (qstr + length gs));
- empty_boxes (length gs); mv_boxes (qstr + length gs) 0 (Suc n), Suc (qstr + length gs + n)))" |
+ (cn_merge_gs cied_gs n qstr;
+ mv_boxes 0 (qstr + length gs) n;
+ mv_boxes qstr 0 (length gs) ;
+ fst cied_f;
+ mv_box (arity f) (Suc (qstr + length gs));
+ empty_boxes (length gs);
+ mv_boxes (qstr + length gs) 0 (Suc n), Suc (qstr + length gs + n)))" |
"rec_ci (Pr n f g) = (let (fa, fp) = rec_ci f in
let (ga, gp) = rec_ci g in
let qstr = max fp gp in
let e = length ga + 7 in
- (mv_box 0 qstr; mv_boxes 1 0 n; fa; mv_box n (Suc qstr); mv_boxes 0 2 n;
- mv_box (Suc qstr) 1; (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @
- [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" |
+ (mv_box 0 qstr;
+ mv_boxes 1 0 n;
+ fa;
+ mv_box n (Suc qstr);
+ mv_boxes 0 2 n;
+ mv_box (Suc qstr) 1;
+ (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @
+ [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" |
"rec_ci (Mn n f) = (let (fa, fp) = rec_ci f in
let len = length fa in
- (mv_boxes 0 (Suc 0) n; (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
- Goto (len + 1), Inc 0, Goto 0]), fp))"
+ (mv_boxes 0 (Suc 0) n;
+ (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
+ Goto (len + 1), Inc 0, Goto 0]), fp))"
--- a/thys2/UF_Rec.thy Wed Jun 26 14:42:42 2013 +0100
+++ b/thys2/UF_Rec.thy Wed Jul 17 10:33:19 2013 +0100
@@ -431,14 +431,8 @@
apply(simp only: misc if_True)
apply(simp only: left_std[symmetric] right_std[symmetric])
apply(simp)
-apply(auto)
-apply(rule_tac x="ka - 1" in exI)
-apply(rule_tac x="l" in exI)
-apply(simp)
-apply (metis Suc_diff_le diff_Suc_Suc diff_zero replicate_Suc)
-apply(rule_tac x="n + 1" in exI)
-apply(simp)
-done
+by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc)
+
lemma UF_simulate:
assumes "tm_wf tm"
@@ -665,6 +659,6 @@
"rec_eval rec_uf [m, cf] = UF m cf"
by (simp add: rec_uf_def)
-
+value "size rec_uf"
end