theory ArchArch_AI

lemma cap_insert_ap_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. 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 (cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap ap asid)) and
   (\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s) and
   ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap and
   (\<lambda>s. ap \<notin> ran (asid_table s) \<and>
        asid_table s (asid_high_bits_of asid) = None)\<rbrace>
  cap_insert cap src dest
  \<lbrace>\<lambda>rv s. invs (s\<lparr>arch_state := arch_state s
                       \<lparr>arm_asid_table := ((arm_asid_table \<circ> arch_state) s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def) apply (strengthen valid_arch_state_strg
                    valid_asid_map_asid_upd_strg valid_vspace_objs_asid_upd_strg ) apply (simp cong: conj_cong) apply (rule hoare_pre) apply (wp cap_insert_simple_mdb cap_insert_iflive
             cap_insert_zombies cap_insert_ifunsafe cap_insert_vspace_objs
             cap_insert_valid_global_refs cap_insert_idle
             valid_irq_node_typ cap_insert_simple_arch_caps_ap) apply (clarsimp simp: is_simple_cap_def cte_wp_at_caps_of_state is_cap_simps) apply (frule safe_parent_cap_is_device) apply (drule safe_parent_cap_range) apply (simp add: cap_range_def) apply (rule conjI) prefer 2 apply (clarsimp simp: obj_at_def a_type_def) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule_tac p="(a,b)" in caps_of_state_valid_cap, fastforce) apply (auto simp: obj_at_def is_tcb_def is_cap_table_def
                    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. 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 (cap = ArchObjectCap (ASIDPoolCap ap asid)) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>s. ap \<notin> ran (asid_table s) \<and> asid_table s (asid_high_bits_of asid) = None)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := ((arm_asid_table \<circ> arch_state) s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<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. 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. cap = ArchObjectCap (ASIDPoolCap ap asid)) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>s. ap \<notin> ran (asid_table s) \<and> asid_table s (asid_high_bits_of asid) = None)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<and> valid_arch_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<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\<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. 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. cap = ArchObjectCap (ASIDPoolCap ap asid)) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>s. ap \<notin> ran (asid_table s) \<and> asid_table s (asid_high_bits_of asid) = None)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>r s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> (valid_arch_state s \<and> ap \<notin> ran (asid_table s) \<and> typ_at (AArch AASIDPool) ap 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> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s (asid_high_bits_of asid) = None) \<and> valid_arch_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> (valid_asid_map s \<and> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s (asid_high_bits_of asid) = None) \<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\<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. 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. cap = ArchObjectCap (ASIDPoolCap ap asid)) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>s. ap \<notin> ran (asid_table s) \<and> asid_table s (asid_high_bits_of asid) = None)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>r s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> ap \<notin> ran (asid_table s) \<and> typ_at (AArch AASIDPool) ap 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> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s (asid_high_bits_of asid) = None \<and> valid_arch_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<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\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q62\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>r s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> ap \<notin> ran (asid_table s) \<and> typ_at (AArch AASIDPool) ap 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> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s (asid_high_bits_of asid) = None \<and> valid_arch_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<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\<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. 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. cap = ArchObjectCap (ASIDPoolCap ap asid)) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>s. ap \<notin> ran (asid_table s) \<and> asid_table s (asid_high_bits_of asid) = None)) s \<Longrightarrow> ?Q62 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. 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. cap = ArchObjectCap (ASIDPoolCap ap asid)) and (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>s. ap \<notin> ran (asid_table s) \<and> asid_table s (asid_high_bits_of asid) = None)) 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> ap \<notin> ran (asid_table s) \<and> typ_at (AArch AASIDPool) ap 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> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s (asid_high_bits_of asid) = None \<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 (\<lambda>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and K (cap = ArchObjectCap (ASIDPoolCap ap asid))) 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None\<rbrakk> \<Longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n))) \<and> cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa \<and> typ_at (AArch AASIDPool) ap s \<and> cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa \<and> (cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<noteq> {} \<longrightarrow> \<not> 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; cap_is_device (ArchObjectCap (ASIDPoolCap ap asid)) = cap_is_device capa\<rbrakk> \<Longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n))) \<and> cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa \<and> typ_at (AArch AASIDPool) ap s \<and> cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa \<and> (cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<noteq> {} \<longrightarrow> \<not> 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; cap_is_device (ArchObjectCap (ASIDPoolCap ap asid)) = cap_is_device capa; cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa\<rbrakk> \<Longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n))) \<and> cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa \<and> typ_at (AArch AASIDPool) ap s \<and> cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<subseteq> cap_range capa \<and> (cap_range (ArchObjectCap (ASIDPoolCap ap asid)) \<noteq> {} \<longrightarrow> \<not> 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n))) \<and> typ_at (AArch AASIDPool) ap s 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n))
 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) ap s 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) ap s
 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n)) 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa\<rbrakk> \<Longrightarrow> \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<forall>r b n. cap \<noteq> Zombie r b n)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b ba 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa; caps_of_state s (a, b) = Some (Zombie ap ba n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b ba 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> ArchObjectCap (ASIDPoolCap ap asid); tcb_cap_valid (ArchObjectCap (ASIDPoolCap ap asid)) dest s; ex_cte_cap_wp_to (appropriate_cte_cap (ArchObjectCap (ASIDPoolCap ap asid))) dest s; caps_of_state s dest = Some NullCap; no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; ako_at (ASIDPool (\<lambda>x. None)) ap s; ap \<notin> ran (asid_table s); asid_table s (asid_high_bits_of asid) = None; \<not> cap_is_device capa; ap \<in> untyped_range capa \<or> ap \<in> obj_refs capa; s \<turnstile> Zombie ap ba n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!