theory Interrupt_C

lemma invokeIRQHandler_SetIRQHandler_ccorres:
  "ccorres dc xfdc
          (invs' and sch_act_simple
            and irq_handler_inv_valid' (SetIRQHandler irq cp slot))
          (UNIV \<inter> {s. irq_' s = ucast irq} \<inter> {s. slot_' s = Ptr slot}
                \<inter> {s. ccap_relation cp (cap_' s)}) []
      (InterruptDecls_H.invokeIRQHandler (SetIRQHandler irq cp slot))
      (Call invokeIRQHandler_SetIRQHandler_'proc)" proof - have valid_objs_invs'_strg: "\<And>s. invs' s \<longrightarrow> valid_objs' s" by (clarsimp) show ?thesis apply (cinit lift: irq_' slot_' cap_' simp: Interrupt_H.invokeIRQHandler_def) apply (rule ccorres_Guard_intStateIRQNode_array_Ptr) apply (rule ccorres_move_array_assertion_irq) apply (simp) apply (ctac(no_vcg) add: getIRQSlot_ccorres[simplified]) apply (rule ccorres_symb_exec_r) apply (ctac(no_vcg) add: cteDeleteOne_ccorres[where w="-1"]) apply (rule ccorres_call) apply (rule cteInsert_ccorres) apply (simp add: pred_conj_def)+ apply (strengthen ntfn_badge_derived_enough_strg
                         invs_mdb_strengthen' valid_objs_invs'_strg) apply (wp cteDeleteOne_other_cap[unfolded o_def]) apply vcg apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def
        gs_set_assn_Delete_cstate_relation[unfolded o_def]) apply (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) apply wp apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
                    ghost_assertion_data_set_def) apply (clarsimp simp: cte_at_irq_node' ucast_nat_def) apply (clarsimp simp: invs_pspace_aligned' cte_wp_at_ctes_of badge_derived'_def
                        Collect_const_mem unat_gt_0 valid_cap_simps' ARM.maxIRQ_def) apply (drule word_le_nat_alt[THEN iffD1]) apply clarsimp apply (drule valid_globals_ex_cte_cap_irq[where irq=irq]) apply auto done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple and irq_handler_inv_valid' (irqhandler_invocation.SetIRQHandler irq cp slot)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (irqhandler_invocation.SetIRQHandler irq cp slot)) (Call invokeIRQHandler_SetIRQHandler_'proc) proof (state)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple and irq_handler_inv_valid' (irqhandler_invocation.SetIRQHandler irq cp slot)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (irqhandler_invocation.SetIRQHandler irq cp slot)) (Call invokeIRQHandler_SetIRQHandler_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<longrightarrow> valid_objs' s proof (state)
this:
invs' ?s1 \<longrightarrow> valid_objs' ?s1

goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple and irq_handler_inv_valid' (irqhandler_invocation.SetIRQHandler irq cp slot)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (irqhandler_invocation.SetIRQHandler irq cp slot)) (Call invokeIRQHandler_SetIRQHandler_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple and irq_handler_inv_valid' (irqhandler_invocation.SetIRQHandler irq cp slot)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (irqhandler_invocation.SetIRQHandler irq cp slot)) (Call invokeIRQHandler_SetIRQHandler_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q465 cap slota irqa) (?Q'465 cap slota irqa) [SKIP] (do irqSlot <- getIRQSlot irq;
y <- cteDeleteOne irqSlot;
cteInsert cp slot irqSlot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>irqa = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irqa) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C)))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
(CALL cteDeleteOne_'proc(\<acute>irqSlot);;
CALL cteInsert_'proc(cap,slota,\<acute>irqSlot))))
 2. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q465 cap slota irqa s \<and> s' \<in> ?Q'465 cap slota irqa proof (prove)
goal (2 subgoals):
 1. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q465 cap slota irqa) (?Q'465 cap slota irqa) [SKIP] (do irqSlot <- getIRQSlot irq;
y <- cteDeleteOne irqSlot;
cteInsert cp slot irqSlot
od) (Guard MemorySafety \<lbrace>irqa = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irqa) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
(CALL cteDeleteOne_'proc(\<acute>irqSlot);;
CALL cteInsert_'proc(cap,slota,\<acute>irqSlot))))
 2. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q465 cap slota irqa s \<and> s' \<in> ?Q'465 cap slota irqa proof (prove)
goal (2 subgoals):
 1. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A473 cap slota irqa) (?C'473 cap slota irqa) [SKIP] (do irqSlot <- getIRQSlot irq;
y <- cteDeleteOne irqSlot;
cteInsert cp slot irqSlot
od) (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C)));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
(CALL cteDeleteOne_'proc(\<acute>irqSlot);;
CALL cteInsert_'proc(cap,slota,\<acute>irqSlot))))
 2. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A473 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> ?C'473 cap slota irqa \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A473 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)) (?C'473 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (do irqSlot <- getIRQSlot irq;
y <- cteDeleteOne irqSlot;
cteInsert cp slot irqSlot
od) (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
(CALL cteDeleteOne_'proc(\<acute>irqSlot);;
CALL cteInsert_'proc(cap,cte_Ptr slot,\<acute>irqSlot))))
 2. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A473 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> ?C'473 cap slota irqa \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q484 cap slota irqa rv) (?Q'484 cap slota irqa rv irqSlot) [SKIP] (do y <- cteDeleteOne rv;
cteInsert cp slot rv
od) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
(CALL cteDeleteOne_'proc(irqSlot);;
CALL cteInsert_'proc(cap,cte_Ptr slot,irqSlot)))
 2. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q484 cap slota irqa\<rbrace>
 3. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 4. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q484 cap slota irqa rv) (?Q'576 cap slota irqa rv irqSlot) [SKIP] (do y <- cteDeleteOne rv;
cteInsert cp slot rv
od) (CALL cteDeleteOne_'proc(irqSlot);;
CALL cteInsert_'proc(cap,cte_Ptr slot,irqSlot))
 2. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) (?Q'576 cap slota irqa rv irqSlot)
 3. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; ?Q484 cap slota irqa rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 4. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q484 cap slota irqa\<rbrace>
 5. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 6. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cap slota irqa rv irqSlot rva xfdca. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q582 cap slota irqa rv irqSlot rva) (?Q'582 cap slota irqa rv irqSlot rva xfdca) [SKIP] (cteInsert cp slot rv) (CALL cteInsert_'proc(cap,cte_Ptr slot,irqSlot))
 2. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap slota irqa rv\<rbrace> cteDeleteOne rv \<lbrace>?Q582 cap slota irqa rv irqSlot\<rbrace>
 3. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) ({s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'582 cap slota irqa rv irqSlot rva (xfdc t)})
 4. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and ?R584 cap slota irqa rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 5. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and ?R584 cap slota irqa a\<rbrace>
 6. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 7. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>cap slota irqa rv irqSlot rva xfdc. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres dc (?xf''609 cap slota irqa rv irqSlot rva xfdc) (?Q582 cap slota irqa rv irqSlot rva) (?C'609 cap slota irqa rv irqSlot rva xfdc) [] (cteInsert cp slot rv) (Call cteInsert_'proc)
 2. \<And>cap slota irqa rv irqSlot rva xfdc s ta sa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdc\<rbrakk> \<Longrightarrow> globals sa = globals sa
 3. \<And>cap slota irqa rv irqSlot rva xfdca a s t. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdca\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = ?xf''609 cap slota irqa rv irqSlot rva xfdca t
 4. \<And>cap slota irqa rv irqSlot rva xfdc s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdc\<rbrakk> \<Longrightarrow> globals (destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s))) = globals s
 5. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap slota irqa rv\<rbrace> cteDeleteOne rv \<lbrace>?Q582 cap slota irqa rv irqSlot\<rbrace>
 6. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) ({s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s)) \<in> ?C'609 cap slota irqa rv irqSlot rva (xfdc t)}})
 7. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and ?R584 cap slota irqa rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 8. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and ?R584 cap slota irqa a\<rbrace>
 9. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 10. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cap slota irqa rv irqSlot rva xfdc s ta sa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdc\<rbrakk> \<Longrightarrow> globals sa = globals sa
 2. \<And>cap slota irqa rv irqSlot rva xfdca a s t. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdca\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = xfdc t
 3. \<And>cap slota irqa rv irqSlot rva xfdc s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; dc rva xfdc\<rbrakk> \<Longrightarrow> globals (destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s))) = globals s
 4. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap slota irqa rv\<rbrace> cteDeleteOne rv \<lbrace>\<lambda>rva. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cp \<or> is_simple_cap' cp) slot and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cp and cte_wp_at' (\<lambda>c. True) slot\<rbrace>
 5. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) ({s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace>}})
 6. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and ?R584 cap slota irqa rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 7. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and ?R584 cap slota irqa a\<rbrace>
 8. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 9. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; cte_Ptr rv = irqSlot\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq) rv\<rbrace> cteDeleteOne rv \<lbrace>\<lambda>rva x. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cp \<or> is_simple_cap' cp) slot x \<and> valid_mdb' x \<and> valid_objs' x \<and> pspace_aligned' x \<and> valid_cap' cp x \<and> cte_wp_at' (\<lambda>c. True) slot x\<rbrace>
 2. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) ({s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace>}})
 3. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and ?R584 cap slota irqa rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 4. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and ?R584 cap slota irqa a\<rbrace>
 5. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 6. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; cte_Ptr rv = irqSlot\<rbrakk> \<Longrightarrow> \<lbrace>?R584 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq) rv\<rbrace> cteDeleteOne rv \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cp \<or> is_simple_cap' cp) slot s \<and> invs' s \<and> invs' s \<and> pspace_aligned' s \<and> valid_cap' cp s \<and> cte_wp_at' (\<lambda>c. True) slot s\<rbrace>
 2. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) ({s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace>}})
 3. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and ?R584 cap slota irqa rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 4. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and ?R584 cap slota irqa a\<rbrace>
 5. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 6. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap slota irqa rv irqSlot. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) ({s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. irqSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr slot) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr rv\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>newCap\<rbrace>}})
 2. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and (\<lambda>a. (cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot and K (slot \<noteq> rv)) a \<and> invs' a \<and> invs' a \<and> pspace_aligned' a \<and> valid_cap' cp a \<and> (cte_wp_at' (\<lambda>x. True) slot and K (slot \<noteq> rv)) a)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'484 cap slota irqa rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 3. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and (\<lambda>b. (cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot and K (slot \<noteq> a)) b \<and> invs' b \<and> invs' b \<and> pspace_aligned' b \<and> valid_cap' cp b \<and> (cte_wp_at' (\<lambda>x. True) slot and K (slot \<noteq> a)) b)\<rbrace>
 4. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'484 cap slota irqa rv (irqSlot_' s)
 5. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap slota irqa rv irqSlot s. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv and (\<lambda>a. (cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot and K (slot \<noteq> rv)) a \<and> invs' a \<and> invs' a \<and> pspace_aligned' a \<and> valid_cap' cp a \<and> (cte_wp_at' (\<lambda>x. True) slot and K (slot \<noteq> rv)) a)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> irqSlot = cte_Ptr rv \<and> (\<forall>t rva. dc rva (xfdc t) \<longrightarrow> True \<and> irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap \<and> irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 2. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and (\<lambda>b. (cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot and K (slot \<noteq> a)) b \<and> invs' b \<and> invs' b \<and> pspace_aligned' b \<and> valid_cap' cp b \<and> (cte_wp_at' (\<lambda>x. True) slot and K (slot \<noteq> a)) b)\<rbrace>
 3. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> (\<forall>t rva. dc rva (xfdc t) \<longrightarrow> True \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap)\<rbrace>
 4. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a and (\<lambda>b. (cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot and K (slot \<noteq> a)) b \<and> invs' b \<and> invs' b \<and> pspace_aligned' b \<and> valid_cap' cp b \<and> (cte_wp_at' (\<lambda>x. True) slot and K (slot \<noteq> a)) b)\<rbrace>
 2. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> (\<forall>t rva. dc rva (xfdc t) \<longrightarrow> True \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap)\<rbrace>
 3. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap slota irqa. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R489 cap (cte_Ptr slot) (UCAST(10 \<rightarrow> 32) irq)\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
return (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>a b. invs' b \<and> cte_wp_at' (\<lambda>ct. True) a b \<and> cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot b \<and> slot \<noteq> a \<and> invs' b \<and> pspace_aligned' b \<and> valid_cap' cp b \<and> cte_wp_at' (\<lambda>x. True) slot b \<and> slot \<noteq> a\<rbrace>
 2. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> (\<forall>t rva. dc rva (xfdc t) \<longrightarrow> True \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap)\<rbrace>
 3. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R489 cap slota irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap slota irqa s rv. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; ((=) \<circ> cte_Ptr) rv (irqSlot_' s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> (\<forall>t rva. dc rva (xfdc t) \<longrightarrow> True \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv \<and> cte_Ptr slot = cte_Ptr slot \<and> ccap_relation cp cap)\<rbrace>
 2. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. ((\<lambda>x a. invs' a \<and> cte_wp_at' (\<lambda>ct. True) (x + 2 ^ cte_level_bits * irqa) a \<and> cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot a \<and> slot \<noteq> x + 2 ^ cte_level_bits * irqa \<and> invs' a \<and> pspace_aligned' a \<and> valid_cap' cp a \<and> cte_wp_at' (\<lambda>x. True) slot a \<and> slot \<noteq> x + 2 ^ cte_level_bits * irqa) \<circ> intStateIRQNode) (ksInterruptState a) a) and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap slota irqa s s'. \<lbrakk>ccap_relation cp cap; slota = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (valid_cap' cp and valid_cap' (capability.IRQHandlerCap irq) and (\<lambda>y. isNotificationCap cp) and cte_wp_at' (badge_derived' cp \<circ> cteCap) slot and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s) and ex_cte_cap_wp_to' isCNodeCap slot)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. ((\<lambda>x a. invs' a \<and> cte_wp_at' (\<lambda>ct. True) (x + 2 ^ cte_level_bits * irqa) a \<and> cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot a \<and> slot \<noteq> x + 2 ^ cte_level_bits * irqa \<and> invs' a \<and> pspace_aligned' a \<and> valid_cap' cp a \<and> cte_wp_at' (\<lambda>x. True) slot a \<and> slot \<noteq> x + 2 ^ cte_level_bits * irqa) \<circ> intStateIRQNode) (ksInterruptState a) a) and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ptr'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; valid_cap' (capability.IRQHandlerCap irq) s; isNotificationCap cp; cte_wp_at' (badge_derived' cp \<circ> cteCap) slot s; ex_cte_cap_wp_to' isCNodeCap slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) ptr' s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. capMasterCap (cteCap x) = capMasterCap cp \<or> is_simple_cap' cp) slot s \<and> slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>x. True) slot s \<and> slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<and> s' \<in> (if unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq) then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ptr' cte ctea. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; isNotificationCap cp; ex_cte_cap_wp_to' isCNodeCap slot s; capAligned (capability.IRQHandlerCap irq); irq \<le> 0x9F; ctes_of s slot = Some cte; ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap irq; capMasterCap (cteCap cte) = capMasterCap cp; (capBadge (cteCap cte), capBadge cp) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<and> unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> irq \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ptr' cte ctea. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; isNotificationCap cp; ex_cte_cap_wp_to' isCNodeCap slot s; capAligned (capability.IRQHandlerCap irq); ctes_of s slot = Some cte; ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap irq; capMasterCap (cteCap cte) = capMasterCap cp; (capBadge (cteCap cte), capBadge cp) \<in> capBadge_ordering False; unat irq \<le> unat 0x9F\<rbrakk> \<Longrightarrow> slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<and> unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> irq \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ptr' cte ctea. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; isNotificationCap cp; ex_cte_cap_wp_to' isCNodeCap slot s; capAligned (capability.IRQHandlerCap irq); ctes_of s slot = Some cte; ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap irq; capMasterCap (cteCap cte) = capMasterCap cp; (capBadge (cteCap cte), capBadge cp) \<in> capBadge_ordering False; unat irq \<le> 159\<rbrakk> \<Longrightarrow> slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> irq \<noteq> 0) proof (prove)
goal (3 subgoals):
 1. \<And>cap s s' ptr' cte ctea. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; isNotificationCap cp; capAligned (capability.IRQHandlerCap irq); ctes_of s slot = Some cte; ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap irq; capMasterCap (cteCap cte) = capMasterCap cp; (capBadge (cteCap cte), capBadge cp) \<in> capBadge_ordering False; unat irq \<le> 159\<rbrakk> \<Longrightarrow> valid_global_refs' s
 2. \<And>cap s s' ptr' cte ctea. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; isNotificationCap cp; capAligned (capability.IRQHandlerCap irq); ctes_of s slot = Some cte; ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap irq; capMasterCap (cteCap cte) = capMasterCap cp; (capBadge (cteCap cte), capBadge cp) \<in> capBadge_ordering False; unat irq \<le> 159\<rbrakk> \<Longrightarrow> valid_objs' s
 3. \<And>cap s s' ptr' cte ctea. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; valid_cap' cp s; isNotificationCap cp; capAligned (capability.IRQHandlerCap irq); ctes_of s slot = Some cte; ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap irq; capMasterCap (cteCap cte) = capMasterCap cp; (capBadge (cteCap cte), capBadge cp) \<in> capBadge_ordering False; unat irq \<le> 159; slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> slot \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> irq \<noteq> 0) proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xfdc (invs' and sch_act_simple and irq_handler_inv_valid' (irqhandler_invocation.SetIRQHandler irq cp slot)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (irqhandler_invocation.SetIRQHandler irq cp slot)) (Call invokeIRQHandler_SetIRQHandler_'proc)

goal:
No subgoals!