theory ArchArch_AC

lemma perform_asid_pool_invocation_pas_refined [wp]:
  "\<lbrace>pas_refined aag and invs and valid_apinv api and K (authorised_asid_pool_inv aag api)\<rbrace>
   perform_asid_pool_invocation api
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: perform_asid_pool_invocation_def) apply (rule hoare_pre) apply (wp get_cap_auth_wp[where aag = aag] set_cap_pas_refined_not_transferable | wpc)+ apply (clarsimp simp: authorised_asid_pool_inv_def cap_links_asid_slot_def
                        is_subject_asid_into_loas aag_cap_auth_def) apply (clarsimp simp: cap_auth_conferred_def arch_cap_auth_conferred_def is_cap_simps
                        is_page_cap_def auth_graph_map_mem pas_refined_all_auth_is_owns
                        pas_refined_refl cli_no_irqs cte_wp_at_caps_of_state
                        invs_psp_aligned invs_vspace_objs invs_arch_state
                 dest!: graph_ofD) apply (clarsimp split: if_split_asm) apply (clarsimp simp add: pas_refined_refl auth_graph_map_def2
                             mask_asid_low_bits_ucast_ucast[symmetric]
                             valid_apinv_def obj_at_def) apply (drule(2) asid_pool_uniqueness) apply (simp add: obj_at_def) apply (case_tac "asid = 0"; simp add: pas_refined_refl) apply (simp add: asid_low_high_bits[rotated, OF arg_cong[where f=ucast]]) apply (clarsimp simp: obj_at_def) apply (frule (2) asid_pool_into_aag) apply (drule kheap_eq_state_vrefsD) apply (clarsimp simp: auth_graph_map_def2 pas_refined_refl) apply (clarsimp simp: pas_refined_def vs_refs_no_global_pts_def) apply (erule subsetD, erule state_asids_to_policy_aux.intros,
         simp add: split_def, rule image_eqI[rotated], erule graph_ofI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and valid_apinv api and K (authorised_asid_pool_inv aag api)\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and valid_apinv api and (\<lambda>y. authorised_asid_pool_inv aag api)\<rbrace> case api of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case api of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and invs and valid_apinv api and (\<lambda>y. authorised_asid_pool_inv aag api)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and invs and valid_apinv api and (\<lambda>y. authorised_asid_pool_inv aag api)) s \<Longrightarrow> \<forall>x xa xb. api = Assign x xa xb \<longrightarrow> pas_refined aag s \<and> is_subject aag (fst xb) \<and> (\<forall>cap. caps_of_state s xb = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>xc. cap = ArchObjectCap xc \<longrightarrow> (\<forall>x xa. xc = ASIDPoolCap x xa \<longrightarrow> True) \<and> (xc = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>x xa xb xd xe. xc = PageCap x xa xb xd xe \<longrightarrow> True) \<and> (\<forall>x xa. xc = PageTableCap x xa \<longrightarrow> True) \<and> (\<forall>xd xe. xc = PageDirectoryCap xd xe \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) xa s \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) xb and K (aag_cap_auth aag (pasObjectAbs aag (fst xb)) (ArchObjectCap $ PageDirectoryCap xd (Some x)))) s \<and> (\<forall>a\<in>graph_of (pool(UCAST(32 \<rightarrow> 10) x \<mapsto> xd)). case a of (x, y) \<Rightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, y)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) x \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag y) \<in> pasPolicy aag)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageDirectoryCap xc xd)). (pasSubject aag, auth, pasObjectAbs aag xc) \<in> pasPolicy aag; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; cap_links_irq aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap xc xd)); ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> cte_wp_at (\<lambda>c. \<not> is_transferable_cap c) (a, b) s \<and> (\<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageDirectoryCap xc (Some x))). (pasSubject aag, auth, pasObjectAbs aag xc) \<in> pasPolicy aag) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap xc (Some x))) \<and> (\<forall>x\<in>graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x then Some xc else pool a). case x of (x, y) \<Rightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, y)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) x \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag y) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; (if aa = UCAST(32 \<rightarrow> 10) x then Some xc else pool aa) = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b xd pool ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap ba xd)); is_subject aag ba; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) \<longrightarrow> (pasASIDAbs aag asid, Control, pasSubject aag) \<in> pasPolicy aag)
 2. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b xd pool ba asid. \<lbrakk>pas_refined aag s; invs s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap ba xd)); is_subject aag ba; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) x) = None; cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) s; 0 < x; x < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x)) None] \<rhd> xa) s; asid_table s (asid_high_bits_of asid) = Some xa; asid && mask local.asid_low_bits = x && mask local.asid_low_bits\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasSubject aag) \<in> pasPolicy aag
 2. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b xd pool ba asid. \<lbrakk>pas_refined aag s; invs s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap ba xd)); is_subject aag ba; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) x) = None; cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) s; 0 < x; x < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of asid) = Some xa; asid && mask local.asid_low_bits = x && mask local.asid_low_bits\<rbrakk> \<Longrightarrow> \<forall>pt. \<not> ako_at (PageTable pt) xa s
 2. \<And>s x xa a b xd pool ba asid. \<lbrakk>pas_refined aag s; invs s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap ba xd)); is_subject aag ba; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) x) = None; cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) s; 0 < x; x < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of asid) = Some xa; asid && mask local.asid_low_bits = x && mask local.asid_low_bits; asid_high_bits_of asid = asid_high_bits_of x\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasSubject aag) \<in> pasPolicy aag
 3. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b xd pool ba asid. \<lbrakk>pas_refined aag s; invs s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap ba xd)); is_subject aag ba; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) x) = None; cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) s; 0 < x; x < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of asid) = Some xa; asid && mask local.asid_low_bits = x && mask local.asid_low_bits; asid_high_bits_of asid = asid_high_bits_of x\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasSubject aag) \<in> pasPolicy aag
 2. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b xd pool ba asid. \<lbrakk>pas_refined aag s; invs s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap ba xd)); is_subject aag ba; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) x) = None; cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) s; 0 < x; x < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x) = Some xa; x && mask local.asid_low_bits = 0; asid_high_bits_of 0 = asid_high_bits_of x; asid = 0\<rbrakk> \<Longrightarrow> (pasASIDAbs aag 0, Control, pasSubject aag) \<in> pasPolicy aag
 2. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; ako_at (ASIDPool pool) xa s; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; kheap s xa = Some (ArchObj (ASIDPool pool)); aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba; (pasObjectAbs aag xa, Control, pasObjectAbs aag ba) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba; (pasObjectAbs aag xa, Control, pasObjectAbs aag ba) \<in> pasPolicy aag; state_vrefs s xa = vs_refs_no_global_pts (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(xa, Control, ba)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some xa \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba asid. \<lbrakk>pas_refined aag s; invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba; (pasSubject aag, Control, pasObjectAbs aag ba) \<in> pasPolicy aag; state_vrefs s xa = vs_refs_no_global_pts (ArchObj (ASIDPool pool)); asid_table s (asid_high_bits_of asid) = Some xa; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba asid. \<lbrakk>invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba; (pasSubject aag, Control, pasObjectAbs aag ba) \<in> pasPolicy aag; state_vrefs s xa = (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool; asid_table s (asid_high_bits_of asid) = Some xa; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag ba) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool aa ba asid. \<lbrakk>invs s; valid_apinv (Assign x xa (a, b)) s; api = Assign x xa (a, b); is_subject aag xa; is_subject aag a; x \<noteq> 0; \<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of x \<and> asid' \<noteq> 0 \<longrightarrow> is_subject_asid aag asid'; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap xc xd)); is_subject aag xc; \<forall>x\<in>set_option xd. label_owns_asid_slot aag (pasSubject aag) x; aa \<noteq> UCAST(32 \<rightarrow> 10) x; pool aa = Some ba; (pasSubject aag, Control, pasObjectAbs aag ba) \<in> pasPolicy aag; state_vrefs s xa = (\<lambda>x. (snd x, UCAST(10 \<rightarrow> 32) (fst x), AASIDPool, Control)) ` graph_of pool; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (ba, UCAST(10 \<rightarrow> 32) aa, AASIDPool, Control) = (snd (aa, ba), UCAST(10 \<rightarrow> 32) (fst (aa, ba)), AASIDPool, Control) proof (prove)
goal:
No subgoals!