theory CSpace_C

lemma setIRQState_ccorres:
  "ccorres dc xfdc
           (\<top> and (\<lambda>s. ucast irq \<le> (ucast Kernel_C.maxIRQ :: machine_word)))
           (UNIV \<inter> {s. irqState_' s = irqstate_to_C irqState}
                 \<inter> {s. irq_' s = ucast irq}  )
           []
           (setIRQState irqState irq)
           (Call setIRQState_'proc )" apply (rule ccorres_gen_asm) apply (cinit simp del: return_bind) apply (rule ccorres_symb_exec_l) apply simp apply (rule_tac r'="dc" and xf'="xfdc" in ccorres_split_nothrow) apply (rule_tac P= "\<lambda>s. st = (ksInterruptState s)"
                      and P'= "(UNIV \<inter> {s. irqState_' s = irqstate_to_C irqState}
                                     \<inter> {s. irq_' s = ucast irq}  )"
                   in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: setInterruptState_def) apply (clarsimp simp: simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                carch_state_relation_def cmachine_state_relation_def) apply (simp add: cinterrupt_relation_def Kernel_C.maxIRQ_def) apply (clarsimp simp:  word_sless_msb_less order_le_less_trans
                            unat_ucast_no_overflow_le word_le_nat_alt ucast_ucast_b
                         split: if_split ) apply ceqv apply (ctac add:  maskInterrupt_ccorres) apply wp apply vcg apply wp apply (simp add: getInterruptState_def gets_def) apply wp apply (simp add: empty_fail_def getInterruptState_def simpler_gets_def) apply clarsimp apply (cases irqState, simp_all) apply (simp add: Kernel_C.IRQSignal_def Kernel_C.IRQInactive_def) apply (simp add: Kernel_C.IRQTimer_def Kernel_C.IRQInactive_def) apply (simp add: Kernel_C.IRQInactive_def Kernel_C.IRQReserved_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>_. True) and (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>) [] (setIRQState irqState irq) (Call setIRQState_'proc) proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>) [] (setIRQState irqState irq) (Call setIRQState_'proc) proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (do st <- getInterruptState;
table <- return (intStateIRQTable st);
y <- setInterruptState (intStateIRQTable_update (\<lambda>_. table(irq := irqState)) st);
doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)
od) (Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState);;
CALL maskInterrupt_'proc(SCAST(32 signed \<rightarrow> 32) (if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then 1 else 0),\<acute>irq))
 2. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (5 subgoals):
 1. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres dc xfdc (?Q15 st) (?Q'15 st) [SKIP] (do table <- return (intStateIRQTable st);
y <- setInterruptState (intStateIRQTable_update (\<lambda>_. table(irq := irqState)) st);
doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)
od) (Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState);;
CALL maskInterrupt_'proc(SCAST(32 signed \<rightarrow> 32) (if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then 1 else 0),\<acute>irq))
 2. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>?Q15\<rbrace>
 4. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 5. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (5 subgoals):
 1. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres dc xfdc (?Q15 st) (?Q'15 st) [SKIP] (do y <- setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st);
doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)
od) (Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState);;
CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>?Q15\<rbrace>
 4. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 5. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (9 subgoals):
 1. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres dc xfdc (?P22 st) (?P'22 st) [SKIP] (setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st)) (Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState))
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. ?P22 st and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P22 rv and ?R22 rv) s \<longrightarrow> s' \<in> ?P'22 rv \<inter> ?R'22 rv} proof (prove)
goal (9 subgoals):
 1. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. st = ksInterruptState \<sigma> \<and> s \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<exists>(rv, \<sigma>')\<in>fst (setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (9 subgoals):
 1. \<And>st \<sigma>. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> {s. st = ksInterruptState \<sigma> \<and> s \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. irq_' s < 0xA0 \<and> (\<exists>(rv, \<sigma>')\<in>fst (setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<sigma>). (\<sigma>', globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s)))}
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; irqState_' x = irqstate_to_C irqState; irq_' x = UCAST(10 \<rightarrow> 32) irq; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq < 0xA0 \<and> (\<exists>xa\<in>fst (modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState \<sigma>))(irq := irqState)) (ksInterruptState \<sigma>))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals x)) (unat irq) (irqstate_to_C irqState))) x) \<in> rf_sr)
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; irqState_' x = irqstate_to_C irqState; irq_' x = UCAST(10 \<rightarrow> 32) irq; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq < 0xA0 \<and> (\<sigma>\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState \<sigma>))(irq := irqState)) (ksInterruptState \<sigma>)\<rparr>, globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals x)) (unat irq) (irqstate_to_C irqState))) x) \<in> rf_sr
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; irqState_' x = irqstate_to_C irqState; irq_' x = UCAST(10 \<rightarrow> 32) irq; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq < 0xA0 \<and> cinterrupt_relation (intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState \<sigma>))(irq := irqState)) (ksInterruptState \<sigma>)) intStateIRQNode_array_Ptr (Arrays.update (intStateIRQTable_' (globals x)) (unat irq) (irqstate_to_C irqState))
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> 0x9F; irqState_' x = irqstate_to_C irqState; irq_' x = UCAST(10 \<rightarrow> 32) irq; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma> \<and> (\<forall>irq\<le>0x9F. irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq < 0xA0 \<and> (\<forall>irqa\<le>0x9F. irqstate_to_C (if irqa = irq then irqState else intStateIRQTable (ksInterruptState \<sigma>) irqa) = Arrays.update (intStateIRQTable_' (globals x)) (unat irq) (irqstate_to_C irqState).[unat irqa])
 2. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 3. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 5. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 6. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 8. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 9. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (8 subgoals):
 1. \<And>st rv' t t'. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) (?d'22 st rv')
 2. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (?d'22 st rv')
 3. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 4. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 5. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 7. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 8. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (7 subgoals):
 1. \<And>st rv rv'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q22 st rv) (?Q'22 st rv rv') [SKIP] (doMachineOp (maskInterrupt (irqState = irqstate.IRQInactive) irq)) (CALL maskInterrupt_'proc(if \<acute>irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>?Q22 st\<rbrace>
 3. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'22 st rv (xfdc s)}
 4. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 6. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 7. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (6 subgoals):
 1. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?R22 st\<rbrace> setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqState)) st) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. disable_'_update (\<lambda>_. if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) s \<in> \<lbrace>\<acute>disable = from_bool (irqState = irqstate.IRQInactive)\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>}}
 3. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and ?R22 st\<rbrace>
 5. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 6. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and ?R22 rv) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (5 subgoals):
 1. \<And>st. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F22 st\<^esub> (?R'22 st) Guard ArrayBounds \<lbrace>\<acute>irq < 0xA0\<rbrace> (\<acute>intStateIRQTable :== Arrays.update \<acute>intStateIRQTable (unat \<acute>irq) \<acute>irqState) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. disable_'_update (\<lambda>_. if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) s \<in> \<lbrace>\<acute>disable = from_bool (irqState = irqstate.IRQInactive)\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>}}
 2. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and (\<lambda>s. True)\<rbrace>
 4. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 5. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and (\<lambda>s. True)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> ?R'22 rv} proof (prove)
goal (4 subgoals):
 1. \<And>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>(=) s\<rbrace> getInterruptState \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and (\<lambda>s. True)\<rbrace>
 3. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 4. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and (\<lambda>s. True)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> {s. irq_' s < 0xA0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s)) \<longrightarrow> (if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (irqState = irqstate.IRQInactive) \<and> irq_' s = UCAST(10 \<rightarrow> 32) irq)}} proof (prove)
goal (3 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> getInterruptState \<lbrace>\<lambda>st. (\<lambda>s. st = ksInterruptState s) and (\<lambda>s. True)\<rbrace>
 2. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 3. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and (\<lambda>s. True)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> {s. irq_' s < 0xA0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s)) \<longrightarrow> (if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (irqState = irqstate.IRQInactive) \<and> irq_' s = UCAST(10 \<rightarrow> 32) irq)}} proof (prove)
goal (3 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<lbrace>?Q9\<rbrace> do s <- get;
return (ksInterruptState s)
od \<lbrace>\<lambda>st a. st = ksInterruptState a\<rbrace>
 2. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 3. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and (\<lambda>s. True)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> {s. irq_' s < 0xA0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s)) \<longrightarrow> (if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (irqState = irqstate.IRQInactive) \<and> irq_' s = UCAST(10 \<rightarrow> 32) irq)}} proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> empty_fail getInterruptState
 2. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ksInterruptState s = ksInterruptState s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and (\<lambda>s. True)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> {s. irq_' s < 0xA0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s)) \<longrightarrow> (if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (irqState = irqstate.IRQInactive) \<and> irq_' s = UCAST(10 \<rightarrow> 32) irq)}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ksInterruptState s = ksInterruptState s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksInterruptState s) and (\<lambda>s. True)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqState\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace> \<inter> {s. irq_' s < 0xA0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (globals_update (intStateIRQTable_'_update (\<lambda>_. Arrays.update (intStateIRQTable_' (globals s)) (unat (irq_' s)) (irqState_' s))) s)) \<longrightarrow> (if irqState_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (irqState = irqstate.IRQInactive) \<and> irq_' s = UCAST(10 \<rightarrow> 32) irq)}} proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = irqstate_to_C irqState; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0\<rbrakk> \<Longrightarrow> (if irqstate_to_C irqState = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (irqState = irqstate.IRQInactive) proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQSignal; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0; irqState = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> (if Kernel_C.IRQSignal = Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = SCAST(32 signed \<rightarrow> 32) false
 2. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQTimer; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0; irqState = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> (if Kernel_C.IRQTimer = Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = SCAST(32 signed \<rightarrow> 32) false
 3. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQReserved; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0; irqState = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> (if Kernel_C.IRQReserved = Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = SCAST(32 signed \<rightarrow> 32) false proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQTimer; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0; irqState = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> (if Kernel_C.IRQTimer = Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = SCAST(32 signed \<rightarrow> 32) false
 2. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQReserved; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0; irqState = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> (if Kernel_C.IRQReserved = Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = SCAST(32 signed \<rightarrow> 32) false proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (s, s') \<in> rf_sr; irqState_' s' = SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQReserved; irq_' s' = UCAST(10 \<rightarrow> 32) irq; (sa, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq < 0xA0; irqState = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> (if Kernel_C.IRQReserved = Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = SCAST(32 signed \<rightarrow> 32) false proof (prove)
goal:
No subgoals!