Organize the two OpenFlow pdfs into one for the AFP

.gitignore

@@ -23,5 +23,4 @@ cabal.sandbox.config
 thy/Examples/generated_code
 
 # generated OpenFlow files…
-thy/OpenFlow/of_doc
-thy/OpenFlow/of_outp
+thy/OpenFlow/output

thy/OpenFlow/Examples/OF_conv_test/OF_conv_test.thy

@@ -7,7 +7,7 @@ imports
   "../../OpenFlowSerialize"
 begin
 
-section\<open>Example: Simple Test for Translation to OpenFlow\<close>
+(*section\<open>Example: Simple Test for Translation to OpenFlow\<close>*)
 
 
 parse_iptables_save SQRL_fw="iptables-save"
@@ -51,7 +51,7 @@ definition "SQRL_fw_simple \<equiv> remdups_rev (to_simple_firewall (upper_closu
 value[code] "SQRL_fw_simple"
 lemma "simple_fw_valid SQRL_fw_simple" by eval
 
-section\<open>Example: SQRL RTBL\<close>
+(*section\<open>Example: SQRL RTBL\<close>*)
 
 parse_ip_route SQRL_rtbl_main = "ip-route"
 value SQRL_rtbl_main

thy/OpenFlow/Examples/RFC2544/RFC2544.thy

@@ -6,7 +6,7 @@ imports
   "../../OpenFlowSerialize"
 begin
 
-section\<open>Example: Simple Test for Translation to OpenFlow\<close>
+(*section\<open>Example: Simple Test for Translation to OpenFlow\<close>*)
 
 
 parse_iptables_save SQRL_fw="iptables-save"
@@ -46,8 +46,6 @@ definition "SQRL_fw_simple \<equiv> remdups_rev (to_simple_firewall (upper_closu
 value[code] "SQRL_fw_simple"
 lemma "simple_fw_valid SQRL_fw_simple" by eval
 
-section\<open>Example: SQRL RTBL\<close>
-
 parse_ip_route SQRL_rtbl_main = "ip-route"
 value SQRL_rtbl_main
 lemma "SQRL_rtbl_main = [\<lparr>routing_match = PrefixMatch 0xC6120100 24, metric = 0, routing_action = \<lparr>output_iface = ''ip1'', next_hop = None\<rparr>\<rparr>,

thy/OpenFlow/OpenFlowDoc.thy

@@ -1,22 +1,10 @@
 text_raw\<open>
-\normalfont
-\title{Verified Migration of Linux Firewalls to SDN}
-\author{Julius Michaelis and Cornelius Diekmann}
-\maketitle
-
-\begin{abstract}
-	We present a system that transforms the main routing table and \texttt{FORWARD} chain of iptables of a Linux-based firewall into a set of static OpenFlow rules.
-	Our implementation is verified against a model of a simplified Linux-based router and we can directly show how much of the original functionality is preserved.
-\end{abstract}
-
-%\tableofcontents
-
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
-
-\input{chap1}
+\twocolumn
+\columnsep 2pc          %    Space between columns
+\textwidth 42pc         % Width of text line.
+\part{Documentation}
+\label{part2}
 \<close>
-
 section\<open>Configuration Translation\<close>
 text_raw\<open>\label{sec:conv}\<close>
 text\<open>
@@ -158,7 +146,7 @@ text\<open>If no matching entry is found, the behavior is undefined.\<close>
 subsubsection\<open>iptables Firewall\<close>
 text_raw\<open>\label{sec:lfwfw}\<close>
 text\<open>The firewall subsystem in a linux router is not any less complex than any of the of the other systems.
-Fortunately, this complexity has been dealt with in~\cite{diekmann2016verified} already and we can directly use the result.\<close>
+Fortunately, this complexity has been dealt with in~\cite{diekmann2016verified,Iptables_Semantics-AFP} already and we can directly use the result.\<close>
 text\<open>In short, one of the results is that a complex \emph{iptables} configuration can be simplified to be represented by a single list of matches that only support the following match conditions:
 \begin{itemize}
   \item (String) prefix matches on the input and output interfaces.
@@ -535,12 +523,3 @@ There are some fundamental differences between Exodus and our work:
 (*<*)
 end
 (*>*)
-
-text_raw\<open>
-
-\input{chap3}
-
-\bibliographystyle{abbrv}
-\bibliography{root}
-\<close>
-(*\embedfile{OpenFlowDoc.tex}*)

thy/OpenFlow/ROOT

@@ -1,25 +1,13 @@
 chapter OpenFlow
-session "OpenFlow_Documentation" = OpenFlow +
-	options [document_output = "of_doc"]
-	theories
-		OpenFlowDoc
-	document_files
-		"root.tex"
-		"chap1.tex"
-		"chap3.tex"
-		"root.bib"
-		"moeptikz.sty"
-		"fig/ofts.pdf"
-		"fig/pipeline.pdf"
-		"fig/rtr.pdf"
-		"bench.csv"
 
 session "OpenFlow" = Iptables_Semantics +
-	options [document_output = "of_outp"]
+	options[document_output = "output"]
+
 	theories[document=false]
-  		"CaesarTheories" (* just some helper lemmas *)
+  		CaesarTheories (* just some helper lemmas *)
 		List_Group
 		Sort_Descending
+
 	theories
 		OpenFlowAction
 		OpenFlowMatches
@@ -29,8 +17,16 @@ session "OpenFlow" = Iptables_Semantics +
 		LinuxRouterOpenFlowTranslation
 		"Examples/OF_conv_test/OF_conv_test"
 		"Examples/RFC2544/RFC2544"
+		OpenFlowDoc
 
 	document_files
 		"root.tex"
+		"chap1.tex"
+		"chap3.tex"
+		"root.bib"
 		"moeptikz.sty"
+		"fig/ofts.pdf"
+		"fig/pipeline.pdf"
+		"fig/rtr.pdf"
+		"bench.csv"
 

thy/OpenFlow/Semantics_OpenFlow.thy

@@ -9,7 +9,7 @@ datatype 'a flowtable_behavior = Action 'a | NoAction | Undefined
 definition "option_to_ftb b \<equiv> case b of Some a \<Rightarrow> Action a | None \<Rightarrow> NoAction"
 definition "ftb_to_option b \<equiv> case b of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None"
 
-section\<open>OpenFlow\<close>
+(*section\<open>OpenFlow\<close>*)
 
 (*https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-switch-v1.5.0.pdf*)
 

thy/OpenFlow/document/root.bib

@@ -361,6 +361,7 @@ @inproceedings{michaelis2016middlebox
 	title={Middlebox Models in Network Verification Research},
 	booktitle={Proceedings of the Seminars Future Internet (FI) and Innovative Internet Technologies and Mobile Communications (IITM), Winter Semester 2015/2016},
 	year={2016},
+	volume={17},
 }
 @article{barras1997coq,
 	title={The Coq proof assistant reference manual: Version 6.1},
@@ -401,3 +402,14 @@ @inproceedings{lantz2010network
 	year={2010},
 	organization={ACM}
 }
+ 	
+@article{Iptables_Semantics-AFP,
+  author  = {Cornelius Diekmann and Lars Hupel},
+  title   = {{I}ptables {S}emantics},
+  journal = {Archive of Formal Proofs},
+  month   = sep,
+  year    = 2016,
+  note    = {\url{http://isa-afp.org/entries/Iptables_Semantics.shtml},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}

thy/OpenFlow/document/root.tex

@@ -51,7 +51,6 @@
 \usepackage{listings}
 \lstset{breaklines=true,numbers=left,numberstyle=\tiny\color{gray},basicstyle=\footnotesize\ttfamily}
 \usepackage{pgfplots}
-\twocolumn
 \columnsep 2pc          %    Space between columns
 \textwidth 42pc         % Width of text line.
 \oddsidemargin 4.5pc
@@ -60,7 +59,7 @@
 \advance\evensidemargin by -1in % Correct for LaTeX gratuitousness
 \marginparwidth 0pt             % Margin pars are not allowed.
 \marginparsep 11pt              % Horizontal space between outer margin and
-\emergencystretch=3cm
+\emergencystretch=10cm
 
 
 % this should be the last package used
@@ -77,9 +76,39 @@
 % for \frqq (whatever that actually is)
 
 \begin{document}
+\title{Verified Migration of Linux Firewalls to SDN}
+\author{Julius Michaelis and Cornelius Diekmann}
+\maketitle
+
+\begin{abstract}
+	We present a system that transforms the main routing table and \texttt{FORWARD} chain of iptables of a Linux-based firewall into a set of static OpenFlow rules.
+	Our implementation is verified against a model of a simplified Linux-based router and we can directly show how much of the original functionality is preserved.
+\end{abstract}
+\vspace{1em}
+
+Please note that this document is organized in two distinct parts.
+The first part contains the necessary definitions, helper lemmas and proofs in all their technicality as made in the theory code.
+The second part reiterates the most important definitions and proofs in a manner that is more suitable for human readers and enriches them with detailed explanations in natural language.
+Any interested reader should start from there.
+
+Many of the considerations that have led to the definitions made here have been explained in \cite{michaelis2016middlebox}.
+
+\tableofcontents
+
+\newpage
+
+\part{Code}
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
 
 \input{session}
 
+\input{chap3}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
@@ -90,3 +119,4 @@
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
+