theory Decode_IF

lemma decode_invocation_reads_respects_f:
  "reads_respects_f aag l
     (silc_inv aag st and pas_refined aag and valid_cap cap and invs and ct_active
                      and cte_wp_at ((=) cap) slot and ex_cte_cap_to 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 (is_subject aag \<circ> cur_thread)
                      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))))
     (decode_invocation label args cap_index slot cap excaps)" unfolding decode_invocation_def fun_app_def apply (rule equiv_valid_guard_imp) apply (wp reads_respects_f[OF decode_untyped_invocation_rev, where Q="\<top>"]
             reads_respects_f[OF decode_cnode_invocation_rev, where Q="\<top>"]
             decode_tcb_invocation_reads_respects_f
             decode_domain_invocation_reads_respects_f
             reads_respects_f[OF decode_irq_control_invocation_rev, where Q="\<top>"]
             reads_respects_f[OF decode_irq_handler_invocation_rev, where Q="\<top>"]
             arch_decode_invocation_reads_respects_f
          | wpc | simp | (rule hoare_pre, wp (once)))+ apply (clarsimp simp: aag_has_Control_iff_owns split_def aag_cap_auth_def) apply (cases cap, simp_all) apply ((clarsimp simp: valid_cap_def cte_wp_at_eq_simp is_cap_simps
                           ex_cte_cap_wp_to_weakenE[OF _ TrueI] cap_auth_conferred_def
                           cap_rights_to_auth_def pas_refined_all_auth_is_owns
            | 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
            | assumption)+)[1] apply (rule conjI, assumption) apply (rule impI, erule subst, rule pas_refined_sita_mem[OF sita_controlled],
          auto simp: cte_wp_at_caps_of_state)[1] apply (rename_tac arch_cap) apply (subgoal_tac "(\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<and>
          (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)") prefer 2 apply (clarsimp simp: cap_links_asid_slot_def label_owns_asid_slot_def) apply (fastforce dest!: pas_refined_Control) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at ((=) cap) slot and ex_cte_cap_wp_to (\<lambda>_. True) 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 is_subject aag \<circ> cur_thread 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)))) (decode_invocation label args cap_index slot cap excaps) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at ((=) cap) slot and ex_cte_cap_wp_to (\<lambda>_. True) 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 is_subject aag \<circ> cur_thread 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)))) (case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped (decode_untyped_invocation 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 label args cap (map fst excaps)) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB (decode_tcb_invocation label args cap slot excaps) | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) (decode_domain_invocation label args excaps) | IRQControlCap \<Rightarrow> liftME InvokeIRQControl (decode_irq_control_invocation label args slot (map fst excaps)) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler (decode_irq_handler_invocation label irq excaps) | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject (arch_decode_invocation label args cap_index slot arch_cap excaps) | _ \<Rightarrow> throwError (InvalidCapability 0)) proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q (case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped (decode_untyped_invocation 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 label args cap (map fst excaps)) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB (decode_tcb_invocation label args cap slot excaps) | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) (decode_domain_invocation label args excaps) | IRQControlCap \<Rightarrow> liftME InvokeIRQControl (decode_irq_control_invocation label args slot (map fst excaps)) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler (decode_irq_handler_invocation label irq excaps) | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject (arch_decode_invocation label args cap_index slot arch_cap excaps) | _ \<Rightarrow> throwError (InvalidCapability 0))
 2. \<And>s. (silc_inv aag st and pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at ((=) cap) slot and ex_cte_cap_wp_to (\<lambda>_. True) 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 is_subject aag \<circ> cur_thread 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> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> pas_refined aag s \<and> s \<turnstile> cap \<and> invs s \<and> ct_active s \<and> cte_wp_at ((=) cap) slot s \<and> ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st94 x xa xb xc) s \<and> x = ?dev81 x xa xb xc \<and> xa = ?bs81 x xa xb xc \<and> xb = ?sz81 x xa xb xc \<and> xc = ?idx81 x xa xb xc) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> silc_inv aag (?st126 x xa xb) s \<and> pas_cap_cur_auth aag (CNodeCap x xa xb)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> silc_inv aag (?st132 x) s \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag x) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag ?st144 s \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag)) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> silc_inv aag (?st152 x) s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> silc_inv aag (?st159 x) s \<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>silc_inv aag st s; pas_refined aag s; s \<turnstile> cap; invs s; ct_active s; cte_wp_at ((=) cap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st94 x xa xb xc) s \<and> x = ?dev81 x xa xb xc \<and> xa = ?bs81 x xa xb xc \<and> xb = ?sz81 x xa xb xc \<and> xc = ?idx81 x xa xb xc) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> silc_inv aag (?st126 x xa xb) s \<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> silc_inv aag (?st132 x) s \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag x) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag ?st144 s \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag)) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> silc_inv aag (?st152 x) s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> silc_inv aag (?st159 x) s \<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 (3 subgoals):
 1. \<And>s x7. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ThreadCap x7; invs s; ct_active s; cte_wp_at ((=) (ThreadCap x7)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st132 x7) s \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag x7
 2. \<And>s. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag ?st144 s \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag)
 3. \<And>s x12. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st159 x12) s \<and> (\<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. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag ?st144 s \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag)
 2. \<And>s x12. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st159 x12) s \<and> (\<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. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> IRQControlCap; invs s; ct_active s; cte_wp_at ((=) IRQControlCap) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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 x12. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st159 x12) s \<and> (\<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>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap x12; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap x12)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) 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 (cur_thread 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> silc_inv aag (?st159 x12) s \<and> (\<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 arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> silc_inv aag (?st159 arch_cap) s \<and> (\<forall>v\<in>acap_asid' arch_cap. 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 arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap; (\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)\<rbrakk> \<Longrightarrow> silc_inv aag (?st159 arch_cap) s \<and> (\<forall>v\<in>acap_asid' arch_cap. is_subject_asid aag v) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)
 2. \<And>s arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<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 arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)
 2. \<And>s arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap; (\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)\<rbrakk> \<Longrightarrow> silc_inv aag (?st159 arch_cap) s \<and> (\<forall>v\<in>acap_asid' arch_cap. 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 arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>asid\<in>acap_asid' arch_cap. (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag; cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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> (\<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 arch_cap\<rbrakk> \<Longrightarrow> (\<forall>x\<in>acap_asid' arch_cap. is_subject_asid aag x) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)
 2. \<And>s arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap; (\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)\<rbrakk> \<Longrightarrow> silc_inv aag (?st159 arch_cap) s \<and> (\<forall>v\<in>acap_asid' arch_cap. 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 arch_cap. \<lbrakk>silc_inv aag st s; pas_refined aag s; s \<turnstile> ArchObjectCap arch_cap; invs s; ct_active s; cte_wp_at ((=) (ArchObjectCap arch_cap)) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>r\<in>set_option (aobj_ref arch_cap). 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 (cur_thread s); is_subject aag (fst slot); \<forall>x\<in>aobj_ref' arch_cap. \<forall>auth\<in>cap_auth_conferred (ArchObjectCap arch_cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap arch_cap); cap_links_irq aag (pasSubject aag) (ArchObjectCap arch_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); cap = ArchObjectCap arch_cap; (\<forall>x\<in>cap_asid' (ArchObjectCap arch_cap). is_subject_asid aag x) \<and> (\<forall>x\<in>set excaps. \<forall>v\<in>cap_asid' (fst x). is_subject_asid aag v)\<rbrakk> \<Longrightarrow> silc_inv aag (?st159 arch_cap) s \<and> (\<forall>v\<in>acap_asid' arch_cap. 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!