theory Interrupt_IF

lemma invoke_irq_handler_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag
                                           and irq_handler_inv_valid irq_inv
                                           and K (authorised_irq_hdl_inv aag irq_inv))
                    (invoke_irq_handler irq_inv)" apply (case_tac irq_inv) apply (simp) apply (rule equiv_valid_guard_imp) apply wpsimp apply fastforce apply (wp reads_respects_f[OF cap_insert_reads_respects]
             cap_delete_one_reads_respects_f[where st=st]
             reads_respects_f[OF get_irq_slot_reads_respects, where Q="\<top>"]
             cap_insert_silc_inv'' cap_delete_one_silc_inv_subject
             cap_delete_one_cte_wp_at_other hoare_weak_lift_imp
             hoare_vcg_ex_lift slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st]
          | simp | simp add: get_irq_slot_def)+ apply (clarsimp simp: pas_refined_def irq_map_wellformed_aux_def) apply ((rule conjI, assumption) | clarsimp simp: conj_comms authorised_irq_hdl_inv_def)+ apply (drule_tac p="(a,b)" in cte_wp_at_norm) apply (elim exE conjE, rename_tac cap') apply (drule_tac cap=cap' in silc_invD) apply assumption apply (fastforce simp: intra_label_cap_def cap_points_to_label_def
                           interrupt_derived_ntfn_cap_identical_refs) apply (fastforce simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def
                          interrupt_derived_ntfn_cap_identical_refs) apply (clarsimp) apply (wpsimp wp: reads_respects_f[OF get_irq_slot_reads_respects, where Q=\<top>]
                    cap_delete_one_reads_respects_f) apply (auto simp: authorised_irq_hdl_inv_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_inv = ACKIrq x1 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv)
 2. \<And>x21 x22 x23. irq_inv = SetIRQHandler x21 x22 x23 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv)
 3. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_inv = ACKIrq x1 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and (\<lambda>y. authorised_irq_hdl_inv aag (ACKIrq x1))) (arch_invoke_irq_handler (ACKIrq x1))
 2. \<And>x21 x22 x23. irq_inv = SetIRQHandler x21 x22 x23 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv)
 3. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (4 subgoals):
 1. \<And>x1. irq_inv = ACKIrq x1 \<Longrightarrow> reads_respects_f aag l (?Q1 x1) (arch_invoke_irq_handler (ACKIrq x1))
 2. \<And>x1 s. \<lbrakk>irq_inv = ACKIrq x1; (silc_inv aag st and pas_refined aag and invs and pas_refined aag and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and (\<lambda>y. authorised_irq_hdl_inv aag (ACKIrq x1))) s\<rbrakk> \<Longrightarrow> ?Q1 x1 s
 3. \<And>x21 x22 x23. irq_inv = SetIRQHandler x21 x22 x23 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv)
 4. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (3 subgoals):
 1. \<And>x1 s. \<lbrakk>irq_inv = ACKIrq x1; (silc_inv aag st and pas_refined aag and invs and pas_refined aag and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and (\<lambda>y. authorised_irq_hdl_inv aag (ACKIrq x1))) s\<rbrakk> \<Longrightarrow> silc_inv aag (?st5 x1) s
 2. \<And>x21 x22 x23. irq_inv = SetIRQHandler x21 x22 x23 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv)
 3. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23. irq_inv = SetIRQHandler x21 x22 x23 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv)
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 s. \<lbrakk>irq_inv = SetIRQHandler x21 x22 x23; silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> pas_refined aag s \<and> ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22 \<and> authorised_irq_hdl_inv aag (SetIRQHandler x21 x22 x23)\<rbrakk> \<Longrightarrow> silc_inv aag (?st49 x21 x22 x23) s \<and> is_subject_irq aag x21 \<and> silc_inv aag (?st62 x21 x22 x23) s \<and> is_subject_irq aag x21 \<and> aag_can_read aag (fst x23) \<and> aag_can_read aag (interrupt_irq_node s x21) \<and> (\<not> cap_points_to_label aag x22 (pasObjectAbs aag (interrupt_irq_node s x21)) \<longrightarrow> (\<exists>x. (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s) \<and> pasObjectAbs aag x = SilcLabel \<and> is_subject aag (interrupt_irq_node s x21) \<and> pasObjectAbs aag x = SilcLabel)) \<and> is_subject aag (fst x23) \<and> is_subject aag (interrupt_irq_node s x21)
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s aa ba. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); silc_inv aag st s; invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived x22) (a, b) s; s \<turnstile> x22; is_ntfn_cap x22; authorised_irq_hdl_inv aag (SetIRQHandler x21 x22 (a, b))\<rbrakk> \<Longrightarrow> silc_inv aag (?st49 x21 x22 (a, b)) s \<and> is_subject_irq aag x21 \<and> silc_inv aag (?st62 x21 x22 (a, b)) s \<and> is_subject_irq aag x21 \<and> aag_can_read aag a \<and> aag_can_read_irq aag x21 \<and> (\<not> cap_points_to_label aag x22 (pasIRQAbs aag x21) \<longrightarrow> (\<exists>x. (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s) \<and> pasObjectAbs aag x = SilcLabel \<and> is_subject_irq aag x21 \<and> pasObjectAbs aag x = SilcLabel)) \<and> is_subject aag a \<and> is_subject_irq aag x21
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s aa ba. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); silc_inv aag st s; invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived x22) (a, b) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>x. pasObjectAbs aag x = SilcLabel \<and> (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s)
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s aa ba. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); silc_inv aag st s; invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); \<exists>c. cte_wp_at ((=) c) (a, b) s \<and> interrupt_derived x22 c\<rbrakk> \<Longrightarrow> \<exists>x. pasObjectAbs aag x = SilcLabel \<and> (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s)
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); silc_inv aag st s; invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'\<rbrakk> \<Longrightarrow> \<exists>x. pasObjectAbs aag x = SilcLabel \<and> (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s)
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') (?slot112 x21 x22 a b s aa ba cap') s
 2. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot112 x21 x22 a b s aa ba cap') s
 3. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>x. pasObjectAbs aag x = SilcLabel \<and> (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s)
 4. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, b) s
 2. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>x. pasObjectAbs aag x = SilcLabel \<and> (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s)
 3. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s aa ba cap'. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); invs s; pas_wellformed aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; s \<turnstile> x22; is_ntfn_cap x22; pas_cap_cur_auth aag x22; is_subject_irq aag x21; is_subject aag a; \<not> cap_points_to_label aag x22 (pasSubject aag); cte_wp_at ((=) cap') (a, b) s; interrupt_derived x22 cap'; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>x. pasObjectAbs aag x = SilcLabel \<and> (\<exists>xa. (x, xa) \<in> slots_holding_overlapping_caps x22 s)
 2. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (1 subgoal):
 1. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (1 subgoal):
 1. \<And>x3. irq_inv = ClearIRQHandler x3 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and pas_refined aag and (\<lambda>y. authorised_irq_hdl_inv aag (ClearIRQHandler x3))) (get_irq_slot x3 >>= cap_delete_one) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>irq_inv = ClearIRQHandler x3; silc_inv aag st s; invs s; pas_refined aag s; authorised_irq_hdl_inv aag (ClearIRQHandler x3)\<rbrakk> \<Longrightarrow> silc_inv aag (?st132 x3) s \<and> is_subject_irq aag x3 \<and> silc_inv aag (?st137 x3) s \<and> is_subject_irq aag x3 proof (prove)
goal:
No subgoals!