theory ArchVSpace_AI

lemma set_pd_invs_unmap':
  "\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and
    (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and
    obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and
    obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and
    obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd')
                       \<and> (\<forall>x \<in> kernel_mapping_slots. pd x = pd' x)) p and
    (\<lambda>s. p \<notin> global_refs s) and
    (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and>
                   is_pd_cap cap \<and>
                   p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and
    (\<lambda>s. \<forall>(a,b)\<in>S'. (\<forall>ref.
                  (ref \<unrhd> p) s \<longrightarrow>
                    (\<exists>p' cap.
                      caps_of_state s p' = Some cap \<and>
                      b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref))))\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def) apply (rule hoare_pre) apply (wp set_pd_valid_objs set_pd_iflive set_pd_zombies
             set_pd_zombies_state_refs set_pd_valid_mdb
             set_pd_zombies_state_hyp_refs
             set_pd_valid_idle set_pd_ifunsafe set_pd_reply_caps
             set_pd_valid_arch set_pd_valid_global set_pd_cur
             set_pd_reply_masters valid_irq_node_typ
             set_pd_vspace_objs_unmap set_pd_valid_vs_lookup_map[where T=T and S="{}" and T'=T' and S'=S']
             valid_irq_handlers_lift
             set_pd_unmap_mappings set_pd_equal_kernel_mappings_triv) apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def valid_objs_caps obj_at_def
    del: disjCI) apply (rule conjI, clarsimp) apply (erule_tac x="(VSRef (ucast c) (Some APageDirectory), q)" in ballE) apply clarsimp apply (frule (1) vs_refs_pages_pdI) apply (clarsimp simp: valid_arch_caps_def) apply (drule_tac p'=q and ref'="VSRef (ucast c) (Some APageDirectory) # r" in vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) apply (drule (1) valid_vs_lookupD) apply (clarsimp) apply (rule conjI) apply clarsimp apply (drule (1) vs_refs_pdI3) apply clarsimp apply (drule_tac p'=q and ref'="VSRef (ucast c) (Some APageDirectory) # r" in vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) apply (erule subsetD[OF vs_refs_pages_subset]) apply (drule_tac p'=q' and ref'="VSRef (ucast d) (Some APageTable) # VSRef (ucast c) (Some APageDirectory) # r"
                 in vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) apply (erule pte_ref_pagesD) apply (drule (1) valid_vs_lookupD) apply clarsimp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and (\<lambda>s. \<forall>(a, b)\<in>S'. \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)))\<rbrace> set_pd p pd \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and (\<lambda>s. \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)))\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and (\<lambda>s. \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)))) s \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s)) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and (\<lambda>s. p \<notin> global_refs s) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and (\<lambda>s. \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)))) s \<Longrightarrow> ((\<lambda>s. \<forall>i. wellformed_pde (pd i)) and valid_objs) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> (valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p) s \<and> (valid_vs_lookup and valid_arch_state and valid_vspace_objs and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> {}) p and (\<lambda>s. \<forall>x\<in>{}. typ_at (AArch APageTable) (snd x) s) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and (\<lambda>s. \<forall>(r, p')\<in>{}. \<forall>ao. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> ako_at ao p' s \<longrightarrow> valid_vspace_obj ao s) and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) and (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt d. ako_at (PageTable pt) q s \<longrightarrow> pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) s \<and> (valid_table_caps and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot cap. caps_of_state s slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<and> valid_caps (caps_of_state s) s \<and> unique_table_caps (caps_of_state s))) s \<and> (unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p \<in> obj_refs cap) slot s))) s \<and> (valid_kernel_mappings and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p) s \<and> (obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and equal_kernel_mappings) s \<and> valid_asid_map s \<and> (valid_global_vspace_mappings s \<and> valid_global_objs s \<and> p \<notin> global_refs s) \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref_pages (pd c) = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))) \<and> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (3 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; case (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref))\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T'\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (3 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T'\<rbrakk> \<Longrightarrow> ((r, p), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q) \<in> vs_lookup_pages1 s
 2. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T'; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T'; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; pde_ref_pages (pd c) = Some q; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> S'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T'; \<exists>slot cap. caps_of_state s slot = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> (\<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))) \<and> (empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> \<forall>r. (r \<unrhd> p) s \<longrightarrow> (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. pde_ref (pd c) = Some q \<longrightarrow> (\<forall>q' pt. kheap s q = Some (ArchObj (PageTable pt)) \<longrightarrow> (\<forall>d. pte_ref_pages (pt d) = Some q' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)))))
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some q; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; (r \<unrhd> p) s; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (3 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T\<rbrakk> \<Longrightarrow> ((r, p), VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q) \<in> vs_lookup_pages1 s
 2. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (3 subgoals):
 1. \<And>s pd' a b cap y c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs_pages (ArchObj (PageDirectory pd'))
 2. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (3 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T\<rbrakk> \<Longrightarrow> ((VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q), VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r, q') \<in> vs_lookup_pages1 s
 2. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; ((VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q') s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (3 subgoals):
 1. \<And>s pd' a b cap y c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T\<rbrakk> \<Longrightarrow> (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable), q') \<in> vs_refs_pages (ArchObj (PageTable pt))
 2. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; ((VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q') s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 3. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; ((VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r) \<unrhd> q') s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s pd' a b cap y r c q q' pt d. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y; c \<notin> kernel_mapping_slots; kheap s q = Some (ArchObj (PageTable pt)); pte_ref_pages (pt d) = Some q'; (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<in> vs_refs (ArchObj (PageDirectory pd')); (VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory), q) \<notin> T; \<exists>slot cap. caps_of_state s slot = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) d) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) c) (Some APageDirectory) # r)
 2. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal (1 subgoal):
 1. \<And>s pd' a b cap y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>i. wellformed_pde (pd i); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd x) s); vs_refs (ArchObj (PageDirectory pd)) = vs_refs (ArchObj (PageDirectory pd')) - T; vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages (ArchObj (PageDirectory pd')) - T' \<union> S'; p \<notin> global_refs s; kheap s p = Some (ArchObj (PageDirectory pd')); \<forall>x\<in>S'. case x of (a, b) \<Rightarrow> \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<exists>aa ba cap. caps_of_state s (aa, ba) = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)); \<forall>x\<in>kernel_mapping_slots. pd x = pd' x; caps_of_state s (a, b) = Some cap; is_pd_cap cap; p \<in> obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd')) \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)) \<or> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap) proof (prove)
goal:
No subgoals!