theory ArchVSpace_AI

lemma set_asid_pool_arch_objs_map:
  "\<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs and
    valid_kernel_mappings and
    ko_at (ArchObj (ASIDPool pool)) ap and
    K (pool asid = None) and
    \<exists>\<rhd> ap and page_directory_at pd and
    (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) \<rbrace>
  set_asid_pool ap (pool(asid \<mapsto> pd))
  \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (simp only: a_type_def[split_simps kernel_object.split arch_kernel_obj.split]) apply (clarsimp simp del: fun_upd_apply
                  split: Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (frule (2) valid_vspace_objsD) apply (clarsimp simp: valid_vspace_objs_def simp del: valid_vspace_obj.simps) apply (case_tac "p = ap") apply (clarsimp simp: obj_at_def
               simp del: fun_upd_apply valid_vspace_obj.simps) apply (clarsimp simp: ran_def) apply (case_tac "a = asid") apply clarsimp apply (rule typ_at_same_type) apply (simp add: obj_at_def a_type_simps) prefer 2 apply assumption apply (simp add: a_type_def) apply clarsimp apply (erule allE, erule impE, rule exI, assumption)+ apply (erule typ_at_same_type) prefer 2 apply assumption apply (simp add: a_type_def) apply (clarsimp simp: obj_at_def a_type_simps) apply (frule (3) asid_pool_map.intro) apply (subst (asm) asid_pool_map.vs_lookup, assumption) apply clarsimp apply (erule disjE) apply (erule_tac x=p in allE, simp) apply (erule impE, blast) apply (erule valid_vspace_obj_same_type) apply (simp add: obj_at_def a_type_def) apply (simp add: a_type_def) apply (clarsimp simp: asid_pool_map.new_lookups_rtrancl) apply (erule disjE) apply clarsimp apply (erule_tac x=p in allE, simp) apply (erule impE, blast) apply (erule valid_vspace_obj_same_type) apply (simp add: obj_at_def a_type_def) apply (simp add: a_type_def) apply (clarsimp simp: asid_pool_map.new_lookups_def empty_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs and valid_kernel_mappings and ako_at (ASIDPool pool) ap and K (pool asid = None) and (\<lambda>s. \<exists>ref. (ref \<rhd> ap) s) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)\<rbrace> set_asid_pool ap (pool(asid \<mapsto> pd)) \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs and valid_kernel_mappings and ako_at (ASIDPool pool) ap and (\<lambda>y. pool asid = None) and (\<lambda>s. \<exists>ref. (ref \<rhd> ap) s) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)\<rbrace> do kobj <- get_object ap;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
od \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and valid_arch_state and valid_global_objs and valid_kernel_mappings and ako_at (ASIDPool pool) ap and (\<lambda>y. pool asid = None) and (\<lambda>s. \<exists>ref. (ref \<rhd> ap) s) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)) s \<Longrightarrow> \<forall>ko. ko_at ko ap s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) \<longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and valid_arch_state and valid_global_objs and valid_kernel_mappings and ako_at (ASIDPool pool) ap and (\<lambda>y. pool asid = None) and (\<lambda>s. \<exists>ref. (ref \<rhd> ap) s) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)) s \<Longrightarrow> \<forall>ko. ko_at ko ap s \<longrightarrow> a_type ko = AArch AASIDPool \<longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref apa. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref apa. \<lbrakk>valid_vspace_objs s; valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p = ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ((kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))) ap = Some (ArchObj ao); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a = asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 3. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 3. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s
 2. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko65 s ref rs pda)
 3. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko65 s ref rs pda)
 4. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 5. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko65 s ref rs pda)
 2. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko65 s ref rs pda)
 3. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 4. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko65 s ref rs pda)
 2. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko65 s ref rs pda)
 3. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 4. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref rs pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (ArchObj (ASIDPool pool))
 2. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 3. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); a = asid \<longrightarrow> pd = x; a \<noteq> asid \<longrightarrow> pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x. (\<exists>a. pool a = Some x) \<longrightarrow> typ_at (AArch APageDirectory) x s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid; \<forall>ao. kheap s ap = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s; typ_at (AArch APageDirectory) x s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid; \<forall>ao. kheap s ap = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko85 s ref rs pda x a)
 2. \<And>s ref rs pda x a. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid; \<forall>ao. kheap s ap = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko85 s ref rs pda x a)
 3. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid; \<forall>ao. kheap s ap = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko85 s ref rs pda x a)
 2. \<And>s ref rs pda x a. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid; \<forall>ao. kheap s ap = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko85 s ref rs pda x a)
 3. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref rs pda x a. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; (rs \<rhd> ap) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); pool a = Some x; a \<noteq> asid; \<forall>ao. kheap s ap = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (ArchObj (ASIDPool pool))
 2. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref apa p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; ako_at (ASIDPool pool) ap s; pool asid = None; (ref \<rhd> ap) s; typ_at (AArch APageDirectory) pd s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; ako_at (ASIDPool apa) ap s; valid_vspace_obj (ASIDPool pool) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); ako_at ao p (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); p \<noteq> ap\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>); kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; (rs, p) \<in> vs_lookup s \<union> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; (rs \<rhd> p) s \<or> (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s; (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko115 s ref p rs ao pda)
 2. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko115 s ref p rs ao pda)
 3. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (ArchObj (ASIDPool pool))
 2. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs, p) \<in> (asid_pool_map.new_lookups ap asid pd)\<^sup>* `` vs_lookup s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; a = rs \<and> b = p \<or> ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd; (a \<rhd> b) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; a = rs \<and> b = p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s; (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> kheap s ap = Some (?ko140 s ref p rs ao pda)
 2. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (?ko140 s ref p rs ao pda)
 3. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ref p rs ao pda. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) = a_type (ArchObj (ASIDPool pool))
 2. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ref p rs ao pda a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); valid_arch_state s; valid_global_objs s; valid_kernel_mappings s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; (ref \<rhd> ap) s; \<forall>x\<in>ran pool. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; kheap s p = Some (ArchObj ao); p \<noteq> ap; kheap s pd = Some (ArchObj (PageDirectory pda)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); asid_pool_map s ap pool asid pd pda; (a \<rhd> b) s; ((a, b), rs, p) \<in> asid_pool_map.new_lookups ap asid pd\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal:
No subgoals!