theory Refine_C

lemma handleInterruptEntry_ccorres:
  "ccorres dc xfdc
           (invs' and sch_act_simple)
           UNIV []
           (callKernel Interrupt) (Call handleInterruptEntry_'proc)" proof - show ?thesis apply (cinit') apply (simp add: callKernel_def handleEvent_def minus_one_norm) apply (rule ccorres_stateAssert) apply (simp add: liftE_bind bind_assoc) apply (ctac (no_vcg) add: getActiveIRQ_ccorres) apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm) apply wpc apply (simp add: irqInvalid_def ucast_helper_simps_32 mask_def) apply (rule ccorres_symb_exec_r) apply (ctac (no_vcg) add: schedule_ccorres) apply (rule ccorres_stateAssert_after) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: activateThread_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 schedule_sch_act_wf schedule_invs'
             | strengthen invs_queues_imp invs_valid_objs_strengthen)+ apply simp apply vcg apply vcg apply (clarsimp simp: irqInvalid_def ucast_ucast_b is_up ucast_helper_simps_32 mask_def) apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply (ctac (no_vcg) add: schedule_ccorres) apply (rule ccorres_stateAssert_after) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: activateThread_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 schedule_sch_act_wf schedule_invs'
             | strengthen invs_queues_imp invs_valid_objs_strengthen)+ apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> ARM.maxIRQ) \<and> rv \<noteq> Some 0x3FF" in hoare_post_imp) apply (clarsimp simp: Kernel_C.maxIRQ_def ARM.maxIRQ_def) apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+ apply (clarsimp simp: invs'_def valid_state'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple) UNIV [] (callKernel Interrupt) (Call handleInterruptEntry_'proc) proof (state)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple) UNIV [] (callKernel Interrupt) (Call handleInterruptEntry_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and sch_act_simple) UNIV [] (callKernel Interrupt) (Call handleInterruptEntry_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q23 ?Q'23 [SKIP] (callKernel Interrupt) (\<acute>irq :== CALL getActiveIRQ_'proc();;
(IF \<acute>irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(\<acute>irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q23 s \<and> s' \<in> ?Q'23 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q23 ?Q'23 [SKIP] (do y <- stateAssert fastpathKernelAssertions [];
y <- liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>irq :== CALL getActiveIRQ_'proc();;
(IF \<acute>irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc()
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q23 s \<and> s' \<in> ?Q'23 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?P30 ?Q'23 [SKIP] (do y <- liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>irq :== CALL getActiveIRQ_'proc();;
(IF \<acute>irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc()
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P30 s) \<and> s' \<in> ?Q'23 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?P30 ?Q'23 [SKIP] (do x <- doMachineOp (getActiveIRQ False);
rv <- case x of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (\<acute>irq :== CALL getActiveIRQ_'proc();;
(IF \<acute>irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc()
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ?P30 s) \<and> s' \<in> ?Q'23 proof (prove)
goal (3 subgoals):
 1. \<And>rv irq. case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> ccorres dc xfdc (?Q39 rv) (?Q'39 rv irq) [SKIP] (do rv <- case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?Q39\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'39 rv (ret__unsigned_long_' t)} proof (prove)
goal (3 subgoals):
 1. \<And>rv irq. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G176 rv) (?Q'39 rv irq) [SKIP] (do rv <- case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. ?G176 rv and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'39 rv (ret__unsigned_long_' t)} proof (prove)
goal (4 subgoals):
 1. \<And>rv irq. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R185 rv) (?R''187 rv irq) [SKIP] (do rv <- return ();
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 3. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> ?R185 rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (4 subgoals):
 1. ccorres dc xfdc (?R185 None) (?R''187 None 0xFFFF) [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL handleSpuriousIRQ_'proc();;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 3. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> ?R185 rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (6 subgoals):
 1. ccorres dc xfdc (?R185 None) ?Q'214 [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ?Q'214
 3. \<And>s. ?R185 None s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 4. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 5. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> ?R185 rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q220 rv) (?Q'220 rv xfdca) [SKIP] (do y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q220\<rbrace>
 3. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'220 rv (xfdc t)})
 4. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 5. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 6. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q220 rv and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'220 rv xfdca) [SKIP] activateThread (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q220\<rbrace>
 3. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'220 rv (xfdc t)})
 4. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 5. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 6. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q220 rv and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'220 rv xfdca) [SKIP] (activateThread >>= return) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q220\<rbrace>
 3. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'220 rv (xfdc t)})
 4. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 5. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 6. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (8 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q249 rv xfdca rva) (?Q'249 rv xfdca rva xfdcb) [SKIP] (return rva) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>?Q249 rv xfdc\<rbrace>
 3. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'249 rv (xfdc t) rva (xfdc ta)}})
 5. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 6. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 7. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (8 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<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> dc rv (xfdc s)}
 2. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}})
 5. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 6. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 7. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (8 subgoals):
 1. \<And>rv xfdca rva xfdcb \<sigma>. \<lbrakk>dc rv xfdca; dc rva xfdcb\<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> dc rv (xfdc (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}})
 5. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 6. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 7. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<lbrace>?R223 None\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 3. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}})
 4. \<And>s. (invs' and ?R223 None) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 5. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 6. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and ?R223 rv) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (5 subgoals):
 1. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() ({s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}})
 2. \<And>s. (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 3. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 4. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (5 subgoals):
 1. \<Gamma>\<turnstile> (?R''187 None 0xFFFF) CALL handleSpuriousIRQ_'proc() UNIV
 2. \<And>s. (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s \<Longrightarrow> \<Gamma>\<turnstile> (?R''187 None 0xFFFF \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 3. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 4. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''187 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (4 subgoals):
 1. \<And>s. (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>True\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) CALL handleSpuriousIRQ_'proc() {s'. (s, s') \<in> rf_sr}
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 3. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R186 rv x2) (?R''188 rv irq x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (IF irq \<noteq> kernel_all_global_addresses.irqInvalid THEN
  CALL handleInterrupt_'proc(irq)
ELSE
  CALL handleSpuriousIRQ_'proc()
FI;;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (3 subgoals):
 1. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> ccorres dc xfdc (?R186 (Some x2) x2) (?R''188 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2) [SKIP] (do rv <- handleInterrupt x2;
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL handleInterrupt_'proc(UCAST(10 \<rightarrow> 32) x2);;
(CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R186 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''188 rv (ret__unsigned_long_' t) x}}} proof (prove)
goal (4 subgoals):
 1. \<And>x2 rv xfdca. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q343 x2 rv) (?Q'343 x2 rv xfdca) [SKIP] (do y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL schedule_'proc();;
(CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>?Q343 x2\<rbrace>
 3. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'349 rv (ret__unsigned_long_' t) x ta rva}}}}
flex-flex pairs:
\<lambda>x2. ?Q'349 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2 \<equiv>\<^sup>? \<lambda>x2 t rv. ?Q'343 x2 rv (xfdc t) proof (prove)
goal (5 subgoals):
 1. \<And>x2 rv xfdca rva xfdcb. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q383 x2 rv xfdca rva) (?Q'383 x2 rv xfdca rva xfdcb) [SKIP] (do y <- activateThread;
stateAssert kernelExitAssertions []
od) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q383 x2 rv xfdc\<rbrace>
 3. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 4. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'393 rv (ret__unsigned_long_' t) x ta rva tb rvb}}}}}
flex-flex pairs:
\<lambda>x2. ?Q'393 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2 \<equiv>\<^sup>? \<lambda>x2 t rv ta rva. ?Q'383 x2 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (5 subgoals):
 1. \<And>x2 rv xfdca rva xfdcb. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q383 x2 rv xfdca rva and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'383 x2 rv xfdca rva xfdcb) [SKIP] activateThread (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q383 x2 rv xfdc\<rbrace>
 3. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 4. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'393 rv (ret__unsigned_long_' t) x ta rva tb rvb}}}}}
flex-flex pairs:
\<lambda>x2. ?Q'393 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2 \<equiv>\<^sup>? \<lambda>x2 t rv ta rva. ?Q'383 x2 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (5 subgoals):
 1. \<And>x2 rv xfdca rva xfdcb. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q383 x2 rv xfdca rva and (\<lambda>s. \<forall>(rv, s')\<in>fst (activateThread s). kernelExitAssertions s')) (?Q'383 x2 rv xfdca rva xfdcb) [SKIP] (activateThread >>= return) (CALL activateThread_'proc();;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q383 x2 rv xfdc\<rbrace>
 3. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 4. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'393 rv (ret__unsigned_long_' t) x ta rva tb rvb}}}}}
flex-flex pairs:
\<lambda>x2. ?Q'393 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2 \<equiv>\<^sup>? \<lambda>x2 t rv ta rva. ?Q'383 x2 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (6 subgoals):
 1. \<And>x2 rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q430 x2 rv xfdca rva xfdcb rvb) (?Q'430 x2 rv xfdca rva xfdcb rvb xfdcc) [SKIP] (return rvb) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>x2 rv xfdca rva xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>?Q430 x2 rv xfdca rva xfdc\<rbrace>
 3. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 5. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>tc rvc. dc rvc (xfdc tc) \<longrightarrow> s'\<lparr>globals := globals tc\<rparr> \<in> ?Q'435 rv (ret__unsigned_long_' t) x ta rva tb rvb tc rvc}}}}}}
flex-flex pairs:
\<lambda>x2. ?Q'435 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2 \<equiv>\<^sup>? \<lambda>x2 t rv ta rva tb rvb. ?Q'430 x2 rv (xfdc t) rva (xfdc ta) rvb (xfdc tb) proof (prove)
goal (6 subgoals):
 1. \<And>x2 rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<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 rvb \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>x2 rv xfdca rva xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 5. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}}} proof (prove)
goal (6 subgoals):
 1. \<And>x2 rv xfdca rva xfdcb rvb xfdcc \<sigma>. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return rvb \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>x2 rv xfdca rva xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 4. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 5. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}}} proof (prove)
goal (5 subgoals):
 1. \<And>x2 rv xfdca rva xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>a\<in>fst (activateThread a). case a of (rv, s') \<Rightarrow> kernelExitAssertions s'\<rbrace> activateThread \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R390 x2 rv\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 3. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R352 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a. invs' and ?R390 x2 a\<rbrace>
 4. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R352 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}}} proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> rv \<noteq> Some 0xFFFF\<rbrace>
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}}} proof (prove)
goal (3 subgoals):
 1. \<And>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> local.maxIRQ) \<and> rv \<noteq> Some 0x3FF \<Longrightarrow> (rv = None \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> invs' a \<and> invs' a \<and> invs' a)) s) \<and> rv \<noteq> Some 0xFFFF
 2. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> local.maxIRQ) \<and> rv \<noteq> Some 0x3FF\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}}} proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R39\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> local.maxIRQ) \<and> rv \<noteq> Some 0x3FF\<rbrace>
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (fastpathKernelAssertions s \<longrightarrow> ((\<lambda>_. True) and ?R39) s) \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> \<lbrace>True\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}}}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> fastpathKernelAssertions s \<longrightarrow> irqs_masked' s \<and> valid_irq_states' s proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xfdc (invs' and sch_act_simple) UNIV [] (callKernel Interrupt) (Call handleInterruptEntry_'proc)

goal:
No subgoals!