theory ArchCSpace_AI

lemma cap_insert_simple_invs:
  "\<lbrace>invs and valid_cap cap and tcb_cap_valid cap dest and
    ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and
    cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}) src and
    cte_wp_at (\<lambda>c. c = cap.NullCap) dest and
    no_cap_to_obj_with_diff_ref cap {dest} and
    (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
    K (is_simple_cap cap \<and> \<not>is_ap_cap cap) and (\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s)\<rbrace>
  cap_insert cap src dest \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre) apply (wp cap_insert_simple_mdb cap_insert_iflive
             cap_insert_zombies cap_insert_ifunsafe
             cap_insert_valid_global_refs cap_insert_idle
             valid_irq_node_typ cap_insert_simple_arch_caps_no_ap) apply (clarsimp simp: is_simple_cap_def cte_wp_at_caps_of_state) apply (frule safe_parent_cap_range) apply simp apply (rule conjI) prefer 2 apply (clarsimp simp: is_cap_simps safe_parent_for_def) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule_tac p="(a,b)" in caps_of_state_valid_cap, fastforce) apply (clarsimp dest!: is_cap_simps' [THEN iffD1]) apply (auto simp add: valid_cap_def [where c="cap.Zombie a b x" for a b x]
              dest: obj_ref_is_tcb obj_ref_is_cap_table split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}) src and cte_wp_at (\<lambda>c. c = NullCap) dest and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and K (is_simple_cap cap \<and> \<not> is_ap_cap cap) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_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 tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}) src and cte_wp_at (\<lambda>c. c = NullCap) dest and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_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> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_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. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_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 tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}) src and cte_wp_at (\<lambda>c. c = NullCap) dest and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_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 tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}) src and cte_wp_at (\<lambda>c. c = NullCap) dest and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s)) s \<Longrightarrow> (valid_objs and valid_cap cap and tcb_cap_valid cap dest) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. cte_wp_at (\<lambda>c. r \<in> obj_refs c) p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)) s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> (valid_mdb and valid_objs and cte_wp_at (\<lambda>c. c = NullCap) dest and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and K (is_simple_cap cap)) s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> (if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest) s \<and> (valid_reply_caps and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) dest and K (\<not> is_master_reply_cap cap)) s \<and> (valid_global_refs and cte_wp_at (\<lambda>scap. cap_range cap \<subseteq> cap_range scap) src) 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) src s) \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> (valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and no_cap_to_obj_with_diff_ref cap {dest} and K (is_simple_cap cap \<and> \<not> is_ap_cap cap)) 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 and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src) 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)) src) s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs cap. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap)) \<and> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> cap_range cap \<subseteq> cap_range capa \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs cap. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap)) \<and> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> cap_range cap \<subseteq> cap_range capa \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs cap. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap)) \<and> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> \<forall>r\<in>obj_refs cap. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap)
 2. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa)
 2. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> \<forall>r\<in>obj_refs cap. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> \<forall>r\<in>obj_refs cap. \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> \<not> is_zombie cap) proof (prove)
goal (1 subgoal):
 1. \<And>s capa r a b capaa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa; r \<in> obj_refs cap; caps_of_state s (a, b) = Some capaa; r \<in> obj_refs capaa; is_zombie capaa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa r a b capaa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa; r \<in> obj_refs cap; r \<in> obj_refs capaa; is_zombie capaa; s \<turnstile> capaa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa ra b n. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_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; tcb_cap_valid cap dest s; ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s; caps_of_state s dest = Some NullCap; is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}; no_cap_to_obj_with_diff_ref cap {dest} s; cap \<noteq> NullCap; caps_of_state s src = Some capa; safe_parent_for (cdt s) src cap capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; \<not> is_ap_cap cap; \<forall>irq\<in>cap_irqs cap. irq_issued irq s; cap_range cap \<subseteq> cap_range capa; ra \<in> obj_refs cap; s \<turnstile> Zombie ra b n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!