theory Tcb_C

lemma checkPrio_ccorres:
  "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
      (tcb_at' auth)
      (UNIV \<inter> {s. prio_' s = prio} \<inter> {s. auth_' s = tcb_ptr_to_ctcb_ptr auth}) []
      (checkPrio prio auth)
      (Call checkPrio_'proc)" apply (cinit lift: prio_' auth_') apply (clarsimp simp: liftE_bindE) apply (rule ccorres_split_nothrow_novcg[where r'="\<lambda>rv rv'. rv' = ucast rv" and xf'=mcp_']) apply (rule threadGet_vcg_corres) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: rf_sr_ksCurThread obj_at'_def projectKOs
                             typ_heap_simps' ctcb_relation_def) apply ceqv apply (simp add: whenE_def del: Collect_const split: if_split) apply (rule conjI; clarsimp) apply (rule ccorres_from_vcg_split_throws) apply vcg apply (rule conseqPre, vcg) apply (clarsimp simp: throwError_def syscall_error_rel_def syscall_error_to_H_cases
                            exception_defs Collect_const_mem rf_sr_ksCurThread return_def
                            seL4_MinPrio_def minPriority_def) apply clarsimp apply (rule ccorres_return_CE) apply clarsimp+ apply wp apply (simp add: guard_is_UNIV_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (tcb_at' auth) (UNIV \<inter> \<lbrace>\<acute>prio = prio\<rbrace> \<inter> \<lbrace>\<acute>auth = tcb_ptr_to_ctcb_ptr auth\<rbrace>) [] (checkPrio prio auth) (Call checkPrio_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>autha prioa. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio\<rbrakk> \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q485 autha prioa) (?Q'485 autha prioa) [SKIP] (doE mcp <- liftE (threadGet tcbMCP auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))
odE) (Guard C_Guard {s. s \<Turnstile>\<^sub>c autha} (\<acute>mcp :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(autha\<rightarrow>[''tcbMCP_C''])));;
(IF \<acute>mcp < prioa 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. \<acute>mcp) \<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>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q485 autha prioa s \<and> s' \<in> ?Q'485 autha prioa proof (prove)
goal (2 subgoals):
 1. ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q485 (tcb_ptr_to_ctcb_ptr auth) prio) (?Q'485 (tcb_ptr_to_ctcb_ptr auth) prio) [SKIP] (do mcp <- threadGet tcbMCP auth;
whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr auth} (\<acute>mcp :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr auth\<rightarrow>[''tcbMCP_C''])));;
(IF \<acute>mcp < prio 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. \<acute>mcp) \<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>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q485 autha prioa s \<and> s' \<in> ?Q'485 autha prioa proof (prove)
goal (6 subgoals):
 1. ccorres (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (?P501 (tcb_ptr_to_ctcb_ptr auth) prio) (?Q'485 (tcb_ptr_to_ctcb_ptr auth) prio) [] (threadGet tcbMCP auth) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr auth} (\<acute>mcp :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr auth\<rightarrow>[''tcbMCP_C'']))))
 2. \<And>rv' t t'. ceqv \<Gamma> mcp_' rv' t t' (IF \<acute>mcp < prio 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. \<acute>mcp) \<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)) (?d'496 rv')
 3. \<And>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp rv') [SKIP] (whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))) (?d'496 rv')
 4. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 5. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 6. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P501 autha prioa and ?R500 autha prioa) s \<and> s' \<in> ?Q'485 autha prioa proof (prove)
goal (6 subgoals):
 1. \<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> tcb_at' auth \<sigma> \<and> True \<and> (\<forall>tcb. ko_at' tcb auth \<sigma> \<longrightarrow> (\<exists>tcb'. x = tcbMCP tcb \<and> cslift s (tcb_ptr_to_ctcb_ptr auth) = Some tcb' \<and> ctcb_relation tcb tcb'))} Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr auth} (\<acute>mcp :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr auth\<rightarrow>[''tcbMCP_C'']))) {s. (\<sigma>, s) \<in> rf_sr \<and> mcp_' s = UCAST(8 \<rightarrow> 32) x}
 2. \<And>rv' t t'. ceqv \<Gamma> mcp_' rv' t t' (IF \<acute>mcp < prio 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. \<acute>mcp) \<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)) (?d'496 rv')
 3. \<And>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp rv') [SKIP] (whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))) (?d'496 rv')
 4. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 5. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 6. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>x \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> tcb_at' auth \<sigma> \<and> True \<and> (\<forall>tcb. ko_at' tcb auth \<sigma> \<longrightarrow> (\<exists>tcb'. x = tcbMCP tcb \<and> cslift s (tcb_ptr_to_ctcb_ptr auth) = Some tcb' \<and> ctcb_relation tcb tcb'))} \<subseteq> {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr auth \<and> (\<sigma>, mcp_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr auth\<rightarrow>[''tcbMCP_C'']))) s) \<in> rf_sr \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr auth\<rightarrow>[''tcbMCP_C''])) = UCAST(8 \<rightarrow> 32) x}
 2. \<And>rv' t t'. ceqv \<Gamma> mcp_' rv' t t' (IF \<acute>mcp < prio 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. \<acute>mcp) \<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)) (?d'496 rv')
 3. \<And>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp rv') [SKIP] (whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))) (?d'496 rv')
 4. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 5. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 6. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. ceqv \<Gamma> mcp_' rv' t t' (IF \<acute>mcp < prio 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. \<acute>mcp) \<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)) (?d'496 rv')
 2. \<And>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp rv') [SKIP] (whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))) (?d'496 rv')
 3. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 4. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 5. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp rv') [SKIP] (whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))) (IF rv' < prio 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. rv') \<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. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 3. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 4. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>mcp. (UCAST(8 \<rightarrow> 32) mcp < prio \<longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp (UCAST(8 \<rightarrow> 32) mcp)) [SKIP] (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp))) (IF True 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) \<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))) \<and> (\<not> UCAST(8 \<rightarrow> 32) mcp < prio \<longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp (UCAST(8 \<rightarrow> 32) mcp)) [SKIP] (returnOk ()) (IF False 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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) \<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. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 3. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 4. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>mcp. UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp (UCAST(8 \<rightarrow> 32) mcp)) [SKIP] (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp))) (\<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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) \<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. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?Q'496 mcp (UCAST(8 \<rightarrow> 32) mcp)) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 4. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' ?Q'496
 5. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>mcp. UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'662 mcp (UCAST(8 \<rightarrow> 32) mcp)) \<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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) {},UNIV
 2. \<And>mcp \<sigma>. UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> \<Gamma>\<turnstile> {s. ?Q496 mcp \<sigma> \<and> s \<in> ?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) \<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 (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 3. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<inter> ?R'662 mcp (UCAST(8 \<rightarrow> 32) mcp)) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 5. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. ?P'663 a b \<inter> ?R'662 a b)
 6. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>mcp \<sigma>. UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> \<Gamma>\<turnstile> {s. ?Q496 mcp \<sigma> \<and> s \<in> ?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<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>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) \<acute>current_syscall_error;;
\<acute>current_syscall_error :== rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) \<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 (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<inter> \<lbrace>True\<rbrace>) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 4. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. ?P'663 a b \<inter> \<lbrace>True\<rbrace>)
 5. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>mcp \<sigma>. UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> {s. ?Q496 mcp \<sigma> \<and> s \<in> ?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)) \<sigma>). (\<sigma>', globals_update (current_syscall_error_'_update (\<lambda>_. rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) (rangeErrorMin_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) (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> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. rangeErrorMax_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) mcp) (rangeErrorMin_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_MinPrio) (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. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<inter> \<lbrace>True\<rbrace>) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 4. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. ?P'663 a b \<inter> \<lbrace>True\<rbrace>)
 5. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp) \<inter> \<lbrace>True\<rbrace>) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 3. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. ?P'663 a b \<inter> \<lbrace>True\<rbrace>)
 4. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q496 mcp) (?P'663 mcp (UCAST(8 \<rightarrow> 32) mcp)) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>?Q496\<rbrace>
 3. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. ?P'663 a b \<inter> \<lbrace>True\<rbrace>)
 4. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>mcp s f. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> ret__unsigned_long_' (global_exn_var_'_update f (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rparr>)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE
 2. \<And>mcp s f. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 3. \<And>mcp. \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<Longrightarrow> wfhandlers [SKIP]
 4. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcp _. True\<rbrace>
 5. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 6. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R500 (tcb_ptr_to_ctcb_ptr auth) prio\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcp _. True\<rbrace>
 2. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 3. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R500 autha prioa) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. guard_is_UNIV (\<lambda>mcp rv'. rv' = UCAST(8 \<rightarrow> 32) mcp) mcp_' (\<lambda>a b. \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 2. \<And>autha prioa s s'. \<lbrakk>autha = tcb_ptr_to_ctcb_ptr auth; prioa = prio; (s, s') \<in> rf_sr; tcb_at' auth s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals!