theory Interrupt_R

lemma invokeIRQHandler_corres:
  "irq_handler_inv_relation i i' \<Longrightarrow>
   corres dc (einvs and irq_handler_inv_valid i)
             (invs' and irq_handler_inv_valid' i')
     (invoke_irq_handler i)
     (InterruptDecls_H.invokeIRQHandler i')" supply arch_invoke_irq_handler.simps[simp del] apply (cases i; simp add: Interrupt_H.invokeIRQHandler_def) apply (rule corres_guard_imp, rule arch_invokeIRQHandler_corres; simp) apply (rename_tac word cap prod) apply clarsimp apply (rule corres_guard_imp) apply (rule corres_split[OF getIRQSlot_corres]) apply simp apply (rule corres_split_nor[OF cap_delete_one_corres]) apply (rule cteInsert_corres, simp+) apply (rule_tac Q="\<lambda>rv s. einvs s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot s
                                  \<and> (a, b) \<noteq> irq_slot
                                  \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s"
                      in hoare_post_imp) apply fastforce apply (wp cap_delete_one_still_derived)+ apply (strengthen invs_mdb_strengthen') apply wp+ apply (simp add: conj_comms eq_commute) apply (wp get_irq_slot_different hoare_drop_imps)+ apply (clarsimp simp: valid_state_def invs_def) apply (erule cte_wp_at_weakenE, simp add: is_derived_use_interrupt) apply fastforce apply (rule corres_guard_imp) apply (rule corres_split[OF getIRQSlot_corres]) apply simp apply (rule cap_delete_one_corres) apply wp+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_handler_inv_relation i i' \<Longrightarrow> corres dc (einvs and irq_handler_inv_valid i) (invs' and irq_handler_inv_valid' i') (invoke_irq_handler i) (InterruptDecls_H.invokeIRQHandler i') proof (prove)
goal (1 subgoal):
 1. irq_handler_inv_relation i i' \<Longrightarrow> corres dc (einvs and irq_handler_inv_valid i) (invs' and irq_handler_inv_valid' i') (invoke_irq_handler i) (InterruptDecls_H.invokeIRQHandler i') proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>i' = AckIRQ x1; i = ACKIrq x1\<rbrakk> \<Longrightarrow> corres dc (einvs and (\<lambda>s. interrupt_states s x1 \<noteq> irq_state.IRQInactive)) (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) x1 \<noteq> irqstate.IRQInactive)) (arch_invoke_irq_handler (ACKIrq x1)) (local.invokeIRQHandler (AckIRQ x1))
 2. \<And>x21 x22 x23. \<lbrakk>\<exists>cap'. i' = irqhandler_invocation.SetIRQHandler x21 cap' (cte_map x23) \<and> cap_relation x22 cap'; i = irq_handler_invocation.SetIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> corres dc (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) (invs' and irq_handler_inv_valid' i') (do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od) (case i' of AckIRQ irq \<Rightarrow> local.invokeIRQHandler (AckIRQ irq) | irqhandler_invocation.ClearIRQHandler irq \<Rightarrow> getIRQSlot irq >>= cteDeleteOne | irqhandler_invocation.SetIRQHandler irq cap slot \<Rightarrow> do irqSlot <- getIRQSlot irq;
cteDeleteOne irqSlot;
cteInsert cap slot irqSlot
od)
 3. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>\<exists>cap'. i' = irqhandler_invocation.SetIRQHandler x21 cap' (cte_map x23) \<and> cap_relation x22 cap'; i = irq_handler_invocation.SetIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> corres dc (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) (invs' and irq_handler_inv_valid' i') (do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od) (case i' of AckIRQ irq \<Rightarrow> local.invokeIRQHandler (AckIRQ irq) | irqhandler_invocation.ClearIRQHandler irq \<Rightarrow> getIRQSlot irq >>= cteDeleteOne | irqhandler_invocation.SetIRQHandler irq cap slot \<Rightarrow> do irqSlot <- getIRQSlot irq;
cteDeleteOne irqSlot;
cteInsert cap slot irqSlot
od)
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (2 subgoals):
 1. \<And>word cap prod. \<lbrakk>\<exists>cap'. i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map prod) \<and> cap_relation cap cap'; i = irq_handler_invocation.SetIRQHandler word cap prod\<rbrakk> \<Longrightarrow> corres dc (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) (invs' and irq_handler_inv_valid' i') (do irq_slot <- get_irq_slot word;
y <- cap_delete_one irq_slot;
cap_insert cap prod irq_slot
od) (case i' of AckIRQ irq \<Rightarrow> local.invokeIRQHandler (AckIRQ irq) | irqhandler_invocation.ClearIRQHandler irq \<Rightarrow> getIRQSlot irq >>= cteDeleteOne | irqhandler_invocation.SetIRQHandler irq cap slot \<Rightarrow> do irqSlot <- getIRQSlot irq;
cteDeleteOne irqSlot;
cteInsert cap slot irqSlot
od)
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (2 subgoals):
 1. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) (do irq_slot <- get_irq_slot word;
y <- cap_delete_one irq_slot;
cap_insert cap (a, b) irq_slot
od) (do irqSlot <- getIRQSlot word;
y <- cteDeleteOne irqSlot;
cteInsert cap' (cte_map (a, b)) irqSlot
od)
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (4 subgoals):
 1. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> corres dc (?Q29 word cap a b cap') (?Q'29 word cap a b cap') (do irq_slot <- get_irq_slot word;
y <- cap_delete_one irq_slot;
cap_insert cap (a, b) irq_slot
od) (do irqSlot <- getIRQSlot word;
y <- cteDeleteOne irqSlot;
cteInsert cap' (cte_map (a, b)) irqSlot
od)
 2. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q29 word cap a b cap' s
 3. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ?Q'29 word cap a b cap' s
 4. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (6 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> corres dc (?R33 word cap a b cap' irq_slot) (?R'33 word cap a b cap' irqSlot) (do y <- cap_delete_one irq_slot;
cap_insert cap (a, b) irq_slot
od) (do y <- cteDeleteOne irqSlot;
cteInsert cap' (cte_map (a, b)) irqSlot
od)
 2. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>?R33 word cap a b cap'\<rbrace>
 3. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>?R'33 word cap a b cap'\<rbrace>
 4. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 5. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 6. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (6 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> corres dc (?R33 word cap a b cap' irq_slot) (?R'33 word cap a b cap' (cte_map irq_slot)) (do y <- cap_delete_one irq_slot;
cap_insert cap (a, b) irq_slot
od) (do y <- cteDeleteOne (cte_map irq_slot);
cteInsert cap' (cte_map (a, b)) (cte_map irq_slot)
od)
 2. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>?R33 word cap a b cap'\<rbrace>
 3. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>?R'33 word cap a b cap'\<rbrace>
 4. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 5. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 6. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (8 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> corres dc (?R38 word cap a b cap' irq_slot irqSlot) (?R'38 word cap a b cap' irq_slot irqSlot) (cap_insert cap (a, b) irq_slot) (cteInsert cap' (cte_map (a, b)) (cte_map irq_slot))
 2. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 word cap a b cap' irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>x. ?R38 word cap a b cap' irq_slot irqSlot\<rbrace>
 3. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 word cap a b cap' (cte_map irq_slot)\<rbrace> cteDeleteOne (cte_map irq_slot) \<lbrace>\<lambda>x. ?R'38 word cap a b cap' irq_slot irqSlot\<rbrace>
 4. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>c. einvs and cte_wp_at can_fast_finalise c and ?Q45 word cap a b cap' c\<rbrace>
 5. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>c. invs' and cte_wp_at' (\<lambda>_. True) c and ?Q'42 word cap a b cap' c\<rbrace>
 6. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 7. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 8. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (7 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 word cap a b cap' irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and (\<lambda>y. (a, b) \<noteq> irq_slot) and cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot and (\<lambda>s. cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s)\<rbrace>
 2. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 word cap a b cap' (cte_map irq_slot)\<rbrace> cteDeleteOne (cte_map irq_slot) \<lbrace>\<lambda>x. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map irq_slot)\<rbrace>
 3. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>c. einvs and cte_wp_at can_fast_finalise c and ?Q45 word cap a b cap' c\<rbrace>
 4. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>c. invs' and cte_wp_at' (\<lambda>_. True) c and ?Q'42 word cap a b cap' c\<rbrace>
 5. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 6. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 7. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (8 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot rv s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot; einvs s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot s \<and> (a, b) \<noteq> irq_slot \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and (\<lambda>y. (a, b) \<noteq> irq_slot) and cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot and (\<lambda>s. cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s)) s
 2. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 word cap a b cap' irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. einvs s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot s \<and> (a, b) \<noteq> irq_slot \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s\<rbrace>
 3. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 word cap a b cap' (cte_map irq_slot)\<rbrace> cteDeleteOne (cte_map irq_slot) \<lbrace>\<lambda>x. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map irq_slot)\<rbrace>
 4. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>c. einvs and cte_wp_at can_fast_finalise c and ?Q45 word cap a b cap' c\<rbrace>
 5. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>c. invs' and cte_wp_at' (\<lambda>_. True) c and ?Q'42 word cap a b cap' c\<rbrace>
 6. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 7. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 8. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (7 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 word cap a b cap' irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. einvs s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot s \<and> (a, b) \<noteq> irq_slot \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s\<rbrace>
 2. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 word cap a b cap' (cte_map irq_slot)\<rbrace> cteDeleteOne (cte_map irq_slot) \<lbrace>\<lambda>x. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map irq_slot)\<rbrace>
 3. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>c. einvs and cte_wp_at can_fast_finalise c and ?Q45 word cap a b cap' c\<rbrace>
 4. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>c. invs' and cte_wp_at' (\<lambda>_. True) c and ?Q'42 word cap a b cap' c\<rbrace>
 5. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 6. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 7. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (6 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'127 word cap a b cap' (cte_map irq_slot)\<rbrace> cteDeleteOne (cte_map irq_slot) \<lbrace>\<lambda>rv s. valid_mdb' s \<and> valid_cap' cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map irq_slot) s\<rbrace>
 2. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>c. einvs and cte_wp_at can_fast_finalise c and (\<lambda>d. (invs and emptyable c) d \<and> valid_list d \<and> valid_sched d \<and> True \<and> (a, b) \<noteq> c \<and> cte_wp_at (is_derived (cdt d) (a, b) cap) (a, b) d \<and> c \<noteq> (a, b) \<and> valid_mdb d)\<rbrace>
 3. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>c. invs' and cte_wp_at' (\<lambda>_. True) c and (\<lambda>d. pspace_distinct' d \<and> pspace_aligned' d \<and> ?P'127 word cap a b cap' c d)\<rbrace>
 4. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 5. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 6. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (6 subgoals):
 1. \<And>word cap a b cap' irq_slot irqSlot. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); irqSlot = cte_map irq_slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'127 word cap a b cap' (cte_map irq_slot)\<rbrace> cteDeleteOne (cte_map irq_slot) \<lbrace>\<lambda>r s. invs' s \<and> valid_cap' cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map irq_slot) s\<rbrace>
 2. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>c. einvs and cte_wp_at can_fast_finalise c and (\<lambda>d. (invs and emptyable c) d \<and> valid_list d \<and> valid_sched d \<and> True \<and> (a, b) \<noteq> c \<and> cte_wp_at (is_derived (cdt d) (a, b) cap) (a, b) d \<and> c \<noteq> (a, b) \<and> valid_mdb d)\<rbrace>
 3. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>c. invs' and cte_wp_at' (\<lambda>_. True) c and (\<lambda>d. pspace_distinct' d \<and> pspace_aligned' d \<and> ?P'127 word cap a b cap' c d)\<rbrace>
 4. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 word cap a b cap') s
 5. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 6. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (5 subgoals):
 1. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?P'171 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>rv s. (a, b) \<noteq> rv \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s \<and> rv \<noteq> (a, b) \<and> valid_mdb s\<rbrace>
 2. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>_. True) a and (\<lambda>a. pspace_distinct' a \<and> pspace_aligned' a \<and> invs' a \<and> valid_cap' cap' a \<and> True)\<rbrace>
 3. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. einvs s \<and> invs s \<and> invs s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> True \<and> ?P'171 word cap a b cap' s)) s
 4. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 5. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (5 subgoals):
 1. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?P'171 word cap a b cap'\<rbrace> get_irq_slot word \<lbrace>\<lambda>rv s. valid_mdb s \<and> rv \<noteq> (a, b) \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s\<rbrace>
 2. \<And>word cap a b cap'. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 word cap a b cap'\<rbrace> getIRQSlot word \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>_. True) a and (\<lambda>a. pspace_distinct' a \<and> pspace_aligned' a \<and> invs' a \<and> valid_cap' cap' a \<and> True)\<rbrace>
 3. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. einvs s \<and> invs s \<and> invs s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> True \<and> ?P'171 word cap a b cap' s)) s
 4. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'33 word cap a b cap') s
 5. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (3 subgoals):
 1. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (einvs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (cap.IRQHandlerCap word)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) (a, b) s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. einvs s \<and> invs s \<and> invs s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> True \<and> valid_mdb s \<and> (valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s) \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s)) s
 2. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> invs' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> invs' s \<and> valid_cap' cap' s \<and> True)) s
 3. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (3 subgoals):
 1. \<And>word cap a b cap' s aa ba. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (cap.IRQHandlerCap word)) (aa, ba) s; cte_wp_at (interrupt_derived cap) (a, b) s; s \<turnstile> cap; is_ntfn_cap cap\<rbrakk> \<Longrightarrow> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s
 2. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> invs' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> invs' s \<and> valid_cap' cap' s \<and> True)) s
 3. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (2 subgoals):
 1. \<And>word cap a b cap' s. \<lbrakk>i = irq_handler_invocation.SetIRQHandler word cap (a, b); cap_relation cap cap'; i' = irqhandler_invocation.SetIRQHandler word cap' (cte_map (a, b)); (invs' and (valid_cap' cap' and valid_cap' (capability.IRQHandlerCap word) and (\<lambda>y. isNotificationCap cap') and cte_wp_at' (badge_derived' cap' \<circ> cteCap) (cte_map (a, b)) and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word) ptr' s) and ex_cte_cap_wp_to' isCNodeCap (cte_map (a, b)))) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> invs' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> invs' s \<and> valid_cap' cap' s \<and> True)) s
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc einvs invs' (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne) proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> corres dc (?Q246 x3) (?Q'246 x3) (get_irq_slot x3 >>= cap_delete_one) (getIRQSlot x3 >>= cteDeleteOne)
 2. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; einvs s\<rbrakk> \<Longrightarrow> ?Q246 x3 s
 3. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; invs' s\<rbrakk> \<Longrightarrow> ?Q'246 x3 s proof (prove)
goal (5 subgoals):
 1. \<And>x3 rv rv'. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; rv' = cte_map rv\<rbrakk> \<Longrightarrow> corres dc (?R250 x3 rv) (?R'250 x3 rv') (cap_delete_one rv) (cteDeleteOne rv')
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q250 x3\<rbrace> get_irq_slot x3 \<lbrace>?R250 x3\<rbrace>
 3. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 x3\<rbrace> getIRQSlot x3 \<lbrace>?R'250 x3\<rbrace>
 4. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q250 x3) s
 5. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'250 x3) s proof (prove)
goal (5 subgoals):
 1. \<And>x3 rv rv'. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; rv' = cte_map rv\<rbrakk> \<Longrightarrow> corres dc (?R250 x3 rv) (?R'250 x3 (cte_map rv)) (cap_delete_one rv) (cteDeleteOne (cte_map rv))
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q250 x3\<rbrace> get_irq_slot x3 \<lbrace>?R250 x3\<rbrace>
 3. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 x3\<rbrace> getIRQSlot x3 \<lbrace>?R'250 x3\<rbrace>
 4. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q250 x3) s
 5. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'250 x3) s proof (prove)
goal (4 subgoals):
 1. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q250 x3\<rbrace> get_irq_slot x3 \<lbrace>\<lambda>a. einvs and cte_wp_at can_fast_finalise a\<rbrace>
 2. \<And>x3. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q'250 x3\<rbrace> getIRQSlot x3 \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>_. True) a\<rbrace>
 3. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q250 x3) s
 4. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'250 x3) s proof (prove)
goal (2 subgoals):
 1. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. einvs s \<and> invs s)) s
 2. \<And>x3 s. \<lbrakk>i' = irqhandler_invocation.ClearIRQHandler x3; i = irq_handler_invocation.ClearIRQHandler x3; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> invs' s)) s proof (prove)
goal:
No subgoals!