theory Interrupt_C

lemma Arch_checkIRQ_ccorres:
  "ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> scast Kernel_C.maxIRQ))
           (liftxf errstate id undefined ret__unsigned_long_')
   \<top> (UNIV \<inter> \<lbrace>irq = \<acute>irq_w\<rbrace>) []
   (checkIRQ irq) (Call Arch_checkIRQ_'proc)" apply (cinit lift: irq_w_' ) apply (simp add: rangeCheck_def unlessE_def ARM.minIRQ_def checkIRQ_def
                    ucast_nat_def word_le_nat_alt[symmetric]
                    linorder_not_le[symmetric] Platform_maxIRQ
                    length_ineq_not_Nil hd_conv_nth cast_simps
               del: Collect_const cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) apply (simp add: throwError_bind) apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) apply vcg apply (rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def
                          exception_defs syscall_error_rel_def
                          syscall_error_to_H_cases) apply clarsimp apply (rule ccorres_return_CE, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (\<lambda>_. True) (UNIV \<inter> \<lbrace>irq = \<acute>irq_w\<rbrace>) [] (checkIRQ irq) (Call Arch_checkIRQ_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>irq_w. irq = irq_w \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?Q246 irq_w) (?Q'246 irq_w) [SKIP] (rangeCheck irq (unat minIRQ) (unat local.maxIRQ)) (IF SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ < irq_w THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q246 irq_w s \<and> s' \<in> ?Q'246 irq_w proof (prove)
goal (2 subgoals):
 1. ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?Q246 irq) (?Q'246 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (IF \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q246 irq_w s \<and> s' \<in> ?Q'246 irq_w proof (prove)
goal (3 subgoals):
 1. \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?Q262 irq) (?S264 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<not> \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?Q262 irq_w s) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?S264 irq_w) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal (3 subgoals):
 1. \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?Q262 irq) (?S264 irq) [SKIP] (throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<not> \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?Q262 irq_w s) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?S264 irq_w) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal (4 subgoals):
 1. \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'272 irq) \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) {},UNIV
 2. \<And>\<sigma>. \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) rv (liftxf errstate id undefined ret__unsigned_long_' s)}
 3. \<not> \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> True) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> UNIV \<inter> ?R'272 irq_w) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMin_C_update (\<lambda>_. 0) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) rv (liftxf errstate id undefined ret__unsigned_long_' s)}
 2. \<not> \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> True) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) \<sigma>). (\<sigma>', globals_update (current_syscall_error_'_update (\<lambda>_. rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) (rangeErrorMin_C_update (\<lambda>_. 0) (type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) (current_syscall_error_' (globals s)))))) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. rangeErrorMax_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) (rangeErrorMin_C_update (\<lambda>_. 0) (type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RangeError) (current_syscall_error_' (globals s)))))) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>))}
 2. \<not> \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> True) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal (2 subgoals):
 1. \<not> \<not> irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then returnOk () else throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> True) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal (2 subgoals):
 1. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>r r'. irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) (liftxf errstate id undefined ret__unsigned_long_') (?R261 irq) (?T263 irq) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>irq_w s s'. \<lbrakk>irq = irq_w; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> True) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> ?R261 irq_w s)) \<and> s' \<in> {s. (\<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (\<not> \<not> irq_w \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> s \<in> ?T263 irq_w)} proof (prove)
goal:
No subgoals!