theory Interrupt_C

lemma Arch_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. handlerSlot_' s = cte_Ptr slot}
            \<inter> {s. controlSlot_' s = cte_Ptr parent}
            \<inter> {s. trigger_' s = from_bool trigger}) hs
      (performIRQControl (ArchIRQControl (IssueIRQHandler irq slot parent trigger)))
      (Call Arch_invokeIRQControl_'proc)" unfolding ARM_H.performIRQControl_def IRQ_def apply (cinit lift: irq_' handlerSlot_' controlSlot_' trigger_'
               simp: ARM_H.performIRQControl_def IRQ_def) apply (rule ccorres_liftE) apply (ctac (no_vcg) add: setIRQTrigger_ccorres) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: invokeIRQControl_expanded_ccorres) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply (wpsimp simp: guard_is_UNIV_def)+ 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>handlerSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>) hs (global.performIRQControl (irqcontrol_invocation.ArchIRQControl (local.irqcontrol_invocation.IssueIRQHandler irq slot parent trigger))) (Call Arch_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>handlerSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>controlSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>) hs (global.performIRQControl (irqcontrol_invocation.ArchIRQControl (local.irqcontrol_invocation.IssueIRQHandler irq slot parent trigger))) (Call Arch_invokeIRQControl_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q297 triggera controlSlot handlerSlot irqa) (?Q'297 triggera controlSlot handlerSlot irqa) (SKIP # hs) (liftE (do y <- doMachineOp (setIRQTrigger irq trigger);
y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od)) (CALL setIRQTrigger_'proc(irqa,triggera);;
(\<acute>ret__unsigned_long :== CALL invokeIRQControl_'proc(irqa,handlerSlot,controlSlot);;
return_C ret__unsigned_long_'_update ret__unsigned_long_'))
 2. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q297 triggera controlSlot handlerSlot irqa s \<and> s' \<in> ?Q'297 triggera controlSlot handlerSlot irqa proof (prove)
goal (2 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv. (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q297 triggera controlSlot handlerSlot irqa) (?Q'297 triggera controlSlot handlerSlot irqa) (SKIP # hs) (do y <- doMachineOp (setIRQTrigger irq trigger);
y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (CALL setIRQTrigger_'proc(irqa,triggera);;
(\<acute>ret__unsigned_long :== CALL invokeIRQControl_'proc(irqa,handlerSlot,controlSlot);;
return_C ret__unsigned_long_'_update ret__unsigned_long_'))
 2. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q297 triggera controlSlot handlerSlot irqa s \<and> s' \<in> ?Q'297 triggera controlSlot handlerSlot irqa proof (prove)
goal (3 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa rv xfdc. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv. (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q307 triggera controlSlot handlerSlot irqa rv) (?Q'307 triggera controlSlot handlerSlot irqa rv xfdc) (SKIP # hs) (do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (\<acute>ret__unsigned_long :== CALL invokeIRQControl_'proc(irqa,handlerSlot,controlSlot);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')
 2. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R307 triggera controlSlot handlerSlot irqa\<rbrace> doMachineOp (setIRQTrigger irq trigger) \<lbrace>?Q307 triggera controlSlot handlerSlot irqa\<rbrace>
 3. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R307 triggera controlSlot handlerSlot irqa) s \<and> s' \<in> {s. trigger_'_update (\<lambda>_. triggera) (irq_'_update (\<lambda>_. irqa) s) \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'307 triggera controlSlot handlerSlot irqa rv (xfdc t)} proof (prove)
goal (3 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa rv xfdc. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv. (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q307 triggera controlSlot handlerSlot irqa rv) (?Q'307 triggera controlSlot handlerSlot irqa rv xfdc) (SKIP # hs) (do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od >>= return) (\<acute>ret__unsigned_long :== CALL invokeIRQControl_'proc(irqa,handlerSlot,controlSlot);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')
 2. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R307 triggera controlSlot handlerSlot irqa\<rbrace> doMachineOp (setIRQTrigger irq trigger) \<lbrace>?Q307 triggera controlSlot handlerSlot irqa\<rbrace>
 3. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R307 triggera controlSlot handlerSlot irqa) s \<and> s' \<in> {s. trigger_'_update (\<lambda>_. triggera) (irq_'_update (\<lambda>_. irqa) s) \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'307 triggera controlSlot handlerSlot irqa rv (xfdc t)} proof (prove)
goal (4 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa rv xfdc rva ret__unsigned_long. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv. (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv)) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q335 triggera controlSlot handlerSlot irqa rv xfdc rva) (?Q'335 triggera controlSlot handlerSlot irqa rv xfdc rva ret__unsigned_long) (SKIP # hs) (return rva) (return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long))
 2. \<And>triggera controlSlot handlerSlot irqa rv xfdc. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R337 triggera controlSlot handlerSlot irqa rv\<rbrace> do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od \<lbrace>?Q335 triggera controlSlot handlerSlot irqa rv xfdc\<rbrace>
 3. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R307 triggera controlSlot handlerSlot irqa\<rbrace> doMachineOp (setIRQTrigger irq trigger) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R337 triggera controlSlot handlerSlot irqa rv\<rbrace>
 4. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R307 triggera controlSlot handlerSlot irqa) s \<and> s' \<in> {s. trigger_'_update (\<lambda>_. triggera) (irq_'_update (\<lambda>_. irqa) s) \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. controlSlot_'_update (\<lambda>_. controlSlot) (handlerSlot_'_update (\<lambda>_. handlerSlot) (irq_'_update (\<lambda>_. irqa) 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>} \<inter> {s'. \<forall>ta rva. ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s'\<lparr>globals := globals ta, ret__unsigned_long_' := ret__unsigned_long_' ta\<rparr> \<in> ?Q'335 triggera controlSlot handlerSlot irqa rv (xfdc t) rva (ret__unsigned_long_' ta)}} proof (prove)
goal (4 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa rv xfdc rva ret__unsigned_long. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return rva \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv) (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>triggera controlSlot handlerSlot irqa rv xfdc. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R337 triggera controlSlot handlerSlot irqa rv\<rbrace> do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R307 triggera controlSlot handlerSlot irqa\<rbrace> doMachineOp (setIRQTrigger irq trigger) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R337 triggera controlSlot handlerSlot irqa rv\<rbrace>
 4. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R307 triggera controlSlot handlerSlot irqa) s \<and> s' \<in> {s. trigger_'_update (\<lambda>_. triggera) (irq_'_update (\<lambda>_. irqa) s) \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. controlSlot_'_update (\<lambda>_. controlSlot) (handlerSlot_'_update (\<lambda>_. handlerSlot) (irq_'_update (\<lambda>_. irqa) 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>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}} proof (prove)
goal (4 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa rv xfdc rva ret__unsigned_long \<sigma>. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return rva \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := ret__unsigned_long, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv) (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := ret__unsigned_long, global_exn_var_' := Return\<rparr>))}
 2. \<And>triggera controlSlot handlerSlot irqa rv xfdc. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R337 triggera controlSlot handlerSlot irqa rv\<rbrace> do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R307 triggera controlSlot handlerSlot irqa\<rbrace> doMachineOp (setIRQTrigger irq trigger) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R337 triggera controlSlot handlerSlot irqa rv\<rbrace>
 4. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R307 triggera controlSlot handlerSlot irqa) s \<and> s' \<in> {s. trigger_'_update (\<lambda>_. triggera) (irq_'_update (\<lambda>_. irqa) s) \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. controlSlot_'_update (\<lambda>_. controlSlot) (handlerSlot_'_update (\<lambda>_. handlerSlot) (irq_'_update (\<lambda>_. irqa) 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>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}} proof (prove)
goal (3 subgoals):
 1. \<And>triggera controlSlot handlerSlot irqa rv xfdc. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R337 triggera controlSlot handlerSlot irqa rv\<rbrace> do y <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>triggera controlSlot handlerSlot irqa. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R307 triggera controlSlot handlerSlot irqa\<rbrace> doMachineOp (setIRQTrigger irq trigger) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>_. True) parent and (\<lambda>_. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R337 triggera controlSlot handlerSlot irqa rv\<rbrace>
 3. \<And>triggera controlSlot handlerSlot irqa s s'. \<lbrakk>triggera = from_bool trigger; controlSlot = cte_Ptr parent; handlerSlot = cte_Ptr slot; irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (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; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R307 triggera controlSlot handlerSlot irqa) s \<and> s' \<in> {s. trigger_'_update (\<lambda>_. triggera) (irq_'_update (\<lambda>_. irqa) s) \<in> UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> \<lbrace>\<acute>trigger = from_bool trigger\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. controlSlot_'_update (\<lambda>_. controlSlot) (handlerSlot_'_update (\<lambda>_. handlerSlot) (irq_'_update (\<lambda>_. irqa) 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>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}} proof (prove)
goal:
No subgoals!