theory ArchVSpace_AI

lemma arch_update_cap_invs_unmap_page_table:
  "\<lbrace>cte_wp_at (is_arch_update cap) p
             and invs and valid_cap cap
             and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s)
             and obj_at (empty_table {}) (obj_ref_of cap)
             and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r
                                \<longrightarrow> \<not> (r \<unrhd> obj_ref_of cap) s) p s)
             and K (is_pt_cap cap \<and> vs_cap_ref cap = None)\<rbrace>
  set_cap cap p
  \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: invs_def valid_state_def) apply (rule hoare_pre) apply (wp arch_update_cap_pspace arch_update_cap_valid_mdb set_cap_idle
             update_cap_ifunsafe valid_irq_node_typ set_cap_typ_at
             set_cap_irq_handlers set_cap_valid_arch_caps
             set_cap_cap_refs_respects_device_region_spec[where ptr = p]) apply (simp add: final_cap_at_eq) apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
                        is_cap_simps cap_master_cap_simps is_valid_vtable_root_def
                        appropriate_cte_cap_irqs is_pt_cap_def
                        fun_eq_iff[where f="cte_refs cap" for cap]
                 dest!: cap_master_cap_eqDs
              simp del: imp_disjL) apply (rule conjI) apply (drule(1) if_unsafe_then_capD [OF caps_of_state_cteD]) apply (clarsimp simp: cap_master_cap_def) apply (erule ex_cte_cap_wp_to_weakenE) apply (clarsimp simp: appropriate_cte_cap_def) apply (rule conjI) apply (drule valid_global_refsD2, clarsimp) apply (simp add: cap_range_def) apply (frule(1) cap_refs_in_kernel_windowD) apply (simp add: cap_range_def gen_obj_refs_def image_def) apply (intro conjI) apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                          cte_wp_at_caps_of_state) apply fastforce apply (clarsimp simp: obj_at_def empty_table_def) apply (clarsimp split: Structures_A.kernel_object.split_asm
                          arch_kernel_obj.split_asm) apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap) p and invs and valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) and obj_at (empty_table {}) (obj_ref_of cap) and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> (r, obj_ref_of cap) \<notin> vs_lookup_pages s) p s) and K (is_pt_cap cap \<and> vs_cap_ref cap = None)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap) p and (valid_pspace 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_arch_caps 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 valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) and obj_at (empty_table {}) (obj_ref_of cap) and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> (r, obj_ref_of cap) \<notin> vs_lookup_pages s) p s) and (\<lambda>y. is_pt_cap cap \<and> vs_cap_ref cap = None)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace 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_arch_caps 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>?Q\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace 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_arch_caps 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. (cte_wp_at (is_arch_update cap) p and (valid_pspace 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_arch_caps 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 valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) and obj_at (empty_table {}) (obj_ref_of cap) and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> (r, obj_ref_of cap) \<notin> vs_lookup_pages s) p s) and (\<lambda>y. is_pt_cap cap \<and> vs_cap_ref cap = None)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (is_arch_update cap) p and (valid_pspace 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_arch_caps 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 valid_cap cap and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) and obj_at (empty_table {}) (obj_ref_of cap) and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> (r, obj_ref_of cap) \<notin> vs_lookup_pages s) p s) and (\<lambda>y. is_pt_cap cap \<and> vs_cap_ref cap = None)) s \<Longrightarrow> (cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p and valid_pspace and valid_cap cap) s \<and> (cte_wp_at (is_arch_update cap) p and valid_mdb) s \<and> (valid_ioc and (\<lambda>s. cap = NullCap \<longrightarrow> \<not> is_original_cap s p)) s \<and> valid_idle s \<and> only_idle s \<and> (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap)) p and if_unsafe_then_cap and (\<lambda>s. cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) p and (\<lambda>s. \<forall>t rights. cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) p s))) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) p and (\<lambda>s. \<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst p = x \<and> snd p = tcb_cnode_index 2)) s \<and> (valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range cap = {})) s \<and> valid_arch_state s \<and> valid_irq_node s \<and> (valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) p s) \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> (valid_arch_caps s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') p s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {p} s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s p = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = p))) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> (cap_refs_in_kernel_window and (\<lambda>s. \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) s \<and> pspace_respects_device_region s \<and> (cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) p) s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (is_arch_update cap) p s \<and> valid_pspace 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 s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings 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 \<and> s \<turnstile> cap \<and> (\<exists>cp. cte_wp_at (\<lambda>c. c = cp) p s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<and> (a, b) \<noteq> p \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) (a, b) s)) \<and> obj_at (empty_table {}) (obj_ref_of cap) s \<and> cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> (r, obj_ref_of cap) \<notin> vs_lookup_pages s) p s \<and> is_pt_cap cap \<and> vs_cap_ref cap = None \<Longrightarrow> cte_wp_at (is_arch_update cap and (\<lambda>c. is_valid_vtable_root c \<longrightarrow> is_valid_vtable_root cap)) p s \<and> (cap = NullCap \<longrightarrow> \<not> is_original_cap s p) \<and> cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap)) p s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) \<and> cte_wp_at (\<lambda>_. True) p s \<and> (\<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> cte_wp_at (is_reply_cap_to t) p s)) \<and> cte_wp_at (\<lambda>_. True) p s \<and> (\<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst p = x \<and> snd p = tcb_cnode_index 2) \<and> global_refs s \<inter> cap_range cap = {} \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) p s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') p s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {p} s \<and> (cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> ((\<forall>oldcap. caps_of_state s p = Some oldcap \<longrightarrow> (is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageTableCap pa asid))) p s \<and> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageTableCap pa asid))) p s
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (3 subgoals):
 1. \<And>s pa asid data capa. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; ArchObjectCap (PageTableCap pa data) = capa\<rbrakk> \<Longrightarrow> capa \<noteq> NullCap
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. ArchObjectCap (PageTableCap pa data) = cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageTableCap pa asid))) p s
 3. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. ArchObjectCap (PageTableCap pa data) = cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageTableCap pa asid))) p s
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data cte_cap. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; \<exists>cap'. ArchObjectCap (PageTableCap pa data) = cap' \<and> appropriate_cte_cap cap' cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> appropriate_cte_cap (ArchObjectCap (PageTableCap pa asid)) cte_cap
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {}
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa data)) = {}\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap pa asid)) = {}
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs (ArchObjectCap (PageTableCap pa data)) \<inter> gen_obj_refs cap = {}); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; \<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa data)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageTableCap pa asid)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageTableCap pa asid)) \<subseteq> cap_range (ArchObjectCap (PageTableCap pa data)) proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s) \<and> (cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p)) proof (prove)
goal (3 subgoals):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap pa asid)) {p} s
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s
 3. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p) proof (prove)
goal (3 subgoals):
 1. \<And>s pa asid data a b capa. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow; (a, b) \<noteq> p; obj_refs capa = {pa}; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref (ArchObjectCap (PageTableCap pa asid))
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s
 3. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pa s
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p) proof (prove)
goal (2 subgoals):
 1. \<And>s pa asid data ko. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow; kheap s pa = Some ko; case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> {}) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False; cap_asid (ArchObjectCap (PageTableCap pa asid)) = None\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p) proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> cap_asid (ArchObjectCap (PageTableCap pa asid)) = None \<and> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y) \<longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = {pa} \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<longrightarrow> (a, b) = p) proof (prove)
goal (1 subgoal):
 1. \<And>s pa asid data a b y asida. \<lbrakk>valid_pspace s; valid_mdb s; cap = ArchObjectCap (PageTableCap pa asid); 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_arch_caps 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; s \<turnstile> ArchObjectCap (PageTableCap pa asid); obj_at (empty_table {}) pa s; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> pa \<notin> obj_refs cap); vs_cap_ref (ArchObjectCap (PageTableCap pa asid)) = None; caps_of_state s p = Some (ArchObjectCap (PageTableCap pa data)); \<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap pa data)) = Some r \<longrightarrow> (r, pa) \<notin> vs_lookup_pages s; arm_kernel_vspace (arch_state s) pa = ArmVSpaceKernelWindow; cap_asid (ArchObjectCap (PageTableCap pa asid)) = None; cap_asid (ArchObjectCap (PageTableCap pa data)) = Some y; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap pa asida))\<rbrakk> \<Longrightarrow> (a, b) = p proof (prove)
goal:
No subgoals!