theory CNode_DR

lemma dcorres_clear_object_caps_asid_pool:
  "dcorres dc \<top> (invs and  cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.ASIDPoolCap w asid))) slot)
    (clear_object_caps w)
    (set_asid_pool w Map.empty)" apply (clarsimp simp:clear_object_caps_def gets_def) apply (rule dcorres_absorb_get_l) apply (subgoal_tac "\<exists>pool. (ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) w) s'") apply (clarsimp simp:invs_def valid_state_def valid_pspace_def valid_mdb_def) apply (drule cte_wp_valid_cap,simp) apply (clarsimp simp:valid_cap_def cap_aligned_def) apply (rule corres_guard_imp) apply (rule select_pick_corres) apply (rule dcorres_set_asid_pool_empty) apply (clarsimp simp: distinct_map distinct_enum_upto inj_on_def intro!:set_eqI) apply (rule iffI) apply (fastforce intro!:opt_cap_asid_pool_not_None) apply (subgoal_tac "b < 2 ^ asid_low_bits") apply simp apply (rule ccontr) apply (drule_tac ba = b in opt_cap_asid_pool_None) apply clarsimp apply clarsimp apply clarsimp apply clarsimp apply (clarsimp simp:invs_def valid_state_def valid_cap_def obj_at_def a_type_def
                       valid_pspace_def dest!: cte_wp_valid_cap) by (clarsimp split: Structures_A.kernel_object.split_asm
                      arch_kernel_obj.split_asm if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) (clear_object_caps w) (set_asid_pool w (\<lambda>x. None)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) (do s <- get;
select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr s = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot
od) (set_asid_pool w (\<lambda>x. None)) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (set_asid_pool w (\<lambda>x. None)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'; \<exists>pool. ako_at (ASIDPool pool) w s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (set_asid_pool w (\<lambda>x. None))
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' pool. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (set_asid_pool w (\<lambda>x. None))
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' pool. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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 w asid)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (set_asid_pool w (\<lambda>x. None))
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' pool. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (set_asid_pool w (\<lambda>x. None))
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' pool. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> dcorres dc (?Q54 s' pool) (?Q'54 s' pool) (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (set_asid_pool w (\<lambda>x. None))
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; transform s' = s\<rbrakk> \<Longrightarrow> ?Q54 s' pool s
 3. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> ?Q'54 s' pool s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' pool. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> dcorres dc (?P58 s' pool) (?Q'54 s' pool) (mapM_x PageTableUnmap_D.empty_slot (?x58 s' pool)) (set_asid_pool w (\<lambda>x. None))
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; transform s' = s\<rbrakk> \<Longrightarrow> (?P58 s' pool and (\<lambda>s. ?x58 s' pool \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> ?Q'54 s' pool s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (Pair w) [0 .e. 2 ^ local.asid_low_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> ((a, b) \<in> Pair w ` {0..<2 ^ local.asid_low_bits}) = (a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y))
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; (a, b) \<in> Pair w ` {0..<2 ^ local.asid_low_bits}\<rbrakk> \<Longrightarrow> a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y)
 2. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y)\<rbrakk> \<Longrightarrow> (a, b) \<in> Pair w ` {0..<2 ^ local.asid_low_bits}
 3. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y)\<rbrakk> \<Longrightarrow> (a, b) \<in> Pair w ` {0..<2 ^ local.asid_low_bits}
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); b < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> (a, b) \<in> Pair w ` {0..<2 ^ local.asid_low_bits}
 2. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y)\<rbrakk> \<Longrightarrow> b < 2 ^ local.asid_low_bits
 3. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y)\<rbrakk> \<Longrightarrow> b < 2 ^ local.asid_low_bits
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' pool a b. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' pool a b. \<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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> valid_idle s'
 2. \<And>s' pool a b. \<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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> \<not> b < 2 ^ local.asid_low_bits
 3. \<And>s' pool a b. \<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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits; opt_cap (w, b) (transform s') = None\<rbrakk> \<Longrightarrow> False
 4. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' pool a b. \<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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> \<not> b < 2 ^ local.asid_low_bits
 2. \<And>s' pool a b. \<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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits; opt_cap (w, b) (transform s') = None\<rbrakk> \<Longrightarrow> False
 3. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' pool a b. \<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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; a = w \<and> (\<exists>y. opt_cap (a, b) (transform s') = Some y); \<not> b < 2 ^ local.asid_low_bits; opt_cap (w, b) (transform s') = None\<rbrakk> \<Longrightarrow> False
 2. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' pool s. \<lbrakk>ako_at (ASIDPool pool) w s'; 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'); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); untyped_mdb (cdt s') (caps_of_state s'); descendants_inc (cdt s') (caps_of_state s'); no_mloop (cdt s'); untyped_inc (cdt s') (caps_of_state s'); ut_revocable (is_original_cap s') (caps_of_state s'); irq_revocable (is_original_cap s') (caps_of_state s'); reply_master_revocable (is_original_cap s') (caps_of_state s'); reply_mdb (cdt s') (caps_of_state 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'; is_aligned w pageBits; typ_at (AArch AASIDPool) w s'; is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch AASIDPool) w and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap w asid))) slot) s'\<rbrakk> \<Longrightarrow> \<exists>pool. ako_at (ASIDPool pool) w s' proof (prove)
goal (1 subgoal):
 1. \<And>s' ko. \<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'; cap_aligned (ArchObjectCap (ASIDPoolCap w asid)); is_aligned asid local.asid_low_bits; asid < 2 ^ local.asid_bits; kheap s' w = Some ko; (case ko of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch AASIDPool\<rbrakk> \<Longrightarrow> \<exists>pool. ko = ArchObj (ASIDPool pool)