theory Refine_C

lemma check_active_irq_corres_C:
  "corres_underlying rf_sr False True (=)
             (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) \<top>
             (checkActiveIRQ) (checkActiveIRQ_C)" apply (simp add: checkActiveIRQ_C_def checkActiveIRQ_def getActiveIRQ_C_def) apply (rule corres_guard_imp) apply (subst bind_assoc[symmetric]) apply (rule corres_split) apply (rule ccorres_corres_u_xf) apply (rule ccorres_rel_imp, rule ccorres_guard_imp) apply (ctac add:getActiveIRQ_ccorres) apply (rule TrueI) apply simp apply assumption apply (rule no_fail_dmo') apply (rule no_fail_getActiveIRQ) apply (clarsimp simp: ucast_helper_simps_32 irqInvalid_def ucast_up_ucast_id
                            is_up_def source_size_def target_size_def word_size mask_def
                      split: option.splits) apply (rule hoare_TrueI)+ apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False True (=) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) (\<lambda>_. True) checkActiveIRQ checkActiveIRQ_C proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False True (=) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) (\<lambda>_. True) (do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od) (do y <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
irq <- gets ret__unsigned_long_';
return (irq \<noteq> kernel_all_global_addresses.irqInvalid)
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr False True (=) ?Q ?Q' (do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od) (do y <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
irq <- gets ret__unsigned_long_';
return (irq \<noteq> kernel_all_global_addresses.irqInvalid)
od)
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr False True (=) ?Q ?Q' (do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od) (do y <- do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od;
return (y \<noteq> kernel_all_global_addresses.irqInvalid)
od)
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres_underlying rf_sr False True ?r'7 ?P7 ?P'7 (doMachineOp (getActiveIRQ False)) (do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od)
 2. \<And>irq y. ?r'7 irq y \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 3. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 5. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. ccorres ?r'7 ret__unsigned_long_' ?P7 (Collect ?P'7) [] (doMachineOp (getActiveIRQ False)) (Call getActiveIRQ_'proc)
 2. no_fail ?P7 (doMachineOp (getActiveIRQ False))
 3. \<And>irq y. ?r'7 irq y \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 4. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 6. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 7. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (10 subgoals):
 1. ccorres ?r'15 ?xf'15 ?Q18 ?Q'18 [] (doMachineOp (getActiveIRQ False)) (Call getActiveIRQ_'proc)
 2. \<And>s. ?P7 s \<Longrightarrow> ?Q18 s
 3. \<And>s. s \<in> Collect ?P'7 \<Longrightarrow> s \<in> ?Q'18
 4. \<And>x y. ?r'15 x (?xf'15 y) \<Longrightarrow> ?r'7 x (ret__unsigned_long_' y)
 5. no_fail ?P7 (doMachineOp (getActiveIRQ False))
 6. \<And>irq y. ?r'7 irq y \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 7. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 8. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 9. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 10. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (9 subgoals):
 1. \<And>s. ?P7 s \<Longrightarrow> True
 2. \<And>s. s \<in> Collect ?P'7 \<Longrightarrow> s \<in> UNIV
 3. \<And>x y. case x of None \<Rightarrow> ret__unsigned_long_' y = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' y = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> ?r'7 x (ret__unsigned_long_' y)
 4. no_fail ?P7 (doMachineOp (getActiveIRQ False))
 5. \<And>irq y. ?r'7 irq y \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 6. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 7. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 8. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 9. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (8 subgoals):
 1. \<And>s. s \<in> Collect ?P'7 \<Longrightarrow> s \<in> UNIV
 2. \<And>x y. case x of None \<Rightarrow> ret__unsigned_long_' y = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' y = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> ?r'7 x (ret__unsigned_long_' y)
 3. no_fail ?P7 (doMachineOp (getActiveIRQ False))
 4. \<And>irq y. ?r'7 irq y \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 5. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 7. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 8. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. \<And>x y. case x of None \<Rightarrow> ret__unsigned_long_' y = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' y = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> ?r'7 x (ret__unsigned_long_' y)
 2. no_fail ?P7 (doMachineOp (getActiveIRQ False))
 3. \<And>irq y. ?r'7 irq y \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 4. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 6. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 7. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. no_fail ?P7 (doMachineOp (getActiveIRQ False))
 2. \<And>irq y. case irq of None \<Rightarrow> y = 0xFFFF | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 3. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 5. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. no_fail ?P26 (getActiveIRQ False)
 2. \<And>irq y. case irq of None \<Rightarrow> y = 0xFFFF | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 3. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 5. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> (?P26 \<circ> ksMachineState and ?Q7) s
 6. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<And>irq y. case irq of None \<Rightarrow> y = 0xFFFF | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> corres_underlying rf_sr False True (=) (?R7 irq) (?R'7 y) (return (\<exists>y. irq = Some y)) (return (y \<noteq> kernel_all_global_addresses.irqInvalid))
 2. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 4. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q7) s
 5. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R7\<rbrace>
 2. \<lbrace>?Q'7\<rbrace> do x <- exec_C \<Gamma> (Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'7\<rbrace>
 3. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q7) s
 4. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q7) s
 2. \<And>s. True \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal:
No subgoals!