From 9718f1bda268f09380e8aaefbb3109cf843bcfda Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
Date: Thu, 4 Feb 2016 00:17:47 -0800
Subject: [PATCH] arch_split: progress on namespacing abstract spec

---
 lib/Qualify.thy                               |  188 +++
 lib/Unqualify.thy                             |  150 +++
 .../ARM/ArchInvariants_AI.thy                 |  867 ++++++++++++++
 proof/invariant-abstract/ARM/ArchTypes_AI.thy |  654 +++++++++++
 proof/invariant-abstract/Invariants_AI.thy    | 1012 +----------------
 spec/abstract/ARM/ArchCSpace_A.thy            |    6 +-
 spec/abstract/ARM/ArchInvocation_A.thy        |    4 +
 spec/abstract/ARM/ArchRetype_A.thy            |    4 +
 spec/abstract/ARM/ArchVMRights_A.thy          |    5 +-
 spec/abstract/ARM/ArchVSpaceAcc_A.thy         |    6 +-
 spec/abstract/ARM/ArchVSpace_A.thy            |   14 +-
 spec/abstract/ARM/Arch_A.thy                  |    4 +
 spec/abstract/ARM/Arch_Structs_A.thy          |   29 +
 spec/abstract/ARM/Init_A.thy                  |    4 +
 spec/abstract/ARM/Machine_A.thy               |   30 +
 spec/abstract/CSpace_A.thy                    |   31 +-
 spec/abstract/Interrupt_A.thy                 |    3 +
 spec/abstract/InvocationLabels_A.thy          |    6 +
 spec/abstract/Invocations_A.thy               |    9 +-
 spec/abstract/Ipc_A.thy                       |    4 +
 spec/abstract/MiscMachine_A.thy               |   61 +-
 spec/abstract/Retype_A.thy                    |    6 +
 spec/abstract/Schedule_A.thy                  |    4 +
 spec/abstract/Structures_A.thy                |   24 +-
 spec/abstract/TcbAcc_A.thy                    |    3 +
 spec/abstract/Tcb_A.thy                       |    3 +
 spec/design/ARM/ArchInvocationLabels_H.thy    |    6 +-
 spec/design/ARM/ArchLabelFuns_H.thy           |    4 +-
 spec/design/Event_H.thy                       |    2 +-
 spec/design/InvocationLabels_H.thy            |    6 +-
 spec/machine/ARM/MachineOps.thy               |   77 +-
 spec/machine/ARM/MachineTypes.thy             |   17 +-
 spec/machine/ARM/Platform.thy                 |    5 +
 spec/machine/ARM/Setup_Locale.thy             |   18 +
 spec/machine/MachineExports.thy               |   40 +
 spec/machine/MachineMonad.thy                 |   93 ++
 36 files changed, 2326 insertions(+), 1073 deletions(-)
 create mode 100644 lib/Qualify.thy
 create mode 100644 lib/Unqualify.thy
 create mode 100644 proof/invariant-abstract/ARM/ArchInvariants_AI.thy
 create mode 100644 proof/invariant-abstract/ARM/ArchTypes_AI.thy
 create mode 100644 spec/machine/ARM/Setup_Locale.thy
 create mode 100644 spec/machine/MachineExports.thy
 create mode 100644 spec/machine/MachineMonad.thy

diff --git a/lib/Qualify.thy b/lib/Qualify.thy
new file mode 100644
index 000000000..46bd26272
--- /dev/null
+++ b/lib/Qualify.thy
@@ -0,0 +1,188 @@
+(*
+  Post-hoc qualification of global constants, facts and types using name space aliasing.
+  Can be used to add mandatory qualification to otherwise non-localised commands (i.e. "record",
+  "instantiation").
+
+  This is a hack that should be replaced with proper "context begin ... end" blocks when
+  commands are appropriately localized.
+*)
+
+theory Qualify
+imports Main
+keywords "qualify" :: thy_decl and "end_qualify" :: thy_decl
+begin
+ML \<open>
+
+structure Data = Theory_Data
+  (
+    type T = (theory * string) option * 
+             ((string * 
+              ((binding Symtab.table) * (* facts *)
+               (binding Symtab.table) * (* consts *)
+               (binding Symtab.table) (* types *))) list);
+    val empty = (NONE, []);
+    val extend = I;
+    fun merge (((_, tabs), (_, tabs')) : T * T) = 
+      (NONE, AList.join (op =) 
+      (fn _ => fn ((facts, consts, types), (facts', consts', types')) =>
+        (Symtab.merge (op =) (facts, facts'), 
+         Symtab.merge (op =) (consts, consts'),
+         Symtab.merge (op =) (types, types')))
+      (tabs, tabs'));
+  );
+
+fun get_qualify thy = fst (Data.get thy);
+
+fun get_tabs_of thy str = 
+  the_default (Symtab.empty, Symtab.empty, Symtab.empty) (AList.lookup (op =) (snd (Data.get thy)) str);
+
+fun get_facts_of thy str = #1 (get_tabs_of thy str);
+
+fun get_consts_of thy str = #2 (get_tabs_of thy str);
+
+fun get_types_of thy str = #3 (get_tabs_of thy str);
+
+fun map_tabs_of str f thy = 
+  Data.map (apsnd (AList.map_default (op =) (str, (Symtab.empty, Symtab.empty, Symtab.empty)) f)) thy;
+
+fun map_facts_of str f thy = map_tabs_of str (@{apply 3(1)} f) thy;
+
+fun map_consts_of str f thy = map_tabs_of str (@{apply 3(2)} f) thy;
+
+fun map_types_of str f thy = map_tabs_of str (@{apply 3(3)} f) thy;
+
+fun make_bind nm = 
+  let
+    val base = Long_Name.explode nm |> tl |> rev |> tl |> rev;
+  in fold (Binding.qualify false) base (Binding.make (Long_Name.base_name nm, Position.none)) end;
+
+fun get_new_facts old_thy facts = 
+  Facts.dest_static false [Global_Theory.facts_of old_thy] facts
+  |> map (fn (nm, _) => `make_bind nm);
+
+fun get_new_consts old_thy consts =
+  let
+    val new_consts = #constants (Consts.dest consts)
+    |> map fst;
+    
+    val consts = 
+      filter (fn nm => not (can (Consts.the_const (Sign.consts_of old_thy)) nm) andalso
+                       can (Consts.the_const consts) nm) new_consts
+      |> map (fn nm => `make_bind nm);
+
+  in consts end;
+
+fun get_new_types old_thy types =
+  let
+    val new_types = #types (Type.rep_tsig types);
+
+    val old_types = #types (Type.rep_tsig (Sign.tsig_of old_thy));
+   
+    val types = (new_types
+      |> Name_Space.fold_table (fn (nm, _) => 
+           not (Name_Space.defined old_types nm) ? cons nm)) []
+      |> map (fn nm => `make_bind nm);
+  in types end;
+
+fun add_qualified qual nm =
+  let
+    val nm' = Long_Name.explode nm |> rev |> tl |> hd;
+  in if qual = nm' then cons nm else I end
+  handle List.Empty => I
+
+fun make_bind_local nm = 
+  let
+    val base = Long_Name.explode nm |> tl |> tl |> rev |> tl |> rev;
+  in fold (Binding.qualify true) base (Binding.make (Long_Name.base_name nm, Position.none)) end;
+
+fun set_global_qualify str thy = 
+  let
+    val _ = Locale.check thy (str, Position.none)
+    val _ = case get_qualify thy of SOME _ => error "Already in a qualify block!" | NONE => ();
+
+    val facts = 
+      Facts.fold_static (fn (nm, _) => add_qualified str nm) (Global_Theory.facts_of thy) []
+      |> map (`make_bind_local)
+
+    val consts = fold (fn (nm, _) => add_qualified str nm) (#constants (Consts.dest (Sign.consts_of thy))) []
+      |> map (`make_bind_local)
+
+    val types = 
+      Name_Space.fold_table (fn (nm, _) => add_qualified str nm) (#types (Type.rep_tsig (Sign.tsig_of thy))) []
+      |> map (`make_bind_local)
+
+
+    val thy' = thy
+     |> map_facts_of str (fold (fn (b, nm) => (Symtab.update (nm, b))) facts)
+     |> map_consts_of str (fold (fn (b, nm) => (Symtab.update (nm, b))) consts)
+     |> map_types_of str (fold (fn (b, nm) => (Symtab.update (nm, b))) types)
+
+    val thy'' = thy'
+    |> Data.map (apfst (K (SOME (thy,str))))
+    |> fold (fn (nm, b) => Global_Theory.alias_fact b nm) (Symtab.dest (get_facts_of thy' str))
+    |> fold (fn (nm, b) => Sign.const_alias b nm) (Symtab.dest (get_consts_of thy' str))
+    |> fold (fn (nm, b) => Sign.type_alias b nm) (Symtab.dest (get_types_of thy' str))
+
+  in thy'' end
+
+val _ =
+  Outer_Syntax.command @{command_keyword qualify} "begin global qualification"
+    (Parse.name >> 
+      (fn str => Toplevel.theory (set_global_qualify str)));
+
+fun syntax_alias global_alias local_alias b name =
+  Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
+    let val b' = Morphism.binding phi b
+    in Context.mapping (global_alias b' name) (local_alias b' name) end);
+
+val fact_alias = syntax_alias Global_Theory.alias_fact Proof_Context.fact_alias;
+val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
+val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
+
+
+
+fun end_global_qualify thy =
+  let
+    val (old_thy, nm) = 
+      case get_qualify thy of
+        SOME x => x 
+      | NONE => error "Not in a global qualify"
+
+    val facts = get_new_facts old_thy (Global_Theory.facts_of thy);
+
+    val consts = get_new_consts old_thy (Sign.consts_of thy);
+
+    val types = get_new_types old_thy (Sign.tsig_of thy);
+
+
+    val thy' = thy
+     |> map_facts_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) facts)
+     |> map_consts_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) consts)
+     |> map_types_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) types)
+     |> (fn thy => fold (Global_Theory.hide_fact true o fst) (Symtab.dest (get_facts_of thy nm)) thy)
+     |> (fn thy => fold (Sign.hide_const true o fst) (Symtab.dest (get_consts_of thy nm)) thy)
+     |> (fn thy => fold (Sign.hide_type true o fst) (Symtab.dest (get_types_of thy nm)) thy)
+     |> Data.map (apfst (K NONE))
+
+    val lthy = Named_Target.begin (nm, Position.none) thy';
+
+    val lthy' = lthy
+      |> fold (uncurry fact_alias o swap) (Symtab.dest (get_facts_of thy' nm))
+      |> fold (uncurry const_alias o swap) (Symtab.dest (get_consts_of thy' nm))
+      |> fold (uncurry type_alias o swap) (Symtab.dest (get_types_of thy' nm));
+
+  in Local_Theory.exit_global lthy' end
+
+val _ =
+  Outer_Syntax.command @{command_keyword end_qualify} "end global qualification"
+    (Scan.succeed
+      (Toplevel.theory end_global_qualify));
+
+
+\<close>
+
+setup \<open>Theory.at_end 
+  (fn thy => case get_qualify thy of SOME (_, nm) => 
+    SOME (end_global_qualify thy) | NONE => NONE)\<close>
+
+end
\ No newline at end of file
diff --git a/lib/Unqualify.thy b/lib/Unqualify.thy
new file mode 100644
index 000000000..a6b8a8b44
--- /dev/null
+++ b/lib/Unqualify.thy
@@ -0,0 +1,150 @@
+(*
+  Drop mandatory qualifiers from internal locale facts, constants and types
+  Optionally add a different qualifier
+*)
+
+theory Unqualify
+imports Main
+keywords "unqualify_facts" :: thy_decl and "unqualify_consts" :: thy_decl and "unqualify_types" :: thy_decl
+begin
+
+ML \<open>
+
+local
+
+fun map_option _ NONE = NONE
+  | map_option f (SOME x) = SOME (f x)
+
+fun make_binding_raw (nm, pos) =
+  let
+    val path = Long_Name.explode nm |> rev;
+    val b' = fold (Binding.qualify true) (tl path) (Binding.make (hd path, pos));
+  in b' end
+
+fun make_binding b =
+  let
+    val nm = Binding.name_of b;
+    val pos = Binding.pos_of b;
+  in make_binding_raw (nm, pos) end
+
+val parse_opt_target = Parse.opt_target >> 
+  (map_option (apfst (fn raw_nm =>
+          case try (unprefix "$") raw_nm of SOME nm' => getenv_strict nm' | NONE => raw_nm)))
+
+val unqualify_parse = parse_opt_target -- Scan.option (Args.parens Parse.name) -- Scan.repeat1 Parse.binding
+
+in
+
+val _ =
+  Outer_Syntax.command @{command_keyword unqualify_facts} "unqualify facts"
+    (unqualify_parse >> (fn ((target,qual),bs) =>
+      Toplevel.local_theory NONE target (fn lthy =>
+      let                            
+        val facts = Proof_Context.facts_of lthy;
+
+        fun retrieve b = Facts.retrieve (Context.Proof lthy) facts (Binding.name_of b, Binding.pos_of b);
+
+
+        val thmss = map (`retrieve) bs
+          |> map (fn ({thms, ...}, b) => (make_binding b, thms));
+
+        val lthy' = Local_Theory.background_theory (fn thy =>
+          let
+            val naming = the_default I (map_option Name_Space.mandatory_path qual) Name_Space.global_naming;
+            val thy' = Context.theory_map (Name_Space.map_naming (K naming)) thy;
+            val export = Morphism.fact (Local_Theory.standard_morphism lthy (Proof_Context.init_global thy));
+          in
+            fold (fn (b, thms) => Global_Theory.store_thms (b,export thms) #> snd) thmss thy'
+          end) lthy
+
+       in
+       lthy'
+       end)))
+
+val k = Parse.for_fixes
+
+
+val _ =
+  Outer_Syntax.command @{command_keyword unqualify_consts} "unqualify consts"
+    (parse_opt_target -- Scan.option (Args.parens Parse.name) -- 
+      Scan.repeat1 (Parse.position Parse.term) >> (fn ((target,qual),bs) =>
+      Toplevel.local_theory NONE target (fn lthy =>
+      let
+
+        val ts = map (`(Syntax.parse_term lthy o fst)) bs;
+
+        fun get_const 
+            (( t as Const ("_type_constraint_", _) $
+                (Const ("_type_constraint_", _) $
+                  Const (nm, _))), (_, pos)) = ((nm, pos), t)
+           | get_const (t as (Const ("_type_constraint_", _) $
+                  Const (nm, _)), (_, pos)) = ((nm, pos), t)
+           | get_const (t, (_,pos)) = error ("Not a constant or abbreviation: " ^ Syntax.string_of_term lthy t ^ Position.here pos)
+
+        val ts' = map (apsnd (Syntax.check_term lthy) o apfst make_binding_raw o get_const) ts;
+
+        val lthy' = Local_Theory.background_theory (fn thy =>
+          let
+            val naming = the_default I (map_option Name_Space.mandatory_path qual) Name_Space.global_naming;
+            val thy' = Context.theory_map (Name_Space.map_naming (K naming)) thy;
+            val export = Morphism.term (Local_Theory.standard_morphism lthy (Proof_Context.init_global thy));
+  
+          in
+            fold (fn (b, t) =>
+              let
+                val b' = make_binding b;
+                val nm = Binding.name_of b';
+              in
+               Sign.add_abbrev nm (b', export t) #> snd
+              end) ts' thy'
+          end) lthy
+
+       in
+       lthy'
+       end)))
+
+
+val _ =
+  Outer_Syntax.command @{command_keyword unqualify_types} "unqualify types"
+    (parse_opt_target -- Scan.option (Args.parens Parse.name) -- 
+      Scan.repeat1 (Parse.position Parse.typ) >> (fn ((target,qual),bs) =>
+      Toplevel.local_theory NONE target (fn lthy =>
+      let
+        
+        fun err (T, pos) = 
+          error ("Not a defined type or type synonym: " ^ Syntax.string_of_typ lthy T ^ Position.here pos)
+
+   
+        val Ts = map (`(Syntax.parse_typ lthy o fst)) bs;
+
+        fun get_type (T, (_, pos)) = case try dest_Type T of
+        SOME (nm, Ts) => (if can dest_funT T then err (T,pos) else ((nm, pos), (T,Ts)))
+        | NONE => err (T,pos)
+
+        fun check_Ts (T,Ts) = (Syntax.check_typ lthy T, 
+          fold Term.add_tfree_namesT Ts [])
+
+        val Ts' = map (apsnd check_Ts o apfst make_binding_raw o get_type) Ts;
+
+        val lthy' = Local_Theory.background_theory (fn thy =>
+          let
+            val naming = the_default I (map_option Name_Space.mandatory_path qual) Name_Space.global_naming;
+            val thy' = Context.theory_map (Name_Space.map_naming (K naming)) thy;
+          in
+            fold (fn (b, (T,frees)) =>
+              let
+                val b' = make_binding b;
+              in
+               Sign.add_type_abbrev lthy (b',frees, T)
+              end) Ts' thy'
+          end) lthy
+
+       in
+       lthy'
+       end)))
+
+end
+
+\<close>
+
+end
\ No newline at end of file
diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy
new file mode 100644
index 000000000..281344a12
--- /dev/null
+++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy
@@ -0,0 +1,867 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory ArchInvariants_AI
+imports "../LevityCatch_AI"
+begin
+
+section "Move this up"
+
+qualify ARM
+
+-- ---------------------------------------------------------------------------
+section "Things to Move Up"
+
+(* FIXME: move to spec level *)
+(* global data and code of the kernel, not covered by any cap *)
+axiomatization
+  kernel_data_refs :: "word32 set"
+
+end_qualify
+
+-- ---------------------------------------------------------------------------
+section "ARM-specific invariant definitions"
+
+context ARM begin
+
+lemmas aa_type_simps =
+  aa_type_def[split_simps arch_kernel_obj.split]
+
+
+definition
+  aobj_at :: "(arch_kernel_obj \<Rightarrow> bool) \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "aobj_at P ref s \<equiv> \<exists>ko. kheap s ref = Some (ArchObj ko) \<and> P ko"
+
+abbreviation
+  "ako_at k \<equiv> aobj_at (op = k)"
+
+definition
+  "vmsz_aligned ref sz \<equiv> is_aligned ref (pageBitsForSize sz)"
+
+definition
+  "wellformed_mapdata sz \<equiv>
+   \<lambda>(asid, vref). 0 < asid \<and> asid \<le> 2^asid_bits - 1
+                \<and> vmsz_aligned vref sz \<and> vref < kernel_base"
+
+definition
+  wellformed_acap :: "arch_cap \<Rightarrow> bool"
+where
+  "wellformed_acap ac \<equiv>
+   case ac of
+     Arch_Structs_A.ASIDPoolCap r as
+       \<Rightarrow> is_aligned as asid_low_bits \<and> as \<le> 2^asid_bits - 1
+   | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> rghts \<in> valid_vm_rights \<and>
+     case_option True (wellformed_mapdata sz) mapdata
+   | Arch_Structs_A.PageTableCap r (Some mapdata) \<Rightarrow>
+     wellformed_mapdata ARMSection mapdata
+   | Arch_Structs_A.PageDirectoryCap r (Some asid) \<Rightarrow>
+     0 < asid \<and> asid \<le> 2^asid_bits - 1
+   | _ \<Rightarrow> True"
+
+lemmas wellformed_acap_simps =
+  wellformed_mapdata_def wellformed_acap_def[split_simps arch_cap.split]
+
+abbreviation
+  "atyp_at T \<equiv> aobj_at (\<lambda>ob. aa_type ob = T)"
+
+(* this time with typ_at. might lead to confusion, but this is how
+   the rest should have been defined.. *)
+abbreviation
+  "asid_pool_at \<equiv> atyp_at AASIDPool"
+abbreviation
+  "page_table_at \<equiv> atyp_at APageTable"
+abbreviation
+  "page_directory_at \<equiv> atyp_at APageDirectory"
+
+definition
+  "pde_at p \<equiv> page_directory_at (p && ~~ mask pd_bits)
+                  and K (is_aligned p 2)"
+definition
+  "pte_at p \<equiv> page_table_at (p && ~~ mask pt_bits)
+                  and K (is_aligned p 2)"
+
+definition
+  valid_arch_cap_ref :: "arch_cap \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_cap_ref ac s \<equiv> (case ac of
+    Arch_Structs_A.ASIDPoolCap r as \<Rightarrow> atyp_at AASIDPool r s
+  | Arch_Structs_A.ASIDControlCap \<Rightarrow> True
+  | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> atyp_at (AIntData sz) r s
+  | Arch_Structs_A.PageTableCap r mapdata \<Rightarrow> atyp_at APageTable r s
+  | Arch_Structs_A.PageDirectoryCap r mapdata\<Rightarrow> atyp_at APageDirectory r s)"
+
+lemmas valid_arch_cap_ref_simps =
+  valid_arch_cap_ref_def[split_simps arch_cap.split]
+
+definition
+  valid_arch_cap :: "arch_cap \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_cap ac s \<equiv> (case ac of
+    Arch_Structs_A.ASIDPoolCap r as \<Rightarrow>
+         atyp_at AASIDPool r s \<and> is_aligned as asid_low_bits
+           \<and> as \<le> 2^asid_bits - 1
+  | Arch_Structs_A.ASIDControlCap \<Rightarrow> True
+  | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow>
+    atyp_at (AIntData sz) r s \<and> rghts \<in> valid_vm_rights \<and>
+    (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2^asid_bits - 1
+                                             \<and> vmsz_aligned ref sz \<and> ref < kernel_base)
+  | Arch_Structs_A.PageTableCap r mapdata \<Rightarrow>
+    atyp_at APageTable r s \<and>
+    (case mapdata of None \<Rightarrow> True
+       | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ asid_bits - 1
+                                \<and> vref < kernel_base
+                                \<and> is_aligned vref (pageBitsForSize ARMSection))
+  | Arch_Structs_A.PageDirectoryCap r mapdata \<Rightarrow>
+    atyp_at APageDirectory r s \<and>
+    case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata)"
+
+lemmas valid_arch_cap_simps =
+  valid_arch_cap_def[split_simps arch_cap.split]
+
+primrec
+  acap_class :: "arch_cap \<Rightarrow> capclass"
+where
+  "acap_class (arch_cap.ASIDPoolCap x y)      = PhysicalClass"
+| "acap_class (arch_cap.ASIDControlCap)       = ASIDMasterClass"
+| "acap_class (arch_cap.PageCap x y sz z)     = PhysicalClass"
+| "acap_class (arch_cap.PageTableCap x y)     = PhysicalClass"
+| "acap_class (arch_cap.PageDirectoryCap x y) = PhysicalClass"
+
+definition
+  valid_ipc_buffer_cap :: "cap \<Rightarrow> word32 \<Rightarrow> bool"
+where
+  "valid_ipc_buffer_cap c bufptr \<equiv>
+         case c of
+              cap.ArchObjectCap (arch_cap.PageCap ref rghts sz mapdata) \<Rightarrow>
+                   is_aligned bufptr msg_align_bits
+
+            | _ \<Rightarrow> True"
+
+primrec
+  valid_pte :: "Arch_Structs_A.pte \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_pte (Arch_Structs_A.InvalidPTE) = \<top>"
+| "valid_pte (Arch_Structs_A.LargePagePTE ptr x y) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMLargePage) (Platform.ptrFromPAddr ptr) s)"
+| "valid_pte (Arch_Structs_A.SmallPagePTE ptr x y) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMSmallPage) (Platform.ptrFromPAddr ptr) s)"
+
+primrec
+  valid_pde :: "Arch_Structs_A.pde \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_pde (Arch_Structs_A.InvalidPDE) = \<top>"
+| "valid_pde (Arch_Structs_A.SectionPDE ptr x y z) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMSection) (Platform.ptrFromPAddr ptr) s)"
+| "valid_pde (Arch_Structs_A.SuperSectionPDE ptr x z) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMSuperSection)
+               (Platform.ptrFromPAddr ptr) s)"
+| "valid_pde (Arch_Structs_A.PageTablePDE ptr x z) =
+   (atyp_at APageTable (Platform.ptrFromPAddr ptr))"
+
+
+definition
+  kernel_mapping_slots :: "12 word set" where
+ "kernel_mapping_slots \<equiv> {x. x \<ge> ucast (kernel_base >> 20)}"
+
+primrec
+  valid_arch_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_obj (Arch_Structs_A.ASIDPool pool) =
+   (\<lambda>s. \<forall>x \<in> ran pool. atyp_at  APageDirectory x s)"
+| "valid_arch_obj (Arch_Structs_A.PageDirectory pd) =
+   (\<lambda>s. \<forall>x \<in> -kernel_mapping_slots. valid_pde (pd x) s)"
+| "valid_arch_obj (Arch_Structs_A.PageTable pt) = (\<lambda>s. \<forall>x. valid_pte (pt x) s)"
+| "valid_arch_obj (DataPage sz) = \<top>"
+
+definition
+  wellformed_pte :: "Arch_Structs_A.pte \<Rightarrow> bool"
+where
+  "wellformed_pte pte \<equiv> case pte of
+     Arch_Structs_A.pte.LargePagePTE p attr r \<Rightarrow>
+       ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
+   | Arch_Structs_A.pte.SmallPagePTE p attr r \<Rightarrow>
+       ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
+   | _ \<Rightarrow> True"
+
+definition
+  wellformed_pde :: "Arch_Structs_A.pde \<Rightarrow> bool"
+where
+  "wellformed_pde pde \<equiv> case pde of
+     Arch_Structs_A.pde.PageTablePDE p attr mw \<Rightarrow> attr \<subseteq> {ParityEnabled}
+   | Arch_Structs_A.pde.SectionPDE p attr mw r \<Rightarrow> r \<in> valid_vm_rights
+   | Arch_Structs_A.pde.SuperSectionPDE p attr r \<Rightarrow> r \<in> valid_vm_rights
+   | _ \<Rightarrow> True"
+
+definition
+  wellformed_arch_obj :: "arch_kernel_obj \<Rightarrow> bool"
+where
+  "wellformed_arch_obj ao \<equiv> case ao of
+     PageTable pt \<Rightarrow> (\<forall>pte\<in>range pt. wellformed_pte pte)
+   | PageDirectory pd \<Rightarrow> (\<forall>pde\<in>range pd. wellformed_pde pde)
+   | _ \<Rightarrow> True"
+
+section "Virtual Memory"
+
+definition
+  equal_kernel_mappings :: "'z::state_ext state \<Rightarrow> bool"
+where
+ "equal_kernel_mappings \<equiv> \<lambda>s.
+    \<forall>x y pd pd'. ako_at (PageDirectory pd) x s
+         \<and> ako_at (PageDirectory pd') y s
+       \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)"
+
+definition
+  pde_ref :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
+where
+  "pde_ref pde \<equiv> case pde of
+    Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | _ \<Rightarrow> None"
+
+datatype vs_ref = VSRef word32 "aa_type option"
+
+definition
+  vs_ref_atype :: "vs_ref \<Rightarrow> aa_type option" where
+ "vs_ref_atype vsref \<equiv> case vsref of VSRef x atype \<Rightarrow> atype"
+
+definition
+  vs_refs :: "arch_kernel_obj \<Rightarrow> (vs_ref \<times> obj_ref) set" where
+  "vs_refs \<equiv> \<lambda>ko. case ko of
+    (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
+  | (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
+      graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
+  | _ \<Rightarrow> {}"
+
+type_synonym vs_chain = "vs_ref list \<times> obj_ref"
+type_synonym 'a rel = "('a \<times> 'a) set"
+
+definition
+  vs_lookup1 :: "'z::state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup1 s \<equiv> {((rs,p),(rs',p')). \<exists>ko r. ako_at ko p s
+                                      \<and> rs' = (r # rs)
+                                      \<and> (r, p') \<in> vs_refs ko}"
+
+abbreviation (input)
+  vs_lookup_trans :: "'z::state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup_trans s \<equiv> (vs_lookup1 s)^*"
+
+abbreviation
+  vs_lookup1_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+  ("_ \<rhd>1 _" [80,80] 81) where
+  "ref \<rhd>1 ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup1 s"
+
+abbreviation
+  vs_lookup_trans_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+  ("_ \<rhd>* _" [80,80] 81) where
+  "ref \<rhd>* ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_trans s"
+
+definition
+  vs_asid_refs :: "(word8 \<rightharpoonup> obj_ref) \<Rightarrow> vs_chain set"
+where
+  "vs_asid_refs t \<equiv> (\<lambda>(r,p). ([VSRef (ucast r) None], p)) ` graph_of t"
+
+definition
+  vs_lookup :: "'z::state_ext state \<Rightarrow> vs_chain set"
+where
+  "vs_lookup \<equiv> \<lambda>s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
+
+abbreviation
+  vs_lookup_abbr :: "vs_ref list \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+  ("_ \<rhd> _" [80,80] 81) where
+  "rs \<rhd> p \<equiv> \<lambda>s. (rs,p) \<in> vs_lookup s"
+
+abbreviation
+  is_reachable_abbr :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" ("\<exists>\<rhd> _" [80] 81) where
+  "\<exists>\<rhd> p \<equiv> \<lambda>s. \<exists>ref. (ref \<rhd> p) s"
+
+definition
+  valid_arch_objs :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_objs \<equiv> \<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ako_at ao p s \<longrightarrow> valid_arch_obj ao s"
+
+definition
+  pde_ref_pages :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
+where
+  "pde_ref_pages pde \<equiv> case pde of
+    Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.SectionPDE ptr x y z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.SuperSectionPDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | _ \<Rightarrow> None"
+
+definition
+  pte_ref_pages :: "Arch_Structs_A.pte \<Rightarrow> obj_ref option"
+where
+  "pte_ref_pages pte \<equiv> case pte of
+    Arch_Structs_A.SmallPagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.LargePagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | _ \<Rightarrow> None"
+
+definition
+  vs_refs_pages :: "arch_kernel_obj \<Rightarrow> (vs_ref \<times> obj_ref) set" where
+  "vs_refs_pages \<equiv> \<lambda>ko. case ko of
+    (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
+  | (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
+      graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x))
+  | (Arch_Structs_A.PageTable pt) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some APageTable), p)) `
+      graph_of (pte_ref_pages o pt)
+  | _ \<Rightarrow> {}"
+
+definition
+  vs_lookup_pages1 :: "'z :: state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup_pages1 s \<equiv> {((rs,p),(rs',p')). \<exists>ko r. ako_at ko p s
+                                          \<and> rs' = (r # rs)
+                                          \<and> (r, p') \<in> vs_refs_pages ko}"
+
+abbreviation (input)
+  vs_lookup_pages_trans :: "'z :: state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup_pages_trans s \<equiv> (vs_lookup_pages1 s)^*"
+
+abbreviation
+  vs_lookup_pages1_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
+  ("_ \<unrhd>1 _" [80,80] 81) where
+  "ref \<unrhd>1 ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_pages1 s"
+
+abbreviation
+  vs_lookup_pages_trans_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
+  ("_ \<unrhd>* _" [80,80] 81) where
+  "ref \<unrhd>* ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_pages_trans s"
+
+definition
+  vs_lookup_pages :: "'z ::state_ext state \<Rightarrow> vs_chain set"
+where
+  "vs_lookup_pages \<equiv> \<lambda>s. vs_lookup_pages_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
+
+abbreviation
+  vs_lookup_pages_abbr :: "vs_ref list \<Rightarrow> obj_ref \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
+  ("_ \<unrhd> _" [80,80] 81) where
+  "rs \<unrhd> p \<equiv> \<lambda>s. (rs,p) \<in> vs_lookup_pages s"
+
+abbreviation
+  is_reachable_pages_abbr :: "obj_ref \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool" ("\<exists>\<unrhd> _" [80] 81) where
+  "\<exists>\<unrhd> p \<equiv> \<lambda>s. \<exists>ref. (ref \<unrhd> p) s"
+
+definition
+  pde_mapping_bits :: "nat"
+where
+ "pde_mapping_bits \<equiv> pageBitsForSize ARMSection"
+
+definition
+  pte_mapping_bits :: "nat"
+where
+ "pte_mapping_bits \<equiv> pageBitsForSize ARMSmallPage"
+
+definition
+  valid_pte_kernel_mappings :: "Arch_Structs_A.pte \<Rightarrow> vspace_ref
+                                   \<Rightarrow> arm_vspace_region_uses \<Rightarrow> bool"
+where
+ "valid_pte_kernel_mappings pte vref uses \<equiv> case pte of
+    Arch_Structs_A.InvalidPTE \<Rightarrow>
+        \<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}.
+                    uses x \<noteq> ArmVSpaceKernelWindow
+  | Arch_Structs_A.SmallPagePTE ptr atts rghts \<Rightarrow>
+        Platform.ptrFromPAddr ptr = vref
+        \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
+             \<and> (use = ArmVSpaceKernelWindow
+                    \<or> use = ArmVSpaceDeviceWindow))
+        \<and> rghts = {}
+  | Arch_Structs_A.LargePagePTE ptr atts rghts \<Rightarrow>
+        Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMLargePage))
+        \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
+             \<and> (use = ArmVSpaceKernelWindow
+                    \<or> use = ArmVSpaceDeviceWindow))
+        \<and> rghts = {}"
+
+definition
+  valid_pt_kernel_mappings :: "vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> arch_kernel_obj \<Rightarrow> bool"
+where
+ "valid_pt_kernel_mappings vref uses obj \<equiv> case obj of
+    PageTable pt \<Rightarrow>
+        \<forall>x. valid_pte_kernel_mappings
+             (pt x) (vref + (ucast x << pte_mapping_bits)) uses
+  | _ \<Rightarrow> False"
+
+definition
+  valid_pde_kernel_mappings :: "Arch_Structs_A.pde \<Rightarrow> vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+ "valid_pde_kernel_mappings pde vref uses \<equiv> case pde of
+    Arch_Structs_A.InvalidPDE \<Rightarrow>
+        (\<lambda>s. \<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
+                    uses x \<noteq> ArmVSpaceKernelWindow)
+  | Arch_Structs_A.PageTablePDE ptr _ _ \<Rightarrow>
+        aobj_at (valid_pt_kernel_mappings vref uses)
+                    (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.SectionPDE ptr atts _ rghts \<Rightarrow>
+        (\<lambda>s. Platform.ptrFromPAddr ptr = vref
+             \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}. uses x = use)
+                   \<and> (use = ArmVSpaceKernelWindow
+                            \<or> use = ArmVSpaceDeviceWindow))
+             \<and> rghts = {})
+  | Arch_Structs_A.SuperSectionPDE ptr atts rghts \<Rightarrow>
+        (\<lambda>s. Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMSuperSection))
+             \<and> (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
+                   uses x = ArmVSpaceKernelWindow)
+             \<and> rghts = {})"
+
+definition
+  valid_pd_kernel_mappings :: "arm_vspace_region_uses \<Rightarrow> 'z::state_ext state
+                                    \<Rightarrow> arch_kernel_obj \<Rightarrow> bool"
+where
+ "valid_pd_kernel_mappings uses \<equiv> \<lambda>s obj.
+  case obj of
+    PageDirectory pd \<Rightarrow>
+      (\<forall>x. valid_pde_kernel_mappings
+             (pd x) (ucast x << pde_mapping_bits) uses s)
+  | _ \<Rightarrow> False"
+
+definition
+  valid_global_pd_mappings :: "'z::state_ext state \<Rightarrow> bool"
+where
+ "valid_global_pd_mappings \<equiv> \<lambda>s.
+  aobj_at (valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s)
+    (arm_global_pd (arch_state s)) s"
+
+definition
+  valid_ao_at :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_arch_obj ao s"
+
+definition
+  "valid_pde_mappings pde \<equiv> case pde of
+    Arch_Structs_A.SectionPDE ptr _ _ _ \<Rightarrow> is_aligned ptr pageBits
+  | Arch_Structs_A.SuperSectionPDE ptr _ _ \<Rightarrow> is_aligned ptr pageBits
+  | _ \<Rightarrow> True"
+
+definition
+  "empty_table S ko \<equiv>
+   case ko of
+     Arch_Structs_A.PageDirectory pd \<Rightarrow>
+       \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> S) \<and>
+            valid_pde_mappings (pd x) \<and>
+            (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = Arch_Structs_A.InvalidPDE)
+   | Arch_Structs_A.PageTable pt \<Rightarrow>
+         pt = (\<lambda>x. Arch_Structs_A.InvalidPTE)
+   | _ \<Rightarrow> False"
+
+definition
+  "valid_kernel_mappings_if_pd S ko \<equiv> case ko of
+    ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
+        \<forall>x r. pde_ref (pd x) = Some r
+                  \<longrightarrow> ((r \<in> S) = (x \<in> kernel_mapping_slots))
+  | _ \<Rightarrow> True"
+
+definition
+  "aligned_pte pte \<equiv>
+     case pte of
+       Arch_Structs_A.LargePagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMLargePage
+     | Arch_Structs_A.SmallPagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMSmallPage
+     | _ \<Rightarrow> True"
+
+lemmas aligned_pte_simps[simp] =
+       aligned_pte_def[split_simps Arch_Structs_A.pte.split]
+
+
+definition
+  valid_global_objs :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_global_objs \<equiv>
+  \<lambda>s. valid_ao_at (arm_global_pd (arch_state s)) s \<and>
+           aobj_at (empty_table (set (arm_global_pts (arch_state s))))
+                  (arm_global_pd (arch_state s)) s \<and>
+      (\<forall>p\<in>set (arm_global_pts (arch_state s)).
+          \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)))"
+
+definition
+  valid_asid_table :: "(word8 \<rightharpoonup> obj_ref) \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_asid_table table \<equiv> \<lambda>s. (\<forall>p \<in> ran table. asid_pool_at p s) \<and>
+                                inj_on table (dom table)"
+
+definition
+  valid_global_pts :: "'z :: state_ext state \<Rightarrow> bool"
+where
+  "valid_global_pts \<equiv> \<lambda>s.
+   \<forall>p \<in> set (arm_global_pts (arch_state s)). atyp_at APageTable p s"
+(* this property now follows from valid_global_objs:
+   "valid_global_objs s \<Longrightarrow> valid_global_pts s" *)
+
+definition
+  valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_state \<equiv> \<lambda>s.
+  atyp_at (AIntData ARMSmallPage) (arm_globals_frame (arch_state s)) s \<and>
+  valid_asid_table (arm_asid_table (arch_state s)) s \<and>
+  page_directory_at (arm_global_pd (arch_state s)) s \<and>
+  valid_global_pts s \<and>
+  is_inv (arm_hwasid_table (arch_state s))
+             (option_map fst o arm_asid_map (arch_state s))"
+
+definition
+  vs_cap_ref :: "arch_cap \<Rightarrow> vs_ref list option"
+where
+  "vs_cap_ref cap \<equiv> case cap of
+   Arch_Structs_A.ASIDPoolCap _ asid \<Rightarrow>
+     Some [VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageDirectoryCap _ (Some asid) \<Rightarrow>
+     Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageTableCap _ (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMSmallPage (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
+           VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMLargePage (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
+           VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMSection (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | _ \<Rightarrow> None"
+
+definition
+  "is_pg_cap cap \<equiv> \<exists>p R sz m. cap =
+   arch_cap.PageCap p R sz m"
+
+definition
+  "is_pd_cap c \<equiv>
+   \<exists>p asid. c = arch_cap.PageDirectoryCap p asid"
+
+definition
+  "is_pt_cap c \<equiv> \<exists>p asid. c = arch_cap.PageTableCap p asid"
+
+definition
+  "cap_asid cap \<equiv> case cap of
+    Arch_Structs_A.PageCap _ _ _ (Some (asid, _)) \<Rightarrow> Some asid
+  | Arch_Structs_A.PageTableCap _ (Some (asid, _)) \<Rightarrow> Some asid
+  | Arch_Structs_A.PageDirectoryCap _ (Some asid) \<Rightarrow> Some asid
+  | _ \<Rightarrow> None"
+
+definition
+  arch_caps_of_state :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap option"
+where
+ "arch_caps_of_state s \<equiv> (\<lambda>p. if (\<exists>acap. fst (get_cap p s) = {(ArchObjectCap acap, s)})
+                         then Some (THE acap. fst (get_cap p s) = {(ArchObjectCap acap, s)})
+                         else None)"
+
+  (* needed for retype: if reachable, then cap, if cap then protected by untyped cap.
+     strengthened for preservation in cap delete: ref in cap must unmap the right objects *)
+definition
+  "valid_vs_lookup \<equiv> \<lambda>s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow>
+  ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
+  (\<exists>p' acap. arch_caps_of_state s p' = Some acap \<and>
+            aobj_ref acap = Some p \<and> vs_cap_ref acap = Some ref)"
+
+definition
+  global_refs :: "'z::state_ext state \<Rightarrow> obj_ref set"
+where
+  "global_refs \<equiv> \<lambda>s.
+  {idle_thread s, arm_globals_frame (arch_state s), arm_global_pd (arch_state s)} \<union>
+   range (interrupt_irq_node s) \<union>
+   set (arm_global_pts (arch_state s))"
+
+definition
+  kernel_window :: "'z::state_ext state \<Rightarrow> obj_ref set"
+where
+  "kernel_window s \<equiv> {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow}"
+
+
+  (* needed for map: installing new object should add only one mapping *)
+definition
+  "valid_table_caps \<equiv> \<lambda>s.
+  \<forall>r p acap. arch_caps_of_state s p = Some acap \<longrightarrow>
+            (is_pd_cap acap \<or> is_pt_cap acap) \<longrightarrow>
+            cap_asid acap = None \<longrightarrow>
+            aobj_ref acap = Some r \<longrightarrow>
+            aobj_at (empty_table (set (arm_global_pts (arch_state s)))) r s"
+
+  (* needed to preserve valid_table_caps in map *)
+definition
+  "unique_table_caps \<equiv> \<lambda>cs. \<forall>p p' cap cap'.
+  cs p = Some cap \<longrightarrow> cs p' = Some cap' \<longrightarrow>
+  cap_asid cap = None \<longrightarrow>
+  aobj_ref cap' = aobj_ref cap \<longrightarrow>
+  (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and>
+  (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)"
+
+definition
+  table_cap_ref :: "arch_cap \<Rightarrow> vs_ref list option"
+where
+  "table_cap_ref cap \<equiv> case cap of
+     Arch_Structs_A.ASIDPoolCap _ asid \<Rightarrow>
+       Some [VSRef (ucast (asid_high_bits_of asid)) None]
+   | Arch_Structs_A.PageDirectoryCap _ (Some asid) \<Rightarrow>
+       Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+             VSRef (ucast (asid_high_bits_of asid)) None]
+   | Arch_Structs_A.PageTableCap _ (Some (asid, vptr)) \<Rightarrow>
+       Some [VSRef (vptr >> 20) (Some APageDirectory),
+             VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+             VSRef (ucast (asid_high_bits_of asid)) None]
+   | _ \<Rightarrow> None"
+
+  (* needed to avoid a single page insertion
+     resulting in multiple valid lookups *)
+definition
+  "unique_table_refs \<equiv> \<lambda>cs. \<forall>p p' cap cap'.
+  cs p = Some cap \<longrightarrow> cs p' = Some cap' \<longrightarrow>
+  aobj_ref cap' = aobj_ref cap \<longrightarrow>
+  table_cap_ref cap' = table_cap_ref cap"
+
+definition
+  valid_kernel_mappings :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_kernel_mappings \<equiv>
+     \<lambda>s. \<forall>ko \<in> ran (kheap s).
+          valid_kernel_mappings_if_pd
+             (set (arm_global_pts (arch_state s))) ko"
+
+definition
+  "valid_arch_caps \<equiv> valid_vs_lookup and valid_table_caps and
+                     (\<lambda>s. unique_table_caps (arch_caps_of_state s)
+                        \<and> unique_table_refs (arch_caps_of_state s))"
+
+definition
+  "valid_machine_state \<equiv>
+   \<lambda>s. \<forall>p. in_user_frame p (s::'z::state_ext state) \<or> underlying_memory (machine_state s) p = 0"
+
+text "objects live in the kernel window"
+definition
+  pspace_in_kernel_window :: "'z::state_ext state \<Rightarrow> bool"
+where
+ "pspace_in_kernel_window \<equiv> \<lambda>s.
+    \<forall>x ko. kheap s x = Some ko \<longrightarrow>
+       (\<forall>y \<in> {x .. x + (2 ^ obj_bits ko) - 1}.
+             arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow)"
+
+definition
+  arch_obj_bits_type :: "aa_type \<Rightarrow> nat"
+where
+ "arch_obj_bits_type T' \<equiv> (case T' of
+    AASIDPool \<Rightarrow> arch_kobj_size (Arch_Structs_A.ASIDPool undefined)
+  | AIntData sz \<Rightarrow> arch_kobj_size (DataPage sz)
+  | APageDirectory \<Rightarrow> arch_kobj_size (Arch_Structs_A.PageDirectory undefined)
+  | APageTable \<Rightarrow> arch_kobj_size (Arch_Structs_A.PageTable undefined))"
+
+section "Lemmas"
+
+lemma vmsz_aligned_ARMSection:
+  "vmsz_aligned vref ARMSection = is_aligned vref (pageBitsForSize ARMSection)"
+  by (simp add: vmsz_aligned_def pageBitsForSize_def)
+
+lemma valid_arch_cap_def2:
+  "valid_arch_cap c s \<equiv> wellformed_acap c \<and> valid_arch_cap_ref c s"
+  apply (rule eq_reflection)
+  apply (cases c)
+    by (auto simp add: wellformed_acap_simps valid_arch_cap_simps
+                          valid_arch_cap_ref_simps vmsz_aligned_ARMSection
+                split: option.splits)
+
+lemmas vs_ref_atype_simps[simp] = vs_ref_atype_def[split_simps vs_ref.split]
+
+lemma vs_lookup1_obj_at:
+  "((rs,p) \<rhd>1 (r # rs,p')) s = aobj_at (\<lambda>ko. (r, p') \<in> vs_refs ko) p s"
+  by (fastforce simp: vs_lookup1_def aobj_at_def)
+
+lemma vs_lookup1I:
+  "\<lbrakk> ako_at ko p s; (r, p') \<in> vs_refs ko;
+          rs' = r # rs \<rbrakk> \<Longrightarrow> ((rs,p) \<rhd>1 (rs',p')) s"
+  by (fastforce simp add: vs_lookup1_def)
+
+lemma vs_lookup1D:
+  "(x \<rhd>1 y) s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs,p) \<and> y = (r # rs,p')
+                          \<and> ako_at ko p s \<and> (r,p') \<in> vs_refs ko"
+  by (cases x, cases y) (fastforce simp: vs_lookup1_def)
+
+lemma vs_lookup_pages1D:
+  "(x \<unrhd>1 y) s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs,p) \<and> y = (r # rs,p')
+                          \<and> ako_at ko p s \<and> (r,p') \<in> vs_refs_pages ko"
+  by (cases x, cases y) (fastforce simp: vs_lookup_pages1_def)
+
+lemma vs_lookup1_stateI:
+  assumes 1: "(r \<rhd>1 r') s"
+  assumes ko: "\<And>ko. ako_at ko (snd r) s \<Longrightarrow> aobj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') (snd r) s'"
+  shows "(r \<rhd>1 r') s'" using 1 ko
+  by (fastforce simp: aobj_at_def vs_lookup1_def)
+
+lemma vs_lookup_trans_sub:
+  assumes ko: "\<And>ko p. ako_at ko p s \<Longrightarrow> aobj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
+  shows "vs_lookup_trans s \<subseteq> vs_lookup_trans s'"
+proof -
+  have "vs_lookup1 s \<subseteq> vs_lookup1 s'"
+    by (fastforce dest: ko elim: vs_lookup1_stateI)
+  thus ?thesis by (rule rtrancl_mono)
+qed
+
+lemma vs_lookup_sub:
+  assumes ko: "\<And>ko p. ako_at ko p s \<Longrightarrow> aobj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
+  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
+  shows "vs_lookup s \<subseteq> vs_lookup s'"
+  unfolding vs_lookup_def
+  apply (rule Image_mono)
+   apply (rule vs_lookup_trans_sub)
+   apply (erule ko)
+  apply (unfold vs_asid_refs_def)
+  apply (rule image_mono)
+  apply (rule table)
+  done
+
+lemma vs_lookup_pages1_stateI:
+  assumes 1: "(r \<unrhd>1 r') s"
+  assumes ko: "\<And>ko. ako_at ko (snd r) s \<Longrightarrow> aobj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') (snd r) s'"
+  shows "(r \<unrhd>1 r') s'" using 1 ko
+  by (fastforce simp: aobj_at_def vs_lookup_pages1_def)
+
+lemma vs_lookup_pages_trans_sub:
+  assumes ko: "\<And>ko p. ako_at ko p s \<Longrightarrow>
+                      aobj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
+  shows "vs_lookup_pages_trans s \<subseteq> vs_lookup_pages_trans s'"
+proof -
+  have "vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'"
+    by (fastforce simp add: ko elim: vs_lookup_pages1_stateI)
+  thus ?thesis by (rule rtrancl_mono)
+qed
+
+lemma vs_lookup_pages_sub:
+  assumes ko: "\<And>ko p. ako_at ko p s \<Longrightarrow>
+                      aobj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
+  assumes table:
+    "graph_of (arm_asid_table (arch_state s)) \<subseteq>
+     graph_of (arm_asid_table (arch_state s'))"
+  shows "vs_lookup_pages s \<subseteq> vs_lookup_pages s'"
+  unfolding vs_lookup_pages_def
+  apply (rule Image_mono)
+   apply (rule vs_lookup_pages_trans_sub)
+   apply (erule ko)
+  apply (unfold vs_asid_refs_def)
+  apply (rule image_mono)
+  apply (rule table)
+  done
+
+lemma vs_lookup_pagesI:
+  "\<lbrakk> ref' \<in> vs_asid_refs (arm_asid_table (arch_state s));
+     (ref',(ref,p)) \<in> (vs_lookup_pages1 s)^*  \<rbrakk> \<Longrightarrow>
+  (ref \<unrhd> p) s"
+  by (simp add: vs_lookup_pages_def) blast
+
+lemma vs_lookup_stateI:
+  assumes 1: "(ref \<rhd> p) s"
+  assumes ko: "\<And>ko p. ako_at ko p s \<Longrightarrow> aobj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
+  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
+  shows "(ref \<rhd> p) s'"
+  using 1 vs_lookup_sub [OF ko table] by blast
+
+lemma valid_arch_objsD:
+  "\<lbrakk> (ref \<rhd> p) s; ako_at ao p s; valid_arch_objs s \<rbrakk> \<Longrightarrow> valid_arch_obj ao s"
+  by (fastforce simp add: valid_arch_objs_def)
+
+(* should work for unmap and non-arch ops *)
+lemma valid_arch_objs_stateI:
+  assumes 1: "valid_arch_objs s"
+  assumes ko: "\<And>ko p. ako_at ko p s' \<Longrightarrow> aobj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
+  assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
+  assumes vao: "\<And>p ref ao'.
+                \<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ako_at ao p s \<longrightarrow> valid_arch_obj ao s;
+                  ako_at ao' p s' \<rbrakk> \<Longrightarrow> valid_arch_obj ao' s'"
+  shows "valid_arch_objs s'"
+  using 1 unfolding valid_arch_objs_def
+  apply clarsimp
+  apply (frule vs_lookup_stateI)
+    apply (erule ko)
+   apply (rule arch)
+  apply (erule allE, erule impE, fastforce)
+  apply (erule (3) vao)
+  done
+
+lemma aobj_at_pspaceI:
+  "\<lbrakk> aobj_at P ref s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> aobj_at P ref s'"
+  by (simp add: aobj_at_def)
+
+
+lemma valid_arch_cap_atyp:
+  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (atyp_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (atyp_at T p s)\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. valid_arch_cap c s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_cap c s\<rbrace>"
+  apply (simp add: valid_arch_cap_def)
+  apply (case_tac c, simp_all)
+  by (wp P)
+
+lemma valid_arch_obj_atyp:
+  assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (atyp_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (atyp_at T p s)\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. valid_arch_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_obj ob s\<rbrace>"
+  apply (cases ob, simp_all)
+     apply (rule hoare_vcg_const_Ball_lift [OF P])
+    apply (rule hoare_vcg_all_lift)
+    apply (rename_tac "fun" x)
+    apply (case_tac "fun x", simp_all add: hoare_vcg_prop P)
+  apply (rule hoare_vcg_ball_lift)
+  apply (rename_tac "fun" x)
+  apply (case_tac "fun x", simp_all add: hoare_vcg_prop P)
+  apply (rule P)
+  done
+
+lemma atyp_at_eq_kheap_obj:
+  "atyp_at AASIDPool p s \<longleftrightarrow>
+   (\<exists>f. kheap s p = Some (ArchObj (Arch_Structs_A.ASIDPool f)))"
+  "atyp_at APageTable p s \<longleftrightarrow>
+   (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))"
+  "atyp_at APageDirectory p s \<longleftrightarrow>
+   (\<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)))"
+  "atyp_at (AIntData sz) p s \<longleftrightarrow>
+   (kheap s p = Some (ArchObj (DataPage sz)))"
+apply (auto simp add: aobj_at_def)
+apply (simp_all add: aa_type_def split: split_if_asm  arch_kernel_obj.splits)
+done
+
+lemma aa_type_AASIDPoolE:
+  "\<lbrakk>aa_type ko = AASIDPool;
+    (\<And>ap. ko = (arch_kernel_obj.ASIDPool ap) \<Longrightarrow> R)\<rbrakk>
+   \<Longrightarrow> R"
+  by (case_tac ko, simp_all add: aa_type_simps split: split_if_asm)
+
+lemma aa_type_APageDirectoryE:
+  "\<lbrakk>aa_type ko = APageDirectory;
+    (\<And>pd. ko = PageDirectory pd \<Longrightarrow> R)\<rbrakk>
+   \<Longrightarrow> R"
+  by (case_tac ko, simp_all add: aa_type_simps split: split_if_asm)
+
+lemma aa_type_APageTableE:
+  "\<lbrakk>aa_type ko = APageTable; (\<And>pt. ko = PageTable pt \<Longrightarrow> R)\<rbrakk>
+   \<Longrightarrow> R"
+  by (case_tac ko, simp_all add: aa_type_simps split: split_if_asm)
+
+lemma aa_type_AIntDataE:
+  "\<lbrakk>aa_type ko = AIntData sz; ko = DataPage sz \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by (case_tac ko, simp_all add: aa_type_simps split: split_if_asm)
+
+
+
+lemmas a_type_elims[elim!] =
+   aa_type_AASIDPoolE aa_type_APageDirectoryE aa_type_APageTableE aa_type_AIntDataE
+
+end
+
+end
diff --git a/proof/invariant-abstract/ARM/ArchTypes_AI.thy b/proof/invariant-abstract/ARM/ArchTypes_AI.thy
new file mode 100644
index 000000000..7a9bbd95e
--- /dev/null
+++ b/proof/invariant-abstract/ARM/ArchTypes_AI.thy
@@ -0,0 +1,654 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+theory ArchTypes_AI
+imports "../LevityCatch_AI"
+begin
+
+-- ---------------------------------------------------------------------------
+section "Things to Move Up"
+
+(* FIXME: move to spec level *)
+(* global data and code of the kernel, not covered by any cap *)
+axiomatization
+  kernel_data_refs :: "word32 set"
+
+-- ---------------------------------------------------------------------------
+section "ARM-specific invariant definitions"
+
+
+definition
+  aobj_at :: "(arch_kernel_obj \<Rightarrow> bool) \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "aobj_at P ref s \<equiv> \<exists>ko. kheap s ref = Some (ArchObj ko) \<and> P ko"
+
+abbreviation
+  "ako_at k \<equiv> aobj_at (op = k)"
+
+definition
+  "vmsz_aligned ref sz \<equiv> is_aligned ref (pageBitsForSize sz)"
+
+definition
+  "wellformed_mapdata sz \<equiv>
+   \<lambda>(asid, vref). 0 < asid \<and> asid \<le> 2^asid_bits - 1
+                \<and> vmsz_aligned vref sz \<and> vref < kernel_base"
+
+definition
+  wellformed_acap :: "arch_cap \<Rightarrow> bool"
+where
+  "wellformed_acap ac \<equiv>
+   case ac of
+     Arch_Structs_A.ASIDPoolCap r as
+       \<Rightarrow> is_aligned as asid_low_bits \<and> as \<le> 2^asid_bits - 1
+   | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> rghts \<in> valid_vm_rights \<and>
+     case_option True (wellformed_mapdata sz) mapdata
+   | Arch_Structs_A.PageTableCap r (Some mapdata) \<Rightarrow>
+     wellformed_mapdata ARMSection mapdata
+   | Arch_Structs_A.PageDirectoryCap r (Some asid) \<Rightarrow>
+     0 < asid \<and> asid \<le> 2^asid_bits - 1
+   | _ \<Rightarrow> True"
+
+abbreviation
+  "atyp_at T \<equiv> aobj_at (\<lambda>ob. aa_type ob = T)"
+
+(* this time with typ_at. might lead to confusion, but this is how
+   the rest should have been defined.. *)
+abbreviation
+  "asid_pool_at \<equiv> atyp_at AASIDPool"
+abbreviation
+  "page_table_at \<equiv> atyp_at APageTable"
+abbreviation
+  "page_directory_at \<equiv> atyp_at APageDirectory"
+
+definition
+  "pde_at p \<equiv> page_directory_at (p && ~~ mask pd_bits)
+                  and K (is_aligned p 2)"
+definition
+  "pte_at p \<equiv> page_table_at (p && ~~ mask pt_bits)
+                  and K (is_aligned p 2)"
+
+
+definition
+  valid_arch_cap_ref :: "arch_cap \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_cap_ref ac s \<equiv> (case ac of
+    Arch_Structs_A.ASIDPoolCap r as \<Rightarrow> atyp_at AASIDPool r s
+  | Arch_Structs_A.ASIDControlCap \<Rightarrow> True
+  | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> atyp_at (AIntData sz) r s
+  | Arch_Structs_A.PageTableCap r mapdata \<Rightarrow> atyp_at APageTable r s
+  | Arch_Structs_A.PageDirectoryCap r mapdata\<Rightarrow> atyp_at APageDirectory r s)"
+
+definition
+  valid_arch_cap :: "arch_cap \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_cap ac s \<equiv> (case ac of
+    Arch_Structs_A.ASIDPoolCap r as \<Rightarrow>
+         atyp_at AASIDPool r s \<and> is_aligned as asid_low_bits
+           \<and> as \<le> 2^asid_bits - 1
+  | Arch_Structs_A.ASIDControlCap \<Rightarrow> True
+  | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow>
+    atyp_at (AIntData sz) r s \<and> rghts \<in> valid_vm_rights \<and>
+    (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2^asid_bits - 1
+                                             \<and> vmsz_aligned ref sz \<and> ref < kernel_base)
+  | Arch_Structs_A.PageTableCap r mapdata \<Rightarrow>
+    atyp_at APageTable r s \<and>
+    (case mapdata of None \<Rightarrow> True
+       | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ asid_bits - 1
+                                \<and> vref < kernel_base
+                                \<and> is_aligned vref (pageBitsForSize ARMSection))
+  | Arch_Structs_A.PageDirectoryCap r mapdata \<Rightarrow>
+    atyp_at APageDirectory r s \<and>
+    case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata)"
+
+primrec
+  acap_class :: "arch_cap \<Rightarrow> capclass"
+where
+  "acap_class (arch_cap.ASIDPoolCap x y)      = PhysicalClass"
+| "acap_class (arch_cap.ASIDControlCap)       = ASIDMasterClass"
+| "acap_class (arch_cap.PageCap x y sz z)     = PhysicalClass"
+| "acap_class (arch_cap.PageTableCap x y)     = PhysicalClass"
+| "acap_class (arch_cap.PageDirectoryCap x y) = PhysicalClass"
+
+definition
+  valid_ipc_buffer_cap :: "cap \<Rightarrow> word32 \<Rightarrow> bool"
+where
+  "valid_ipc_buffer_cap c bufptr \<equiv>
+         case c of
+              cap.ArchObjectCap (arch_cap.PageCap ref rghts sz mapdata) \<Rightarrow>
+                   is_aligned bufptr msg_align_bits
+
+            | _ \<Rightarrow> True"
+
+primrec
+  valid_pte :: "Arch_Structs_A.pte \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_pte (Arch_Structs_A.InvalidPTE) = \<top>"
+| "valid_pte (Arch_Structs_A.LargePagePTE ptr x y) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMLargePage) (Platform.ptrFromPAddr ptr) s)"
+| "valid_pte (Arch_Structs_A.SmallPagePTE ptr x y) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMSmallPage) (Platform.ptrFromPAddr ptr) s)"
+
+primrec
+  valid_pde :: "Arch_Structs_A.pde \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_pde (Arch_Structs_A.InvalidPDE) = \<top>"
+| "valid_pde (Arch_Structs_A.SectionPDE ptr x y z) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMSection) (Platform.ptrFromPAddr ptr) s)"
+| "valid_pde (Arch_Structs_A.SuperSectionPDE ptr x z) =
+   (\<lambda>s. is_aligned ptr pageBits \<and>
+        atyp_at (AIntData ARMSuperSection)
+               (Platform.ptrFromPAddr ptr) s)"
+| "valid_pde (Arch_Structs_A.PageTablePDE ptr x z) =
+   (atyp_at APageTable (Platform.ptrFromPAddr ptr))"
+
+
+definition
+  kernel_mapping_slots :: "12 word set" where
+ "kernel_mapping_slots \<equiv> {x. x \<ge> ucast (kernel_base >> 20)}"
+
+primrec
+  valid_arch_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_obj (Arch_Structs_A.ASIDPool pool) =
+   (\<lambda>s. \<forall>x \<in> ran pool. atyp_at  APageDirectory x s)"
+| "valid_arch_obj (Arch_Structs_A.PageDirectory pd) =
+   (\<lambda>s. \<forall>x \<in> -kernel_mapping_slots. valid_pde (pd x) s)"
+| "valid_arch_obj (Arch_Structs_A.PageTable pt) = (\<lambda>s. \<forall>x. valid_pte (pt x) s)"
+| "valid_arch_obj (DataPage sz) = \<top>"
+
+definition
+  wellformed_pte :: "Arch_Structs_A.pte \<Rightarrow> bool"
+where
+  "wellformed_pte pte \<equiv> case pte of
+     Arch_Structs_A.pte.LargePagePTE p attr r \<Rightarrow>
+       ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
+   | Arch_Structs_A.pte.SmallPagePTE p attr r \<Rightarrow>
+       ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
+   | _ \<Rightarrow> True"
+
+lemmas
+  wellformed_pte_simps[simp] =
+  wellformed_pte_def[split_simps Arch_Structs_A.pte.split]
+
+definition
+  wellformed_pde :: "Arch_Structs_A.pde \<Rightarrow> bool"
+where
+  "wellformed_pde pde \<equiv> case pde of
+     Arch_Structs_A.pde.PageTablePDE p attr mw \<Rightarrow> attr \<subseteq> {ParityEnabled}
+   | Arch_Structs_A.pde.SectionPDE p attr mw r \<Rightarrow> r \<in> valid_vm_rights
+   | Arch_Structs_A.pde.SuperSectionPDE p attr r \<Rightarrow> r \<in> valid_vm_rights
+   | _ \<Rightarrow> True"
+
+lemmas
+  wellformed_pde_simps[simp] =
+  wellformed_pde_def[split_simps Arch_Structs_A.pde.split]
+
+definition
+  wellformed_arch_obj :: "arch_kernel_obj \<Rightarrow> bool"
+where
+  "wellformed_arch_obj ao \<equiv> case ao of
+     PageTable pt \<Rightarrow> (\<forall>pte\<in>range pt. wellformed_pte pte)
+   | PageDirectory pd \<Rightarrow> (\<forall>pde\<in>range pd. wellformed_pde pde)
+   | _ \<Rightarrow> True"
+
+lemmas
+  wellformed_arch_obj_simps[simp] =
+  wellformed_arch_obj_def[split_simps arch_kernel_obj.split]
+
+section "Virtual Memory"
+
+definition
+  equal_kernel_mappings :: "'z::state_ext state \<Rightarrow> bool"
+where
+ "equal_kernel_mappings \<equiv> \<lambda>s.
+    \<forall>x y pd pd'. ako_at (PageDirectory pd) x s
+         \<and> ako_at (PageDirectory pd') y s
+       \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)"
+
+definition
+  pde_ref :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
+where
+  "pde_ref pde \<equiv> case pde of
+    Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | _ \<Rightarrow> None"
+
+datatype vs_ref = VSRef word32 "aa_type option"
+
+definition
+  vs_ref_atype :: "vs_ref \<Rightarrow> aa_type option" where
+ "vs_ref_atype vsref \<equiv> case vsref of VSRef x atype \<Rightarrow> atype"
+
+definition
+  vs_refs :: "arch_kernel_obj \<Rightarrow> (vs_ref \<times> obj_ref) set" where
+  "vs_refs \<equiv> \<lambda>ko. case ko of
+    (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
+  | (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
+      graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
+  | _ \<Rightarrow> {}"
+
+type_synonym vs_chain = "vs_ref list \<times> obj_ref"
+type_synonym 'a rel = "('a \<times> 'a) set"
+
+definition
+  vs_lookup1 :: "'z::state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup1 s \<equiv> {((rs,p),(rs',p')). \<exists>ko r. ako_at ko p s
+                                      \<and> rs' = (r # rs)
+                                      \<and> (r, p') \<in> vs_refs ko}"
+
+abbreviation (input)
+  vs_lookup_trans :: "'z::state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup_trans s \<equiv> (vs_lookup1 s)^*"
+
+abbreviation
+  vs_lookup1_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+  ("_ \<rhd>1 _" [80,80] 81) where
+  "ref \<rhd>1 ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup1 s"
+
+abbreviation
+  vs_lookup_trans_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+  ("_ \<rhd>* _" [80,80] 81) where
+  "ref \<rhd>* ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_trans s"
+
+definition
+  vs_asid_refs :: "(word8 \<rightharpoonup> obj_ref) \<Rightarrow> vs_chain set"
+where
+  "vs_asid_refs t \<equiv> (\<lambda>(r,p). ([VSRef (ucast r) None], p)) ` graph_of t"
+
+definition
+  vs_lookup :: "'z::state_ext state \<Rightarrow> vs_chain set"
+where
+  "vs_lookup \<equiv> \<lambda>s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
+
+abbreviation
+  vs_lookup_abbr :: "vs_ref list \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+  ("_ \<rhd> _" [80,80] 81) where
+  "rs \<rhd> p \<equiv> \<lambda>s. (rs,p) \<in> vs_lookup s"
+
+abbreviation
+  is_reachable_abbr :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" ("\<exists>\<rhd> _" [80] 81) where
+  "\<exists>\<rhd> p \<equiv> \<lambda>s. \<exists>ref. (ref \<rhd> p) s"
+
+definition
+  valid_arch_objs :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_objs \<equiv> \<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ako_at ao p s \<longrightarrow> valid_arch_obj ao s"
+
+definition
+  pde_ref_pages :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
+where
+  "pde_ref_pages pde \<equiv> case pde of
+    Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.SectionPDE ptr x y z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.SuperSectionPDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | _ \<Rightarrow> None"
+
+definition
+  pte_ref_pages :: "Arch_Structs_A.pte \<Rightarrow> obj_ref option"
+where
+  "pte_ref_pages pte \<equiv> case pte of
+    Arch_Structs_A.SmallPagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.LargePagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
+  | _ \<Rightarrow> None"
+
+definition
+  vs_refs_pages :: "arch_kernel_obj \<Rightarrow> (vs_ref \<times> obj_ref) set" where
+  "vs_refs_pages \<equiv> \<lambda>ko. case ko of
+    (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
+  | (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
+      graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x))
+  | (Arch_Structs_A.PageTable pt) \<Rightarrow>
+      (\<lambda>(r,p). (VSRef (ucast r) (Some APageTable), p)) `
+      graph_of (pte_ref_pages o pt)
+  | _ \<Rightarrow> {}"
+
+definition
+  vs_lookup_pages1 :: "'z :: state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup_pages1 s \<equiv> {((rs,p),(rs',p')). \<exists>ko r. ako_at ko p s
+                                          \<and> rs' = (r # rs)
+                                          \<and> (r, p') \<in> vs_refs_pages ko}"
+
+abbreviation (input)
+  vs_lookup_pages_trans :: "'z :: state_ext state \<Rightarrow> vs_chain rel" where
+  "vs_lookup_pages_trans s \<equiv> (vs_lookup_pages1 s)^*"
+
+abbreviation
+  vs_lookup_pages1_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
+  ("_ \<unrhd>1 _" [80,80] 81) where
+  "ref \<unrhd>1 ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_pages1 s"
+
+abbreviation
+  vs_lookup_pages_trans_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
+  ("_ \<unrhd>* _" [80,80] 81) where
+  "ref \<unrhd>* ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_pages_trans s"
+
+definition
+  vs_lookup_pages :: "'z ::state_ext state \<Rightarrow> vs_chain set"
+where
+  "vs_lookup_pages \<equiv> \<lambda>s. vs_lookup_pages_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
+
+abbreviation
+  vs_lookup_pages_abbr :: "vs_ref list \<Rightarrow> obj_ref \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
+  ("_ \<unrhd> _" [80,80] 81) where
+  "rs \<unrhd> p \<equiv> \<lambda>s. (rs,p) \<in> vs_lookup_pages s"
+
+abbreviation
+  is_reachable_pages_abbr :: "obj_ref \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool" ("\<exists>\<unrhd> _" [80] 81) where
+  "\<exists>\<unrhd> p \<equiv> \<lambda>s. \<exists>ref. (ref \<unrhd> p) s"
+
+definition
+  pde_mapping_bits :: "nat"
+where
+ "pde_mapping_bits \<equiv> pageBitsForSize ARMSection"
+
+definition
+  pte_mapping_bits :: "nat"
+where
+ "pte_mapping_bits \<equiv> pageBitsForSize ARMSmallPage"
+
+definition
+  valid_pte_kernel_mappings :: "Arch_Structs_A.pte \<Rightarrow> vspace_ref
+                                   \<Rightarrow> arm_vspace_region_uses \<Rightarrow> bool"
+where
+ "valid_pte_kernel_mappings pte vref uses \<equiv> case pte of
+    Arch_Structs_A.InvalidPTE \<Rightarrow>
+        \<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}.
+                    uses x \<noteq> ArmVSpaceKernelWindow
+  | Arch_Structs_A.SmallPagePTE ptr atts rghts \<Rightarrow>
+        Platform.ptrFromPAddr ptr = vref
+        \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
+             \<and> (use = ArmVSpaceKernelWindow
+                    \<or> use = ArmVSpaceDeviceWindow))
+        \<and> rghts = {}
+  | Arch_Structs_A.LargePagePTE ptr atts rghts \<Rightarrow>
+        Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMLargePage))
+        \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
+             \<and> (use = ArmVSpaceKernelWindow
+                    \<or> use = ArmVSpaceDeviceWindow))
+        \<and> rghts = {}"
+
+definition
+  valid_pt_kernel_mappings :: "vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> arch_kernel_obj \<Rightarrow> bool"
+where
+ "valid_pt_kernel_mappings vref uses obj \<equiv> case obj of
+    PageTable pt \<Rightarrow>
+        \<forall>x. valid_pte_kernel_mappings
+             (pt x) (vref + (ucast x << pte_mapping_bits)) uses
+  | _ \<Rightarrow> False"
+
+definition
+  valid_pde_kernel_mappings :: "Arch_Structs_A.pde \<Rightarrow> vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+ "valid_pde_kernel_mappings pde vref uses \<equiv> case pde of
+    Arch_Structs_A.InvalidPDE \<Rightarrow>
+        (\<lambda>s. \<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
+                    uses x \<noteq> ArmVSpaceKernelWindow)
+  | Arch_Structs_A.PageTablePDE ptr _ _ \<Rightarrow>
+        aobj_at (valid_pt_kernel_mappings vref uses)
+                    (Platform.ptrFromPAddr ptr)
+  | Arch_Structs_A.SectionPDE ptr atts _ rghts \<Rightarrow>
+        (\<lambda>s. Platform.ptrFromPAddr ptr = vref
+             \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}. uses x = use)
+                   \<and> (use = ArmVSpaceKernelWindow
+                            \<or> use = ArmVSpaceDeviceWindow))
+             \<and> rghts = {})
+  | Arch_Structs_A.SuperSectionPDE ptr atts rghts \<Rightarrow>
+        (\<lambda>s. Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMSuperSection))
+             \<and> (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
+                   uses x = ArmVSpaceKernelWindow)
+             \<and> rghts = {})"
+
+definition
+  valid_pd_kernel_mappings :: "arm_vspace_region_uses \<Rightarrow> 'z::state_ext state
+                                    \<Rightarrow> arch_kernel_obj \<Rightarrow> bool"
+where
+ "valid_pd_kernel_mappings uses \<equiv> \<lambda>s obj.
+  case obj of
+    PageDirectory pd \<Rightarrow>
+      (\<forall>x. valid_pde_kernel_mappings
+             (pd x) (ucast x << pde_mapping_bits) uses s)
+  | _ \<Rightarrow> False"
+
+definition
+  valid_global_pd_mappings :: "'z::state_ext state \<Rightarrow> bool"
+where
+ "valid_global_pd_mappings \<equiv> \<lambda>s.
+  aobj_at (valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s)
+    (arm_global_pd (arch_state s)) s"
+
+definition
+  valid_ao_at :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_arch_obj ao s"
+
+definition
+  "valid_pde_mappings pde \<equiv> case pde of
+    Arch_Structs_A.SectionPDE ptr _ _ _ \<Rightarrow> is_aligned ptr pageBits
+  | Arch_Structs_A.SuperSectionPDE ptr _ _ \<Rightarrow> is_aligned ptr pageBits
+  | _ \<Rightarrow> True"
+
+definition
+  "empty_table S ko \<equiv>
+   case ko of
+     Arch_Structs_A.PageDirectory pd \<Rightarrow>
+       \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> S) \<and>
+            valid_pde_mappings (pd x) \<and>
+            (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = Arch_Structs_A.InvalidPDE)
+   | Arch_Structs_A.PageTable pt \<Rightarrow>
+         pt = (\<lambda>x. Arch_Structs_A.InvalidPTE)
+   | _ \<Rightarrow> False"
+
+definition
+  "valid_kernel_mappings_if_pd S ko \<equiv> case ko of
+    ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
+        \<forall>x r. pde_ref (pd x) = Some r
+                  \<longrightarrow> ((r \<in> S) = (x \<in> kernel_mapping_slots))
+  | _ \<Rightarrow> True"
+
+definition
+  "aligned_pte pte \<equiv>
+     case pte of
+       Arch_Structs_A.LargePagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMLargePage
+     | Arch_Structs_A.SmallPagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMSmallPage
+     | _ \<Rightarrow> True"
+
+lemmas aligned_pte_simps[simp] =
+       aligned_pte_def[split_simps Arch_Structs_A.pte.split]
+
+
+definition
+  valid_global_objs :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_global_objs \<equiv>
+  \<lambda>s. valid_ao_at (arm_global_pd (arch_state s)) s \<and>
+           aobj_at (empty_table (set (arm_global_pts (arch_state s))))
+                  (arm_global_pd (arch_state s)) s \<and>
+      (\<forall>p\<in>set (arm_global_pts (arch_state s)).
+          \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)))"
+
+definition
+  valid_asid_table :: "(word8 \<rightharpoonup> obj_ref) \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_asid_table table \<equiv> \<lambda>s. (\<forall>p \<in> ran table. asid_pool_at p s) \<and>
+                                inj_on table (dom table)"
+
+definition
+  valid_global_pts :: "'z :: state_ext state \<Rightarrow> bool"
+where
+  "valid_global_pts \<equiv> \<lambda>s.
+   \<forall>p \<in> set (arm_global_pts (arch_state s)). atyp_at APageTable p s"
+(* this property now follows from valid_global_objs:
+   "valid_global_objs s \<Longrightarrow> valid_global_pts s" *)
+
+definition
+  valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_arch_state \<equiv> \<lambda>s.
+  atyp_at (AIntData ARMSmallPage) (arm_globals_frame (arch_state s)) s \<and>
+  valid_asid_table (arm_asid_table (arch_state s)) s \<and>
+  page_directory_at (arm_global_pd (arch_state s)) s \<and>
+  valid_global_pts s \<and>
+  is_inv (arm_hwasid_table (arch_state s))
+             (option_map fst o arm_asid_map (arch_state s))"
+
+definition
+  vs_cap_ref :: "arch_cap \<Rightarrow> vs_ref list option"
+where
+  "vs_cap_ref cap \<equiv> case cap of
+   Arch_Structs_A.ASIDPoolCap _ asid \<Rightarrow>
+     Some [VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageDirectoryCap _ (Some asid) \<Rightarrow>
+     Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageTableCap _ (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMSmallPage (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
+           VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMLargePage (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
+           VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMSection (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | Arch_Structs_A.PageCap word rights ARMSuperSection (Some (asid, vptr)) \<Rightarrow>
+     Some [VSRef (vptr >> 20) (Some APageDirectory),
+           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+           VSRef (ucast (asid_high_bits_of asid)) None]
+ | _ \<Rightarrow> None"
+
+definition
+  "is_pg_cap cap \<equiv> \<exists>p R sz m. cap =
+   arch_cap.PageCap p R sz m"
+
+definition
+  "is_pd_cap c \<equiv>
+   \<exists>p asid. c = arch_cap.PageDirectoryCap p asid"
+
+definition
+  "is_pt_cap c \<equiv> \<exists>p asid. c = arch_cap.PageTableCap p asid"
+
+definition
+  "cap_asid cap \<equiv> case cap of
+    Arch_Structs_A.PageCap _ _ _ (Some (asid, _)) \<Rightarrow> Some asid
+  | Arch_Structs_A.PageTableCap _ (Some (asid, _)) \<Rightarrow> Some asid
+  | Arch_Structs_A.PageDirectoryCap _ (Some asid) \<Rightarrow> Some asid
+  | _ \<Rightarrow> None"
+
+definition
+  arch_caps_of_state :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap option"
+where
+ "arch_caps_of_state s \<equiv> (\<lambda>p. if (\<exists>acap. fst (get_cap p s) = {(ArchObjectCap acap, s)})
+                         then Some (THE acap. fst (get_cap p s) = {(ArchObjectCap acap, s)})
+                         else None)"
+
+  (* needed for retype: if reachable, then cap, if cap then protected by untyped cap.
+     strengthened for preservation in cap delete: ref in cap must unmap the right objects *)
+definition
+  "valid_vs_lookup \<equiv> \<lambda>s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow>
+  ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
+  (\<exists>p' acap. arch_caps_of_state s p' = Some acap \<and>
+            aobj_ref acap = Some p \<and> vs_cap_ref acap = Some ref)"
+
+definition
+  global_refs :: "'z::state_ext state \<Rightarrow> obj_ref set"
+where
+  "global_refs \<equiv> \<lambda>s.
+  {idle_thread s, arm_globals_frame (arch_state s), arm_global_pd (arch_state s)} \<union>
+   range (interrupt_irq_node s) \<union>
+   set (arm_global_pts (arch_state s))"
+
+definition
+  kernel_window :: "'z::state_ext state \<Rightarrow> obj_ref set"
+where
+  "kernel_window s \<equiv> {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow}"
+
+
+  (* needed for map: installing new object should add only one mapping *)
+definition
+  "valid_table_caps \<equiv> \<lambda>s.
+  \<forall>r p acap. arch_caps_of_state s p = Some acap \<longrightarrow>
+            (is_pd_cap acap \<or> is_pt_cap acap) \<longrightarrow>
+            cap_asid acap = None \<longrightarrow>
+            aobj_ref acap = Some r \<longrightarrow>
+            aobj_at (empty_table (set (arm_global_pts (arch_state s)))) r s"
+
+  (* needed to preserve valid_table_caps in map *)
+definition
+  "unique_table_caps \<equiv> \<lambda>cs. \<forall>p p' cap cap'.
+  cs p = Some cap \<longrightarrow> cs p' = Some cap' \<longrightarrow>
+  cap_asid cap = None \<longrightarrow>
+  aobj_ref cap' = aobj_ref cap \<longrightarrow>
+  (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and>
+  (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)"
+
+definition
+  table_cap_ref :: "arch_cap \<Rightarrow> vs_ref list option"
+where
+  "table_cap_ref cap \<equiv> case cap of
+     Arch_Structs_A.ASIDPoolCap _ asid \<Rightarrow>
+       Some [VSRef (ucast (asid_high_bits_of asid)) None]
+   | Arch_Structs_A.PageDirectoryCap _ (Some asid) \<Rightarrow>
+       Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+             VSRef (ucast (asid_high_bits_of asid)) None]
+   | Arch_Structs_A.PageTableCap _ (Some (asid, vptr)) \<Rightarrow>
+       Some [VSRef (vptr >> 20) (Some APageDirectory),
+             VSRef (asid && mask asid_low_bits) (Some AASIDPool),
+             VSRef (ucast (asid_high_bits_of asid)) None]
+   | _ \<Rightarrow> None"
+
+  (* needed to avoid a single page insertion
+     resulting in multiple valid lookups *)
+definition
+  "unique_table_refs \<equiv> \<lambda>cs. \<forall>p p' cap cap'.
+  cs p = Some cap \<longrightarrow> cs p' = Some cap' \<longrightarrow>
+  aobj_ref cap' = aobj_ref cap \<longrightarrow>
+  table_cap_ref cap' = table_cap_ref cap"
+
+definition
+  valid_kernel_mappings :: "'z::state_ext state \<Rightarrow> bool"
+where
+  "valid_kernel_mappings \<equiv>
+     \<lambda>s. \<forall>ko \<in> ran (kheap s).
+          valid_kernel_mappings_if_pd
+             (set (arm_global_pts (arch_state s))) ko"
+
+definition
+  "valid_arch_caps \<equiv> valid_vs_lookup and valid_table_caps and
+                     (\<lambda>s. unique_table_caps (arch_caps_of_state s)
+                        \<and> unique_table_refs (arch_caps_of_state s))"
+
+definition
+  "valid_machine_state \<equiv>
+   \<lambda>s. \<forall>p. in_user_frame p (s::'z::state_ext state) \<or> underlying_memory (machine_state s) p = 0"
+
+text "objects live in the kernel window"
+definition
+  pspace_in_kernel_window :: "'z::state_ext state \<Rightarrow> bool"
+where
+ "pspace_in_kernel_window \<equiv> \<lambda>s.
+    \<forall>x ko. kheap s x = Some ko \<longrightarrow>
+       (\<forall>y \<in> {x .. x + (2 ^ obj_bits ko) - 1}.
+             arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow)"
+
+end
diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy
index ba9dfa897..e7597ddd4 100644
--- a/proof/invariant-abstract/Invariants_AI.thy
+++ b/proof/invariant-abstract/Invariants_AI.thy
@@ -9,17 +9,9 @@
  *)
 
 theory Invariants_AI
-imports LevityCatch_AI
+imports "./$L4V_ARCH/ArchInvariants_AI"
 begin
 
--- ---------------------------------------------------------------------------
-section "Things to Move Up"
-
-(* FIXME: move to spec level *)
-(* global data and code of the kernel, not covered by any cap *)
-axiomatization
-  kernel_data_refs :: "word32 set"
-
 -- ---------------------------------------------------------------------------
 section "Invariant Definitions for Abstract Spec"
 
@@ -53,6 +45,7 @@ abbreviation
 abbreviation
   "ko_at k \<equiv> obj_at (op = k)"
 
+
 (*
  * sseefried: 'itcb' is projection of the "mostly preserved" fields of 'tcb'. Many functions
  * in the spec will leave these fields of a TCB unchanged. The 'crunch' tool is easily able
@@ -129,11 +122,6 @@ lemma st_tcb_at_def: "st_tcb_at test \<equiv> obj_at (\<lambda>ko. \<exists>tcb.
 
 text {* An alternative formulation that allows abstraction over type: *}
 
-datatype aa_type =
-    AASIDPool
-  | APageTable
-  | APageDirectory
-  | AIntData vmpage_size
 
 datatype a_type =
     ATCB
@@ -152,30 +140,11 @@ where
          | TCB tcb                  \<Rightarrow> ATCB
          | Endpoint endpoint        \<Rightarrow> AEndpoint
          | Notification notification   \<Rightarrow> ANTFN
-         | ArchObj ao               \<Rightarrow> AArch (case ao of
-           PageTable pt             \<Rightarrow> APageTable
-         | PageDirectory pd         \<Rightarrow> APageDirectory
-         | DataPage sz              \<Rightarrow> AIntData sz
-         | Arch_Structs_A.ASIDPool f \<Rightarrow> AASIDPool)"
+         | ArchObj ao               \<Rightarrow> AArch (aa_type ao)"
 
 abbreviation
   "typ_at T \<equiv> obj_at (\<lambda>ob. a_type ob = T)"
 
-(* this time with typ_at. might lead to confusion, but this is how
-   the rest should have been defined.. *)
-abbreviation
-  "asid_pool_at \<equiv> typ_at (AArch AASIDPool)"
-abbreviation
-  "page_table_at \<equiv> typ_at (AArch APageTable)"
-abbreviation
-  "page_directory_at \<equiv> typ_at (AArch APageDirectory)"
-
-definition
-  "pde_at p \<equiv> page_directory_at (p && ~~ mask pd_bits)
-                  and K (is_aligned p 2)"
-definition
-  "pte_at p \<equiv> page_table_at (p && ~~ mask pt_bits)
-                  and K (is_aligned p 2)"
 
 text {* cte with property at *}
 
@@ -252,8 +221,6 @@ definition
   "cap_aligned c \<equiv>
    is_aligned (obj_ref_of c) (cap_bits c) \<and> cap_bits c < word_bits"
 
-definition
-  "vmsz_aligned ref sz \<equiv> is_aligned ref (pageBitsForSize sz)"
 
 text {*
   Below, we define several predicates for capabilities on the abstract specification.
@@ -265,28 +232,6 @@ text {*
   Eventually, we will combine all predicates into @{text valid_cap}.
 *}
 
-definition
-  "wellformed_mapdata sz \<equiv>
-   \<lambda>(asid, vref). 0 < asid \<and> asid \<le> 2^asid_bits - 1
-                \<and> vmsz_aligned vref sz \<and> vref < kernel_base"
-
-datatype capclass =
-  PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass
-
-definition
-  wellformed_acap :: "arch_cap \<Rightarrow> bool"
-where
-  "wellformed_acap ac \<equiv>
-   case ac of
-     Arch_Structs_A.ASIDPoolCap r as
-       \<Rightarrow> is_aligned as asid_low_bits \<and> as \<le> 2^asid_bits - 1
-   | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> rghts \<in> valid_vm_rights \<and>
-     case_option True (wellformed_mapdata sz) mapdata
-   | Arch_Structs_A.PageTableCap r (Some mapdata) \<Rightarrow>
-     wellformed_mapdata ARMSection mapdata
-   | Arch_Structs_A.PageDirectoryCap r (Some asid) \<Rightarrow>
-     0 < asid \<and> asid \<le> 2^asid_bits - 1
-   | _ \<Rightarrow> True"
 
 definition
   wellformed_cap :: "cap \<Rightarrow> bool"
@@ -318,12 +263,7 @@ where
   | Structures_A.IRQHandlerCap irq \<Rightarrow> True
   | Structures_A.Zombie r b n \<Rightarrow>
       (case b of None \<Rightarrow> tcb_at r s | Some b \<Rightarrow> cap_table_at b r s)
-  | Structures_A.ArchObjectCap ac \<Rightarrow> (case ac of
-    Arch_Structs_A.ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s
-  | Arch_Structs_A.ASIDControlCap \<Rightarrow> True
-  | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> typ_at (AArch (AIntData sz)) r s
-  | Arch_Structs_A.PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s
-  | Arch_Structs_A.PageDirectoryCap r mapdata\<Rightarrow>typ_at(AArch APageDirectory) r s)"
+  | Structures_A.ArchObjectCap ac \<Rightarrow> valid_arch_cap_ref ac s"
 
 
 definition
@@ -345,39 +285,13 @@ where
   | Structures_A.Zombie r b n \<Rightarrow>
          (case b of None \<Rightarrow> tcb_at r s \<and> n \<le> 5
                   | Some b \<Rightarrow> cap_table_at b r s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0)
-  | Structures_A.ArchObjectCap ac \<Rightarrow> (case ac of
-    Arch_Structs_A.ASIDPoolCap r as \<Rightarrow>
-         typ_at (AArch AASIDPool) r s \<and> is_aligned as asid_low_bits
-           \<and> as \<le> 2^asid_bits - 1
-  | Arch_Structs_A.ASIDControlCap \<Rightarrow> True
-  | Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow>
-    typ_at (AArch (AIntData sz)) r s \<and> rghts \<in> valid_vm_rights \<and>
-    (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2^asid_bits - 1
-                                             \<and> vmsz_aligned ref sz \<and> ref < kernel_base)
-  | Arch_Structs_A.PageTableCap r mapdata \<Rightarrow>
-    typ_at (AArch APageTable) r s \<and>
-    (case mapdata of None \<Rightarrow> True
-       | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ asid_bits - 1
-                                \<and> vref < kernel_base
-                                \<and> is_aligned vref (pageBitsForSize ARMSection))
-  | Arch_Structs_A.PageDirectoryCap r mapdata \<Rightarrow>
-    typ_at (AArch APageDirectory) r s \<and>
-    case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata))"
+  | Structures_A.ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s)"
 
 abbreviation
   valid_cap_syn :: "'z::state_ext state \<Rightarrow> cap \<Rightarrow> bool" ("_ \<turnstile> _" [60, 60] 61)
 where
   "s \<turnstile> c \<equiv> valid_cap c s"
 
-primrec
-  acap_class :: "arch_cap \<Rightarrow> capclass"
-where
-  "acap_class (arch_cap.ASIDPoolCap x y)      = PhysicalClass"
-| "acap_class (arch_cap.ASIDControlCap)       = ASIDMasterClass"
-| "acap_class (arch_cap.PageCap x y sz z)     = PhysicalClass"
-| "acap_class (arch_cap.PageTableCap x y)     = PhysicalClass"
-| "acap_class (arch_cap.PageDirectoryCap x y) = PhysicalClass"
-
 primrec
   cap_class :: "cap \<Rightarrow> capclass"
 where
@@ -441,15 +355,7 @@ where
     tcb_cnode_index 4 \<mapsto> (tcb_ipcframe, tcb_ipcframe_update,
                           (\<lambda>_ _. is_arch_cap or (op = cap.NullCap)))]"
 
-definition
-  valid_ipc_buffer_cap :: "cap \<Rightarrow> word32 \<Rightarrow> bool"
-where
-  "valid_ipc_buffer_cap c bufptr \<equiv>
-         case c of
-              cap.ArchObjectCap (arch_cap.PageCap ref rghts sz mapdata) \<Rightarrow>
-                   is_aligned bufptr msg_align_bits
 
-            | _ \<Rightarrow> True"
 
 definition
   valid_fault :: "ExceptionTypes_A.fault \<Rightarrow> bool"
@@ -524,80 +430,6 @@ where
 
 
 
-definition
-  kernel_mapping_slots :: "12 word set" where
- "kernel_mapping_slots \<equiv> {x. x \<ge> ucast (kernel_base >> 20)}"
-
-definition
-  equal_kernel_mappings :: "'z::state_ext state \<Rightarrow> bool"
-where
- "equal_kernel_mappings \<equiv> \<lambda>s.
-    \<forall>x y pd pd'. ko_at (ArchObj (PageDirectory pd)) x s
-         \<and> ko_at (ArchObj (PageDirectory pd')) y s
-       \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)"
-
-primrec
-  valid_pte :: "Arch_Structs_A.pte \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_pte (Arch_Structs_A.InvalidPTE) = \<top>"
-| "valid_pte (Arch_Structs_A.LargePagePTE ptr x y) =
-   (\<lambda>s. is_aligned ptr pageBits \<and>
-        typ_at (AArch (AIntData ARMLargePage)) (Platform.ptrFromPAddr ptr) s)"
-| "valid_pte (Arch_Structs_A.SmallPagePTE ptr x y) =
-   (\<lambda>s. is_aligned ptr pageBits \<and>
-        typ_at (AArch (AIntData ARMSmallPage)) (Platform.ptrFromPAddr ptr) s)"
-
-primrec
-  valid_pde :: "Arch_Structs_A.pde \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_pde (Arch_Structs_A.InvalidPDE) = \<top>"
-| "valid_pde (Arch_Structs_A.SectionPDE ptr x y z) =
-   (\<lambda>s. is_aligned ptr pageBits \<and>
-        typ_at (AArch (AIntData ARMSection)) (Platform.ptrFromPAddr ptr) s)"
-| "valid_pde (Arch_Structs_A.SuperSectionPDE ptr x z) =
-   (\<lambda>s. is_aligned ptr pageBits \<and>
-        typ_at (AArch (AIntData ARMSuperSection))
-               (Platform.ptrFromPAddr ptr) s)"
-| "valid_pde (Arch_Structs_A.PageTablePDE ptr x z) =
-   (typ_at (AArch APageTable) (Platform.ptrFromPAddr ptr))"
-
-primrec
-  valid_arch_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_arch_obj (Arch_Structs_A.ASIDPool pool) =
-   (\<lambda>s. \<forall>x \<in> ran pool. typ_at (AArch APageDirectory) x s)"
-| "valid_arch_obj (Arch_Structs_A.PageDirectory pd) =
-   (\<lambda>s. \<forall>x \<in> -kernel_mapping_slots. valid_pde (pd x) s)"
-| "valid_arch_obj (Arch_Structs_A.PageTable pt) = (\<lambda>s. \<forall>x. valid_pte (pt x) s)"
-| "valid_arch_obj (DataPage sz) = \<top>"
-
-definition
-  wellformed_pte :: "Arch_Structs_A.pte \<Rightarrow> bool"
-where
-  "wellformed_pte pte \<equiv> case pte of
-     Arch_Structs_A.pte.LargePagePTE p attr r \<Rightarrow>
-       ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
-   | Arch_Structs_A.pte.SmallPagePTE p attr r \<Rightarrow>
-       ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
-   | _ \<Rightarrow> True"
-
-definition
-  wellformed_pde :: "Arch_Structs_A.pde \<Rightarrow> bool"
-where
-  "wellformed_pde pde \<equiv> case pde of
-     Arch_Structs_A.pde.PageTablePDE p attr mw \<Rightarrow> attr \<subseteq> {ParityEnabled}
-   | Arch_Structs_A.pde.SectionPDE p attr mw r \<Rightarrow> r \<in> valid_vm_rights
-   | Arch_Structs_A.pde.SuperSectionPDE p attr r \<Rightarrow> r \<in> valid_vm_rights
-   | _ \<Rightarrow> True"
-
-definition
-  wellformed_arch_obj :: "arch_kernel_obj \<Rightarrow> bool"
-where
-  "wellformed_arch_obj ao \<equiv> case ao of
-     PageTable pt \<Rightarrow> (\<forall>pte\<in>range pt. wellformed_pte pte)
-   | PageDirectory pd \<Rightarrow> (\<forall>pde\<in>range pd. wellformed_pde pde)
-   | _ \<Rightarrow> True"
-
 definition
   valid_obj :: "obj_ref \<Rightarrow> Structures_A.kernel_object \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
 where
@@ -613,293 +445,7 @@ definition
 where
   "valid_objs s \<equiv> \<forall>ptr \<in> dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s"
 
-definition
-  pde_ref :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
-where
-  "pde_ref pde \<equiv> case pde of
-    Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
-  | _ \<Rightarrow> None"
 
-datatype vs_ref = VSRef word32 "aa_type option"
-
-definition
-  vs_ref_atype :: "vs_ref \<Rightarrow> aa_type option" where
- "vs_ref_atype vsref \<equiv> case vsref of VSRef x atype \<Rightarrow> atype"
-
-definition
-  vs_refs :: "Structures_A.kernel_object \<Rightarrow> (vs_ref \<times> obj_ref) set" where
-  "vs_refs \<equiv> \<lambda>ko. case ko of
-    ArchObj (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
-      (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
-  | ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
-      (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
-      graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
-  | _ \<Rightarrow> {}"
-
-type_synonym vs_chain = "vs_ref list \<times> obj_ref"
-type_synonym 'a rel = "('a \<times> 'a) set"
-
-definition
-  vs_lookup1 :: "'z::state_ext state \<Rightarrow> vs_chain rel" where
-  "vs_lookup1 s \<equiv> {((rs,p),(rs',p')). \<exists>ko r. ko_at ko p s
-                                      \<and> rs' = (r # rs)
-                                      \<and> (r, p') \<in> vs_refs ko}"
-
-abbreviation (input)
-  vs_lookup_trans :: "'z::state_ext state \<Rightarrow> vs_chain rel" where
-  "vs_lookup_trans s \<equiv> (vs_lookup1 s)^*"
-
-abbreviation
-  vs_lookup1_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-  ("_ \<rhd>1 _" [80,80] 81) where
-  "ref \<rhd>1 ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup1 s"
-
-abbreviation
-  vs_lookup_trans_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-  ("_ \<rhd>* _" [80,80] 81) where
-  "ref \<rhd>* ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_trans s"
-
-definition
-  vs_asid_refs :: "(word8 \<rightharpoonup> obj_ref) \<Rightarrow> vs_chain set"
-where
-  "vs_asid_refs t \<equiv> (\<lambda>(r,p). ([VSRef (ucast r) None], p)) ` graph_of t"
-
-definition
-  vs_lookup :: "'z::state_ext state \<Rightarrow> vs_chain set"
-where
-  "vs_lookup \<equiv> \<lambda>s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
-
-abbreviation
-  vs_lookup_abbr :: "vs_ref list \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-  ("_ \<rhd> _" [80,80] 81) where
-  "rs \<rhd> p \<equiv> \<lambda>s. (rs,p) \<in> vs_lookup s"
-
-abbreviation
-  is_reachable_abbr :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" ("\<exists>\<rhd> _" [80] 81) where
-  "\<exists>\<rhd> p \<equiv> \<lambda>s. \<exists>ref. (ref \<rhd> p) s"
-
-definition
-  valid_arch_objs :: "'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_arch_objs \<equiv> \<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ko_at (ArchObj ao) p s \<longrightarrow> valid_arch_obj ao s"
-
-definition
-  pde_ref_pages :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
-where
-  "pde_ref_pages pde \<equiv> case pde of
-    Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
-  | Arch_Structs_A.SectionPDE ptr x y z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
-  | Arch_Structs_A.SuperSectionPDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
-  | _ \<Rightarrow> None"
-
-definition
-  pte_ref_pages :: "Arch_Structs_A.pte \<Rightarrow> obj_ref option"
-where
-  "pte_ref_pages pte \<equiv> case pte of
-    Arch_Structs_A.SmallPagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
-  | Arch_Structs_A.LargePagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
-  | _ \<Rightarrow> None"
-
-definition
-  vs_refs_pages :: "Structures_A.kernel_object \<Rightarrow> (vs_ref \<times> obj_ref) set" where
-  "vs_refs_pages \<equiv> \<lambda>ko. case ko of
-    ArchObj (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
-      (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
-  | ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
-      (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
-      graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x))
-  | ArchObj (Arch_Structs_A.PageTable pt) \<Rightarrow>
-      (\<lambda>(r,p). (VSRef (ucast r) (Some APageTable), p)) `
-      graph_of (pte_ref_pages o pt)
-  | _ \<Rightarrow> {}"
-
-definition
-  vs_lookup_pages1 :: "'z :: state_ext state \<Rightarrow> vs_chain rel" where
-  "vs_lookup_pages1 s \<equiv> {((rs,p),(rs',p')). \<exists>ko r. ko_at ko p s
-                                          \<and> rs' = (r # rs)
-                                          \<and> (r, p') \<in> vs_refs_pages ko}"
-
-abbreviation (input)
-  vs_lookup_pages_trans :: "'z :: state_ext state \<Rightarrow> vs_chain rel" where
-  "vs_lookup_pages_trans s \<equiv> (vs_lookup_pages1 s)^*"
-
-abbreviation
-  vs_lookup_pages1_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
-  ("_ \<unrhd>1 _" [80,80] 81) where
-  "ref \<unrhd>1 ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_pages1 s"
-
-abbreviation
-  vs_lookup_pages_trans_abbr :: "vs_chain \<Rightarrow> vs_chain \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
-  ("_ \<unrhd>* _" [80,80] 81) where
-  "ref \<unrhd>* ref' \<equiv> \<lambda>s. (ref,ref') \<in> vs_lookup_pages_trans s"
-
-definition
-  vs_lookup_pages :: "'z ::state_ext state \<Rightarrow> vs_chain set"
-where
-  "vs_lookup_pages \<equiv> \<lambda>s. vs_lookup_pages_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
-
-abbreviation
-  vs_lookup_pages_abbr :: "vs_ref list \<Rightarrow> obj_ref \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool"
-  ("_ \<unrhd> _" [80,80] 81) where
-  "rs \<unrhd> p \<equiv> \<lambda>s. (rs,p) \<in> vs_lookup_pages s"
-
-abbreviation
-  is_reachable_pages_abbr :: "obj_ref \<Rightarrow> 'z :: state_ext state \<Rightarrow> bool" ("\<exists>\<unrhd> _" [80] 81) where
-  "\<exists>\<unrhd> p \<equiv> \<lambda>s. \<exists>ref. (ref \<unrhd> p) s"
-
-definition
-  pde_mapping_bits :: "nat"
-where
- "pde_mapping_bits \<equiv> pageBitsForSize ARMSection"
-
-definition
-  pte_mapping_bits :: "nat"
-where
- "pte_mapping_bits \<equiv> pageBitsForSize ARMSmallPage"
-
-definition
-  valid_pte_kernel_mappings :: "Arch_Structs_A.pte \<Rightarrow> vspace_ref
-                                   \<Rightarrow> arm_vspace_region_uses \<Rightarrow> bool"
-where
- "valid_pte_kernel_mappings pte vref uses \<equiv> case pte of
-    Arch_Structs_A.InvalidPTE \<Rightarrow>
-        \<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}.
-                    uses x \<noteq> ArmVSpaceKernelWindow
-  | Arch_Structs_A.SmallPagePTE ptr atts rghts \<Rightarrow>
-        Platform.ptrFromPAddr ptr = vref
-        \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
-             \<and> (use = ArmVSpaceKernelWindow
-                    \<or> use = ArmVSpaceDeviceWindow))
-        \<and> rghts = {}
-  | Arch_Structs_A.LargePagePTE ptr atts rghts \<Rightarrow>
-        Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMLargePage))
-        \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
-             \<and> (use = ArmVSpaceKernelWindow
-                    \<or> use = ArmVSpaceDeviceWindow))
-        \<and> rghts = {}"
-
-definition
-  valid_pt_kernel_mappings :: "vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
-where
- "valid_pt_kernel_mappings vref uses obj \<equiv> case obj of
-    ArchObj (PageTable pt) \<Rightarrow>
-        \<forall>x. valid_pte_kernel_mappings
-             (pt x) (vref + (ucast x << pte_mapping_bits)) uses
-  | _ \<Rightarrow> False"
-
-definition
-  valid_pde_kernel_mappings :: "Arch_Structs_A.pde \<Rightarrow> vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-where
- "valid_pde_kernel_mappings pde vref uses \<equiv> case pde of
-    Arch_Structs_A.InvalidPDE \<Rightarrow>
-        (\<lambda>s. \<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
-                    uses x \<noteq> ArmVSpaceKernelWindow)
-  | Arch_Structs_A.PageTablePDE ptr _ _ \<Rightarrow>
-        obj_at (valid_pt_kernel_mappings vref uses)
-                    (Platform.ptrFromPAddr ptr)
-  | Arch_Structs_A.SectionPDE ptr atts _ rghts \<Rightarrow>
-        (\<lambda>s. Platform.ptrFromPAddr ptr = vref
-             \<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}. uses x = use)
-                   \<and> (use = ArmVSpaceKernelWindow
-                            \<or> use = ArmVSpaceDeviceWindow))
-             \<and> rghts = {})
-  | Arch_Structs_A.SuperSectionPDE ptr atts rghts \<Rightarrow>
-        (\<lambda>s. Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMSuperSection))
-             \<and> (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
-                   uses x = ArmVSpaceKernelWindow)
-             \<and> rghts = {})"
-
-definition
-  valid_pd_kernel_mappings :: "arm_vspace_region_uses \<Rightarrow> 'z::state_ext state
-                                    \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
-where
- "valid_pd_kernel_mappings uses \<equiv> \<lambda>s obj.
-  case obj of
-    ArchObj (PageDirectory pd) \<Rightarrow>
-      (\<forall>x. valid_pde_kernel_mappings
-             (pd x) (ucast x << pde_mapping_bits) uses s)
-  | _ \<Rightarrow> False"
-
-definition
-  valid_global_pd_mappings :: "'z::state_ext state \<Rightarrow> bool"
-where
- "valid_global_pd_mappings \<equiv> \<lambda>s.
-  obj_at (valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s)
-    (arm_global_pd (arch_state s)) s"
-
-definition
-  valid_ao_at :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ko_at (ArchObj ao) p s \<and> valid_arch_obj ao s"
-
-definition
-  "valid_pde_mappings pde \<equiv> case pde of
-    Arch_Structs_A.SectionPDE ptr _ _ _ \<Rightarrow> is_aligned ptr pageBits
-  | Arch_Structs_A.SuperSectionPDE ptr _ _ \<Rightarrow> is_aligned ptr pageBits
-  | _ \<Rightarrow> True"
-
-definition
-  "empty_table S ko \<equiv>
-   case ko of
-     ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
-       \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> S) \<and>
-            valid_pde_mappings (pd x) \<and>
-            (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = Arch_Structs_A.InvalidPDE)
-   | ArchObj (Arch_Structs_A.PageTable pt) \<Rightarrow>
-         pt = (\<lambda>x. Arch_Structs_A.InvalidPTE)
-   | _ \<Rightarrow> False"
-
-definition
-  "valid_kernel_mappings_if_pd S ko \<equiv> case ko of
-    ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
-        \<forall>x r. pde_ref (pd x) = Some r
-                  \<longrightarrow> ((r \<in> S) = (x \<in> kernel_mapping_slots))
-  | _ \<Rightarrow> True"
-
-definition
-  "aligned_pte pte \<equiv>
-     case pte of
-       Arch_Structs_A.LargePagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMLargePage
-     | Arch_Structs_A.SmallPagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMSmallPage
-     | _ \<Rightarrow> True"
-
-lemmas aligned_pte_simps[simp] =
-       aligned_pte_def[split_simps Arch_Structs_A.pte.split]
-
-definition
-  valid_global_objs :: "'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_global_objs \<equiv>
-  \<lambda>s. valid_ao_at (arm_global_pd (arch_state s)) s \<and>
-           obj_at (empty_table (set (arm_global_pts (arch_state s))))
-                  (arm_global_pd (arch_state s)) s \<and>
-      (\<forall>p\<in>set (arm_global_pts (arch_state s)).
-          \<exists>pt. ko_at (ArchObj (PageTable pt)) p s \<and> (\<forall>x. aligned_pte (pt x)))"
-
-definition
-  valid_asid_table :: "(word8 \<rightharpoonup> obj_ref) \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_asid_table table \<equiv> \<lambda>s. (\<forall>p \<in> ran table. asid_pool_at p s) \<and>
-                                inj_on table (dom table)"
-
-definition
-  valid_global_pts :: "'z :: state_ext state \<Rightarrow> bool"
-where
-  "valid_global_pts \<equiv> \<lambda>s.
-   \<forall>p \<in> set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s"
-(* this property now follows from valid_global_objs:
-   "valid_global_objs s \<Longrightarrow> valid_global_pts s" *)
-
-definition
-  valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_arch_state \<equiv> \<lambda>s.
-  typ_at (AArch (AIntData ARMSmallPage)) (arm_globals_frame (arch_state s)) s \<and>
-  valid_asid_table (arm_asid_table (arch_state s)) s \<and>
-  page_directory_at (arm_global_pd (arch_state s)) s \<and>
-  valid_global_pts s \<and>
-  is_inv (arm_hwasid_table (arch_state s))
-             (option_map fst o arm_asid_map (arch_state s))"
 
 definition
   pd_at_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
@@ -1013,15 +559,6 @@ where
          {x .. x + (2 ^ obj_bits ko - 1)} \<inter>
          {y .. y + (2 ^ obj_bits ko' - 1)} = {}"
 
-text "objects live in the kernel window"
-definition
-  pspace_in_kernel_window :: "'z::state_ext state \<Rightarrow> bool"
-where
- "pspace_in_kernel_window \<equiv> \<lambda>s.
-    \<forall>x ko. kheap s x = Some ko \<longrightarrow>
-       (\<forall>y \<in> {x .. x + (2 ^ obj_bits ko) - 1}.
-             arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow)"
-
 primrec
   live :: "Structures_A.kernel_object \<Rightarrow> bool"
 where
@@ -1061,6 +598,13 @@ where
                          then Some (THE cap. fst (get_cap p s) = {(cap, s)})
                          else None)"
 
+lemma arch_caps_of_state_def2:
+  "arch_caps_of_state s = (\<lambda>p. case caps_of_state s p of Some (ArchObjectCap ac) \<Rightarrow> Some ac | _ \<Rightarrow> None)"
+  apply (simp add: arch_caps_of_state_def caps_of_state_def)
+  apply (rule ext)
+  apply (simp split: if_splits cap.splits)
+  by (safe; simp)
+
 primrec
   cte_refs :: "cap \<Rightarrow> (irq \<Rightarrow> obj_ref) \<Rightarrow> cslot_ptr set"
 where
@@ -1240,13 +784,13 @@ definition
 where
   "valid_refs R \<equiv> \<lambda>s. \<forall>cref. \<not>cte_wp_at (\<lambda>c. R \<inter> cap_range c \<noteq> {}) cref s"
 
+text "caps point at objects in the kernel window"
 definition
-  global_refs :: "'z::state_ext state \<Rightarrow> obj_ref set"
+  cap_refs_in_kernel_window :: "'z::state_ext state \<Rightarrow> bool"
 where
-  "global_refs \<equiv> \<lambda>s.
-  {idle_thread s, arm_globals_frame (arch_state s), arm_global_pd (arch_state s)} \<union>
-   range (interrupt_irq_node s) \<union>
-   set (arm_global_pts (arch_state s))"
+ "cap_refs_in_kernel_window \<equiv> \<lambda>s. valid_refs
+         {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} s"
+
 
 definition
   valid_global_refs :: "'z::state_ext state \<Rightarrow> bool"
@@ -1275,131 +819,7 @@ definition valid_irq_states :: "'z::state_ext state \<Rightarrow> bool" where
   "valid_irq_states \<equiv> \<lambda>s.
     valid_irq_masks (interrupt_states s) (irq_masks (machine_state s))"
 
-text "caps point at objects in the kernel window"
-definition
-  cap_refs_in_kernel_window :: "'z::state_ext state \<Rightarrow> bool"
-where
- "cap_refs_in_kernel_window \<equiv> \<lambda>s. valid_refs
-         {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} s"
 
-definition
-  vs_cap_ref :: "cap \<Rightarrow> vs_ref list option"
-where
-  "vs_cap_ref cap \<equiv> case cap of
-   Structures_A.ArchObjectCap (Arch_Structs_A.ASIDPoolCap _ asid) \<Rightarrow>
-     Some [VSRef (ucast (asid_high_bits_of asid)) None]
- | Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow>
-     Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-           VSRef (ucast (asid_high_bits_of asid)) None]
- | Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ (Some (asid, vptr))) \<Rightarrow>
-     Some [VSRef (vptr >> 20) (Some APageDirectory),
-           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-           VSRef (ucast (asid_high_bits_of asid)) None]
- | Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMSmallPage (Some (asid, vptr))) \<Rightarrow>
-     Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
-           VSRef (vptr >> 20) (Some APageDirectory),
-           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-           VSRef (ucast (asid_high_bits_of asid)) None]
- | Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMLargePage (Some (asid, vptr))) \<Rightarrow>
-     Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
-           VSRef (vptr >> 20) (Some APageDirectory),
-           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-           VSRef (ucast (asid_high_bits_of asid)) None]
- | Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMSection (Some (asid, vptr))) \<Rightarrow>
-     Some [VSRef (vptr >> 20) (Some APageDirectory),
-           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-           VSRef (ucast (asid_high_bits_of asid)) None]
- | Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMSuperSection (Some (asid, vptr))) \<Rightarrow>
-     Some [VSRef (vptr >> 20) (Some APageDirectory),
-           VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-           VSRef (ucast (asid_high_bits_of asid)) None]
- | _ \<Rightarrow> None"
-
-definition
-  "is_pg_cap cap \<equiv> \<exists>p R sz m. cap =
-   cap.ArchObjectCap (arch_cap.PageCap p R sz m)"
-
-definition
-  "is_pd_cap c \<equiv>
-   \<exists>p asid. c = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid)"
-
-definition
-  "is_pt_cap c \<equiv> \<exists>p asid. c = cap.ArchObjectCap (arch_cap.PageTableCap p asid)"
-
-definition
-  "cap_asid cap \<equiv> case cap of
-    Structures_A.ArchObjectCap (Arch_Structs_A.PageCap _ _ _ (Some (asid, _))) \<Rightarrow> Some asid
-  | Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
-  | Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
-  | _ \<Rightarrow> None"
-
-  (* needed for retype: if reachable, then cap, if cap then protected by untyped cap.
-     strengthened for preservation in cap delete: ref in cap must unmap the right objects *)
-definition
-  "valid_vs_lookup \<equiv> \<lambda>s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow>
-  ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
-  (\<exists>p' cap. caps_of_state s p' = Some cap \<and>
-            p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)"
-
-  (* needed for map: installing new object should add only one mapping *)
-definition
-  "valid_table_caps \<equiv> \<lambda>s.
-  \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow>
-            (is_pd_cap cap \<or> is_pt_cap cap) \<longrightarrow>
-            cap_asid cap = None \<longrightarrow>
-            r \<in> obj_refs cap \<longrightarrow>
-            obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s"
-
-  (* needed to preserve valid_table_caps in map *)
-definition
-  "unique_table_caps \<equiv> \<lambda>cs. \<forall>p p' cap cap'.
-  cs p = Some cap \<longrightarrow> cs p' = Some cap' \<longrightarrow>
-  cap_asid cap = None \<longrightarrow>
-  obj_refs cap' = obj_refs cap \<longrightarrow>
-  (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and>
-  (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)"
-
-definition
-  table_cap_ref :: "cap \<Rightarrow> vs_ref list option"
-where
-  "table_cap_ref cap \<equiv> case cap of
-     Structures_A.ArchObjectCap (Arch_Structs_A.ASIDPoolCap _ asid) \<Rightarrow>
-       Some [VSRef (ucast (asid_high_bits_of asid)) None]
-   | Structures_A.ArchObjectCap
-       (Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow>
-       Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-             VSRef (ucast (asid_high_bits_of asid)) None]
-   | Structures_A.ArchObjectCap
-       (Arch_Structs_A.PageTableCap _ (Some (asid, vptr))) \<Rightarrow>
-       Some [VSRef (vptr >> 20) (Some APageDirectory),
-             VSRef (asid && mask asid_low_bits) (Some AASIDPool),
-             VSRef (ucast (asid_high_bits_of asid)) None]
-   | _ \<Rightarrow> None"
-
-  (* needed to avoid a single page insertion
-     resulting in multiple valid lookups *)
-definition
-  "unique_table_refs \<equiv> \<lambda>cs. \<forall>p p' cap cap'.
-  cs p = Some cap \<longrightarrow> cs p' = Some cap' \<longrightarrow>
-  obj_refs cap' = obj_refs cap \<longrightarrow>
-  table_cap_ref cap' = table_cap_ref cap"
-
-definition
-  valid_kernel_mappings :: "'z::state_ext state \<Rightarrow> bool"
-where
-  "valid_kernel_mappings \<equiv>
-     \<lambda>s. \<forall>ko \<in> ran (kheap s).
-          valid_kernel_mappings_if_pd
-             (set (arm_global_pts (arch_state s))) ko"
-
-definition
-  "valid_arch_caps \<equiv> valid_vs_lookup and valid_table_caps and
-                     (\<lambda>s. unique_table_caps (caps_of_state s)
-                        \<and> unique_table_refs (caps_of_state s))"
-
-definition
-  "valid_machine_state \<equiv>
-   \<lambda>s. \<forall>p. in_user_frame p (s::'z::state_ext state) \<or> underlying_memory (machine_state s) p = 0"
 
 definition
   valid_state :: "'z::state_ext state \<Rightarrow> bool"
@@ -1462,6 +882,7 @@ definition
 where
  "obj_irq_refs cap \<equiv> (Inl ` obj_refs cap) \<union> (Inr ` cap_irqs cap)"
 
+
 definition
   "obj_bits_type T \<equiv> case T of
     ACapTable n \<Rightarrow> 4 + n
@@ -1469,11 +890,7 @@ definition
   | ATCB \<Rightarrow> obj_bits (TCB undefined)
   | AEndpoint \<Rightarrow> obj_bits (Endpoint undefined)
   | ANTFN \<Rightarrow> obj_bits (Notification undefined)
-  | AArch T' \<Rightarrow> (case T' of
-    AASIDPool \<Rightarrow> obj_bits (ArchObj (Arch_Structs_A.ASIDPool undefined))
-  | AIntData sz \<Rightarrow> obj_bits (ArchObj (DataPage sz))
-  | APageDirectory \<Rightarrow> obj_bits (ArchObj (Arch_Structs_A.PageDirectory undefined))
-  | APageTable \<Rightarrow> obj_bits (ArchObj (Arch_Structs_A.PageTable undefined)))"
+  | AArch T' \<Rightarrow> arch_obj_bits_type T'"
 
 definition
   "typ_range p T \<equiv> {p .. p + 2^obj_bits_type T - 1}"
@@ -1537,122 +954,13 @@ lemma valid_bound_tcb_Some[simp]:
   "valid_bound_tcb (Some x) = tcb_at x"
   by (auto simp: valid_bound_tcb_def)
 
-lemmas wellformed_acap_simps =
-  wellformed_mapdata_def wellformed_acap_def[split_simps arch_cap.split]
-
 lemmas wellformed_cap_simps =
   wellformed_acap_simps wellformed_cap_def[split_simps cap.split]
 
-lemmas valid_cap_ref_simps' =
-  valid_cap_ref_def[split_simps cap.split arch_cap.split]
-
-(*Pure wizardry*)
-lemma valid_cap_ref_simps :
-  "valid_cap_ref NullCap (s\<Colon>'z_1\<Colon>state_ext state) = True \<and>
-valid_cap_ref (UntypedCap (x\<Colon>word32) (xa\<Colon>nat) (xb\<Colon>nat)) (sa\<Colon>'z_1\<Colon>state_ext state) =
-(valid_untyped (UntypedCap x xa xb) sa \<and> xb \<le> (2\<Colon>nat) ^ xa \<and> x \<noteq> (0\<Colon>word32)) \<and>
-valid_cap_ref (EndpointCap (xc\<Colon>word32) (xd\<Colon>word32) (xe\<Colon>rights set))
- (sb\<Colon>'z_1\<Colon>state_ext state) =
-ep_at xc sb \<and>
-valid_cap_ref (NotificationCap (xf\<Colon>word32) (xg\<Colon>word32) (xh\<Colon>rights set))
- (sc\<Colon>'z_1\<Colon>state_ext state) =
-ntfn_at xf sc \<and>
-valid_cap_ref (ReplyCap (xi\<Colon>word32) (xj\<Colon>bool)) (sd\<Colon>'z_1\<Colon>state_ext state) =
-tcb_at xi sd \<and>
-valid_cap_ref (CNodeCap (xk\<Colon>word32) (xl\<Colon>nat) (xm\<Colon>bool list))
- (se\<Colon>'z_1\<Colon>state_ext state) =
-cap_table_at xl xk se \<and>
-valid_cap_ref (ThreadCap (xn\<Colon>word32)) (sf\<Colon>'z_1\<Colon>state_ext state) = tcb_at xn sf \<and>
-valid_cap_ref DomainCap (sp\<Colon>'z_1\<Colon>state_ext state) = True \<and>
-valid_cap_ref IRQControlCap (sg\<Colon>'z_1\<Colon>state_ext state) = True \<and>
-valid_cap_ref (IRQHandlerCap (xo\<Colon>word8)) (sh\<Colon>'z_1\<Colon>state_ext state) = True \<and>
-valid_cap_ref (Zombie (xp\<Colon>word32) (xq\<Colon>nat option) (xr\<Colon>nat))
- (si\<Colon>'z_1\<Colon>state_ext state) =
-(case xq of None \<Rightarrow> tcb_at xp si | Some (b\<Colon>nat) \<Rightarrow> cap_table_at b xp si) \<and>
-valid_cap_ref (ArchObjectCap (ASIDPoolCap (xs\<Colon>word32) (xt\<Colon>word32)))
- (sj\<Colon>'z_1\<Colon>state_ext state) =
-asid_pool_at xs sj \<and>
-valid_cap_ref (ArchObjectCap ASIDControlCap) (sk\<Colon>'z_1\<Colon>state_ext state) = True \<and>
-valid_cap_ref
- (ArchObjectCap
-   (PageCap (xu\<Colon>word32) (xv\<Colon>rights set) (xw\<Colon>vmpage_size)
-     (xx\<Colon>(word32 \<times> word32) option)))
- (sl\<Colon>'z_1\<Colon>state_ext state) =
-typ_at (AArch (AIntData xw)) xu sl \<and>
-valid_cap_ref
- (ArchObjectCap (PageTableCap (xy\<Colon>word32) (xz\<Colon>(word32 \<times> word32) option)))
- (sm\<Colon>'z_1\<Colon>state_ext state) =
-page_table_at xy sm \<and>
-valid_cap_ref (ArchObjectCap (PageDirectoryCap (ya\<Colon>word32) (yb\<Colon>word32 option)))
- (sn\<Colon>'z_1\<Colon>state_ext state) =
-page_directory_at ya sn"
-  by (rule valid_cap_ref_simps')
-
-lemmas valid_cap_simps' = valid_cap_def[split_simps cap.split arch_cap.split]
-
-lemma valid_cap_simps :
-  "(s\<Colon>'z_1\<Colon>state_ext state) \<turnstile> NullCap = (cap_aligned NullCap \<and> True) \<and>
-(sa\<Colon>'z_1\<Colon>state_ext state) \<turnstile> UntypedCap (x\<Colon>word32) (xa\<Colon>nat) (xb\<Colon>nat) =
-(cap_aligned (UntypedCap x xa xb) \<and>
- valid_untyped (UntypedCap x xa xb) sa \<and>
- (4\<Colon>nat) \<le> xa \<and> xb \<le> (2\<Colon>nat) ^ xa \<and> x \<noteq> (0\<Colon>word32)) \<and>
-(sb\<Colon>'z_1\<Colon>state_ext state) \<turnstile> EndpointCap (xc\<Colon>word32) (xd\<Colon>word32) (xe\<Colon>rights set) =
-(cap_aligned (EndpointCap xc xd xe) \<and> ep_at xc sb) \<and>
-(sc\<Colon>'z_1\<Colon>state_ext state) \<turnstile> NotificationCap (xf\<Colon>word32) (xg\<Colon>word32)
-                        (xh\<Colon>rights set) =
-(cap_aligned (NotificationCap xf xg xh) \<and> ntfn_at xf sc \<and> AllowGrant \<notin> xh) \<and>
-(sd\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ReplyCap (xi\<Colon>word32) (xj\<Colon>bool) =
-(cap_aligned (ReplyCap xi xj) \<and> tcb_at xi sd) \<and>
-(se\<Colon>'z_1\<Colon>state_ext state) \<turnstile> CNodeCap (xk\<Colon>word32) (xl\<Colon>nat) (xm\<Colon>bool list) =
-(cap_aligned (CNodeCap xk xl xm) \<and>
- cap_table_at xl xk se \<and> xl \<noteq> (0\<Colon>nat) \<and> length xm \<le> (32\<Colon>nat)) \<and>
-(sf\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ThreadCap (xn\<Colon>word32) =
-(cap_aligned (ThreadCap xn) \<and> tcb_at xn sf) \<and>
-(sp\<Colon>'z_1\<Colon>state_ext state) \<turnstile> DomainCap = (cap_aligned DomainCap \<and> True) \<and>
-(sg\<Colon>'z_1\<Colon>state_ext state) \<turnstile> IRQControlCap = (cap_aligned IRQControlCap \<and> True) \<and>
-(sh\<Colon>'z_1\<Colon>state_ext state) \<turnstile> IRQHandlerCap (xo\<Colon>word8) =
-(cap_aligned (IRQHandlerCap xo) \<and> xo \<le> maxIRQ) \<and>
-(si\<Colon>'z_1\<Colon>state_ext state) \<turnstile> Zombie (xp\<Colon>word32) (xq\<Colon>nat option) (xr\<Colon>nat) =
-(cap_aligned (Zombie xp xq xr) \<and>
- (case xq of None \<Rightarrow> tcb_at xp si \<and> xr \<le> (5\<Colon>nat)
-  | Some (b\<Colon>nat) \<Rightarrow> cap_table_at b xp si \<and> xr \<le> (2\<Colon>nat) ^ b \<and> b \<noteq> (0\<Colon>nat))) \<and>
-(sj\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ArchObjectCap (ASIDPoolCap (xs\<Colon>word32) (xt\<Colon>word32)) =
-(cap_aligned (ArchObjectCap (ASIDPoolCap xs xt)) \<and>
- asid_pool_at xs sj \<and>
- is_aligned xt asid_low_bits \<and> xt \<le> (2\<Colon>word32) ^ asid_bits - (1\<Colon>word32)) \<and>
-(sk\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ArchObjectCap ASIDControlCap =
-(cap_aligned (ArchObjectCap ASIDControlCap) \<and> True) \<and>
-(sl\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ArchObjectCap
-                        (PageCap (xu\<Colon>word32) (xv\<Colon>rights set) (xw\<Colon>vmpage_size)
-                          (xx\<Colon>(word32 \<times> word32) option)) =
-(cap_aligned (ArchObjectCap (PageCap xu xv xw xx)) \<and>
- typ_at (AArch (AIntData xw)) xu sl \<and>
- xv \<in> valid_vm_rights \<and>
- (case xx of None \<Rightarrow> True
-  | Some (asid, ref\<Colon>word32) \<Rightarrow>
-      (0\<Colon>word32) < asid \<and>
-      asid \<le> (2\<Colon>word32) ^ asid_bits - (1\<Colon>word32) \<and>
-      vmsz_aligned ref xw \<and> ref < kernel_base)) \<and>
-(sm\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ArchObjectCap
-                        (PageTableCap (xy\<Colon>word32)
-                          (xz\<Colon>(word32 \<times> word32) option)) =
-(cap_aligned (ArchObjectCap (PageTableCap xy xz)) \<and>
- page_table_at xy sm \<and>
- (case xz of None \<Rightarrow> True
-  | Some (asid, vref\<Colon>word32) \<Rightarrow>
-      (0\<Colon>word32) < asid \<and>
-      asid \<le> (2\<Colon>word32) ^ asid_bits - (1\<Colon>word32) \<and>
-      vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))) \<and>
-(sn\<Colon>'z_1\<Colon>state_ext state) \<turnstile> ArchObjectCap
-                        (PageDirectoryCap (ya\<Colon>word32) (yb\<Colon>word32 option)) =
-(cap_aligned (ArchObjectCap (PageDirectoryCap ya yb)) \<and>
- page_directory_at ya sn \<and>
- (case yb of None \<Rightarrow> True
-  | Some (asid\<Colon>word32) \<Rightarrow>
-      (0\<Colon>word32) < asid \<and> asid \<le> (2\<Colon>word32) ^ asid_bits - (1\<Colon>word32)))"
- by (rule valid_cap_simps')
-
+lemmas valid_cap_ref_simps =
+  valid_cap_ref_def[split_simps cap.split]
 
+lemmas valid_cap_simps = valid_cap_def[split_simps cap.split]
 
 lemma is_ep:
   "is_ep ko = (\<exists>ep. ko = Endpoint ep)"
@@ -1747,9 +1055,7 @@ lemma cte_at_def:
   "cte_at p s \<equiv> \<exists>cap. fst (get_cap p s) = {(cap,s)}"
   by (simp add: cte_wp_at_def)
 
-lemma vmsz_aligned_ARMSection:
-  "vmsz_aligned vref ARMSection = is_aligned vref (pageBitsForSize ARMSection)"
-  by (simp add: vmsz_aligned_def pageBitsForSize_def)
+
 
 lemma valid_cap_def2:
   "s \<turnstile> c \<equiv> cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s"
@@ -1759,12 +1065,7 @@ lemma valid_cap_def2:
                                valid_cap_ref_simps
                         split: option.splits)
     apply (fastforce+)[4]
-  apply (rename_tac arch_cap)
-  apply (case_tac arch_cap)
-    apply (auto simp add: valid_cap_simps wellformed_acap_simps
-                          valid_cap_ref_simps vmsz_aligned_ARMSection
-                split: option.splits)
-done
+  by (simp add: valid_arch_cap_def2)
 
 lemma tcb_cnode_index_distinct[simp]:
   "(tcb_cnode_index n = tcb_cnode_index m)
@@ -1822,17 +1123,7 @@ lemma st_tcb_idle_cap_valid_Null [simp]:
                      pred_tcb_at_def obj_at_def
                      valid_ipc_buffer_cap_def)
 
-lemmas
-  wellformed_pte_simps[simp] =
-  wellformed_pte_def[split_simps Arch_Structs_A.pte.split]
 
-lemmas
-  wellformed_pde_simps[simp] =
-  wellformed_pde_def[split_simps Arch_Structs_A.pde.split]
-
-lemmas
-  wellformed_arch_obj_simps[simp] =
-  wellformed_arch_obj_def[split_simps arch_kernel_obj.split]
  
 lemma valid_objsI [intro]:
   "(\<And>obj x. kheap s x = Some obj \<Longrightarrow> valid_obj x obj s) \<Longrightarrow> valid_objs s"
@@ -1842,138 +1133,12 @@ lemma valid_objsE [elim]:
   "\<lbrakk> valid_objs s; kheap s x = Some obj; valid_obj x obj s \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
   unfolding valid_objs_def by (auto simp: dom_def)
 
-lemmas vs_ref_atype_simps[simp] = vs_ref_atype_def[split_simps vs_ref.split]
-
-lemma vs_lookup1_obj_at:
-  "((rs,p) \<rhd>1 (r # rs,p')) s = obj_at (\<lambda>ko. (r, p') \<in> vs_refs ko) p s"
-  by (fastforce simp: vs_lookup1_def obj_at_def)
-
-lemma vs_lookup1I:
-  "\<lbrakk> ko_at ko p s; (r, p') \<in> vs_refs ko;
-          rs' = r # rs \<rbrakk> \<Longrightarrow> ((rs,p) \<rhd>1 (rs',p')) s"
-  by (fastforce simp add: vs_lookup1_def)
-
-lemma vs_lookup1D:
-  "(x \<rhd>1 y) s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs,p) \<and> y = (r # rs,p')
-                          \<and> ko_at ko p s \<and> (r,p') \<in> vs_refs ko"
-  by (cases x, cases y) (fastforce simp: vs_lookup1_def)
-
-lemma vs_lookup_pages1D:
-  "(x \<unrhd>1 y) s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs,p) \<and> y = (r # rs,p')
-                          \<and> ko_at ko p s \<and> (r,p') \<in> vs_refs_pages ko"
-  by (cases x, cases y) (fastforce simp: vs_lookup_pages1_def)
 
 lemma obj_at_ko_at:
   "obj_at P p s \<Longrightarrow> \<exists>ko. ko_at ko p s \<and> P ko"
   by (auto simp add: obj_at_def)
 
-lemma vs_lookup1_stateI:
-  assumes 1: "(r \<rhd>1 r') s"
-  assumes ko: "\<And>ko. ko_at ko (snd r) s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') (snd r) s'"
-  shows "(r \<rhd>1 r') s'" using 1 ko
-  by (fastforce simp: obj_at_def vs_lookup1_def)
 
-lemma vs_lookup_trans_sub:
-  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
-  shows "vs_lookup_trans s \<subseteq> vs_lookup_trans s'"
-proof -
-  have "vs_lookup1 s \<subseteq> vs_lookup1 s'"
-    by (fastforce dest: ko elim: vs_lookup1_stateI)
-  thus ?thesis by (rule rtrancl_mono)
-qed
-
-lemma vs_lookup_sub:
-  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
-  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
-  shows "vs_lookup s \<subseteq> vs_lookup s'"
-  unfolding vs_lookup_def
-  apply (rule Image_mono)
-   apply (rule vs_lookup_trans_sub)
-   apply (erule ko)
-  apply (unfold vs_asid_refs_def)
-  apply (rule image_mono)
-  apply (rule table)
-  done
-
-lemma vs_lookup_pages1_stateI:
-  assumes 1: "(r \<unrhd>1 r') s"
-  assumes ko: "\<And>ko. ko_at ko (snd r) s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') (snd r) s'"
-  shows "(r \<unrhd>1 r') s'" using 1 ko
-  by (fastforce simp: obj_at_def vs_lookup_pages1_def)
-
-lemma vs_lookup_pages_trans_sub:
-  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow>
-                      obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
-  shows "vs_lookup_pages_trans s \<subseteq> vs_lookup_pages_trans s'"
-proof -
-  have "vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'"
-    by (fastforce simp add: ko elim: vs_lookup_pages1_stateI)
-  thus ?thesis by (rule rtrancl_mono)
-qed
-
-lemma vs_lookup_pages_sub:
-  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow>
-                      obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
-  assumes table:
-    "graph_of (arm_asid_table (arch_state s)) \<subseteq>
-     graph_of (arm_asid_table (arch_state s'))"
-  shows "vs_lookup_pages s \<subseteq> vs_lookup_pages s'"
-  unfolding vs_lookup_pages_def
-  apply (rule Image_mono)
-   apply (rule vs_lookup_pages_trans_sub)
-   apply (erule ko)
-  apply (unfold vs_asid_refs_def)
-  apply (rule image_mono)
-  apply (rule table)
-  done
-
-lemma vs_lookup_pagesI:
-  "\<lbrakk> ref' \<in> vs_asid_refs (arm_asid_table (arch_state s));
-     (ref',(ref,p)) \<in> (vs_lookup_pages1 s)^*  \<rbrakk> \<Longrightarrow>
-  (ref \<unrhd> p) s"
-  by (simp add: vs_lookup_pages_def) blast
-
-lemma vs_lookup_stateI:
-  assumes 1: "(ref \<rhd> p) s"
-  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
-  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
-  shows "(ref \<rhd> p) s'"
-  using 1 vs_lookup_sub [OF ko table] by blast
-
-lemma valid_arch_objsD:
-  "\<lbrakk> (ref \<rhd> p) s; ko_at (ArchObj ao) p s; valid_arch_objs s \<rbrakk> \<Longrightarrow> valid_arch_obj ao s"
-  by (fastforce simp add: valid_arch_objs_def)
-
-(* should work for unmap and non-arch ops *)
-lemma valid_arch_objs_stateI:
-  assumes 1: "valid_arch_objs s"
-  assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
-  assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
-  assumes vao: "\<And>p ref ao'.
-                \<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_arch_obj ao s;
-                  ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> valid_arch_obj ao' s'"
-  shows "valid_arch_objs s'"
-  using 1 unfolding valid_arch_objs_def
-  apply clarsimp
-  apply (frule vs_lookup_stateI)
-    apply (erule ko)
-   apply (rule arch)
-  apply (erule allE, erule impE, fastforce)
-  apply (erule (3) vao)
-  done
-
-lemma asid_pool_at_ko:
-  "asid_pool_at p s \<Longrightarrow> \<exists>pool. ko_at (ArchObj (Arch_Structs_A.ASIDPool pool)) p s"
-  apply (clarsimp simp: obj_at_def a_type_def)
-  apply (case_tac ko, simp_all split: split_if_asm)
-  apply (rename_tac arch_kernel_obj)
-  apply (case_tac arch_kernel_obj, auto)
-  done
-
-lemma typ_at_pg:
-  "typ_at (AArch (AIntData sz)) buf s = ko_at (ArchObj (DataPage sz)) buf s"
-  unfolding obj_at_def
-  by (auto simp: a_type_def split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm split_if_asm)
 
 lemma symreftype_inverse[simp]:
   "symreftype (symreftype t) = t"
@@ -2328,23 +1493,7 @@ lemma only_idleI:
 lemmas cap_asid_simps [simp] =
   cap_asid_def [split_simps cap.split arch_cap.split option.split prod.split]
 
-text {*
-  A pointer is inside a user frame if its top bits point to any object
-  of type @{text IntData}.
-*}
-lemma in_user_frame_def:
-  "in_user_frame p \<equiv> \<lambda>s.
-   \<exists>sz. typ_at (AArch (AIntData sz)) (p && ~~ mask (pageBitsForSize sz)) s"
-  apply (rule eq_reflection, rule ext)
-  apply (simp add: in_user_frame_def obj_at_def)
-  apply (rule_tac f=Ex in arg_cong)
-  apply (rule ext, rule iffI)
-   apply (simp add: a_type_simps)
-  apply clarsimp
-  apply (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
-  apply (rename_tac arch_kernel_obj)
-  apply (case_tac arch_kernel_obj, simp_all add: a_type_simps)
-  done
+
 
 lemma obj_at_weakenE:
   "\<lbrakk> obj_at P r s; \<And>ko. P ko \<Longrightarrow> P' ko \<rbrakk> \<Longrightarrow> obj_at P' r s"
@@ -2434,22 +1583,22 @@ lemma cte_wp_at_pspaceI:
 
 lemma valid_cap_pspaceI:
   "\<lbrakk> s \<turnstile> cap; kheap s = kheap s' \<rbrakk> \<Longrightarrow> s' \<turnstile> cap"
-  unfolding valid_cap_def
-  by (cases cap)
-     (auto intro: obj_at_pspaceI cte_wp_at_pspaceI
+  unfolding valid_cap_def valid_arch_cap_def
+  apply (cases cap)
+   by  (auto intro: obj_at_pspaceI aobj_at_pspaceI cte_wp_at_pspaceI
            simp: obj_range_def valid_untyped_def pred_tcb_at_def
           split: arch_cap.split option.split sum.split)
 
 lemma valid_arch_obj_pspaceI:
   "\<lbrakk> valid_arch_obj obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_obj obj s'"
   apply (cases obj, simp_all)
-    apply (simp add: obj_at_def)
+    apply (simp add: aobj_at_def)
    apply (erule allEI)
    apply (rename_tac "fun" x)
-   apply (case_tac "fun x", simp_all add: obj_at_def)
+   apply (case_tac "fun x", simp_all add: aobj_at_def)
   apply (erule ballEI)
   apply (rename_tac "fun" x)
-  apply (case_tac "fun x", simp_all add: obj_at_def)
+  apply (case_tac "fun x", simp_all add: aobj_at_def)
   done
 
 (* FIXME-NTFN: ugly proof *)
@@ -2967,8 +2116,8 @@ lemma obj_bits_T:
    apply (clarsimp simp: obj_bits.simps well_formed_cnode_n_def
                          length_set_helper length_helper cte_level_bits_def)
   apply (rename_tac arch_kernel_obj)
-  apply (case_tac arch_kernel_obj, simp_all add: obj_bits.simps)
-  done
+  by (case_tac arch_kernel_obj, simp_all add: obj_bits.simps aa_type_def arch_obj_bits_type_def)
+
 
 lemma obj_range_T:
   "obj_range p v = typ_range p (a_type v)"
@@ -3006,6 +2155,11 @@ lemma cap_aligned_Null [simp]:
   "cap_aligned (cap.NullCap)"
   by (simp add: cap_aligned_def word_bits_def is_aligned_def)
 
+lemma atyp_at_typ_at: 
+  assumes P: "\<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
+  shows "\<lbrace>\<lambda>s. P (atyp_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (atyp_at T p s)\<rbrace>"
+  by (simp add: atyp_at_def2 P)
+
 lemma valid_cap_typ:
   assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
   shows      "\<lbrace>\<lambda>s. valid_cap c s\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap c s\<rbrace>"
@@ -3026,11 +2180,7 @@ lemma valid_cap_typ:
     apply (rule hoare_vcg_prop)
    apply (rule hoare_vcg_conj_lift [OF P])
    apply (rule hoare_vcg_prop)
-  apply (rename_tac arch_cap)
-  apply (case_tac arch_cap,
-         simp_all add: P P[where P=id, simplified]
-                       hoare_vcg_prop)
-  apply (auto intro: hoare_vcg_conj_lift [OF P] hoare_vcg_prop)
+  apply (wp valid_arch_cap_atyp atyp_at_typ_at P)
   done
 
 lemma valid_tcb_state_typ:
@@ -3089,19 +2239,7 @@ lemma valid_ntfn_typ:
   apply (rule hoare_vcg_conj_lift [OF hoare_vcg_prop], simp add: P)
   done
 
-lemma valid_arch_obj_typ:
-  assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
-  shows      "\<lbrace>\<lambda>s. valid_arch_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_obj ob s\<rbrace>"
-  apply (cases ob, simp_all)
-    apply (rule hoare_vcg_const_Ball_lift [OF P])
-   apply (rule hoare_vcg_all_lift)
-   apply (rename_tac "fun" x)
-   apply (case_tac "fun x", simp_all add: hoare_vcg_prop P)
-  apply (rule hoare_vcg_ball_lift)
-  apply (rename_tac "fun" x)
-  apply (case_tac "fun x", simp_all add: hoare_vcg_prop P)
-  apply (rule P)
-  done
+lemmas valid_arch_obj_typ = valid_arch_obj_atyp[OF atyp_at_typ_at]
 
 lemma valid_obj_typ:
   assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
@@ -3202,12 +2340,13 @@ lemma typ_at_range:
         apply (erule is_aligned_no_overflow)
        apply (clarsimp simp: valid_obj_def valid_cs_def valid_cs_size_def)
       apply (auto simp: a_type_def typ_range_def interval_empty obj_bits_type_def word_bits_def
-                        arch_kobj_size_bounded[simplified word_bits_conv]
+                        arch_kobj_size_bounded[simplified word_bits_conv] aa_type_def
+                        arch_obj_bits_type_def
                   dest!: is_aligned_no_overflow
                | simp split: arch_kernel_obj.splits)+
   done
 
-lemma typ_at_eq_kheap_obj:
+lemma typ_at_eq_kheap_obj':
   "typ_at ATCB p s \<longleftrightarrow> (\<exists>tcb. kheap s p = Some (TCB tcb))"
   "typ_at AEndpoint p s \<longleftrightarrow> (\<exists>ep. kheap s p = Some (Endpoint ep))"
   "typ_at ANTFN p s \<longleftrightarrow> (\<exists>ntfn. kheap s p = Some (Notification ntfn))"
@@ -3215,74 +2354,37 @@ lemma typ_at_eq_kheap_obj:
    (\<exists>cs. kheap s p = Some (CNode n cs) \<and> well_formed_cnode_n n cs)"
   "typ_at AGarbage p s \<longleftrightarrow>
    (\<exists>n cs. kheap s p = Some (CNode n cs) \<and> \<not> well_formed_cnode_n n cs)"
-  "typ_at (AArch AASIDPool) p s \<longleftrightarrow>
-   (\<exists>f. kheap s p = Some (ArchObj (Arch_Structs_A.ASIDPool f)))"
-  "typ_at (AArch APageTable) p s \<longleftrightarrow>
-   (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))"
-  "typ_at (AArch APageDirectory) p s \<longleftrightarrow>
-   (\<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)))"
-  "typ_at (AArch (AIntData sz)) p s \<longleftrightarrow>
-   (kheap s p = Some (ArchObj (DataPage sz)))"
-apply (auto simp add: obj_at_def a_type_def)
+apply (auto simp add: obj_at_def  a_type_def)
 apply (case_tac ko, simp_all add: wf_unique
-                    split: split_if_asm arch_kernel_obj.splits, fastforce?)+
+                    split: split_if_asm kernel_object.splits )
 done
 
+lemmas typ_at_eq_kheap_obj = typ_at_eq_kheap_obj' atyp_at_eq_kheap_obj[simplified atyp_at_def2]
+
 lemma a_type_ACapTableE:
   "\<lbrakk>a_type ko = ACapTable n;
     (!!cs. \<lbrakk>ko = CNode n cs; well_formed_cnode_n n cs\<rbrakk> \<Longrightarrow> R)\<rbrakk>
    \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
+  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
+  
 lemma a_type_AGarbageE:
   "\<lbrakk>a_type ko = AGarbage;
     (!!n cs. \<lbrakk>ko = CNode n cs; \<not> well_formed_cnode_n n cs\<rbrakk> \<Longrightarrow> R)\<rbrakk>
    \<Longrightarrow> R"
-  apply (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
-  apply (rename_tac arch_kernel_obj)
-  apply (case_tac arch_kernel_obj, simp_all add: a_type_simps)
-  done
+  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
+
 lemma a_type_ATCBE:
   "\<lbrakk>a_type ko = ATCB; (!!tcb. ko = TCB tcb \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
+  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
+
 lemma a_type_AEndpointE:
   "\<lbrakk>a_type ko = AEndpoint; (!!ep. ko = Endpoint ep \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
+  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
+
 lemma a_type_ANTFNE:
   "\<lbrakk>a_type ko = ANTFN; (!!ntfn. ko = Notification ntfn \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
-lemma a_type_AASIDPoolE:
-  "\<lbrakk>a_type ko = AArch AASIDPool;
-    (!!ap. ko = ArchObj (arch_kernel_obj.ASIDPool ap) \<Longrightarrow> R)\<rbrakk>
-   \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
-lemma a_type_APageDirectoryE:
-  "\<lbrakk>a_type ko = AArch APageDirectory;
-    (!!pd. ko = ArchObj (PageDirectory pd) \<Longrightarrow> R)\<rbrakk>
-   \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
-lemma a_type_APageTableE:
-  "\<lbrakk>a_type ko = AArch APageTable; (!!pt. ko = ArchObj (PageTable pt) \<Longrightarrow> R)\<rbrakk>
-   \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
-lemma a_type_AIntDataE:
-  "\<lbrakk>a_type ko = AArch (AIntData sz); ko = ArchObj (DataPage sz) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm,
-      rename_tac arch_kernel_obj,
-      case_tac arch_kernel_obj, simp_all add: a_type_simps)
+  by (case_tac ko, simp_all add: a_type_simps split: split_if_asm)
+
 
 lemmas a_type_elims[elim!] =
    a_type_ACapTableE a_type_AGarbageE a_type_ATCBE
diff --git a/spec/abstract/ARM/ArchCSpace_A.thy b/spec/abstract/ARM/ArchCSpace_A.thy
index f9b13076d..7da7c2f96 100644
--- a/spec/abstract/ARM/ArchCSpace_A.thy
+++ b/spec/abstract/ARM/ArchCSpace_A.thy
@@ -18,7 +18,7 @@ theory ArchCSpace_A
 imports
   ArchVSpace_A
 begin
-
+context ARM begin
 
 text {* For some purposes capabilities to physical objects are treated
 differently to others. *}
@@ -53,6 +53,9 @@ definition
               \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1
     | _ \<Rightarrow> arch_same_region_as cp cp')"
 
+(* Proofs don't want to see this definition *)
+declare same_aobject_as_def[simp]
+
 text {* Only caps with sufficient rights can be recycled. *}
 definition
   arch_has_recycle_rights :: "arch_cap \<Rightarrow> bool" where
@@ -61,3 +64,4 @@ definition
    | _ \<Rightarrow> True"
 
 end
+end
diff --git a/spec/abstract/ARM/ArchInvocation_A.thy b/spec/abstract/ARM/ArchInvocation_A.thy
index 8837ec2ad..aedacc560 100644
--- a/spec/abstract/ARM/ArchInvocation_A.thy
+++ b/spec/abstract/ARM/ArchInvocation_A.thy
@@ -18,6 +18,8 @@ theory ArchInvocation_A
 imports "../Structures_A"
 begin
 
+context ARM begin
+
 text {* These datatypes encode the arguments to the various possible
 ARM-specific system calls. Selectors are defined for various fields
 for convenience elsewhere. *}
@@ -76,3 +78,5 @@ datatype arch_copy_register_sets =
 typedecl arch_irq_control_invocation
 
 end
+
+end
diff --git a/spec/abstract/ARM/ArchRetype_A.thy b/spec/abstract/ARM/ArchRetype_A.thy
index 6e89adcb8..3f33039c7 100644
--- a/spec/abstract/ARM/ArchRetype_A.thy
+++ b/spec/abstract/ARM/ArchRetype_A.thy
@@ -20,6 +20,8 @@ imports
   ArchInvocation_A
 begin
 
+context ARM begin
+
 text {* This is a placeholder function. We may wish to extend the specification
   with explicitly tagging kernel data regions in memory. *}
 definition
@@ -60,3 +62,5 @@ where
   | _ \<Rightarrow> return ()"
 
 end
+
+end
diff --git a/spec/abstract/ARM/ArchVMRights_A.thy b/spec/abstract/ARM/ArchVMRights_A.thy
index 221b1407d..d4c6ddb54 100644
--- a/spec/abstract/ARM/ArchVMRights_A.thy
+++ b/spec/abstract/ARM/ArchVMRights_A.thy
@@ -11,9 +11,11 @@
 chapter "ARM-Specific Virtual-Memory Rights"
 
 theory ArchVMRights_A
-imports "../CapRights_A"
+imports "../CapRights_A" "../../machine/ARM/Setup_Locale"
 begin
 
+context ARM begin
+
 text {*
 This theory provides architecture-specific definitions and datatypes
 for virtual-memory support.
@@ -51,5 +53,6 @@ definition
      then (if AllowWrite \<in> rs then vm_read_write else vm_read_only)
    else vm_kernel_only)"
 
+end
 
 end
diff --git a/spec/abstract/ARM/ArchVSpaceAcc_A.thy b/spec/abstract/ARM/ArchVSpaceAcc_A.thy
index 1677f5420..d90f27916 100644
--- a/spec/abstract/ARM/ArchVSpaceAcc_A.thy
+++ b/spec/abstract/ARM/ArchVSpaceAcc_A.thy
@@ -18,6 +18,8 @@ theory ArchVSpaceAcc_A
 imports "../KHeap_A"
 begin
 
+context ARM begin
+
 text {* 
   This part of the specification is fairly concrete as the machine architecture
   is visible to the user in seL4 and therefore needs to be described.
@@ -183,6 +185,8 @@ definition
 where
   "lookup_pt_slot_no_fail pt vptr \<equiv> 
      let pt_index = ((vptr >> 12) && 0xff) 
-     in pt + (pt_index << 2)" 
+     in pt + (pt_index << 2)"
+
+end
 
 end
diff --git a/spec/abstract/ARM/ArchVSpace_A.thy b/spec/abstract/ARM/ArchVSpace_A.thy
index 0b416baf1..876c08b2d 100644
--- a/spec/abstract/ARM/ArchVSpace_A.thy
+++ b/spec/abstract/ARM/ArchVSpace_A.thy
@@ -18,6 +18,8 @@ theory ArchVSpace_A
 imports "../Retype_A"
 begin
 
+context ARM begin
+
 text {* Save the set of entries that would be inserted into a page table or
 page directory to map various different sizes of frame at a given virtual
 address. *}
@@ -51,17 +53,17 @@ where
     returnOk $ Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, [p, p + 4  .e.  p + 60])
   odE"
 
-definition get_master_pde :: "word32 \<Rightarrow> (Arch_Structs_A.pde,'z::state_ext)s_monad"
+definition get_master_pde :: "word32 \<Rightarrow> (Arch_Structs_A.ARM.pde,'z::state_ext)s_monad"
   where "get_master_pde ptr \<equiv> do
     pde \<leftarrow> (get_pde (ptr && ~~ mask 6));
-    (case pde of Arch_Structs_A.pde.SuperSectionPDE _ _ _ \<Rightarrow> return pde
+    (case pde of Arch_Structs_A.ARM.pde.SuperSectionPDE _ _ _ \<Rightarrow> return pde
     | _ \<Rightarrow> get_pde ptr)
   od"
 
-definition get_master_pte :: "word32 \<Rightarrow> (Arch_Structs_A.pte, 'z::state_ext)s_monad"
+definition get_master_pte :: "word32 \<Rightarrow> (Arch_Structs_A.ARM.pte, 'z::state_ext)s_monad"
   where "get_master_pte ptr \<equiv> do
     pte \<leftarrow> (get_pte (ptr && ~~ mask 6));
-    (case pte of Arch_Structs_A.pte.LargePagePTE _ _ _ \<Rightarrow> return pte
+    (case pte of Arch_Structs_A.ARM.pte.LargePagePTE _ _ _ \<Rightarrow> return pte
     | _ \<Rightarrow> get_pte ptr)
   od"
 
@@ -750,6 +752,8 @@ definition
   in_user_frame :: "word32 \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
   "in_user_frame p s \<equiv>
    \<exists>sz. kheap s (p && ~~ mask (pageBitsForSize sz)) =
-        Some (ArchObj (DataPage sz))"           
+        Some (ArchObj (DataPage sz))"
+
+end
 
 end
diff --git a/spec/abstract/ARM/Arch_A.thy b/spec/abstract/ARM/Arch_A.thy
index 5b149cea2..829408168 100644
--- a/spec/abstract/ARM/Arch_A.thy
+++ b/spec/abstract/ARM/Arch_A.thy
@@ -18,6 +18,8 @@ theory Arch_A
 imports "../TcbAcc_A"
 begin
 
+context ARM begin
+
 definition "page_bits \<equiv> pageBits"
 
 text {* The ARM architecture does not provide any additional operations on its
@@ -234,3 +236,5 @@ definition
 od"
 
 end
+
+end
diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy
index 87f684e56..96c86af19 100644
--- a/spec/abstract/ARM/Arch_Structs_A.thy
+++ b/spec/abstract/ARM/Arch_Structs_A.thy
@@ -21,6 +21,8 @@ imports
   ArchVMRights_A
 begin
 
+context ARM begin
+
 text {*
 This theory provides architecture-specific definitions and datatypes 
 including architecture-specific capabilities and objects.
@@ -182,6 +184,10 @@ currently active page directory. The second component of
 @{text "arm_asid_map"} values is the address of that page directory.
 *}
 
+end
+
+qualify ARM
+
 record arch_state =
   arm_globals_frame :: obj_ref
   arm_asid_table    :: "word8 \<rightharpoonup> obj_ref"
@@ -192,6 +198,10 @@ record arch_state =
   arm_global_pts    :: "obj_ref list"
   arm_kernel_vspace :: arm_vspace_region_uses
 
+end_qualify
+
+context ARM begin
+
 definition
   pd_bits :: "nat" where
   "pd_bits \<equiv> pageBits + 2"
@@ -200,4 +210,23 @@ definition
   pt_bits :: "nat" where
   "pt_bits \<equiv> pageBits - 2"
 
+
+section "Type declarations for invariant definitions"
+
+datatype aa_type =
+    AASIDPool
+  | APageTable
+  | APageDirectory
+  | AIntData vmpage_size
+
+definition aa_type :: "arch_kernel_obj \<Rightarrow> aa_type"
+where 
+ "aa_type ao \<equiv> (case ao of
+           PageTable pt             \<Rightarrow> APageTable
+         | PageDirectory pd         \<Rightarrow> APageDirectory
+         | DataPage sz              \<Rightarrow> AIntData sz
+         | ASIDPool f \<Rightarrow> AASIDPool)"
+
+end
+
 end
diff --git a/spec/abstract/ARM/Init_A.thy b/spec/abstract/ARM/Init_A.thy
index 72878c83e..0aeb868dc 100644
--- a/spec/abstract/ARM/Init_A.thy
+++ b/spec/abstract/ARM/Init_A.thy
@@ -18,6 +18,8 @@ theory Init_A
 imports "../Retype_A"
 begin
 
+context ARM begin
+
 text {* 
   This is not a specification of true kernel
   initialisation. This theory describes a dummy initial state only, to
@@ -112,5 +114,7 @@ definition
     exst = ext_init 
   \<rparr>"
 
+end
+
 
 end
diff --git a/spec/abstract/ARM/Machine_A.thy b/spec/abstract/ARM/Machine_A.thy
index 29d7df2bf..0c021e807 100644
--- a/spec/abstract/ARM/Machine_A.thy
+++ b/spec/abstract/ARM/Machine_A.thy
@@ -22,6 +22,8 @@ imports
   "../../machine/$L4V_ARCH/MachineTypes"
 begin
 
+context ARM begin
+
 text {*
   The specification is written with abstract type names for object
   references, user pointers, word-based data, cap references, and so
@@ -109,4 +111,32 @@ definition
   new_context :: "user_context" where
   "new_context \<equiv> (\<lambda>r. 0) (CPSR := 0x150)"
 
+text {* Miscellaneous definitions of constants used in modelling machine
+operations. *}
+
+definition
+  nat_to_cref :: "nat \<Rightarrow> nat \<Rightarrow> cap_ref" where
+  "nat_to_cref ln n \<equiv> drop (word_bits - ln)
+                           (to_bl (of_nat n :: machine_word))"
+
+definition
+ "msg_info_register \<equiv> msgInfoRegister"
+definition
+ "msg_registers \<equiv> msgRegisters"
+definition
+ "cap_register \<equiv> capRegister"
+definition
+ "badge_register \<equiv> badgeRegister"
+definition
+ "frame_registers \<equiv> frameRegisters"
+definition
+ "gp_registers \<equiv> gpRegisters"
+definition
+ "exception_message \<equiv> exceptionMessage"
+definition
+ "syscall_message \<equiv> syscallMessage"
+
+
+end
+
 end
diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy
index 3d667b177..1963e6f48 100644
--- a/spec/abstract/CSpace_A.thy
+++ b/spec/abstract/CSpace_A.thy
@@ -23,6 +23,23 @@ imports
   "~~/src/HOL/Library/Prefix_Order"
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "arch_update_cap_data :: data \<Rightarrow> arch_cap \<Rightarrow> cap"
+  "arch_derive_cap :: arch_cap \<Rightarrow> (arch_cap,'z::state_ext) se_monad"
+  "arch_finalise_cap :: arch_cap \<Rightarrow> bool \<Rightarrow> (cap,'z::state_ext) s_monad"
+  "arch_is_physical :: arch_cap \<Rightarrow> bool"
+  "arch_same_region_as :: arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
+  "same_aobject_as :: arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
+  "arch_has_recycle_rights :: arch_cap \<Rightarrow> bool"
+  "arch_recycle_cap :: bool \<Rightarrow> arch_cap \<Rightarrow> (arch_cap,'z::state_ext) s_monad"
+
+  "msg_max_length :: nat"
+  "cap_transfer_data_size :: nat"
+  "msg_max_extra_caps :: nat"
+  "msg_align_bits :: nat"
+
+
+
 text {* This theory develops an abstract model of \emph{capability
 spaces}, or CSpace, in seL4. The CSpace of a thread can be thought of
 as the set of all capabilities it has access to. More precisely, it
@@ -632,11 +649,6 @@ definition
   | EndpointCap oref badge cr      \<Rightarrow> Some badge
   | _                              \<Rightarrow> None"
 
-text {* For some purposes capabilities to physical objects are treated
-differently to others. *}
-definition
-  arch_is_physical :: "arch_cap \<Rightarrow> bool" where
-  "arch_is_physical cap \<equiv> case cap of ASIDControlCap \<Rightarrow> False | _ \<Rightarrow> True"
 
 definition
   is_physical :: "cap \<Rightarrow> bool" where
@@ -686,8 +698,7 @@ definition
     | (ArchObjectCap ac, ArchObjectCap ac') \<Rightarrow> same_aobject_as ac ac'
     | _ \<Rightarrow> same_region_as cp cp')"
 
-(* Proofs don't want to see this definition *)
-declare same_aobject_as_def[simp]
+
 
 text {*
 The function @{text "should_be_parent_of"}
@@ -889,4 +900,10 @@ definition
         | _ \<Rightarrow> fail) od
   | RecycleCall slot \<Rightarrow> cap_recycle slot"
 
+
+section "Cap classification used to define invariants"
+
+datatype capclass =
+  PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass
+
 end
diff --git a/spec/abstract/Interrupt_A.thy b/spec/abstract/Interrupt_A.thy
index 0cd1ac082..2163fb5e0 100644
--- a/spec/abstract/Interrupt_A.thy
+++ b/spec/abstract/Interrupt_A.thy
@@ -18,6 +18,9 @@ theory Interrupt_A
 imports Ipc_A
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "arch_invoke_irq_control :: arch_irq_control_invocation \<Rightarrow> (unit,'z::state_ext) p_monad"
+  setInterruptMode
 text {* Tests whether an IRQ identifier is in use. *}
 definition
   is_irq_active :: "irq \<Rightarrow> (bool,'z::state_ext) s_monad" where
diff --git a/spec/abstract/InvocationLabels_A.thy b/spec/abstract/InvocationLabels_A.thy
index 33084673e..364ced27a 100644
--- a/spec/abstract/InvocationLabels_A.thy
+++ b/spec/abstract/InvocationLabels_A.thy
@@ -20,6 +20,12 @@ imports
   "../design/$L4V_ARCH/ArchLabelFuns_H"
 begin
 
+unqualify_types (in "$L4V_ARCH") 
+  data
+
+unqualify_consts (in "$L4V_ARCH") 
+  "data_to_nat :: data \<Rightarrow> nat"
+
 definition
   invocation_type :: "data \<Rightarrow> invocation_label"
 where
diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy
index 1382160ff..455919876 100644
--- a/spec/abstract/Invocations_A.thy
+++ b/spec/abstract/Invocations_A.thy
@@ -18,6 +18,11 @@ theory Invocations_A
 imports "./$L4V_ARCH/ArchInvocation_A"
 begin
 
+unqualify_types (in "$L4V_ARCH")
+  arch_copy_register_sets
+  arch_irq_control_invocation
+  arch_invocation
+
 text {* These datatypes encode the arguments to the available system calls. *}
 
 datatype cnode_invocation =
@@ -32,8 +37,8 @@ datatype cnode_invocation =
 datatype untyped_invocation =
     Retype cslot_ptr obj_ref obj_ref apiobject_type nat "cslot_ptr list"
 
-datatype tcb_invocation =
-    WriteRegisters machine_word bool "machine_word list" arch_copy_register_sets
+datatype tcb_invocation =                                          
+    WriteRegisters machine_word bool "machine_word list" ARM.arch_copy_register_sets
   | ReadRegisters machine_word bool machine_word arch_copy_register_sets
   | CopyRegisters machine_word machine_word bool bool bool bool arch_copy_register_sets
   | ThreadControl machine_word cslot_ptr
diff --git a/spec/abstract/Ipc_A.thy b/spec/abstract/Ipc_A.thy
index d5826e39c..66d591f18 100644
--- a/spec/abstract/Ipc_A.thy
+++ b/spec/abstract/Ipc_A.thy
@@ -18,6 +18,10 @@ theory Ipc_A
 imports Tcb_A
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "set_message_info :: obj_ref \<Rightarrow> message_info \<Rightarrow> (unit,'z::state_ext) s_monad"
+  "lookup_ipc_buffer :: bool \<Rightarrow> obj_ref \<Rightarrow> (obj_ref option,'z::state_ext) s_monad"
+
 section {* Getting and setting the message info register. *}
 
 definition
diff --git a/spec/abstract/MiscMachine_A.thy b/spec/abstract/MiscMachine_A.thy
index 977c06d2b..9572fc774 100644
--- a/spec/abstract/MiscMachine_A.thy
+++ b/spec/abstract/MiscMachine_A.thy
@@ -15,33 +15,47 @@ Utilities for the machine level which are not machine-dependent.
 chapter "Machine Accessor Functions"
 
 theory MiscMachine_A
-imports "./$L4V_ARCH/Machine_A"
+imports "./$L4V_ARCH/Machine_A" "../machine/MachineExports"
 begin
 
-text {* Miscellaneous definitions of constants used in modelling machine
-operations. *}
+unqualify_types (in "$L4V_ARCH")
+  user_context 
+  register 
+  data 
+  obj_ref
+  asid_index
+  asid_pool_index
+  cap_ref
+  length_type
+  vspace_ref
+  data_offset
 
-definition
-  nat_to_cref :: "nat \<Rightarrow> nat \<Rightarrow> cap_ref" where
-  "nat_to_cref ln n \<equiv> drop (word_bits - ln)
-                           (to_bl (of_nat n :: machine_word))"
 
-definition
- "msg_info_register \<equiv> msgInfoRegister"
-definition
- "msg_registers \<equiv> msgRegisters"
-definition
- "cap_register \<equiv> capRegister"
-definition
- "badge_register \<equiv> badgeRegister"
-definition
- "frame_registers \<equiv> frameRegisters"
-definition
- "gp_registers \<equiv> gpRegisters"
-definition
- "exception_message \<equiv> exceptionMessage"
-definition
- "syscall_message \<equiv> syscallMessage"
+unqualify_consts (in "$L4V_ARCH")
+  "nat_to_cref :: nat \<Rightarrow> nat \<Rightarrow> cap_ref"
+  "msg_info_register :: register"
+  "msg_registers :: register list"
+  "cap_register :: register"
+  "badge_register :: register"
+  "frame_registers :: register list"
+  "gp_registers :: register list"
+  "exception_message :: register list"
+  "syscall_message :: register list"
+
+  "new_context :: user_context"
+  "slot_bits :: nat"
+  "oref_to_data   :: obj_ref \<Rightarrow> data"
+  "data_to_oref   :: data \<Rightarrow> obj_ref"
+  "vref_to_data   :: vspace_ref \<Rightarrow> data"
+  "data_to_vref   :: data \<Rightarrow> vspace_ref"
+  "nat_to_len     :: nat \<Rightarrow> length_type"
+  "data_to_nat    :: data \<Rightarrow> nat"
+  "data_to_16     :: data \<Rightarrow> 16 word"
+  "data_to_cptr :: data \<Rightarrow> cap_ref"
+  "data_offset_to_nat :: data_offset \<Rightarrow> nat"
+  "combine_ntfn_badges :: data \<Rightarrow> data \<Rightarrow> data"
+  "combine_ntfn_msgs :: data \<Rightarrow> data \<Rightarrow> data" 
+
 
 type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
 
@@ -57,4 +71,5 @@ definition
   set_register :: "register \<Rightarrow> data \<Rightarrow> unit user_monad" where
   "set_register r v \<equiv> modify (\<lambda>uc. uc (r := v))"
 
+
 end
diff --git a/spec/abstract/Retype_A.thy b/spec/abstract/Retype_A.thy
index 0c1eb0d97..09326c272 100644
--- a/spec/abstract/Retype_A.thy
+++ b/spec/abstract/Retype_A.thy
@@ -22,6 +22,12 @@ imports
   "./$L4V_ARCH/ArchRetype_A"
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "arch_default_cap :: aobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> arch_cap"
+  "default_arch_object :: aobject_type \<Rightarrow> nat \<Rightarrow> arch_kernel_obj"
+  "init_arch_objects :: apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
+
+
 section "Creating Caps"
 
 text {* The original capability created when an object of a given type is
diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy
index 00cacce11..e999cad91 100644
--- a/spec/abstract/Schedule_A.thy
+++ b/spec/abstract/Schedule_A.thy
@@ -18,6 +18,10 @@ theory Schedule_A
 imports "./$L4V_ARCH/Arch_A"
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "arch_switch_to_thread :: obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
+  "arch_switch_to_idle_thread :: (unit,'z::state_ext) s_monad"
+
 abbreviation
   "idle st \<equiv> st = Structures_A.IdleThreadState"
 
diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy
index d42e35781..e435699c8 100644
--- a/spec/abstract/Structures_A.thy
+++ b/spec/abstract/Structures_A.thy
@@ -18,8 +18,28 @@ chapter "Basic Data Structures"
 theory Structures_A
 imports
   "./$L4V_ARCH/Arch_Structs_A"
-  "../machine/$L4V_ARCH/MachineOps"
-begin
+  "../machine/MachineExports"
+
+begin     
+
+unqualify_types (in "$L4V_ARCH")
+  aobject_type 
+  arch_cap 
+  vm_rights
+  arch_kernel_obj
+  arch_state
+        
+
+unqualify_consts (in "$L4V_ARCH")
+  "acap_rights :: arch_cap \<Rightarrow> vm_rights"
+  "acap_rights_update :: vm_rights \<Rightarrow> arch_cap \<Rightarrow> arch_cap"
+  "arch_kobj_size :: arch_kernel_obj \<Rightarrow> nat"
+  "arch_obj_size :: arch_cap \<Rightarrow> nat"
+  "aobj_ref :: arch_cap \<rightharpoonup> obj_ref"
+  "asid_high_bits :: nat"
+  "asid_low_bits :: nat"
+
+
 
 text {*
   User mode can request these objects to be created by retype:
diff --git a/spec/abstract/TcbAcc_A.thy b/spec/abstract/TcbAcc_A.thy
index 2234fda0d..0b12f022c 100644
--- a/spec/abstract/TcbAcc_A.thy
+++ b/spec/abstract/TcbAcc_A.thy
@@ -18,6 +18,9 @@ theory TcbAcc_A
 imports CSpace_A
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "in_user_frame :: obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
+
 text {* Store or load a word at an offset from an IPC buffer. *}
 definition
   store_word_offs :: "obj_ref \<Rightarrow> nat \<Rightarrow> machine_word \<Rightarrow> (unit,'z::state_ext) s_monad" where
diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy
index 106fa2e1a..ea39f12ef 100644
--- a/spec/abstract/Tcb_A.thy
+++ b/spec/abstract/Tcb_A.thy
@@ -18,6 +18,9 @@ theory Tcb_A
 imports TcbAcc_A Schedule_A
 begin
 
+unqualify_consts (in "$L4V_ARCH")
+  "arch_activate_idle_thread :: obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
+
 section "Activating Threads"
 
 text {* Threads that are active always have a master Reply capability to
diff --git a/spec/design/ARM/ArchInvocationLabels_H.thy b/spec/design/ARM/ArchInvocationLabels_H.thy
index 13b65e45b..ced1ca4c6 100644
--- a/spec/design/ARM/ArchInvocationLabels_H.thy
+++ b/spec/design/ARM/ArchInvocationLabels_H.thy
@@ -11,9 +11,11 @@
 chapter "Architecture-specific Invocation Labels"
 
 theory ArchInvocationLabels_H
-imports "../../../lib/Enumeration"
+imports "../../../lib/Enumeration" "../../machine/ARM/Setup_Locale"
 begin
 
+qualify ARM
+
 text {*
   An enumeration of arch-specific system call labels.
 *}
@@ -89,6 +91,6 @@ instance by (intro_classes, simp add: enum_alt_arch_invocation_label)
 end
 
 (*>*)
-
+end_qualify
 
 end
diff --git a/spec/design/ARM/ArchLabelFuns_H.thy b/spec/design/ARM/ArchLabelFuns_H.thy
index 16e5d5e50..2730ae7db 100644
--- a/spec/design/ARM/ArchLabelFuns_H.thy
+++ b/spec/design/ARM/ArchLabelFuns_H.thy
@@ -14,6 +14,8 @@ theory ArchLabelFuns_H
 imports "../InvocationLabels_H"
 begin
 
+context ARM begin
+
 text {*
   Arch-specific functions on invocation labels
 *}
@@ -39,6 +41,6 @@ where
       | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow>   True
       | _ \<Rightarrow>   False
       )"
-
+end
 
 end
diff --git a/spec/design/Event_H.thy b/spec/design/Event_H.thy
index bc36a0828..dd98bbfb7 100644
--- a/spec/design/Event_H.thy
+++ b/spec/design/Event_H.thy
@@ -11,7 +11,7 @@
 chapter "Kernel Events"
 
 theory Event_H
-imports "../machine/$L4V_ARCH/MachineTypes"
+imports "../machine/MachineExports"
 begin
 
 text {*
diff --git a/spec/design/InvocationLabels_H.thy b/spec/design/InvocationLabels_H.thy
index 065c076c8..b2487fcc1 100644
--- a/spec/design/InvocationLabels_H.thy
+++ b/spec/design/InvocationLabels_H.thy
@@ -18,6 +18,10 @@ text {*
   An enumeration of all system call labels.
 *}
 
+unqualify_types (in "$L4V_ARCH")
+  arch_invocation_label
+
+
 datatype invocation_label =
     InvalidInvocation
   | UntypedRetype
@@ -47,7 +51,7 @@ datatype invocation_label =
   | IRQClearIRQHandler
   | IRQSetMode
   | DomainSetSet
-  | ArchInvocationLabel ArchInvocationLabels_H.arch_invocation_label
+  | ArchInvocationLabel arch_invocation_label
 
 (* invocation_label instance proofs *)
 (*<*)
diff --git a/spec/machine/ARM/MachineOps.thy b/spec/machine/ARM/MachineOps.thy
index 419ada94b..8b1a84118 100644
--- a/spec/machine/ARM/MachineOps.thy
+++ b/spec/machine/ARM/MachineOps.thy
@@ -14,7 +14,7 @@ theory MachineOps
 imports
   "../../../lib/WordSetup"
   "../../../lib/wp/NonDetMonad"
-  MachineTypes
+  "../MachineMonad"
 begin
 
 section "Wrapping and Lifting Machine Operations"
@@ -34,66 +34,8 @@ text {*
   All this is done only to avoid a large number of axioms (2 for each operation).
 *}
 
-definition
-  ignore_failure :: "('s,unit) nondet_monad \<Rightarrow> ('s,unit) nondet_monad"
-  where 
-  "ignore_failure f \<equiv> 
-  \<lambda>s. if fst (f s) = {} then ({((),s)},False) else (fst (f s), False)"
-
-text {* The wrapper doesn't do anything for usual operations: *}
-lemma failure_consistent:
-  "\<lbrakk> empty_fail f; no_fail \<top> f \<rbrakk> \<Longrightarrow> ignore_failure f = f"
-  apply (simp add: ignore_failure_def empty_fail_def no_fail_def)
-  apply (rule ext)
-  apply (auto intro: prod_eqI)
-  done
-  
-text {* And it has the desired properties *}
-lemma ef_ignore_failure [simp]:
-  "empty_fail (ignore_failure f)"
-  by (simp add: empty_fail_def ignore_failure_def)
-
-lemma no_fail_ignore_failure [simp, intro!]:
-  "no_fail \<top> (ignore_failure f)"
-  by (simp add: no_fail_def ignore_failure_def)
-
-
-type_synonym 'a machine_rest_monad = "(machine_state_rest, 'a) nondet_monad"
-
-definition
-  machine_rest_lift :: "'a machine_rest_monad \<Rightarrow> 'a machine_monad"
-where
-  "machine_rest_lift f \<equiv> do
-    mr \<leftarrow> gets machine_state_rest;
-    (r, mr') \<leftarrow> select_f (f mr);
-    modify (\<lambda>s. s \<lparr> machine_state_rest := mr' \<rparr>);
-    return r
-  od"
-
-lemma ef_machine_rest_lift [simp, intro!]:
-  "empty_fail f \<Longrightarrow> empty_fail (machine_rest_lift f)"
-  apply (clarsimp simp: empty_fail_def machine_rest_lift_def simpler_gets_def 
-                        select_f_def bind_def simpler_modify_def return_def)
-  apply force
-  done
-    
-lemma no_fail_machine_state_rest [intro!]:
-  "no_fail P f \<Longrightarrow> no_fail (P o machine_state_rest) (machine_rest_lift f)"
-  apply (simp add: no_fail_def machine_rest_lift_def simpler_gets_def 
-                        select_f_def bind_def simpler_modify_def return_def)
-  apply force
-  done
- 
-lemma no_fail_machine_state_rest_T [simp, intro!]:
-  "no_fail \<top> f \<Longrightarrow> no_fail \<top> (machine_rest_lift f)"
-  apply (drule no_fail_machine_state_rest)
-  apply (simp add: o_def)
-  done
-
-
-definition
-  "machine_op_lift \<equiv> machine_rest_lift o ignore_failure"
 
+qualify ARM
 
 section "The Operations"
 
@@ -372,6 +314,10 @@ where
   debugPrint_def[simp]:
  "debugPrint \<equiv> \<lambda>message. return ()"
 
+end_qualify
+
+context ARM begin
+
 
 -- "Interrupt controller operations"
 
@@ -545,15 +491,14 @@ definition
   mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size  .e.  ptr + 2 ^ bits - 1]"
 
 
+
+
 section "User Monad"
 
 type_synonym user_context = "register \<Rightarrow> machine_word"
 
 type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
 
-translations
-  (type) "'a user_monad" <= (type) "(register \<Rightarrow> machine_word, 'a) nondet_monad"
-
 definition
   getRegister :: "register \<Rightarrow> machine_word user_monad" 
 where
@@ -571,3 +516,9 @@ definition
   "setNextPC \<equiv> setRegister LR_svc"
 
 end
+
+translations
+  (type) "'a ARM.user_monad" <= (type) "(ARM.register \<Rightarrow> ARM.machine_word, 'a) nondet_monad"
+
+
+end
diff --git a/spec/machine/ARM/MachineTypes.thy b/spec/machine/ARM/MachineTypes.thy
index 25df5c3df..a41587401 100644
--- a/spec/machine/ARM/MachineTypes.thy
+++ b/spec/machine/ARM/MachineTypes.thy
@@ -15,9 +15,12 @@ imports
   "../../../lib/Enumeration"
   "../../../lib/WordSetup"
   "../../../lib/wp/NonDetMonad"
+  Setup_Locale
   Platform
 begin
 
+qualify ARM
+
 (* !!! Generated File !!! Skeleton in ../haskell-translator/ARMMachineTypes.thy *)
 
 text {*
@@ -49,16 +52,21 @@ datatype register =
 
 type_synonym machine_word = "word32"
 
+
+
 consts
 initContext :: "(register * machine_word) list"
 
 consts
 sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_word"
 
+
+
 (*<*)
 (* register instance proofs *)
 (*<*)
 instantiation register :: enum begin
+ 
 definition
   enum_register: "enum_class.enum \<equiv> 
     [ 
@@ -181,13 +189,6 @@ record
 
 consts irq_oracle :: "nat \<Rightarrow> word8"
 
-text {*
-  The machine monad is used for operations on the state defined above.
-*}
-type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
-
-translations
-  (type) "'c machine_monad" <= (type) "(machine_state, 'c) nondet_monad"
 
 text {*
   After kernel initialisation all IRQs are masked.
@@ -312,6 +313,6 @@ instance by (intro_classes, simp add: enum_alt_vmpage_size)
 end
 
 (*>*)
-
+end_qualify
 
 end
diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy
index 9d9c30958..4d6f2b7be 100644
--- a/spec/machine/ARM/Platform.thy
+++ b/spec/machine/ARM/Platform.thy
@@ -14,8 +14,11 @@ theory Platform
 imports
   "../../../lib/Lib"
   "../../../lib/WordEnum"
+  Setup_Locale
 begin
 
+context ARM begin
+
 text {*
   This theory lists platform-specific types and basic constants, in particular
   the types of interrupts and physical addresses, constants for the
@@ -70,3 +73,5 @@ definition
   "maxIRQ \<equiv> 63"
 
 end
+
+end
diff --git a/spec/machine/ARM/Setup_Locale.thy b/spec/machine/ARM/Setup_Locale.thy
new file mode 100644
index 000000000..1d2a32d6a
--- /dev/null
+++ b/spec/machine/ARM/Setup_Locale.thy
@@ -0,0 +1,18 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+
+theory Setup_Locale
+imports "../../../lib/Qualify" "../../../lib/Unqualify"
+begin
+
+locale ARM
+
+end
\ No newline at end of file
diff --git a/spec/machine/MachineExports.thy b/spec/machine/MachineExports.thy
new file mode 100644
index 000000000..f456ece2f
--- /dev/null
+++ b/spec/machine/MachineExports.thy
@@ -0,0 +1,40 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+
+theory MachineExports
+imports "./$L4V_ARCH/MachineOps"
+begin
+  
+unqualify_types (in "$L4V_ARCH")
+  machine_word 
+  vmfault_type
+  irq
+
+unqualify_consts (in "$L4V_ARCH")
+  "getActiveIRQ :: (irq option) machine_monad"
+  "maskInterrupt :: bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
+  "freeMemory :: machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
+  "loadWord :: machine_word \<Rightarrow> machine_word machine_monad"
+  "storeWord :: machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
+  "storeWordVM :: machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
+  "setNextPC :: machine_word \<Rightarrow> unit user_monad"
+  "getRestartPC :: machine_word user_monad"
+  "setRegister :: register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
+  "getRegister :: register \<Rightarrow> machine_word user_monad"
+  "sanitiseRegister :: register \<Rightarrow> machine_word \<Rightarrow> machine_word"
+  "initContext :: (register * machine_word) list"
+  "exceptionMessage :: register list"
+  "syscallMessage :: register list"
+  "gpRegisters :: register list"
+  "frameRegisters :: register list"
+  "setInterruptMode :: irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
+
+end
diff --git a/spec/machine/MachineMonad.thy b/spec/machine/MachineMonad.thy
new file mode 100644
index 000000000..bef7c40ac
--- /dev/null
+++ b/spec/machine/MachineMonad.thy
@@ -0,0 +1,93 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+
+theory MachineMonad
+imports "./$L4V_ARCH/MachineTypes"
+begin
+  
+unqualify_types (in "$L4V_ARCH")
+  machine_state
+  machine_state_rest
+
+unqualify_consts (in "$L4V_ARCH")
+  "machine_state_rest :: machine_state \<Rightarrow> machine_state_rest"
+  "machine_state_rest_update :: (machine_state_rest \<Rightarrow> machine_state_rest) \<Rightarrow> machine_state \<Rightarrow> machine_state"
+
+text {*
+  The machine monad is used for operations on the state defined above.
+*}
+type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
+
+translations
+  (type) "'c machine_monad" <= (type) "(machine_state, 'c) nondet_monad"
+
+type_synonym 'a machine_rest_monad = "(machine_state_rest, 'a) nondet_monad"
+
+definition
+  machine_rest_lift :: "'a machine_rest_monad \<Rightarrow> 'a machine_monad"
+where
+  "machine_rest_lift f \<equiv> do
+    mr \<leftarrow> gets machine_state_rest;
+    (r, mr') \<leftarrow> select_f (f mr);
+    modify (\<lambda>s. s \<lparr> machine_state_rest := mr' \<rparr>);
+    return r
+  od"
+
+
+definition
+  ignore_failure :: "('s,unit) nondet_monad \<Rightarrow> ('s,unit) nondet_monad"
+  where 
+  "ignore_failure f \<equiv> 
+  \<lambda>s. if fst (f s) = {} then ({((),s)},False) else (fst (f s), False)"
+
+text {* The wrapper doesn't do anything for usual operations: *}
+lemma failure_consistent:
+  "\<lbrakk> empty_fail f; no_fail \<top> f \<rbrakk> \<Longrightarrow> ignore_failure f = f"
+  apply (simp add: ignore_failure_def empty_fail_def no_fail_def)
+  apply (rule ext)
+  apply (auto intro: prod_eqI)
+  done
+  
+text {* And it has the desired properties *}
+lemma ef_ignore_failure [simp]:
+  "empty_fail (ignore_failure f)"
+  by (simp add: empty_fail_def ignore_failure_def)
+
+lemma no_fail_ignore_failure [simp, intro!]:
+  "no_fail \<top> (ignore_failure f)"
+  by (simp add: no_fail_def ignore_failure_def)
+
+
+lemma ef_machine_rest_lift [simp, intro!]:
+  "empty_fail f \<Longrightarrow> empty_fail (machine_rest_lift f)"
+  apply (clarsimp simp: empty_fail_def machine_rest_lift_def simpler_gets_def 
+                        select_f_def bind_def simpler_modify_def return_def)
+  apply force
+  done
+    
+lemma no_fail_machine_state_rest [intro!]:
+  "no_fail P f \<Longrightarrow> no_fail (P o machine_state_rest) (machine_rest_lift f)"
+  apply (simp add: no_fail_def machine_rest_lift_def simpler_gets_def 
+                        select_f_def bind_def simpler_modify_def return_def)
+  apply force
+  done
+ 
+lemma no_fail_machine_state_rest_T [simp, intro!]:
+  "no_fail \<top> f \<Longrightarrow> no_fail \<top> (machine_rest_lift f)"
+  apply (drule no_fail_machine_state_rest)
+  apply (simp add: o_def)
+  done
+
+definition
+  "machine_op_lift \<equiv> machine_rest_lift o ignore_failure"
+
+
+end