theory ArchVSpace_AI

lemma arch_update_cap_invs_unmap_page:
  "\<lbrace>(\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> \<not> (ref \<unrhd> p') s) \<and> is_arch_update cap c) p s)
             and invs and valid_cap cap
             and K (is_pg_cap cap)\<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 clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
                        is_cap_simps cap_master_cap_simps
                        fun_eq_iff appropriate_cte_cap_irqs
                        is_pt_cap_def is_valid_vtable_root_def
                 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) subgoal by (simp add: cap_range_def) apply (rule conjI[rotated]) apply (frule(1) cap_refs_in_kernel_windowD) apply (simp add: cap_range_def) apply (drule unique_table_refs_no_cap_asidE[where S="{p}"]) apply (simp add: valid_arch_caps_def) apply (simp add: no_cap_to_obj_with_diff_ref_def table_cap_ref_def Ball_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap c) p s) and invs and valid_cap cap and K (is_pg_cap cap)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap c) p s) 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>y. is_pg_cap cap)\<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. ((\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap c) p s) 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>y. is_pg_cap cap)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap c) p s) 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>y. is_pg_cap cap)) 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. \<lbrakk>cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap c) p s; valid_pspace 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_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> cap; is_pg_cap cap\<rbrakk> \<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> cte_wp_at (is_arch_update 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> 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 \<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_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 \<longrightarrow> (\<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> (is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s p = Some oldcap \<longrightarrow> (is_pt_cap cap \<and> 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 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' \<or> is_pt_cap cap \<and> 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 dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageCap dev pa R sz m))) p s \<and> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (2 subgoals):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageCap dev pa R sz m))) p s
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (3 subgoals):
 1. \<And>s dev p R sz m rghts mapdata capa. \<lbrakk>valid_pspace 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_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 (PageCap dev p R sz m); cap = ArchObjectCap (PageCap dev p R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev p rghts sz mapdata)) = Some ref \<longrightarrow> (ref, p) \<notin> vs_lookup_pages s; ArchObjectCap (PageCap dev p rghts sz mapdata) = capa\<rbrakk> \<Longrightarrow> capa \<noteq> NullCap
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. ArchObjectCap (PageCap dev pa rghts sz mapdata) = cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageCap dev pa R sz m))) p s
 3. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (2 subgoals):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. ArchObjectCap (PageCap dev pa rghts sz mapdata) = cap' \<and> appropriate_cte_cap cap' cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (PageCap dev pa R sz m))) p s
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (2 subgoals):
 1. \<And>s dev pa R sz m rghts mapdata cte_cap. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s; \<exists>cap'. ArchObjectCap (PageCap dev pa rghts sz mapdata) = cap' \<and> appropriate_cte_cap cap' cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> appropriate_cte_cap (ArchObjectCap (PageCap dev pa R sz m)) cte_cap
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {} \<and> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (2 subgoals):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev pa R sz m)) = {}
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (2 subgoals):
 1. \<And>s dev p R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev p R sz m); cap = ArchObjectCap (PageCap dev p R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev p rghts sz mapdata)) = Some ref \<longrightarrow> (ref, p) \<notin> vs_lookup_pages s; global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev p rghts sz mapdata)) = {}\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap dev p R sz m)) = {}
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace 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_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 (PageCap dev_ p_ R_ sz_ m_); cap = ArchObjectCap (PageCap dev_ p_ R_ sz_ m_); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev_ p_ rghts_ sz_ mapdata_)) = Some ref \<longrightarrow> (ref, p_) \<notin> vs_lookup_pages s_; global_refs s_ \<inter> cap_range (ArchObjectCap (PageCap dev_ p_ rghts_ sz_ mapdata_)) = {}\<rbrakk> \<Longrightarrow> global_refs s_ \<inter> cap_range (ArchObjectCap (PageCap dev_ p_ R_ sz_ m_)) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s \<and> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)) proof (prove)
goal (2 subgoals):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata))
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s proof (prove)
goal (2 subgoals):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s; \<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> (\<forall>ref\<in>cap_range (ArchObjectCap (PageCap dev pa R sz m)). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> cap_range (ArchObjectCap (PageCap dev pa R sz m)) \<subseteq> cap_range (ArchObjectCap (PageCap dev pa rghts sz mapdata))
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s proof (prove)
goal (1 subgoal):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); caps_of_state s p = Some (ArchObjectCap (PageCap dev pa rghts sz mapdata)); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s proof (prove)
goal (2 subgoals):
 1. \<And>s dev p R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev p R sz m); cap = ArchObjectCap (PageCap dev p R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev p rghts sz mapdata)) = Some ref \<longrightarrow> (ref, p) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> unique_table_refs (caps_of_state s)
 2. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s; no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) {p} s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s proof (prove)
goal (1 subgoal):
 1. \<And>s dev pa R sz m rghts mapdata. \<lbrakk>valid_pspace 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_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 (PageCap dev pa R sz m); cap = ArchObjectCap (PageCap dev pa R sz m); \<forall>ref. vs_cap_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) = Some ref \<longrightarrow> (ref, pa) \<notin> vs_lookup_pages s; no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa rghts sz mapdata)) {p} s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap dev pa R sz m)) {p} s proof (prove)
goal:
No subgoals!