theory Interrupt_C

lemma invokeIRQControl_expanded_ccorres:
  "ccorres (\<lambda>_ r. r = scast EXCEPTION_NONE) (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
      (do x <- setIRQState irqstate.IRQSignal irq;
          cteInsert (capability.IRQHandlerCap irq) parent slot
       od)
      (Call invokeIRQControl_'proc)" apply (cinit' lift: irq_' controlSlot_' handlerSlot_') apply (ctac add: setIRQState_ccorres) apply csymbr apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: cteInsert_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 wp+ apply clarsimp apply (vcg exspec=setIRQState_modifies) apply (clarsimp simp: is_simple_cap'_def isCap_simps valid_cap_simps' capAligned_def
                        word_bits_def) apply (rule conjI) apply (fastforce simp: word_bits_def intro!: ucast_maxIRQ_le_eq) apply (simp add: invs_mdb' invs_valid_objs' invs_pspace_aligned') apply (rule conjI) apply (clarsimp simp: maxIRQ_def Kernel_C.maxIRQ_def) apply unat_arith apply simp apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift
                        cap_to_H_def c_valid_cap_def cl_valid_cap_def
                        word_bw_assocs mask_twice maxIRQ_def Kernel_C.maxIRQ_def ucast_ucast_a
                        is_up ucast_ucast_b is_down) apply (subst less_mask_eq) apply (rule le_m1_iff_lt[THEN iffD1,THEN iffD1]) apply simp apply (erule order.trans, simp) apply (rule word_eqI) apply (simp add: nth_ucast word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>_ r. r = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) 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 (do x <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (Call invokeIRQControl_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> ccorres (\<lambda>_ r. r = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret__unsigned_long_' (?Q302 handlerSlot controlSlot irqa) (?Q'302 handlerSlot controlSlot irqa) (SKIP # hs) (do x <- setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) parent slot
od) (CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa);;
(\<acute>ret__struct_cap_C :== CALL cap_irq_handler_cap_new_'proc(UCAST(32 \<rightarrow> 32) irqa);;
(CALL cteInsert_'proc(\<acute>ret__struct_cap_C,controlSlot,handlerSlot);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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> ?Q302 handlerSlot controlSlot irqa s \<and> s' \<in> ?Q'302 handlerSlot controlSlot irqa proof (prove)
goal (4 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdc. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>_ r. r = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret__unsigned_long_' (?Q310 handlerSlot controlSlot irqa rv) (?Q'310 handlerSlot controlSlot irqa rv xfdc) (SKIP # hs) (cteInsert (capability.IRQHandlerCap irq) parent slot) (\<acute>ret__struct_cap_C :== CALL cap_irq_handler_cap_new_'proc(UCAST(32 \<rightarrow> 32) irqa);;
(CALL cteInsert_'proc(\<acute>ret__struct_cap_C,controlSlot,handlerSlot);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>?Q310 handlerSlot controlSlot irqa\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'310 handlerSlot controlSlot irqa rv (xfdc s)}
 4. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (4 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> ccorres (\<lambda>_ r. r = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret__unsigned_long_' (?Q310 handlerSlot controlSlot irqa rv) (?G'339 handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C) (SKIP # hs) (cteInsert (capability.IRQHandlerCap irq) parent slot) (CALL cteInsert_'proc(ret__struct_cap_C,controlSlot,handlerSlot);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>?Q310 handlerSlot controlSlot irqa\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) sa) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> ?G'339 handlerSlot controlSlot irqa rv (xfdc s) v}}
 4. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (4 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> ccorres (\<lambda>_ r. r = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret__unsigned_long_' (?Q310 handlerSlot controlSlot irqa rv) (?G'339 handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C) (SKIP # hs) (cteInsert (capability.IRQHandlerCap irq) parent slot >>= return) (CALL cteInsert_'proc(ret__struct_cap_C,controlSlot,handlerSlot);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>?Q310 handlerSlot controlSlot irqa\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) sa) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> ?G'339 handlerSlot controlSlot irqa rv (xfdc s) v}}
 4. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (5 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdca ret__struct_cap_C rva xfdc. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdca; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>_ r. r = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret__unsigned_long_' (?Q403 handlerSlot controlSlot irqa rv xfdca ret__struct_cap_C rva) (?Q'403 handlerSlot controlSlot irqa rv xfdca ret__struct_cap_C rva xfdc) (SKIP # hs) (return rva) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R405 handlerSlot controlSlot irqa rv\<rbrace> cteInsert (capability.IRQHandlerCap irq) parent slot \<lbrace>?Q403 handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' (capability.IRQHandlerCap irq) and cte_wp_at' (\<lambda>c. True) parent and ?R405 handlerSlot controlSlot irqa rv\<rbrace>
 4. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) sa) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. handlerSlot) (srcSlot_'_update (\<lambda>_. controlSlot) (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'403 handlerSlot controlSlot irqa rv (xfdc s) v rva (xfdc t)}}}
 5. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (5 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdca ret__struct_cap_C rva xfdc. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdca; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap; dc rva xfdc\<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. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return rva \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ret__unsigned_long_' s = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE}
 2. \<And>handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R405 handlerSlot controlSlot irqa rv\<rbrace> cteInsert (capability.IRQHandlerCap irq) parent slot \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' (capability.IRQHandlerCap irq) and cte_wp_at' (\<lambda>c. True) parent and ?R405 handlerSlot controlSlot irqa rv\<rbrace>
 4. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) s) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. handlerSlot) (srcSlot_'_update (\<lambda>_. controlSlot) (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}
 5. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (5 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdca ret__struct_cap_C rva xfdc \<sigma>. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdca; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap; dc rva xfdc\<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_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE}
 2. \<And>handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R405 handlerSlot controlSlot irqa rv\<rbrace> cteInsert (capability.IRQHandlerCap irq) parent slot \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' (capability.IRQHandlerCap irq) and cte_wp_at' (\<lambda>c. True) parent and ?R405 handlerSlot controlSlot irqa rv\<rbrace>
 4. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) s) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. handlerSlot) (srcSlot_'_update (\<lambda>_. controlSlot) (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}
 5. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (4 subgoals):
 1. \<And>handlerSlot controlSlot irqa rv xfdc ret__struct_cap_C. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq; dc rv xfdc; cap_irq_handler_cap_lift ret__struct_cap_C = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R405 handlerSlot controlSlot irqa rv\<rbrace> cteInsert (capability.IRQHandlerCap irq) parent slot \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<lbrace>?R310 handlerSlot controlSlot irqa\<rbrace> setIRQState irqstate.IRQSignal irq \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' (capability.IRQHandlerCap irq) and cte_wp_at' (\<lambda>c. True) parent and ?R405 handlerSlot controlSlot irqa rv\<rbrace>
 3. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) s) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. handlerSlot) (srcSlot_'_update (\<lambda>_. controlSlot) (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}
 4. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and ?R310 handlerSlot controlSlot irqa) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (2 subgoals):
 1. \<And>handlerSlot controlSlot irqa. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; irqa = UCAST(10 \<rightarrow> 32) irq\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 handlerSlot controlSlot irqa) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,irqa) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = capIRQ_' (capIRQ_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) irqa) s) && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. handlerSlot) (srcSlot_'_update (\<lambda>_. controlSlot) (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr parent\<rbrace> \<inter> \<lbrace>ccap_relation (capability.IRQHandlerCap irq) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}
 2. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and (\<lambda>s. cte_wp_at' (\<lambda>a. capMasterCap (cteCap a) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent s \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> valid_cap' (capability.IRQHandlerCap irq) s \<and> cte_wp_at' (\<lambda>a. True) parent s \<and> True)) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'310 (cte_Ptr slot) (cte_Ptr parent) (UCAST(10 \<rightarrow> 32) irq)) CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal,UCAST(10 \<rightarrow> 32) irq) {s. \<forall>v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {})}
 2. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and (\<lambda>s. cte_wp_at' (\<lambda>a. capMasterCap (cteCap a) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent s \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> valid_cap' (capability.IRQHandlerCap irq) s \<and> cte_wp_at' (\<lambda>a. True) parent s \<and> True)) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> ?R'310 handlerSlot controlSlot irqa proof (prove)
goal (1 subgoal):
 1. \<And>handlerSlot controlSlot irqa s s'. \<lbrakk>handlerSlot = cte_Ptr slot; controlSlot = cte_Ptr parent; 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 (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) and (\<lambda>s. cte_wp_at' (\<lambda>a. capMasterCap (cteCap a) = capMasterCap (capability.IRQHandlerCap irq) \<or> is_simple_cap' (capability.IRQHandlerCap irq)) parent s \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> valid_cap' (capability.IRQHandlerCap irq) s \<and> cte_wp_at' (\<lambda>a. True) parent s \<and> True)) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQSignal\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} \<inter> {s. \<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = irqa && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s\<lparr>globals := globals s\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {})} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> irq \<le> local.maxIRQ \<and> (\<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {})) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> valid_mdb' s
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> valid_objs' s \<and> pspace_aligned' s \<and> irq \<le> local.maxIRQ \<and> (\<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {})) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> valid_objs' s \<and> pspace_aligned' s \<and> irq \<le> local.maxIRQ \<and> (\<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {})) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> irq \<le> local.maxIRQ \<and> (\<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {})) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> irq \<le> local.maxIRQ
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F\<rbrakk> \<Longrightarrow> irq \<le> 0x9F
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<And>s s' n na. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; n < 2 ^ LENGTH(32); n \<le> 159; na < 2 ^ LENGTH(10); unat (UCAST(10 \<rightarrow> 32) irq) = n; unat irq = na\<rbrakk> \<Longrightarrow> na \<le> 159
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<forall>t v. cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> s'\<lparr>globals := globals s'\<lparr>intStateIRQTable_' := intStateIRQTable_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation (capability.IRQHandlerCap irq) v then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> irq = UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) irq && mask 8) proof (prove)
goal (2 subgoals):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq < 2 ^ 8
 2. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> irq = UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) irq) proof (prove)
goal (3 subgoals):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> 0 < 2 ^ 8
 2. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq \<le> 2 ^ 8 - 1
 3. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> irq = UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) irq) proof (prove)
goal (2 subgoals):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq \<le> 2 ^ 8 - 1
 2. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> irq = UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) irq) proof (prove)
goal (1 subgoal):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> irq = UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) irq) proof (prove)
goal (1 subgoal):
 1. \<And>s s' v n. \<lbrakk>(s, s') \<in> rf_sr; invs' s; cte_wp_at' (\<lambda>_. True) parent s; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; cap_irq_handler_cap_lift v = \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>; cap_lift v = Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = UCAST(10 \<rightarrow> 32) irq && mask 8\<rparr>)\<rbrakk> \<Longrightarrow> n < size irq \<longrightarrow> irq !! n = UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) irq) !! n proof (prove)
goal:
No subgoals!