theory ArchVSpace_AI

lemma set_asid_pool_valid_arch_caps_map:
  "\<lbrace>valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs
    and valid_vspace_objs and ko_at (ArchObj (ASIDPool pool)) ap
    and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap
                                   \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ((VSRef (ucast asid) (Some AASIDPool)) # rf))
                              \<and> (VSRef (ucast asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]))
    and page_directory_at pd
    and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s)
    and K (pool asid = None)\<rbrace>
  set_asid_pool ap (pool(asid \<mapsto> pd))
  \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply clarsimp apply (frule obj_at_not_pt_not_in_global_pts[where p=pd], clarsimp+) apply (simp add: a_type_def) apply (frule obj_at_not_pt_not_in_global_pts[where p=ap], clarsimp+) apply (clarsimp simp: obj_at_def valid_arch_caps_def
                        caps_of_state_after_update) apply (clarsimp simp: a_type_def
                 split: Structures_A.kernel_object.split_asm if_split_asm
                        arch_kernel_obj.split_asm) apply (frule(3) asid_pool_map.intro) apply (simp add: fun_upd_def[symmetric]) apply (rule conjI) apply (simp add: valid_vs_lookup_def
                    caps_of_state_after_update[folded fun_upd_def]
                    obj_at_def) apply (subst asid_pool_map.vs_lookup_pages2, assumption) apply simp apply (clarsimp simp: asid_pool_map.new_lookups_def) apply (frule(2) vs_lookup_vs_lookup_pagesI, simp add: valid_arch_state_def) apply (simp add: second_level_tables_def) apply (drule(2) ref_is_unique) apply (simp add: valid_vs_lookup_def) apply clarsimp+ apply (simp add: valid_arch_state_def) apply (rule valid_objs_caps, simp) apply fastforce apply (simp add: valid_table_caps_def
                   caps_of_state_after_update[folded fun_upd_def] obj_at_def
              del: imp_disjL) apply (clarsimp simp del: imp_disjL) apply (drule(1) caps_of_state_valid_cap)+ apply (auto simp add: valid_cap_def is_pt_cap_def is_pd_cap_def obj_at_def
                        a_type_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs and valid_vspace_objs and ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and K (pool asid = None)\<rbrace> set_asid_pool ap (pool(asid \<mapsto> pd)) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs and valid_vspace_objs and ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None])) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and (\<lambda>y. pool asid = None)\<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_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs and valid_vspace_objs and ako_at (ASIDPool pool) ap and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf)) \<and> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None])) and typ_at (AArch APageDirectory) pd and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) and (\<lambda>y. pool asid = None)) s \<Longrightarrow> \<forall>ko. ko_at ko ap s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) \<longrightarrow> valid_arch_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko rf a b cap. \<lbrakk>valid_arch_caps s; valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; ako_at (ASIDPool pool) ap s; typ_at (AArch APageDirectory) pd s; (rf \<rhd> ap) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); ko_at ko ap s; a_type ko = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rbrakk> \<Longrightarrow> valid_arch_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko rf a b cap. \<lbrakk>valid_arch_caps s; valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; ako_at (ASIDPool pool) ap s; typ_at (AArch APageDirectory) pd s; (rf \<rhd> ap) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); ko_at ko ap s; a_type ko = a_type (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))); pd \<notin> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> valid_arch_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko rf a b cap. \<lbrakk>valid_arch_caps s; valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; ako_at (ASIDPool pool) ap s; obj_at (\<lambda>ob. (case ob of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory) pd s; (rf \<rhd> ap) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); ko_at ko ap s; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch AASIDPool; pd \<notin> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> valid_arch_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko rf a b cap. \<lbrakk>valid_arch_caps s; valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; ako_at (ASIDPool pool) ap s; obj_at (\<lambda>ob. (case ob of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory) pd s; (rf \<rhd> ap) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); ko_at ko ap s; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch AASIDPool; pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> valid_arch_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap koa. \<lbrakk>valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; (case koa of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory; kheap s pd = Some koa; empty_table (set (second_level_tables (arch_state s))) koa; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := \<lambda>a. if a = ap then Some (ArchObj (ASIDPool (\<lambda>a. if a = asid then Some pd else pool a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) \<and> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>)
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> \<forall>p ref. (ref \<unrhd> p) (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> \<forall>p ref. (ref, p) \<in> vs_lookup_pages s \<union> asid_pool_map.new_lookups ap asid pd `` vs_lookup_pages s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> \<forall>p ref. (ref, p) \<in> asid_pool_map.new_lookups ap asid pd `` vs_lookup_pages s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_vs_lookup s
 2. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> unique_table_refs (caps_of_state s)
 3. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 4. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 5. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_caps (caps_of_state s) s
 6. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s; rf = aa\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 7. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> unique_table_refs (caps_of_state s)
 2. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 4. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_caps (caps_of_state s) s
 5. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s; rf = aa\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 6. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table s) s
 2. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_caps (caps_of_state s) s
 3. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s; rf = aa\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 4. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s\<rbrakk> \<Longrightarrow> valid_caps (caps_of_state s) s
 2. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s; rf = aa\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 3. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s rf a b cap x3 aa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (arm_global_pts (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (arm_global_pts (arch_state s)); ap \<notin> set (arm_global_pts (arch_state s)); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); asid_pool_map s ap pool asid pd x3; (aa \<unrhd> ap) s; (aa \<rhd> ap) s; rf = aa\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> aa \<noteq> [VSRef 0 None]) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # aa))
 2. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> valid_table_caps (s\<lparr>kheap := (kheap s)(ap \<mapsto> ArchObj (ASIDPool (pool(asid \<mapsto> pd))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3\<rbrakk> \<Longrightarrow> \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> ap \<in> obj_refs cap \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3 aa ba capa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; caps_of_state s (a, b) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3; caps_of_state s (aa, ba) = Some capa; is_pd_cap capa \<or> is_pt_cap capa; cap_asid capa = None; ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) proof (prove)
goal (1 subgoal):
 1. \<And>s rf a b cap x3 aa ba capa. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory x3)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory x3)); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> (\<exists>ko. kheap s r = Some ko \<and> empty_table (set (second_level_tables (arch_state s))) ko); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_arch_state s; valid_global_objs s; valid_objs s; valid_vspace_objs s; kheap s ap = Some (ArchObj (ASIDPool pool)); (rf \<rhd> ap) s; pool asid = None; UCAST(10 \<rightarrow> 32) asid = 0 \<longrightarrow> rf \<noteq> [VSRef 0 None]; pd \<in> obj_refs cap; vs_cap_ref cap = Some (VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rf); pd \<notin> set (second_level_tables (arch_state s)); ap \<notin> set (second_level_tables (arch_state s)); valid_vs_lookup s; asid_pool_map s ap pool asid pd x3; is_pd_cap capa \<or> is_pt_cap capa; cap_asid capa = None; ap \<in> obj_refs capa; s \<turnstile> cap; s \<turnstile> capa\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (ASIDPool (pool(asid \<mapsto> pd)))) proof (prove)
goal:
No subgoals!