arch_split: progress on namespacing abstract spec

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 =
+datatype tcb_invocation =                                          
-    WriteRegisters machine_word bool "machine_word list" arch_copy_register_sets
+    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

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

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
+unqualify_types (in "$L4V_ARCH")
-operations. *}
+  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
+unqualify_consts (in "$L4V_ARCH")
- "msg_info_register \<equiv> msgInfoRegister"
+  "nat_to_cref :: nat \<Rightarrow> nat \<Rightarrow> cap_ref"
-definition
+  "msg_info_register :: register"
- "msg_registers \<equiv> msgRegisters"
+  "msg_registers :: register list"
-definition
+  "cap_register :: register"
- "cap_register \<equiv> capRegister"
+  "badge_register :: register"
-definition
+  "frame_registers :: register list"
- "badge_register \<equiv> badgeRegister"
+  "gp_registers :: register list"
-definition
+  "exception_message :: register list"
- "frame_registers \<equiv> frameRegisters"
+  "syscall_message :: register list"
-definition
+
- "gp_registers \<equiv> gpRegisters"
+  "new_context :: user_context"
-definition
+  "slot_bits :: nat"
- "exception_message \<equiv> exceptionMessage"
+  "oref_to_data   :: obj_ref \<Rightarrow> data"
-definition
+  "data_to_oref   :: data \<Rightarrow> obj_ref"
- "syscall_message \<equiv> syscallMessage"
+  "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

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

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"
 

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"
+  "../machine/MachineExports"
-begin
+
+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:

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

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

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

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

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 {*

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 *)
 (*<*)

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

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

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

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

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

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