diff --git a/.github/workflows/proof.yml b/.github/workflows/proof.yml
index 0b87ad548..03af34d8a 100644
--- a/.github/workflows/proof.yml
+++ b/.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
diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md
index 9781ee7cd..2368fdb09 100644
--- a/CONTRIBUTORS.md
+++ b/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
diff --git a/ROOTS b/ROOTS
index 1610af891..2a6be940a 100644
--- a/ROOTS
+++ b/ROOTS
@@ -8,4 +8,5 @@ camkes
 sys-init
 lib
 lib/Word_Lib
-lib/sep_algebra
\ No newline at end of file
+lib/sep_algebra
+lib/EVTutorial
diff --git a/lib/EVTutorial/EquivValidTutorial.thy b/lib/EVTutorial/EquivValidTutorial.thy
new file mode 100644
index 000000000..870e30fda
--- /dev/null
+++ b/lib/EVTutorial/EquivValidTutorial.thy
@@ -0,0 +1,717 @@
+(*
+ * Copyright 2020, The University of Melbourne (ABN 84 002 705 224)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *
+ * Developers of future substantial additions to this tutorial may wish to
+ * append their names to the author list in its document root.tex file.
+ *)
+
+theory EquivValidTutorial
+imports Lib.EquivValid
+begin
+
+text \<open>
+This tutorial provides a basic introduction to the seL4 verification repository's
+EquivValid library, which formalises proof machinery first
+introduced by the CPP'12 paper:
+  ``Noninterference for Operating System Kernels''
+  by Murray, Matichuk, Brassil, Gammie, and Klein \cite{Murray_MBGK_12}.
+This mostly comes in the form of worked examples.
+
+EquivValid statements are used to phrase seL4's information-flow security lemmas,
+because they can be used to assert that a function preserves (or establishes)
+``observable equivalence'' of system state, as seen by some attacker model.
+The ``Valid'' part of EquivValid is based on the fact that the Isabelle definition
+for Hoare triples in the seL4 proof base is called \<open>valid\<close>. The EquivValid statements
+\<open>equiv_valid\<close>, \<open>equiv_valid_2\<close> are therefore the ``equivalence'' versions of \<open>valid\<close>.
+In \cite{Murray_MBGK_12},
+EquivValid statements are referred to as ``ev'' or ``ev2'' statements.
+These roughly (but not exactly) correspond to \<open>equiv_valid\<close> and \<open>equiv_valid_2\<close>
+(resp.) in the Isabelle theories.
+
+This tutorial will assume that the reader knows how to use the weakest precondition tool,
+``wp'', to discharge Hoare triples. More information on this is available in the
+Lib.WPTutorial theory in the seL4 verification repo.
+\<close>
+
+
+section \<open> Preliminaries \<close>
+
+text \<open> It will be best to think of an EquivValid statement as akin to a Hoare triple.
+Recall that a Hoare triple consists of a precondition, function, and postcondition.
+This following basic example of a Hoare triple asserts that, for any \<^emph>\<open>single\<close> run
+of the function \<open>f\<close>, assuming the precondition \<open>P\<close> holds prior to that run,
+the postcondition \<open>Q\<close> will hold afterwards. \<close>
+
+term "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
+thm valid_def
+
+text \<open> Similarly to a Hoare triple, an EquivValid statement makes an assertion
+about the possible executions (or ``runs'') of some function.
+However, rather than making an assertion about single runs of the function,
+it instead makes assertions about \<^emph>\<open>relations between\<close> runs of that function.
+In this sense, EquivValid statements could be thought of as \<^emph>\<open>relational\<close> Hoare triples. \<close>
+
+text \<open> This tutorial will introduce some syntactic sugar to emphasise the similarity
+between Hoare triples and EquivValid statements.
+(Here, \<open>\<top>\<top>\<close> is an alias provided by Lib.NonDetMonad for the trivial binary predicate,
+which always returns \<open>True\<close>; similarly, there is also \<open>\<bottom>\<bottom>\<close> for \<open>False\<close>.) \<close>
+
+abbreviation
+  equiv_valid_sugar ::
+  "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s,'b) nondet_monad \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
+  ("\<lbrace>|_|, _\<rbrace>/ _ /\<lbrace>|_|\<rbrace>")
+where
+  "\<lbrace>|A|, P\<rbrace> f \<lbrace>|B|\<rbrace> \<equiv> equiv_valid \<top>\<top> A B P f"
+
+text \<open> This most basic form of an EquivValid statement asserts that,
+for any \<^emph>\<open>pair\<close> of runs of the function \<open>f\<close>,
+assuming the \<^emph>\<open>pre-equivalence\<close> \<open>A\<close> relates the initial states of the two runs
+(and the precondition \<open>P\<close> holds initially for both runs),
+the \<^emph>\<open>post-equivalence\<close> \<open>B\<close> will relate the final states of the two runs afterwards. \<close>
+
+term "\<lbrace>|A|, P\<rbrace> f \<lbrace>|B|\<rbrace>"
+term "equiv_valid \<top>\<top> A B P f"
+
+text \<open> The following Isabelle theorem in the EquivValid library gives
+a definition for \<open>equiv_valid\<close> that is closest to that of ``ev'' as presented in
+\cite{Murray_MBGK_12};
+this is what we will use to unfold \<open>equiv_valid\<close> statements in this tutorial: \<close>
+
+thm equiv_valid_def2[simplified equiv_valid_2_def]
+
+text \<open> In the seL4 EquivValid library, the \<open>equiv_valid\<close> definition also includes,
+as a convenience, an \<^emph>\<open>invariant equivalence\<close> \<open>I\<close> that it asserts as both pre- and
+post-equivalence. We will ignore this convenience for the rest of this tutorial. \<close>
+
+lemma "equiv_valid I \<top>\<top> \<top>\<top> P f = equiv_valid \<top>\<top> I I P f"
+  unfolding equiv_valid_def2 equiv_valid_2_def
+  by simp
+
+text \<open> Furthermore, the library version of \<open>equiv_valid\<close> is defined in terms of a
+version \<open>spec_equiv_valid\<close> that supports restricting the attention of the statement to
+a particular initial state. We will avoid encountering \<open>spec_equiv_valid\<close> for the rest
+of this tutorial, by unfolding \<open>equiv_valid_def2\<close> instead of \<open>equiv_valid_def\<close>. \<close>
+
+\<comment> \<open>Specialised\<close>
+thm equiv_valid_def
+    equiv_valid_def[simplified spec_equiv_valid_def equiv_valid_2_def]
+
+text \<open> Finally, the library also contains both simplified and more general forms of
+EquivValid statement; the more general forms allow proof engineers to specify the
+equivalences and functions on which they are asserted in a more fine-grained fashion
+than is allowed by \<open>equiv_valid\<close>. These will be addressed further later in this tutorial. \<close>
+
+\<comment> \<open>Simplified for A = B.\<close>
+lemma "equiv_valid_inv I A P f" unfolding equiv_valid_def2 oops
+\<comment> \<open>Generalised to allow specifying equivalence R on return values.\<close>
+lemma "equiv_valid_rv_inv I A R P f" unfolding equiv_valid_2_def oops
+\<comment> \<open>Generalised further.\<close>
+lemma "equiv_valid_rv I A B R P f" unfolding equiv_valid_2_def oops
+lemma "equiv_valid_2 I A B R P P' f f'" unfolding equiv_valid_2_def oops
+
+
+section \<open> Example setting: a room with a view \<close>
+
+text \<open> EquivValid statements assert equivalences between system states in alternative runs
+of a given program; for this tutorial we define a basic structure for the system state: \<close>
+
+record 'val Room =
+  desk :: 'val
+  window :: 'val
+  outbox :: 'val
+  inbox :: 'val
+  job :: "'val \<Rightarrow> 'val"
+
+text \<open> The state equivalences of interest will then be of the kind
+``\<open>desk\<close> has the same value in both states'', and so forth.
+We will typically use these to specify the attacker's assumed ability to make
+observations of (or otherwise know) the contents of those parts of the state. \<close>
+
+definition desk_equivalence :: "'val Room \<Rightarrow> 'val Room \<Rightarrow> bool"
+where
+  "desk_equivalence r1 r2 \<equiv> desk r1 = desk r2"
+
+definition window_equivalence :: "'val Room \<Rightarrow> 'val Room \<Rightarrow> bool"
+where
+  "window_equivalence r1 r2 \<equiv> window r1 = window r2"
+
+text \<open> We could just as well define equivalences similarly for
+\<open>inbox\<close>, \<open>outbox\<close>, or \<open>job\<close> -- we omit these here. \<close>
+
+text \<open> Furthermore, you can use the \<open>And\<close> alias provided by Lib.NonDetMonad
+to write the conjunction of two binary predicates.
+(Similarly, there is also an \<open>Or\<close> alias for disjunction.)\<close>
+
+thm bipred_conj_def bipred_disj_def
+lemma
+  "(desk_equivalence And window_equivalence) r1 r2 =
+   (desk r1 = desk r2 \<and> window r1 = window r2)"
+  unfolding bipred_conj_def desk_equivalence_def window_equivalence_def
+  by simp
+
+text \<open> In this setting, we might consider a trivial program that just returns
+the contents of \<open>desk\<close>; note, there is no difference between these two ways
+of expressing it: \<close>
+lemma "gets desk = do document \<leftarrow> gets desk; return document od"
+  by simp
+
+text \<open> Or, we might consider some programs that transfer values from one part
+of the state to another, write constants to state, execute functions
+that can themselves be found in state, or some combination of these: \<close>
+
+definition reveal_desk_to_window :: "('val Room, unit) nondet_monad"
+where
+  "reveal_desk_to_window \<equiv> modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)"
+
+definition sanitise_desk :: "('val::zero Room, unit) nondet_monad"
+where
+  "sanitise_desk \<equiv> modify (\<lambda>s. s\<lparr>desk := 0\<rparr>)"
+
+definition work_at_desk :: "('val Room, unit) nondet_monad"
+where
+  "work_at_desk \<equiv>
+     do modify (\<lambda>s. s\<lparr>desk := inbox s\<rparr>);
+        modify (\<lambda>s. s\<lparr>desk := (job s) (desk s)\<rparr>);
+        modify (\<lambda>s. s\<lparr>outbox := desk s\<rparr>)
+     od"
+
+definition work_sanitise_reveal :: "('val::zero Room, unit) nondet_monad"
+where
+  "work_sanitise_reveal \<equiv>
+     do work_at_desk;
+        sanitise_desk;
+        reveal_desk_to_window
+     od"
+
+
+section \<open> Attacker models expressible using EquivValid statements \<close>
+
+subsection \<open> An attacker with access to return values \<close>
+
+text \<open> The most basic form of \<open>equiv_valid\<close> asserts an information-flow security property
+that would be appropriate against an attacker that can see only the program's return value:
+that any two runs of this program will give the same return value.\footnote{If you think
+this doesn't sound like a very useful program, you'd be spot on: Our goal here is
+to prove that the program would be stubbornly uninformative to such an attacker.}
+
+Of course, we will find that we can't expect to prove this unless we place some
+restrictions on the runs under consideration.
+Consider the case where we are maximally permissive with the pre- and post-equivalences
+(by supplying \<open>\<top>\<top>\<close>) and precondition (by supplying \<open>\<top>\<close>): \<close>
+
+lemma gets_desk_return_leak:
+  \<comment> \<open> No restrictions on pre-equivalence, precondition, or post-equivalence. \<close>
+  "\<lbrace>|\<top>\<top>|, \<top>\<rbrace> gets desk \<lbrace>|\<top>\<top>|\<rbrace>"
+  find_theorems intro
+  \<comment> \<open> There happens to be an applicable \<open>gets\<close> rule for \<open>equiv_valid_inv\<close>. \<close>
+  thm gets_ev''
+  apply(rule gets_ev'')
+  \<comment> \<open> \<open>equiv_valid\<close> requires the return value to be the same in both runs.
+     As expected, we are stuck, as we don't know that the contents of \<open>desk\<close>
+     were initially the same for both runs. \<close>
+  nitpick
+  oops
+
+text \<open> How might we know that \<open>gets desk\<close> will return the same value for each of
+a given pair of runs?
+
+One way we might know this is if the pre-equivalence tells us that we can assume
+that \<open>desk\<close> initially has the same value in both runs.
+This might be appropriate to assume, for example:
+(1) after executing some function that equalises the value of \<open>desk\<close> between
+   all runs under consideration, or
+(2) when the attacker already knows the contents of \<open>desk\<close>.
+Note that these are just two ways of saying that we consider it to be acceptable
+for the attacker to know the initial contents of \<open>desk\<close>.
+
+We can specify this formally by setting \<open>desk_equivalence\<close> as the pre-equivalence.%
+\footnote{To avoid complicating things for now, we'll also set the post-equivalence
+to be the same as the pre-equivalence. Examples of proving \<open>equiv_valid\<close> statements
+with a different pre- and post-equivalence will be addressed later in this tutorial.}
+The resulting EquivValid statement's demand for equal return values is easily provable
+for \<open>gets desk\<close>, using the \<open>gets\<close> rule for \<open>equiv_valid\<close> we found earlier: \<close>
+
+lemma gets_desk_equiv_return:
+  \<comment> \<open> Pre-equivalence (and post-equivalence):
+      The value of \<open>desk\<close> is equal initially (and finally) for both runs. \<close>
+  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>
+     gets desk
+   \<lbrace>|desk_equivalence|\<rbrace>"
+  find_theorems intro
+  apply(rule gets_ev'')
+  unfolding desk_equivalence_def
+  by simp
+
+text \<open> Note that the \<open>equiv_valid_rv\<close> form of EquivValid allows you to customise the
+relationship demanded between return values to be something other than equality: \<close>
+lemma "\<lbrace>|\<top>\<top>|, \<top>\<rbrace> f \<lbrace>|\<top>\<top>|\<rbrace> = equiv_valid_rv \<top>\<top> \<top>\<top> \<top>\<top> (=) \<top> f"
+  by (simp add:equiv_valid_def2) \<comment> \<open> Try replacing the \<open>(=)\<close> here. \<close>
+
+
+subsection \<open> An attacker with a window into the system state \<close>
+
+text \<open> As a rule of thumb, we use an EquivValid statement's pre-equivalence to specify
+the secrecy (or initial attacker knowledge) of values in system state, and use the
+post-equivalence to specify the attacker's powers of observation.
+
+Suppose now a scenario where the desk in our room initially contains secrets,
+and we wish to prevent these secrets from affecting what is observable to an attacker
+with binoculars pointed at the window. In this case:
+\begin{enumerate}
+\item We \<^emph>\<open>do not\<close> include \<open>desk_equivalence\<close> in the pre-equivalence, as we
+      do not consider it acceptable for the attacker to know the initial contents of \<open>desk\<close>.
+
+\item Furthermore, we \<^emph>\<open>do\<close> include \<open>window_equivalence\<close> in the post-equivalence, as we
+      do consider that the attacker will be able to observe the final contents of \<open>window\<close>.
+\end{enumerate}
+
+Clearly, in this situation, using \<open>modify\<close> to transfer the contents of \<open>desk\<close>
+to \<open>window\<close> would constitute an unacceptable information leak.
+So we should be encouraged to see that the following \<open>equiv_valid\<close>
+statement is not provable: \<close>
+
+lemma reveal_desk_window_leak:
+  \<comment> \<open> Pre-equivalence and post-equivalence:
+      The value of \<open>window\<close> is equal initially and finally for both runs. \<close>
+  "\<lbrace>|window_equivalence|, \<top>\<rbrace>
+     reveal_desk_to_window
+   \<lbrace>|window_equivalence|\<rbrace>"
+  unfolding reveal_desk_to_window_def
+  \<comment> \<open> We find an applicable \<open>modify\<close> rule for \<open>equiv_valid_inv\<close>. \<close>
+  find_theorems intro
+  apply(rule modify_ev'')
+  \<comment> \<open> Applying it, we see that it demands that \<open>window_equivalence\<close> holds
+      between the final states of both runs. \<close>
+  unfolding window_equivalence_def
+  apply clarsimp
+  \<comment> \<open> We should not expect to be able to prove this, because we have
+      said nothing about the initial value of desk in these runs. \<close>
+  oops (* Try: nitpick *)
+
+text \<open> As before, however, we should expect this to hold with a pre-equivalence
+that includes \<open>desk_equivalence\<close>. \<close>
+
+lemma reveal_desk_equiv_window_equiv:
+  "\<lbrace>|desk_equivalence And window_equivalence|, \<top>\<rbrace>
+     reveal_desk_to_window
+   \<lbrace>|desk_equivalence And window_equivalence|\<rbrace>"
+  unfolding reveal_desk_to_window_def
+  apply(rule modify_ev'')
+  unfolding bipred_conj_def desk_equivalence_def window_equivalence_def
+  by clarsimp
+
+
+section \<open> The typical toolkit \<close>
+
+subsection \<open> Using and customising the \<open>wp\<close> tool's rule set \<close>
+
+text \<open> Recall the lemma we proved for \<open>gets desk\<close>: \<close>
+thm gets_desk_equiv_return
+text \<open> Instead of using any of the \<open>gets\<close> rules for \<open>equiv_valid\<close> directly, we can
+also try using the \<open>wp\<close> tool to see if it has any applicable rules in its rule set: \<close>
+thm wp_ev
+
+text \<open>Before applying \<open>wp\<close> to EquivValid statements in this fashion, we may need
+to use the rule \<open>pre_ev\<close> to weaken their precondition.
+This allows us to apply rules that are designed to be applied when the precondition
+is a schematic variable, so as to infer a weakest precondition for the statement to hold.
+It then leaves a goal for later to show that our original precondition implies
+the weaker one that was inferred.\<close>
+thm pre_ev
+\<comment> \<open> Note: \<open>pre_ev\<close> is just the standard \<open>hoare_pre\<close> + \<open>equiv_valid_guard_imp\<close> \<close>
+thm hoare_pre
+thm equiv_valid_guard_imp
+
+text \<open> Applying the \<open>wp\<close> tactic then works because the \<open>gets_ev\<close> rule happens to be
+in the \<open>wp\<close> tool's rule set: \<close>
+thm gets_ev
+
+lemma gets_desk_equiv_return_using_wp:
+  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>
+     gets desk
+   \<lbrace>|desk_equivalence|\<rbrace>"
+  \<comment> \<open> Use \<open>pre_ev\<close> to weaken the precondition of the \<open>equiv_valid\<close> statement
+       and make the \<open>wp\<close> method applicable. \<close>
+  apply(rule pre_ev)
+   apply wp
+  unfolding desk_equivalence_def
+  by simp
+
+text \<open> You can freely customise the \<open>wp\<close> rule set as needed, whether to
+add new rules, or to replace rules with ones that are more applicable
+in a given situation.
+
+For example, the \<open>modify_ev\<close> rule is not part of the default \<open>wp\<close> rule set: \<close>
+
+thm reveal_desk_equiv_window_equiv
+  modify_ev
+
+lemma reveal_desk_equiv_window_equiv_using_wp:
+  "\<lbrace>|desk_equivalence And window_equivalence|, \<top>\<rbrace>
+     reveal_desk_to_window
+   \<lbrace>|desk_equivalence And window_equivalence|\<rbrace>"
+  unfolding reveal_desk_to_window_def
+  apply(rule pre_ev)
+   apply(wp add:modify_ev)
+  unfolding bipred_conj_def desk_equivalence_def window_equivalence_def
+  by clarsimp
+
+text \<open> As another example:
+It might be the \<^emph>\<open>precondition\<close> for both runs that tells us that \<open>desk\<close> has
+a fixed initial constant value \<open>c\<close> that is common to both runs.
+(This might be the case if, even if we might normally use \<open>desk\<close> for
+secrets, we happen to have just executed a ``flush'' function that writes \<open>c\<close> to
+\<open>desk\<close> before this point in the program, for all pairs of runs we care to compare.)
+
+Here we can modify the wp rule set to invoke \<open>gets_ev''\<close> for \<open>equiv_valid\<close>,
+which is better than the default \<open>gets_ev\<close> rule for situations like this
+where we actually need to use the precondition: \<close>
+thm gets_ev''
+
+lemma example_precond_desk_return:
+  \<comment> \<open> Precondition: The value of desk is some fixed value \<open>c\<close>.
+      \<open>equiv_valid\<close> then assumes that this precondition applies to both runs. \<close>
+  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
+     gets desk
+   \<lbrace>|\<top>\<top>|\<rbrace>"
+  apply(wp del:gets_ev add:gets_ev'')
+  by force
+
+text \<open> Relying on such a precondition, a similar argument is possible
+when proving that \<open>reveal_desk_to_window\<close> preserves \<open>window_equivalence\<close>: \<close>
+thm modify_ev''
+
+lemma reveal_const_desk_preserves_window_equiv:
+  \<comment> \<open> Precondition: Desk initially has a fixed constant \<open>c\<close>.
+      \<open>equiv_valid\<close> then assumes that this precondition applies to both runs. \<close>
+  "\<lbrace>|window_equivalence|, (\<lambda>s. desk s = c)\<rbrace>
+     reveal_desk_to_window
+   \<lbrace>|window_equivalence|\<rbrace>"
+  unfolding reveal_desk_to_window_def
+  apply(wp add:modify_ev'')
+  unfolding window_equivalence_def
+  by clarsimp
+
+text \<open> Finally, new EquivValid rules that we expect to be exercised
+often can be added to the \<open>wp\<close> rule set using a declaration: \<close>
+declare modify_ev[wp]
+
+
+subsection \<open> Remainder of worked example using \<open>wp\<close> tool \<close>
+
+text \<open> Let's use all this to prove that our overarching program,
+\<open>work_sanitise_reveal\<close>, is secure against the attacker at the window
+with the binoculars (i.e. preserves \<open>window_equivalence\<close>). \<close>
+
+thm work_sanitise_reveal_def
+
+text \<open> First, we expect these two statements to be provable, because
+\<open>work_at_desk\<close> and \<open>sanitise_desk\<close> have nothing to do with the window. \<close>
+
+lemma work_at_desk_preserves_window_equiv:
+  "\<lbrace>|window_equivalence|, P\<rbrace>
+     work_at_desk
+   \<lbrace>|window_equivalence|\<rbrace>"
+  unfolding work_at_desk_def
+  apply wp \<comment> \<open> Instead of \<open>apply(wp add:modify_ev)\<close> \<close>
+  unfolding window_equivalence_def
+  by force
+
+lemma sanitise_desk_preserves_window_equiv:
+  "\<lbrace>|window_equivalence|, P\<rbrace>
+     sanitise_desk
+   \<lbrace>|window_equivalence|\<rbrace>"
+  unfolding sanitise_desk_def
+  apply(rule pre_ev)
+   apply wp \<comment> \<open> Instead of \<open>apply(wp add:modify_ev)\<close> \<close>
+  unfolding window_equivalence_def
+  by force
+
+text \<open> The consequence of all this is that \<open>work_at_desk\<close> might freely
+shuttle secrets between \<open>inbox\<close> and \<open>outbox\<close> via \<open>desk\<close>, and execute
+a secret \<open>job\<close> on them, but it does not allow any of these secrets
+to affect what is visible at \<open>window\<close>.
+
+The mere fact of \<^emph>\<open>excluding\<close> any equivalences on \<open>inbox\<close>, \<open>outbox\<close>, or
+\<open>job\<close> from the pre- and post-equivalence of these statements
+implies both:
+\begin{enumerate}
+\item We \<^emph>\<open>do not\<close> consider it acceptable for the attacker to know the
+      initial values of \<open>inbox\<close> and \<open>outbox\<close> in these locations;
+      even the \<open>job\<close> to be executed may differ between the runs.
+      All of these are therefore secrets to be protected by the property.
+
+\item We \<^emph>\<open>do\<close> consider it acceptable for \<open>inbox\<close>, \<open>outbox\<close>, and \<open>job\<close>
+      to contain secret values after the program has finished executing.
+\end{enumerate} \<close>
+
+text \<open> We will, however, need that \<open>sanitise_desk\<close> establishes the precondition
+demanded by our recently proved lemma: that \<open>desk\<close> contains a constant. \<close>
+thm reveal_const_desk_preserves_window_equiv
+
+text \<open> Note that this is a regular (non-EquivValid) Hoare triple: \<close>
+lemma sanitise_desk_sets_zero:
+  "\<lbrace>P\<rbrace> sanitise_desk \<lbrace>\<lambda>r s. desk s = 0\<rbrace>"
+  unfolding sanitise_desk_def
+  apply(rule pre_ev)
+   apply wp
+  by force
+
+text \<open> We can now use all these lemmas to have \<open>wp\<close> discharge that
+our overarching program \<open>work_sanitise_reveal\<close> preserves \<open>window_equivalence\<close>. \<close>
+
+lemma work_sanitise_reveal_preserves_window_equiv:
+  "\<lbrace>|window_equivalence|, \<top>\<rbrace>
+     work_sanitise_reveal
+   \<lbrace>|window_equivalence|\<rbrace>"
+  unfolding work_sanitise_reveal_def
+  apply(wp add:reveal_const_desk_preserves_window_equiv[where c=0]
+               sanitise_desk_preserves_window_equiv
+               sanitise_desk_sets_zero
+               work_at_desk_preserves_window_equiv)
+  by force
+
+
+section \<open> The advanced toolkit \<close>
+
+subsection \<open> More general forms of EquivValid statements \<close>
+
+text \<open> Lib.EquivValid provides rules for discharging \<open>equiv_valid_inv\<close> statements for
+the basic monad primitives \<open>return\<close> and \<open>bind\<close>, and some of the more basic functions
+like \<open>gets\<close> (already seen); potentially in a number of variants. \<close>
+
+thm return_ev
+  bind_ev
+  gets_ev gets_ev' gets_ev''
+  modify_ev modify_ev' modify_ev''
+
+text \<open> On rare occasions you may find a need to use some of the more general
+forms of EquivValid. These are all defined in terms of the most general form,
+\<open>equiv_valid_2\<close>, which allows full customisation of
+(1) return value equivalence \<open>R\<close>,
+(2) differing pre-equivalence \<open>A\<close> vs post-equivalence \<open>B\<close>, and even
+(3) differing preconditions \<open>P,P'\<close> and functions \<open>f,f'\<close> for each run.
+(In \cite{Murray_MBGK_12}, \<open>equiv_valid_2\<close> is referred to as ``ev2''.) \<close>
+
+\<comment> \<open>Generalised to allow specifying equivalence R on return values.\<close>
+lemma "equiv_valid_rv_inv I A R P f" unfolding equiv_valid_2_def oops
+\<comment> \<open>Generalised further.\<close>
+lemma "equiv_valid_rv I A B R P f" unfolding equiv_valid_2_def oops
+lemma "equiv_valid_2 I A B R P P' f f'" unfolding equiv_valid_2_def oops
+
+text \<open> If you ever have a need to unfold an \<open>equiv_valid\<close> statement to its
+\<open>equiv_valid_2\<close> form -- perhaps as part of a more involved manual proof --
+it is often better to unfold \<open>equiv_valid_def2\<close> rather than \<open>equiv_valid_def\<close>.
+
+Lib.EquivValid also provides various rules for discharging \<open>equiv_valid_2\<close>
+statements for the basic monad primitives. For example: \<close>
+
+thm return_ev2
+  equiv_valid_2_bind equiv_valid_2_bind_pre equiv_valid_2_bind_general
+  modify_ev2
+
+lemma reveal_desk_equiv_window_equiv_using_ev2:
+  "\<lbrace>|desk_equivalence And window_equivalence|, \<top>\<rbrace>
+     reveal_desk_to_window
+   \<lbrace>|desk_equivalence And window_equivalence|\<rbrace>"
+  unfolding reveal_desk_to_window_def
+  apply(clarsimp simp:equiv_valid_def2)
+  \<comment> \<open> After peeling back to \<open>equiv_valid_2\<close> form, we can use its \<open>modify\<close> rule. \<close>
+  find_theorems intro
+  apply(rule modify_ev2)
+  unfolding desk_equivalence_def window_equivalence_def
+  by simp
+
+text \<open> The basic \<open>equiv_valid\<close> form and its rule set may sometimes
+be too restrictive, due to their demand for return values to be equal.
+
+For example, if we ever needed to prove an \<open>equiv_valid\<close> statement about
+\<open>do s \<leftarrow> get; return (f s) od\<close>, we would need to unfold it to \<open>equiv_valid_2\<close> form.
+This is because \<open>equiv_valid\<close> and its bind rule \<open>bind_ev_pre\<close> will both demand
+that the return value of \<open>get\<close> (the entire state) be the same for both runs;
+however, we might only need (or know) the parts of the state inspected
+by the function \<open>f\<close> to be the same. Say \<open>f\<close> was \<open>desk\<close>: \<close>
+
+thm bind_ev_pre
+    equiv_valid_def2[simplified equiv_valid_2_def]
+
+lemma pitfall1_using_bind_ev:
+  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
+     do
+       s \<leftarrow> get;
+       return (desk s)
+     od
+   \<lbrace>|\<top>\<top>|\<rbrace>"
+  \<comment> \<open> Using the bind rule for \<open>equiv_valid\<close> splits the goal into
+      two \<open>equiv_valid\<close> statements, one for each of \<open>get\<close> and \<open>return\<close>.
+      It will ask us to prove them in reverse order. \<close>
+  apply(rule bind_ev_pre)
+     \<comment> \<open> The \<open>wp\<close> tool discharges the \<open>return (desk s)\<close> part trivially: \<close>
+     apply wp
+    \<comment> \<open> But the return value of \<open>get\<close> is the entire state: \<close>
+    apply(clarsimp simp:equiv_valid_def2 equiv_valid_2_def)
+    apply(clarsimp simp add:get_def)
+    \<comment> \<open> This causes us to get stuck, because we have no idea whether the state
+        is equivalent for parts of the room other than the desk. \<close>
+    oops
+
+text \<open> Therefore we need to use \<open>equiv_valid_2\<close> and its bind rule \<open>equiv_valid_2_bind_pre\<close>;
+these will allow us to specify the equivalence \<open>R\<close> to be asserted between
+the return values of the \<open>get\<close>. \<close>
+
+thm equiv_valid_2_bind_pre
+  equiv_valid_2_def
+
+text \<open> Another anti-pattern to avoid when applying the bind rules directly is leaving
+intermediate preconditions unspecified; the automation is liable to guess \<open>False\<close>,
+which will later be unprovable.
+
+Here, the \<open>force\<close> tactic correctly infers that \<open>desk_equivalence\<close> is the equivalence \<open>R\<close>
+that we need between the return values from \<open>get\<close>.
+However, it guesses an incorrect postcondition: \<close>
+
+lemma pitfall2_using_bind_ev2:
+  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
+     do
+       s \<leftarrow> get;
+       return (desk s)
+     od
+   \<lbrace>|\<top>\<top>|\<rbrace>"
+  \<comment> \<open> First we need to peel it back to \<open>equiv_valid_2\<close> form, so we can apply its bind rule. \<close>
+  apply(clarsimp simp:equiv_valid_def2)
+  apply(rule equiv_valid_2_bind_pre)
+       \<comment> \<open> Here \<open>wp\<close> infers correctly that the equivalence between the
+          intermediate return values needs to be \<open>\<lambda>rv rv'. desk rv = desk rv'\<close>,
+          i.e. that \<open>desk\<close> has the same value in the state returned by \<open>get\<close> in both runs. \<close>
+       apply(wp add:return_ev2)
+      apply(clarsimp simp:equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)
+      \<comment> \<open> The \<open>force\<close> tactic just guesses \<open>False\<close> for the postcondition for both steps. \<close>
+      apply(force simp add:get_def)
+     \<comment> \<open> As these next two goals are Hoare triples, we use the \<open>wp\<close> tool, as usual for
+         Hoare triples in the seL4 proof base. See Lib.WPTutorial for more information. \<close>
+     apply wp
+    apply wp
+   \<comment> \<open> Now we are stuck because \<open>force\<close> guessed \<open>False\<close> as a premise
+      to discharge the goal earlier, giving us an unsatisfiable goal here. \<close>
+   oops
+
+text \<open> We can avoid this by giving \<open>equiv_valid_2\<close>'s bind rule a little more information. \<close>
+
+lemma precond_get_return_desk:
+  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
+     do
+       s \<leftarrow> get;
+       return (desk s)
+     od
+   \<lbrace>|\<top>\<top>|\<rbrace>"
+  apply(clarsimp simp:equiv_valid_def2)
+  \<comment> \<open> We want to use the fact that \<open>desk\<close> contains \<open>c\<close> initially for both runs.
+    So we give it here. \<close>
+  apply(rule_tac P="(\<lambda>s. desk s = c)" and P'="(\<lambda>s. desk s = c)" in equiv_valid_2_bind_pre)
+       apply(wp add:return_ev2)
+      apply(clarsimp simp:equiv_valid_def2 equiv_valid_2_def)
+      \<comment> \<open> No need to guess anything. \<close>
+      apply(force simp add:get_def)
+     \<comment> \<open> Use \<open>wp\<close> tactic to discharge the two Hoare triples; see Lib.WPTutorial for more info. \<close>
+     apply wp
+    apply wp
+   apply force
+  apply force
+  done
+
+subsection \<open> A note on what is currently available and why \<close>
+
+text \<open> As noted in \cite{Murray_MBGK_12}, the machinery developed of this kind
+(available in Lib.EquivValid's default \<open>wp\<close> rule set) is mostly geared
+towards \<open>equiv_valid_inv\<close>; this is an abbrevation for the simplified case of
+\<open>equiv_valid\<close> where the post-equivalence is the same as the pre-equivalence: \<close>
+
+lemma "equiv_valid_inv I A P f" unfolding equiv_valid_def2 equiv_valid_2_def oops
+
+text \<open> The reason for this is that the seL4 infoflow proofs take the approach of defining an
+\emph{unwinding} relation \cite{Goguen_Meseguer_84}: an equivalence relation
+flexible enough to describe what we think ought to continue to look the same between
+all possible pairs of executions as seen by a given attacker model.%
+\footnote{If every pair of executions being compared is like a wound-up rope ladder thrown
+over the side of a ship, then the rungs of those ladders would be the unwinding relation.}
+
+However, the EquivValid library merely provides a way to reason about equivalences,
+so it is not prescriptive about taking this approach.
+
+Furthermore, the overall unwinding relation for a system may be composed from a number of
+equivalences, which may each hold or not at different times, in a manner that depends on
+where we are in the system.%
+\footnote{This is like saying that the first six rungs of the ladder may be made of wood,
+but the next seven rungs may be made of aluminium, and so on.}
+As it happens, this is the case for seL4's unwinding relation, but the number of ev sub-lemmas
+needing to be proved for differing pre-/post-equivalences is rather limited at current time of
+writing, hence the lack of machinery.%
+\footnote{This may perhaps be the lemma covering the step between the sixth and seventh
+rung of our imaginary wood-and-aluminium--runged ladder.} \<close>
+
+
+subsection \<open> Proving EquivValid with differing pre- and post-equivalences \<close>
+
+text \<open> So far we have only proved \<open>equiv_valid\<close> statements
+whose pre-equivalence is the same as their post-equivalence.
+
+We will now attempt to prove an \<open>equiv_valid\<close> statement where they differ.
+
+This allows us to say, for example, that although usually we use the desk
+for secrets:
+(1) at this point in the program we happened to make sure that
+    desk contains the same value for any two runs we care to check, and
+(2) we don't care if desk contains the same value for both runs afterwards. \<close>
+
+lemma reveal_desk_equiv_to_window_equiv:
+  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>  \<comment> \<open> Pre-equivalence: The value of \<open>desk\<close> is
+                                 the same initially in both runs. \<close>
+     reveal_desk_to_window
+   \<lbrace>|window_equivalence|\<rbrace>" \<comment> \<open> Post-equivalence: The value of \<open>window\<close> is required to be
+                                the same at the end of both runs; no longer so for \<open>desk\<close>. \<close>
+  unfolding reveal_desk_to_window_def
+  apply(rule modify_ev'')
+  unfolding window_equivalence_def desk_equivalence_def
+  by simp
+
+text \<open> This is handy, because we might subsequently copy secrets into the desk,
+in which case \<open>desk_equivalence\<close> would no longer hold in the post-equivalence.
+
+As before, the mere fact of \<^emph>\<open>excluding\<close> any equivalence on \<open>inbox\<close> from the
+pre-equivalence implies we \<^emph>\<open>do not\<close> consider it acceptable for the attacker
+to know \<open>inbox\<close>'s initial value; it is therefore a secret to be protected by this property.
+Conversely, the absence of \<open>desk_equivalence\<close> from the post-equivalence implies
+that we \<^emph>\<open>do\<close> consider it acceptable for the desk to contain secrets after the program
+has finished executing.
+
+Consequently, this \<open>equiv_valid\<close> statement is provable: \<close>
+
+lemma desk_equiv_no_longer_needed:
+  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>
+       do reveal_desk_to_window;
+          modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>)
+       od
+   \<lbrace>|window_equivalence|\<rbrace>"
+  \<comment> \<open> Use \<open>pre_ev\<close> to weaken the precondition of the \<open>equiv_valid\<close> statement. \<close>
+  apply(rule pre_ev)
+   \<comment> \<open> Use \<open>bind_ev_general\<close> to split the goal into \<open>equiv_valid\<close> statements for
+       each of the two \<open>modify\<close> commands. It will ask us to prove them in reverse order. \<close>
+   apply(rule bind_ev_general)
+     \<comment> \<open> Prove \<open>equiv_valid\<close> for \<open>desk := inbox\<close> manually. \<close>
+     apply clarsimp
+     apply(rule modify_ev'')
+     \<comment> \<open> The \<open>force\<close> tactic has enough information here to figure out that
+         the intermediate equivalence \<open>B\<close> needs to be \<open>window_equivalence\<close>. \<close>
+     apply(force simp:window_equivalence_def desk_equivalence_def)
+    \<comment> \<open> This happens to be the post-equivalence for the \<open>equiv_valid\<close> lemma
+        we just proved for \<open>window := desk\<close>, so we can reuse that lemma here. \<close>
+    using reveal_desk_equiv_to_window_equiv
+    unfolding window_equivalence_def
+    apply force
+   apply wp
+  apply force
+  done
+
+end
diff --git a/lib/EVTutorial/ROOT b/lib/EVTutorial/ROOT
new file mode 100644
index 000000000..e3fdbe838
--- /dev/null
+++ b/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"
diff --git a/lib/EVTutorial/document/root.bib b/lib/EVTutorial/document/root.bib
new file mode 100644
index 000000000..2969ae754
--- /dev/null
+++ b/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},
+}
diff --git a/lib/EVTutorial/document/root.tex b/lib/EVTutorial/document/root.tex
new file mode 100644
index 000000000..534fd2ee9
--- /dev/null
+++ b/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:
diff --git a/lib/EquivValid.thy b/lib/EquivValid.thy
index 939baeb69..27bb032b6 100644
--- a/lib/EquivValid.thy
+++ b/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
diff --git a/lib/tests.xml b/lib/tests.xml
index 6c9612b24..4e2715818 100644
--- a/lib/tests.xml
+++ b/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>