theory ArchVSpace_AI

lemma invalidate_asid_entry_invs [wp]:
  "\<lbrace>invs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: invalidate_asid_entry_def invalidate_asid_def
                   invalidate_hw_asid_entry_def) apply (rule hoare_pre, wp load_hw_asid_wp) apply (clarsimp simp del: fun_upd_apply) apply (clarsimp simp: invs_def valid_state_def valid_irq_node_def
                        valid_arch_caps_def valid_table_caps_def
                        valid_kernel_mappings_def valid_global_objs_def
                        valid_global_refs_def global_refs_def
                        valid_vs_lookup_def second_level_tables_def
                        vs_lookup_arch_update vs_lookup_pages_arch_update
                        valid_vspace_objs_def valid_arch_state_def
                  simp del: fun_upd_apply) apply (rule conjI) apply (clarsimp simp: comp_upd_simp is_inv_None_upd) apply (clarsimp simp: valid_asid_map_def valid_machine_state_def) apply (rule conjI) apply (erule order_trans[rotated], clarsimp) apply (simp add: pd_at_asid_arch_up') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some y) (do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(the maybe_hw_asid := None)\<rparr>\<rparr>)
od);
asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> (if \<exists>y. map_option fst (arm_asid_map (arch_state s) asid) = Some y then \<lambda>sa. invs (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>) else (\<lambda>s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>invs s; arm_asid_map (arch_state s) asid = Some (y, b)\<rbrakk> \<Longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; 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\<rbrakk> \<Longrightarrow> is_inv ((arm_hwasid_table (arch_state s))(y := None)) (map_option fst \<circ> (arm_asid_map (arch_state s))(asid := None)) \<and> valid_machine_state (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; 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\<rbrakk> \<Longrightarrow> is_inv ((arm_hwasid_table (arch_state s))(y := None)) (map_option fst \<circ> (arm_asid_map (arch_state s))(asid := None))
 2. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; 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\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; 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\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings 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; dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> dom (arm_asid_map (arch_state s)) - {asid} \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {asid} \<times> UNIV. case x of (asida, hwasid, pd) \<Rightarrow> vspace_at_asid asida pd (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> asida \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings 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; dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> dom (arm_asid_map (arch_state s)) - {asid} \<subseteq> {0..mask local.asid_bits}
 2. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings 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; dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> \<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {asid} \<times> UNIV. case x of (asida, hwasid, pd) \<Rightarrow> vspace_at_asid asida pd (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> asida \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>arm_asid_map (arch_state s) asid = Some (y, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings 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; dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> \<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {asid} \<times> UNIV. case x of (asida, hwasid, pd) \<Rightarrow> vspace_at_asid asida pd (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(y := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> asida \<noteq> 0 proof (prove)
goal:
No subgoals!