theory ArchADT_IF_Refine_C

lemma check_active_irq_corres_C[ADT_IF_Refine_assms]:
  "corres_underlying rf_sr False False (=) \<top> \<top> (checkActiveIRQ_if tc) (checkActiveIRQ_C_if tc)" apply (simp add: checkActiveIRQ_if_def checkActiveIRQ_C_if_def) apply (simp add: getActiveIRQ_C_def) apply (subst bind_assoc[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[where r'="\<lambda>a c. case a of None \<Rightarrow> c = ucast irqInvalid
                                                                | Some x \<Rightarrow> c = ucast x \<and> c \<noteq> ucast irqInvalid",
                                        OF ccorres_corres_u_xf]) apply (rule ccorres_guard_imp) apply (rule ccorres_rel_imp, rule ccorres_guard_imp) apply (rule getActiveIRQ_ccorres) apply simp+ apply (case_tac x; simp add: ucast_helper_simps_32 irqInvalid_def2) apply simp+ apply (rule no_fail_dmo') apply (rule no_fail_getActiveIRQ) apply (rule corres_trivial, clarsimp split: if_split option.splits) apply wp+ apply simp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (checkActiveIRQ_if tc) (checkActiveIRQ_C_if tc) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (do irq <- doMachineOp (getActiveIRQ False);
return (irq, tc)
od) (do y <- getActiveIRQ_C;
irq <- gets ret__unsigned_long_';
return (if irq = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) irq), tc)
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (do irq <- doMachineOp (getActiveIRQ False);
return (irq, tc)
od) (do y <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
irq <- gets ret__unsigned_long_';
return (if irq = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) irq), tc)
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (\<lambda>_. True) (\<lambda>_. True) (do irq <- doMachineOp (getActiveIRQ False);
return (irq, tc)
od) (do y <- do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od;
return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc)
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr False False (=) ?Q2 ?Q'2 (do irq <- doMachineOp (getActiveIRQ False);
return (irq, tc)
od) (do y <- do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od;
return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc)
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. True \<Longrightarrow> ?Q'2 s proof (prove)
goal (7 subgoals):
 1. ccorres (\<lambda>a c. case a of None \<Rightarrow> c = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> c = UCAST(10 \<rightarrow> 32) x \<and> c \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid) ret__unsigned_long_' ?P6 (Collect ?P'6) [] (doMachineOp (getActiveIRQ False)) (com.Call getActiveIRQ_'proc)
 2. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 3. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 4. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 6. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 7. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. ccorres (\<lambda>a c. case a of None \<Rightarrow> c = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> c = UCAST(10 \<rightarrow> 32) x \<and> c \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid) ret__unsigned_long_' ?Q16 ?Q'16 [] (doMachineOp (getActiveIRQ False)) (com.Call getActiveIRQ_'proc)
 2. \<And>s. ?P6 s \<Longrightarrow> ?Q16 s
 3. \<And>s. s \<in> Collect ?P'6 \<Longrightarrow> s \<in> ?Q'16
 4. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 5. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 6. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 9. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (12 subgoals):
 1. ccorres ?r'20 ?xf'20 ?Q23 ?Q'23 [] (doMachineOp (getActiveIRQ False)) (com.Call getActiveIRQ_'proc)
 2. \<And>s. ?Q16 s \<Longrightarrow> ?Q23 s
 3. \<And>s. s \<in> ?Q'16 \<Longrightarrow> s \<in> ?Q'23
 4. \<And>x y. ?r'20 x (?xf'20 y) \<Longrightarrow> case x of None \<Rightarrow> ret__unsigned_long_' y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> ret__unsigned_long_' y = UCAST(10 \<rightarrow> 32) x \<and> ret__unsigned_long_' y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid
 5. \<And>s. ?P6 s \<Longrightarrow> ?Q16 s
 6. \<And>s. s \<in> Collect ?P'6 \<Longrightarrow> s \<in> ?Q'16
 7. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 8. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 9. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 10. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s. ?Q16 s \<Longrightarrow> True
 2. \<And>s. s \<in> ?Q'16 \<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> case x of None \<Rightarrow> ret__unsigned_long_' y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> ret__unsigned_long_' y = UCAST(10 \<rightarrow> 32) x \<and> ret__unsigned_long_' y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid
 4. \<And>s. ?P6 s \<Longrightarrow> ?Q16 s
 5. \<And>s. s \<in> Collect ?P'6 \<Longrightarrow> s \<in> ?Q'16
 6. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 7. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 8. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 10. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (9 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> case x of None \<Rightarrow> ret__unsigned_long_' y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> ret__unsigned_long_' y = UCAST(10 \<rightarrow> 32) x \<and> ret__unsigned_long_' y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid
 2. \<And>s. ?P6 s \<Longrightarrow> ?Q16 s
 3. \<And>s. s \<in> Collect ?P'6 \<Longrightarrow> s \<in> ?Q'16
 4. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 5. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 6. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 9. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>s. ?P6 s \<Longrightarrow> ?Q16 s
 2. \<And>s. s \<in> Collect ?P'6 \<Longrightarrow> s \<in> ?Q'16
 3. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 4. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 5. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 7. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 8. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. no_fail ?P6 (doMachineOp (getActiveIRQ False))
 2. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 3. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. True \<Longrightarrow> ((\<lambda>s. s \<in> ?Q'16) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. no_fail ?P35 (getActiveIRQ False)
 2. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 3. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P35 \<circ> ksMachineState and ?Q6) s
 6. \<And>s. True \<Longrightarrow> ((\<lambda>s. s \<in> ?Q'16) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>irq y. case irq of None \<Rightarrow> y = UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid | Some x \<Rightarrow> y = UCAST(10 \<rightarrow> 32) x \<and> y \<noteq> UCAST(32 \<rightarrow> 32) kernel_all_global_addresses.irqInvalid \<Longrightarrow> corres_underlying rf_sr False False (=) (?R6 irq) (?R'6 y) (return (irq, tc)) (return (if y = kernel_all_global_addresses.irqInvalid then None else Some (UCAST(32 \<rightarrow> 10) y), tc))
 2. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>s. s \<in> ?Q'16) and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irq _. True\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> do x <- exec_C \<Gamma> (com.Call getActiveIRQ_'proc);
gets ret__unsigned_long_'
od \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q6) s
 4. \<And>s. True \<Longrightarrow> ((\<lambda>s. s \<in> ?Q'16) and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and (\<lambda>s. True)) s
 2. \<And>s. True \<Longrightarrow> ((\<lambda>s. s \<in> ?Q'16) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> ?Q'16 proof (prove)
goal:
No subgoals!