theory Tcb_R

lemma checkPrio_corres:
  "corres (ser \<oplus> dc) (tcb_at auth) (tcb_at' auth)
     (check_prio p auth) (checkPrio p auth)" apply (simp add: check_prio_def checkPrio_def) apply (rule corres_guard_imp) apply (simp add: liftE_bindE) apply (rule corres_split[OF threadGet_corres[where r="(=)"]]) apply (clarsimp simp: tcb_relation_def) apply (rule_tac rvr = dc and
                        R = \<top> and
                       R' = \<top> in
               whenE_throwError_corres'[where m="returnOk ()" and m'="returnOk ()", simplified]) apply (simp add: minPriority_def) apply (clarsimp simp: minPriority_def) apply (rule corres_returnOkTT) apply (simp add: minPriority_def) apply (wp gct_wp)+ apply (simp add: cur_tcb_def cur_tcb'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> dc) (tcb_at auth) (tcb_at' auth) (check_prio p auth) (checkPrio p auth) proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> dc) (tcb_at auth) (tcb_at' auth) (doE mcp <- liftE (thread_get tcb_mcpriority auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)))
odE) (doE mcp <- liftE (threadGet tcbMCP auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))
odE) proof (prove)
goal (3 subgoals):
 1. corres (ser \<oplus> dc) ?Q ?Q' (doE mcp <- liftE (thread_get tcb_mcpriority auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)))
odE) (doE mcp <- liftE (threadGet tcbMCP auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))
odE)
 2. \<And>s. tcb_at auth s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' auth s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres (ser \<oplus> dc) ?Q ?Q' (do mcp <- thread_get tcb_mcpriority auth;
whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)))
od) (do mcp <- threadGet tcbMCP auth;
whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))
od)
 2. \<And>s. tcb_at auth s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' auth s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_mcpriority tcb = tcbMCP tcb'
 2. \<And>mcp mcpa. mcp = mcpa \<Longrightarrow> corres (ser \<oplus> dc) (?R4 mcp) (?R'4 mcpa) (whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)))) (whenE (UCAST(8 \<rightarrow> 32) mcpa < p) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcpa))))
 3. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>?R'4\<rbrace>
 5. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 6. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>mcp mcpa. mcp = mcpa \<Longrightarrow> corres (ser \<oplus> dc) (?R4 mcp) (?R'4 mcpa) (whenE (UCAST(8 \<rightarrow> 32) mcp < p) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)))) (whenE (UCAST(8 \<rightarrow> 32) mcpa < p) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcpa))))
 2. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>?R'4\<rbrace>
 4. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 5. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>mcp mcpa. mcp = mcpa \<Longrightarrow> ser (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(8 \<rightarrow> 32) mcp)) (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcpa))
 2. \<And>mcp mcpa s s'. \<lbrakk>mcp = mcpa; (s, s') \<in> state_relation; True; True\<rbrakk> \<Longrightarrow> (UCAST(8 \<rightarrow> 32) mcp < p) = (UCAST(8 \<rightarrow> 32) mcpa < p)
 3. \<And>mcp mcpa. \<lbrakk>mcp = mcpa; \<not> UCAST(8 \<rightarrow> 32) mcp < p\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?Q13 mcp) (?Q'14 mcpa) (returnOk ()) (returnOk ())
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>\<lambda>mcp. (\<lambda>_. True) and ?Q13 mcp\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcpa. (\<lambda>_. True) and ?Q'14 mcpa\<rbrace>
 6. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 7. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>mcp mcpa s s'. \<lbrakk>mcp = mcpa; (s, s') \<in> state_relation; True; True\<rbrakk> \<Longrightarrow> (UCAST(8 \<rightarrow> 32) mcp < p) = (UCAST(8 \<rightarrow> 32) mcpa < p)
 2. \<And>mcp mcpa. \<lbrakk>mcp = mcpa; \<not> UCAST(8 \<rightarrow> 32) mcp < p\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?Q13 mcp) (?Q'14 mcpa) (returnOk ()) (returnOk ())
 3. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>\<lambda>mcp. (\<lambda>_. True) and ?Q13 mcp\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcpa. (\<lambda>_. True) and ?Q'14 mcpa\<rbrace>
 5. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 6. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>mcp mcpa. \<lbrakk>mcp = mcpa; \<not> UCAST(8 \<rightarrow> 32) mcp < p\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?Q13 mcp) (?Q'14 mcpa) (returnOk ()) (returnOk ())
 2. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>\<lambda>mcp. (\<lambda>_. True) and ?Q13 mcp\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcpa. (\<lambda>_. True) and ?Q'14 mcpa\<rbrace>
 4. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 5. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>mcp mcpa. \<lbrakk>mcp = mcpa; \<not> UCAST(8 \<rightarrow> 32) mcp < p\<rbrakk> \<Longrightarrow> dc () ()
 2. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>\<lambda>mcp. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcpa. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 5. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> thread_get tcb_mcpriority auth \<lbrace>\<lambda>mcp. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> threadGet tcbMCP auth \<lbrace>\<lambda>mcpa. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ?Q4) s
 4. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at auth s \<Longrightarrow> (tcb_at auth and ((\<lambda>_. True) and (\<lambda>_. True))) s
 2. \<And>s. tcb_at' auth s \<Longrightarrow> (tcb_at' auth and ((\<lambda>_. True) and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!