# HG changeset patch # User Christian Urban # Date 1374053599 -3600 # Node ID 4457185b22ef4b15fc5c1c70ee7a48ef6e50f213 # Parent ccec33db31d4014ea580c7c8f140d9adbc4bc8d4 added slides diff -r ccec33db31d4 -r 4457185b22ef ROOT --- 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 diff -r ccec33db31d4 -r 4457185b22ef Slides/Slides1.thy --- /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 \ 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 \ inv_begin n (s, tp) = inv_begin0 n tp" and + "s = 1 \ inv_begin n (s, tp) = inv_begin1 n tp" and + "s = 2 \ inv_begin n (s, tp) = inv_begin2 n tp" and + "s = 3 \ inv_begin n (s, tp) = inv_begin3 n tp" and + "s = 4 \ inv_begin n (s, tp) = inv_begin4 n tp" and + "s \ {0,1,2,3,4} \ inv_begin n (s, l, r) = False" +apply(case_tac [!] tp) +by (auto) + + +lemma inv1: + shows "0 < (n::nat) \ 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 \ 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 \ measure_begin_step (s, l, r) = length r" and + "s = 3 \ measure_begin_step (s, l, r) = (if r = [] \ r = [Bk] then 1 else 0)" and + "s = 4 \ measure_begin_step (s, l, r) = length l" and + "s \ {2,3,4} \ measure_begin_step (s, l, r) = 0" +by (simp_all) + +lemma inv_begin01: + assumes "n > 1" + shows "inv_begin0 n (l, r) = (n > 1 \ (l, r) = (Oc \ (n - 2), [Oc, Oc, Bk, Oc]))" +using assms by auto + +lemma inv_begin02: + assumes "n = 1" + shows "inv_begin0 n (l, r) = (n = 1 \ (l, r) = ([], [Bk, Oc, Bk, Oc]))" +using assms by auto + +(*>*) + + + +text_raw {* + \renewcommand{\slidecaption}{SMAL, 16 July 2013} + \newcommand{\bl}[1]{#1} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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 "\"}\\ + \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 "\"}\\ + \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 "\"}\\ + \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{ + \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 "\"}\\[1mm] + \hspace{5mm}@{text "\"}@{term "tp"}.\\ + \hspace{7mm}if @{term "P tp"} holds then\\ + \hspace{7mm}@{text "\"}@{term n}. such that\\ + \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\"}\\ + \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 "\"}\\[1mm] + \hspace{5mm}@{text "\"}@{term "tp"}.\\ + \hspace{7mm}if @{term "P tp"} holds then\\ + \hspace{7mm}@{text "\"}@{term n}. @{text "\ 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{ + \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 "\"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ + @{thm (lhs) inv_begin2.simps} & @{text "\"} & @{thm (rhs) inv_begin2.simps}\\ + @{thm (lhs) inv_begin3.simps} & @{text "\"} & @{thm (rhs) inv_begin3.simps}\\ + @{thm (lhs) inv_begin4.simps} & @{text "\"} & @{thm (rhs) inv_begin4.simps}\\ + @{thm (lhs) inv_begin0.simps} & @{text "\"} & @{thm (rhs) inv_begin01} @{text "\"}& (halting state)\\ + & & @{thm (rhs) inv_begin02}\smallskip \\ + \hline + @{thm (lhs) inv_loop1.simps} & @{text "\"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\"}\\ + & & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\ + @{thm (lhs) inv_loop0.simps} & @{text "\"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\ + \hline + @{thm (lhs) inv_end1.simps} & @{text "\"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ + @{thm (lhs) inv_end0.simps} & @{text "\"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ + \hline + \end{tabular} + \end{center} + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Register Machines}% + + \begin{itemize} + \item instructions + + \begin{center} + \begin{tabular}{rcl@ {\hspace{10mm}}l} + @{text "I"} & $::=$ & @{term "Inc R\"} & increment register @{text "R"} by one\\ + & $\mid$ & @{term "Dec R\ L\"} & if content of @{text R} is non-zero,\\ + & & & then decrement it by one\\ + & & & otherwise jump to instruction @{text L}\\ + & $\mid$ & @{term "Goto L\"} & jump to instruction @{text L} + \end{tabular} + \end{center} + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{ + \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 diff -r ccec33db31d4 -r 4457185b22ef Slides/Slides2.thy --- /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 \ 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 \ inv_begin n (s, tp) = inv_begin0 n tp" and + "s = 1 \ inv_begin n (s, tp) = inv_begin1 n tp" and + "s = 2 \ inv_begin n (s, tp) = inv_begin2 n tp" and + "s = 3 \ inv_begin n (s, tp) = inv_begin3 n tp" and + "s = 4 \ inv_begin n (s, tp) = inv_begin4 n tp" and + "s \ {0,1,2,3,4} \ inv_begin n (s, l, r) = False" +apply(case_tac [!] tp) +by (auto) + + +lemma inv1: + shows "0 < (n::nat) \ 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 \ 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 \ measure_begin_step (s, l, r) = length r" and + "s = 3 \ measure_begin_step (s, l, r) = (if r = [] \ r = [Bk] then 1 else 0)" and + "s = 4 \ measure_begin_step (s, l, r) = length l" and + "s \ {2,3,4} \ measure_begin_step (s, l, r) = 0" +by (simp_all) + +lemma inv_begin01: + assumes "n > 1" + shows "inv_begin0 n (l, r) = (n > 1 \ (l, r) = (Oc \ (n - 2), [Oc, Oc, Bk, Oc]))" +using assms by auto + +lemma inv_begin02: + assumes "n = 1" + shows "inv_begin0 n (l, r) = (n = 1 \ (l, r) = ([], [Bk, Oc, Bk, Oc]))" +using assms by auto + +(*>*) + + + +text_raw {* + \renewcommand{\slidecaption}{ITP, 24 July 2013} + \newcommand{\bl}[1]{#1} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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 "\"}\\ + \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 "\"}\\ + \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 "\"}\\ + \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{ + \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 "\"}\\[1mm] + \hspace{5mm}@{text "\"}@{term "tp"}.\\ + \hspace{7mm}if @{term "P tp"} holds then\\ + \hspace{7mm}@{text "\"}@{term n}. such that\\ + \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\"}\\ + \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 "\"}\\[1mm] + \hspace{5mm}@{text "\"}@{term "tp"}.\\ + \hspace{7mm}if @{term "P tp"} holds then\\ + \hspace{7mm}@{text "\"}@{term n}. @{text "\ 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{ + \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 "\"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ + @{thm (lhs) inv_begin2.simps} & @{text "\"} & @{thm (rhs) inv_begin2.simps}\\ + @{thm (lhs) inv_begin3.simps} & @{text "\"} & @{thm (rhs) inv_begin3.simps}\\ + @{thm (lhs) inv_begin4.simps} & @{text "\"} & @{thm (rhs) inv_begin4.simps}\\ + @{thm (lhs) inv_begin0.simps} & @{text "\"} & @{thm (rhs) inv_begin01} @{text "\"}& (halting state)\\ + & & @{thm (rhs) inv_begin02}\smallskip \\ + \hline + @{thm (lhs) inv_loop1.simps} & @{text "\"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\"}\\ + & & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\ + @{thm (lhs) inv_loop0.simps} & @{text "\"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\ + \hline + @{thm (lhs) inv_end1.simps} & @{text "\"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ + @{thm (lhs) inv_end0.simps} & @{text "\"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ + \hline + \end{tabular} + \end{center} + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Register Machines}% + + \begin{itemize} + \item instructions + + \begin{center} + \begin{tabular}{rcl@ {\hspace{10mm}}l} + @{text "I"} & $::=$ & @{term "Inc R\"} & increment register @{text "R"} by one\\ + & $\mid$ & @{term "Dec R\ L\"} & if content of @{text R} is non-zero,\\ + & & & then decrement it by one\\ + & & & otherwise jump to instruction @{text L}\\ + & $\mid$ & @{term "Goto L\"} & jump to instruction @{text L} + \end{tabular} + \end{center} + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{ + \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 diff -r ccec33db31d4 -r 4457185b22ef paper.pdf Binary file paper.pdf has changed diff -r ccec33db31d4 -r 4457185b22ef scala/comp1.scala --- 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(_ ++ _) +} } diff -r ccec33db31d4 -r 4457185b22ef scala/comp2.scala --- 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) } } diff -r ccec33db31d4 -r 4457185b22ef scala/ex.scala --- 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)) -*/ diff -r ccec33db31d4 -r 4457185b22ef scala/recs2.scala --- 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))) diff -r ccec33db31d4 -r 4457185b22ef slides1.pdf Binary file slides1.pdf has changed diff -r ccec33db31d4 -r 4457185b22ef slides2.pdf Binary file slides2.pdf has changed diff -r ccec33db31d4 -r 4457185b22ef thys2/Translation2.thy --- 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 (\ 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))" diff -r ccec33db31d4 -r 4457185b22ef thys2/UF_Rec.thy --- 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