theory ArchFinalise_AI

lemma set_asid_pool_invs_table:
  "\<lbrace>\<lambda>s. invs s \<and> asid_pool_at p s
       \<and> (\<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))
       \<and> (\<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p) s)
       \<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
       set_asid_pool p Map.empty
  \<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
                 (arm_asid_table (arch_state s))(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def) apply (rule hoare_pre) apply (wp valid_irq_node_typ set_asid_pool_typ_at
             set_asid_pool_empty_table_objs
             valid_irq_handlers_lift set_asid_pool_empty_table_lookup
             set_asid_pool_empty_valid_asid_map
          | strengthen valid_arch_state_table_strg)+ apply (clarsimp simp: conj_comms) apply (rule context_conjI) apply clarsimp apply (frule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) apply clarsimp apply (drule obj_ref_elemD) apply (frule(2) unique_table_refsD,
          unfold obj_refs.simps aobj_ref.simps option.simps,
          assumption) apply (clarsimp simp: vs_cap_ref_def table_cap_ref_def
                  split: cap.split_asm arch_cap.split_asm) apply clarsimp apply (drule vs_asid_refsI) apply (drule vs_lookupI, rule rtrancl_refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> typ_at (AArch AASIDPool) p s \<and> (\<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base))) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p) \<notin> vs_lookup s \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s)\<rbrace> set_asid_pool p (\<lambda>x. None) \<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> typ_at (AArch AASIDPool) p s \<and> (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base))) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p) \<notin> vs_lookup s \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s)\<rbrace> set_asid_pool p (\<lambda>x. None) \<lbrace>\<lambda>x 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 base \<mapsto> p)\<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 base \<mapsto> p)\<rparr>\<rparr>) \<and> valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<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 base \<mapsto> p)\<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 (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> set_asid_pool p (\<lambda>x. None) \<lbrace>\<lambda>x 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 base \<mapsto> p)\<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 base \<mapsto> p)\<rparr>\<rparr>) \<and> valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>) \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<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 base \<mapsto> p)\<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>
 2. \<And>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> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> typ_at (AArch AASIDPool) p s \<and> (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base))) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p) \<notin> vs_lookup s \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s) \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>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> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> typ_at (AArch AASIDPool) p s \<and> (\<exists>a b. caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base))) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p) \<notin> vs_lookup s \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s) \<Longrightarrow> 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> typ_at (AArch AASIDPool) p s \<and> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> (valid_vspace_objs and typ_at (AArch AASIDPool) p) s \<and> (valid_vs_lookup and typ_at (AArch AASIDPool) p and (\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))) s \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<and> (valid_global_objs and valid_arch_state) s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> (valid_asid_map s \<and> typ_at (AArch AASIDPool) p s \<and> (\<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s) \<and> (\<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup 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 proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base))\<rbrakk> \<Longrightarrow> (\<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s) \<and> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base))\<rbrakk> \<Longrightarrow> \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s
 2. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (2 subgoals):
 1. \<And>s a b asid'. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); ([VSRef asid' None] \<rhd> p) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (2 subgoals):
 1. \<And>s a b asid'. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); ([VSRef asid' None] \<rhd> p) s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef asid' None]\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (2 subgoals):
 1. \<And>s a b asid' aa ba cap. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); ([VSRef asid' None] \<rhd> p) s; caps_of_state s (aa, ba) = Some cap; p \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef asid' None]\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (2 subgoals):
 1. \<And>s a b asid' aa ba cap. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); ([VSRef asid' None] \<rhd> p) s; caps_of_state s (aa, ba) = Some cap; vs_cap_ref cap = Some [VSRef asid' None]; obj_refs cap = {p}\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (2 subgoals):
 1. \<And>s a b asid' aa ba cap. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); ([VSRef asid' None] \<rhd> p) s; caps_of_state s (aa, ba) = Some cap; vs_cap_ref cap = Some [VSRef asid' None]; obj_refs cap = {p}; table_cap_ref cap = table_cap_ref (ArchObjectCap (ASIDPoolCap p base))\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> Some p \<notin> asid_table s ` (dom (asid_table s) - {asid_high_bits_of base}) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; asid_table s x = Some p\<rbrakk> \<Longrightarrow> x = asid_high_bits_of base proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> x = asid_high_bits_of base proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_kernel_mappings s; valid_table_caps s; valid_vs_lookup s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); typ_at (AArch AASIDPool) p s; \<forall>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], p') \<notin> vs_lookup s; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap p base)); \<forall>asid'. ([VSRef asid' None], p) \<notin> vs_lookup s; ([VSRef (UCAST(7 \<rightarrow> 32) x) None] \<rhd> p) s\<rbrakk> \<Longrightarrow> x = asid_high_bits_of base proof (prove)
goal:
No subgoals!