lib: A tutorial and some 'modify' monad rules for Lib.EquivValid

Thanks to Toby Murray (@tobycmurray) for early feedback.

Signed-off-by: Robert Sison <robert.sison@unimelb.edu.au>

.github/workflows/proof.yml

@@ -51,7 +51,7 @@ jobs:
       with:
         L4V_ARCH: ${{ matrix.arch }}
         isa_branch: ts-2020
-        session: ExecSpec ASpec AInvs
+        session: ExecSpec ASpec AInvs EVTutorial
 
   refine:
     name: Refine

CONTRIBUTORS.md

@@ -68,6 +68,7 @@ order).
 * Thomas Sewell, Data61, NICTA & UNSW
 * Michael Sproul, Data61
 * Rupert Shuttleworth, NICTA
+* Robert Sison, The University of Melbourne
 * Miki Tanaka, Data61, NICTA
 * Vernon Tang, NICTA
 * Sophie Taylor, Data61, NICTA

ROOTS

@@ -8,4 +8,5 @@ camkes
 sys-init
 lib
 lib/Word_Lib
-lib/sep_algebra
+lib/sep_algebra
+lib/EVTutorial

lib/EVTutorial/ROOT

@@ -0,0 +1,15 @@
+(*
+ * Copyright 2020, The University of Melbourne (ABN 84 002 705 224)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+chapter Lib
+
+session EVTutorial = Lib +
+  options [document = pdf]
+  theories
+    EquivValidTutorial
+  document_files
+    "root.bib"
+    "root.tex"

lib/EVTutorial/document/root.bib

@@ -0,0 +1,30 @@
+# Copyright 2020, The University of Melbourne (ABN 84 002 705 224)
+#
+# SPDX-License-Identifier: CC-BY-SA-4.0
+#
+
+@inproceedings{Murray_MBGK_12,
+    author           = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Klein, Gerwin},
+    editor           = {{Chris Hawblitzel and Dale Miller}},
+    month            = dec,
+    year             = {2012},
+    keywords         = {information flow, refinement, scheduling, state monads},
+    address          = {Kyoto, Japan},
+    title            = {Noninterference for Operating System Kernels},
+    pages            = {126--142},
+    booktitle        = {International Conference on Certified Programs and Proofs},
+    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/6004.pdf},
+    publisher        = {Springer},
+    isbn             = {978-3-642-35307-9}
+  }
+
+@INPROCEEDINGS{Goguen_Meseguer_84,
+  author={J. A. {Goguen} and J. {Meseguer}},
+  booktitle={1984 IEEE Symposium on Security and Privacy},
+  title={Unwinding and Inference Control},
+  year={1984},
+  volume={},
+  number={},
+  pages={75--87},
+  publisher = {{IEEE} Computer Society},
+}

lib/EVTutorial/document/root.tex

@@ -0,0 +1,49 @@
+%
+% Copyright 2020, The University of Melbourne (ABN 84 002 705 224)
+%
+% SPDX-License-Identifier: CC-BY-SA-4.0
+%
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% Ensure words with ligatures like 'fi' are searchable in pdf
+%   https://tex.stackexchange.com/a/57867
+\input{glyphtounicode}
+\pdfgentounicode=1
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{EquivValid Tutorial\thanks{\copyright~The University of Melbourne (ABN 84 002 705 224); licensed under Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)}}
+% Remove footnote mark for copyright notice.
+%   https://tex.stackexchange.com/a/14866
+\renewcommand\footnotemark{}
+\author{Robert Sison}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{alpha}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

lib/EquivValid.thy

@@ -267,6 +267,30 @@ lemma modify_ev2:
   apply(clarsimp simp: equiv_valid_2_def in_monad)
   using assms by auto
 
+lemma modify_ev:
+  "equiv_valid I A B
+     (\<lambda> s. \<forall> s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t))
+     (modify f)"
+  apply(clarsimp simp:equiv_valid_def2)
+  apply(rule modify_ev2)
+  by auto
+
+lemma modify_ev':
+  "equiv_valid I A B
+     (\<lambda> s. \<forall> t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t))
+     (modify f)"
+  apply(clarsimp simp:equiv_valid_def2)
+  apply(rule modify_ev2)
+  by auto
+
+lemma modify_ev'':
+  assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P t\<rbrakk> \<Longrightarrow> I (f s) (f t) \<and> B (f s) (f t)"
+  shows "equiv_valid I A B P (modify f)"
+  apply(clarsimp simp:equiv_valid_def2)
+  apply(rule modify_ev2)
+  using assms by auto
+
+
 lemma put_ev2:
   assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x'"
   shows

lib/tests.xml

@@ -20,6 +20,7 @@
         <test name="Concurrency" depends="Lib">../isabelle/bin/isabelle build -v -d .. Concurrency</test>
         <test name="CLib" depends="Lib CParser">../isabelle/bin/isabelle build -v -d .. CLib</test>
         <test name="LibTest" depends="Lib CParser Refine" cpu-timeout="1800">../isabelle/bin/isabelle build -v -d .. LibTest</test>
+        <test name="EVTutorial" depends="Lib">../isabelle/bin/isabelle build -v -d .. EVTutorial</test>
     </set>
 
 </testsuite>