theory Interrupt_C

lemma invokeIRQControl_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
      (invs' and cte_at' parent and (\<lambda>_. (ucast irq) \<le> (ucast Kernel_C.maxIRQ :: machine_word)))
      (UNIV \<inter> {s. irq_' s = ucast irq}
                  \<inter> {s. controlSlot_' s = cte_Ptr parent}
                  \<inter> {s. handlerSlot_' s = cte_Ptr slot}) hs
      (performIRQControl (Invocations_H.IssueIRQHandler irq slot parent))
      (Call invokeIRQControl_'proc)" unfolding performIRQControl_def apply simp apply (rule ccorres_liftE) apply (rule ccorres_rel_imp) apply (rule ccorres_guard_imp) apply (rule invokeIRQControl_expanded_ccorres) apply assumption apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>) hs (global.performIRQControl (Invocations_H.irqcontrol_invocation.IssueIRQHandler irq slot parent)) (Call invokeIRQControl_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>) hs (case Invocations_H.irqcontrol_invocation.IssueIRQHandler irq slot parent of irqcontrol_invocation.ArchIRQControl invok \<Rightarrow> Arch.performIRQControl invok | Invocations_H.irqcontrol_invocation.IssueIRQHandler irq handlerSlot controlSlot \<Rightarrow> withoutPreemption $ do setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) controlSlot handlerSlot
od) (Call invokeIRQControl_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (\<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>) hs (liftE (do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od)) (Call invokeIRQControl_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv. (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv)) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (\<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>) hs (do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (Call invokeIRQControl_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres ?r'8 ?xf'8 (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (\<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>) hs (do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (Call invokeIRQControl_'proc)
 2. \<And>x y. ?r'8 x (?xf'8 y) \<Longrightarrow> (K (K (\<lambda>_. False)) \<currency> dc) (Inr x) (liftxf errstate id (K ()) ret__unsigned_long_' y) proof (prove)
goal (4 subgoals):
 1. ccorres ?r'8 ?xf'8 ?Q11 ?Q'11 hs (do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (Call invokeIRQControl_'proc)
 2. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) s \<Longrightarrow> ?Q11 s
 3. \<And>s. s \<in> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace> \<Longrightarrow> s \<in> ?Q'11
 4. \<And>x y. ?r'8 x (?xf'8 y) \<Longrightarrow> (K (K (\<lambda>_. False)) \<currency> dc) (Inr x) (liftxf errstate id (K ()) ret__unsigned_long_' y) proof (prove)
goal (3 subgoals):
 1. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) s \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) s
 2. \<And>s. s \<in> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>
 3. \<And>x y. ret__unsigned_long_' y = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<Longrightarrow> (K (K (\<lambda>_. False)) \<currency> dc) (Inr x) (liftxf errstate id (K ()) ret__unsigned_long_' y) proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>handlerSlot = cte_Ptr slot\<rbrace>
 2. \<And>x y. ret__unsigned_long_' y = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<Longrightarrow> (K (K (\<lambda>_. False)) \<currency> dc) (Inr x) (liftxf errstate id (K ()) ret__unsigned_long_' y) proof (prove)
goal:
No subgoals!