theory Syscall_AC

lemma decode_invocation_authorised:
  "\<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and (is_subject aag \<circ> cur_thread) and
    cte_wp_at ((=) cap) slot and ex_cte_cap_to slot and domain_sep_inv (pasMaySendIrqs aag) st' and
    real_cte_at slot and
    (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) and
    (\<lambda>s. \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_to r s) and
    (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s) and
    (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> (fst x)) and
    (\<lambda>s. \<forall>x \<in> set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) and
    (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at ((=) (fst x)) (snd x) s) and
    (\<lambda>s. \<forall>x \<in> set excaps. real_cte_at (snd x) s) and
    (\<lambda>s. \<forall>x \<in> set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s) and
    (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s) and
    K (is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and>
       (\<forall>slot \<in> set excaps. is_subject aag (fst (snd slot))) \<and>
       (\<forall>slot \<in> set excaps. pas_cap_cur_auth aag (fst slot)))\<rbrace>
   decode_invocation info_label args ptr slot cap excaps
   \<lbrace>\<lambda>rv. authorised_invocation aag rv\<rbrace>, -" unfolding decode_invocation_def apply (rule hoare_pre) apply (wp decode_untyped_invocation_authorised
             decode_cnode_invocation_auth_derived
             decode_cnode_inv_authorised
             decode_tcb_invocation_authorised decode_tcb_inv_wf
             decode_arch_invocation_authorised
          | strengthen cnode_eq_strg
          | wpc | simp add: comp_def authorised_invocation_def decode_invocation_def
                       split del: if_split del: hoare_True_E_R
          | wp (once) hoare_FalseE_R)+ apply (clarsimp simp: aag_has_Control_iff_owns split_def aag_cap_auth_def) apply (cases cap, simp_all) apply (fastforce simp: cte_wp_at_caps_of_state) apply (clarsimp simp: valid_cap_def obj_at_def is_ep cap_auth_conferred_def
                               cap_rights_to_auth_def ball_Un) apply (fastforce simp: valid_cap_def cap_auth_conferred_def cap_rights_to_auth_def
                                obj_at_def is_ep
                        intro!: owns_ep_owns_receivers) apply (fastforce simp: cap_auth_conferred_def cap_rights_to_auth_def) apply (clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def
                             pas_refined_Control[symmetric] reply_cap_rights_to_auth_def) apply ((clarsimp simp: valid_cap_def is_cap_simps pas_refined_all_auth_is_owns
                            ex_cte_cap_wp_to_weakenE[OF _ TrueI]
                            cap_auth_conferred_def cap_rights_to_auth_def
              | rule conjI | (subst split_paired_Ex[symmetric], erule exI)
              | erule cte_wp_at_weakenE
              | drule(1) bspec
              | erule eq_no_cap_to_obj_with_diff_ref)+)[1] apply (simp only: domain_sep_inv_def) apply (rule impI, erule subst, rule pas_refined_sita_mem [OF sita_controlled],
           auto simp: cte_wp_at_caps_of_state)[1] apply (clarsimp simp add: cap_links_irq_def ) apply (drule (1) pas_refined_Control, simp) apply (clarsimp simp: cap_links_asid_slot_def label_owns_asid_slot_def) apply (fastforce dest!: pas_refined_Control) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and is_subject aag \<circ> cur_thread and cte_wp_at ((=) cap) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and domain_sep_inv (pasMaySendIrqs aag) st' and real_cte_at slot and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) and (\<lambda>s. \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s) and K (is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>slot\<in>set excaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set excaps. pas_cap_cur_auth aag (fst slot)))\<rbrace> decode_invocation info_label args ptr slot cap excaps \<lbrace>authorised_invocation aag\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and is_subject aag \<circ> cur_thread and cte_wp_at ((=) cap) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and domain_sep_inv (pasMaySendIrqs aag) st' and real_cte_at slot and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) and (\<lambda>s. \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s) and K (is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>slot\<in>set excaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set excaps. pas_cap_cur_auth aag (fst slot)))\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation info_label args slot cap (map fst excaps) | EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | ReplyCap thread False rights \<Rightarrow> returnOk $ InvokeReply thread slot (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation info_label args cap (map fst excaps) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation info_label args cap slot excaps | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation info_label args excaps | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation info_label args slot (map fst excaps) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation info_label irq excaps | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation info_label args ptr slot arch_cap excaps | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>authorised_invocation aag\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation info_label args slot cap (map fst excaps) | EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | ReplyCap thread False rights \<Rightarrow> returnOk $ InvokeReply thread slot (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation info_label args cap (map fst excaps) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation info_label args cap slot excaps | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation info_label args excaps | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation info_label args slot (map fst excaps) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation info_label irq excaps | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation info_label args ptr slot arch_cap excaps | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>authorised_invocation aag\<rbrace>, -
 2. \<And>s. (pas_refined aag and valid_cap cap and invs and ct_active and is_subject aag \<circ> cur_thread and cte_wp_at ((=) cap) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and domain_sep_inv (pasMaySendIrqs aag) st' and real_cte_at slot and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) and (\<lambda>s. \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s) and K (is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>slot\<in>set excaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set excaps. pas_cap_cur_auth aag (fst slot)))) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> s \<turnstile> cap \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) cap) slot s \<and> ex_cte_cap_wp_to (\<lambda>_. True) slot s \<and> domain_sep_inv (pasMaySendIrqs aag) st' s \<and> real_cte_at slot s \<and> (\<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>x\<in>set excaps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s) \<and> (\<forall>x\<in>set excaps. real_cte_at (snd x) s) \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s) \<and> (\<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s) \<and> is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>slot\<in>set excaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set excaps. pas_cap_cur_auth aag (fst slot)) \<Longrightarrow> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> cte_wp_at ((=) (UntypedCap x xa xb xc)) slot s \<and> (\<forall>x\<in>set excaps. \<exists>a b. cte_wp_at ((=) (fst x)) (a, b) s) \<and> s \<turnstile> UntypedCap x xa xb xc \<and> cte_wp_at ((=) (UntypedCap x xa xb xc)) slot s \<and> (\<forall>x\<in>set excaps. \<exists>a b. cte_wp_at ((=) (fst x)) (a, b) s) \<and> x = ?dev88 x xa xb xc \<and> xa = ?base88 x xa xb xc \<and> xb = ?sz88 x xa xb xc \<and> xc = ?idx88 x xa xb xc \<and> (\<forall>ref\<in>{xa..xa + 2 ^ xb - 1}. is_subject aag ref)) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<longrightarrow> (\<exists>ep. ko_at (Endpoint ep) x s \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (AllowGrantReply \<in> xb \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> (pasSubject aag, Reply, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> s \<turnstile> CNodeCap x xa xb \<and> pas_cap_cur_auth aag (CNodeCap x xa xb)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> tcb_at x s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x) \<and> cap \<noteq> DomainCap \<and> (cap = IRQControlCap \<longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> is_subject_irq aag x) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> s \<turnstile> ArchObjectCap x \<and> cte_wp_at ((=) (ArchObjectCap x)) slot s \<and> (\<forall>x\<in>set excaps. case x of (cap, slot) \<Rightarrow> cte_wp_at ((=) cap) slot s) \<and> pas_cap_cur_auth aag (ArchObjectCap x) \<and> (\<forall>v\<in>acap_asid' x. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. case x of (cap, slot) \<Rightarrow> aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \<and> is_subject aag (fst slot) \<and> (\<forall>v\<in>cap_asid' cap. is_subject_asid aag v))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> cap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) cap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s; \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) cap; cap_links_irq aag (pasSubject aag) cap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot)\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> cte_wp_at ((=) (UntypedCap x xa xb xc)) slot s \<and> (\<forall>x\<in>set excaps. \<exists>a b. cte_wp_at ((=) (fst x)) (a, b) s) \<and> s \<turnstile> UntypedCap x xa xb xc \<and> cte_wp_at ((=) (UntypedCap x xa xb xc)) slot s \<and> (\<forall>x\<in>set excaps. \<exists>a b. cte_wp_at ((=) (fst x)) (a, b) s) \<and> x = ?dev88 x xa xb xc \<and> xa = ?base88 x xa xb xc \<and> xb = ?sz88 x xa xb xc \<and> xc = ?idx88 x xa xb xc) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<longrightarrow> (\<exists>ep. ko_at (Endpoint ep) x s \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (AllowGrantReply \<in> xb \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> (AllowGrant \<in> xb \<longrightarrow> is_subject aag x) \<and> (pasSubject aag, Reply, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> s \<turnstile> CNodeCap x xa xb \<and> cap_links_asid_slot aag (pasSubject aag) (CNodeCap x xa xb) \<and> cap_links_irq aag (pasSubject aag) (CNodeCap x xa xb)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> tcb_at x s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x) \<and> cap \<noteq> DomainCap \<and> (cap = IRQControlCap \<longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> is_subject_irq aag x) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> s \<turnstile> ArchObjectCap x \<and> cte_wp_at ((=) (ArchObjectCap x)) slot s \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap x) \<and> (\<forall>v\<in>acap_asid' x. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)) proof (prove)
goal (9 subgoals):
 1. \<And>s x21 x22 x23 x24. \<lbrakk>pas_refined aag s; s \<turnstile> UntypedCap x21 x22 x23 x24; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>{x22..x22 + 2 ^ x23 - 1}. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap x21 x22 x23 x24); cap_links_irq aag (pasSubject aag) (UntypedCap x21 x22 x23 x24); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set excaps. \<exists>a b. cte_wp_at ((=) (fst x)) (a, b) s) \<and> x21 = ?dev88 x21 x22 x23 x24 \<and> x22 = ?base88 x21 x22 x23 x24 \<and> x23 = ?sz88 x21 x22 x23 x24 \<and> x24 = ?idx88 x21 x22 x23 x24
 2. \<And>s x31 x32 x33. \<lbrakk>pas_refined aag s; s \<turnstile> EndpointCap x31 x32 x33; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (EndpointCap x31 x32 x33)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x31 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (EndpointCap x31 x32 x33). (pasSubject aag, auth, pasObjectAbs aag x31) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x31 x32 x33); cap_links_irq aag (pasSubject aag) (EndpointCap x31 x32 x33); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> AllowWrite \<in> x33 \<longrightarrow> (\<exists>ep. ko_at (Endpoint ep) x31 s \<and> (AllowGrant \<in> x33 \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> (pasSubject aag, Grant, pasObjectAbs aag x31) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x31) \<in> pasPolicy aag) \<and> (AllowGrantReply \<in> x33 \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x31) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x31) \<in> pasPolicy aag)
 3. \<And>s x41 x42 x43. \<lbrakk>pas_refined aag s; s \<turnstile> NotificationCap x41 x42 x43; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x41 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (NotificationCap x41 x42 x43). (pasSubject aag, auth, pasObjectAbs aag x41) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (NotificationCap x41 x42 x43); cap_links_irq aag (pasSubject aag) (NotificationCap x41 x42 x43); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> AllowWrite \<in> x43 \<longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag x41) \<in> pasPolicy aag
 4. \<And>s x51 x52 x53. \<lbrakk>pas_refined aag s; s \<turnstile> ReplyCap x51 x52 x53; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ReplyCap x51 x52 x53). (pasSubject aag, auth, pasObjectAbs aag x51) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ReplyCap x51 x52 x53); cap_links_irq aag (pasSubject aag) (ReplyCap x51 x52 x53); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<not> x52 \<longrightarrow> (AllowGrant \<in> x53 \<longrightarrow> is_subject aag x51) \<and> (pasSubject aag, Reply, pasObjectAbs aag x51) \<in> pasPolicy aag
 5. \<And>s x7. \<lbrakk>pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x7 s; \<forall>y\<in>dom tcb_cap_cases. ex_cte_cap_wp_to (\<lambda>_. True) (x7, y) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x7
 6. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 7. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 8. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 9. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (8 subgoals):
 1. \<And>s x31 x32 x33. \<lbrakk>pas_refined aag s; s \<turnstile> EndpointCap x31 x32 x33; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (EndpointCap x31 x32 x33)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x31 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (EndpointCap x31 x32 x33). (pasSubject aag, auth, pasObjectAbs aag x31) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x31 x32 x33); cap_links_irq aag (pasSubject aag) (EndpointCap x31 x32 x33); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> AllowWrite \<in> x33 \<longrightarrow> (\<exists>ep. ko_at (Endpoint ep) x31 s \<and> (AllowGrant \<in> x33 \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> (pasSubject aag, Grant, pasObjectAbs aag x31) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x31) \<in> pasPolicy aag) \<and> (AllowGrantReply \<in> x33 \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x31) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x31) \<in> pasPolicy aag)
 2. \<And>s x41 x42 x43. \<lbrakk>pas_refined aag s; s \<turnstile> NotificationCap x41 x42 x43; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x41 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (NotificationCap x41 x42 x43). (pasSubject aag, auth, pasObjectAbs aag x41) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (NotificationCap x41 x42 x43); cap_links_irq aag (pasSubject aag) (NotificationCap x41 x42 x43); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> AllowWrite \<in> x43 \<longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag x41) \<in> pasPolicy aag
 3. \<And>s x51 x52 x53. \<lbrakk>pas_refined aag s; s \<turnstile> ReplyCap x51 x52 x53; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ReplyCap x51 x52 x53). (pasSubject aag, auth, pasObjectAbs aag x51) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ReplyCap x51 x52 x53); cap_links_irq aag (pasSubject aag) (ReplyCap x51 x52 x53); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<not> x52 \<longrightarrow> (AllowGrant \<in> x53 \<longrightarrow> is_subject aag x51) \<and> (pasSubject aag, Reply, pasObjectAbs aag x51) \<in> pasPolicy aag
 4. \<And>s x7. \<lbrakk>pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x7 s; \<forall>y\<in>dom tcb_cap_cases. ex_cte_cap_wp_to (\<lambda>_. True) (x7, y) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x7
 5. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 6. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 7. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 8. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (8 subgoals):
 1. \<And>s x31 x32 x33 ko ep a. \<lbrakk>pas_refined aag s; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (EndpointCap x31 x32 x33)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; ex_nonz_cap_to x31 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. cap_aligned (fst x) \<and> (case fst x of UntypedCap dev p b f \<Rightarrow> valid_untyped (fst x) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True); \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. \<exists>ko. kheap s (fst (snd x)) = Some ko \<and> is_cap_table (length (snd (snd x))) ko; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (EndpointCap x31 x32 x33); cap_links_irq aag (pasSubject aag) (EndpointCap x31 x32 x33); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>case fst slot of NullCap \<Rightarrow> {} | EndpointCap oref badge r \<Rightarrow> cap_rights_to_auth r True | NotificationCap oref badge r \<Rightarrow> cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False | ReplyCap oref x xa \<Rightarrow> reply_cap_rights_to_auth x xa | ArchObjectCap x \<Rightarrow> arch_cap_auth_conferred x | _ \<Rightarrow> {Control}. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = EndpointCap x31 x32 x33; cap_aligned (EndpointCap x31 x32 x33); kheap s (fst slot) = Some ko; is_cap_table (length (snd slot)) ko; kheap s x31 = Some (Endpoint ep); \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag x31) \<in> pasPolicy aag; AllowWrite \<in> x33; AllowGrant \<in> x33; (a, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> is_subject aag a
 2. \<And>s x41 x42 x43. \<lbrakk>pas_refined aag s; s \<turnstile> NotificationCap x41 x42 x43; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x41 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (NotificationCap x41 x42 x43). (pasSubject aag, auth, pasObjectAbs aag x41) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (NotificationCap x41 x42 x43); cap_links_irq aag (pasSubject aag) (NotificationCap x41 x42 x43); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> AllowWrite \<in> x43 \<longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag x41) \<in> pasPolicy aag
 3. \<And>s x51 x52 x53. \<lbrakk>pas_refined aag s; s \<turnstile> ReplyCap x51 x52 x53; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ReplyCap x51 x52 x53). (pasSubject aag, auth, pasObjectAbs aag x51) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ReplyCap x51 x52 x53); cap_links_irq aag (pasSubject aag) (ReplyCap x51 x52 x53); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<not> x52 \<longrightarrow> (AllowGrant \<in> x53 \<longrightarrow> is_subject aag x51) \<and> (pasSubject aag, Reply, pasObjectAbs aag x51) \<in> pasPolicy aag
 4. \<And>s x7. \<lbrakk>pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x7 s; \<forall>y\<in>dom tcb_cap_cases. ex_cte_cap_wp_to (\<lambda>_. True) (x7, y) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x7
 5. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 6. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 7. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 8. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (7 subgoals):
 1. \<And>s x41 x42 x43. \<lbrakk>pas_refined aag s; s \<turnstile> NotificationCap x41 x42 x43; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x41 s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (NotificationCap x41 x42 x43). (pasSubject aag, auth, pasObjectAbs aag x41) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (NotificationCap x41 x42 x43); cap_links_irq aag (pasSubject aag) (NotificationCap x41 x42 x43); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> AllowWrite \<in> x43 \<longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag x41) \<in> pasPolicy aag
 2. \<And>s x51 x52 x53. \<lbrakk>pas_refined aag s; s \<turnstile> ReplyCap x51 x52 x53; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ReplyCap x51 x52 x53). (pasSubject aag, auth, pasObjectAbs aag x51) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ReplyCap x51 x52 x53); cap_links_irq aag (pasSubject aag) (ReplyCap x51 x52 x53); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<not> x52 \<longrightarrow> (AllowGrant \<in> x53 \<longrightarrow> is_subject aag x51) \<and> (pasSubject aag, Reply, pasObjectAbs aag x51) \<in> pasPolicy aag
 3. \<And>s x7. \<lbrakk>pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x7 s; \<forall>y\<in>dom tcb_cap_cases. ex_cte_cap_wp_to (\<lambda>_. True) (x7, y) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x7
 4. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 5. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 6. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 7. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (6 subgoals):
 1. \<And>s x51 x52 x53. \<lbrakk>pas_refined aag s; s \<turnstile> ReplyCap x51 x52 x53; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ReplyCap x51 x52 x53). (pasSubject aag, auth, pasObjectAbs aag x51) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ReplyCap x51 x52 x53); cap_links_irq aag (pasSubject aag) (ReplyCap x51 x52 x53); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<not> x52 \<longrightarrow> (AllowGrant \<in> x53 \<longrightarrow> is_subject aag x51) \<and> (pasSubject aag, Reply, pasObjectAbs aag x51) \<in> pasPolicy aag
 2. \<And>s x7. \<lbrakk>pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x7 s; \<forall>y\<in>dom tcb_cap_cases. ex_cte_cap_wp_to (\<lambda>_. True) (x7, y) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x7
 3. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 4. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 5. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 6. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (5 subgoals):
 1. \<And>s x7. \<lbrakk>pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_nonz_cap_to x7 s; \<forall>y\<in>dom tcb_cap_cases. ex_cte_cap_wp_to (\<lambda>_. True) (x7, y) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>set excaps. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s) \<and> is_subject aag x7
 2. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 4. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 5. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> DomainCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) DomainCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x. \<forall>auth\<in>cap_auth_conferred DomainCap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) DomainCap; cap_links_irq aag (pasSubject aag) DomainCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = DomainCap\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 3. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 4. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; cap_links_irq aag (pasSubject aag) IRQControlCap; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQControlCap\<rbrakk> \<Longrightarrow> args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag
 2. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 3. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (2 subgoals):
 1. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); cap_links_irq aag (pasSubject aag) (IRQHandlerCap x10); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 2. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (2 subgoals):
 1. \<And>s x10. \<lbrakk>pas_refined aag s; s \<turnstile> IRQHandlerCap x10; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (IRQHandlerCap x10)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; ex_cte_cap_wp_to (\<lambda>_. True) (interrupt_irq_node s x10, []) s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) (IRQHandlerCap x10); (pasSubject aag, Control, pasIRQAbs aag x10) \<in> pasPolicy aag; \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> (\<forall>irq\<in>cap_irqs_controlled (fst slot). (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> is_subject_irq aag x10
 2. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (1 subgoal):
 1. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap x12); cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> cap_links_asid_slot aag (pasSubject aag) (fst slot) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal (1 subgoal):
 1. \<And>s x12. \<lbrakk>pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; is_subject aag (cur_thread s); cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; domain_sep_inv (pasMaySendIrqs aag) st' s; real_cte_at slot s; \<forall>r\<in>set_option (aobj_ref x12). ex_nonz_cap_to r s; \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s; \<forall>x\<in>set excaps. s \<turnstile> fst x; \<forall>x\<in>set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s; \<forall>x\<in>set excaps. real_cte_at (snd x) s; \<forall>x\<in>set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s; \<forall>x\<in>set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s; is_subject aag (fst slot); \<forall>x\<in>aobj_ref' x12. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap x12). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>asid\<in>acap_asid' x12. (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag; cap_links_irq aag (pasSubject aag) (ArchObjectCap x12); \<forall>slot\<in>set excaps. is_subject aag (fst (snd slot)); \<forall>slot\<in>set excaps. (\<forall>x\<in>obj_refs_ac (fst slot). \<forall>auth\<in>cap_auth_conferred (fst slot). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst slot). is_subject aag x) \<and> (\<forall>asid\<in>cap_asid' (fst slot). (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag) \<and> cap_links_irq aag (pasSubject aag) (fst slot); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>v\<in>acap_asid' x12. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v) proof (prove)
goal:
No subgoals!