theory Tcb_C

lemma invokeTCB_Resume_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
     (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple)
     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) []
   (invokeTCB (Resume t)) (Call invokeTCB_Resume_'proc)" apply (cinit lift: thread_') apply (simp add: liftE_def return_returnOk) apply (ctac(no_vcg) add: restart_ccorres) apply (rule ccorres_return_CE, simp+)[1] apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>) [] (invokeTCB (tcbinvocation.Resume t)) (Call invokeTCB_Resume_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q53 thread) (?Q'53 thread) [SKIP] (liftE (do y <- ThreadDecls_H.restart t;
return []
od)) (CALL restart_'proc(thread);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q53 thread s \<and> s' \<in> ?Q'53 thread proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q53 (tcb_ptr_to_ctcb_ptr t)) (?Q'53 (tcb_ptr_to_ctcb_ptr t)) [SKIP] (do y <- ThreadDecls_H.restart t;
returnOk []
od) (CALL restart_'proc(tcb_ptr_to_ctcb_ptr t);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q53 thread s \<and> s' \<in> ?Q'53 thread proof (prove)
goal (3 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q67 rv) (?Q'67 rv xfdc) [SKIP] (returnOk []) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R76 (tcb_ptr_to_ctcb_ptr t)\<rbrace> ThreadDecls_H.restart t \<lbrace>?Q67\<rbrace>
 3. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and sch_act_simple and ?R76 thread) s \<and> s' \<in> {s. target_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>target = thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'73 thread t rv}
flex-flex pairs:
?Q'73 (tcb_ptr_to_ctcb_ptr t) \<equiv>\<^sup>? \<lambda>t rv. ?Q'67 rv (xfdc t) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R76 (tcb_ptr_to_ctcb_ptr t)\<rbrace> ThreadDecls_H.restart t \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and sch_act_simple and ?R76 thread) s \<and> s' \<in> {s. target_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>target = thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> [] = []\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and sch_act_simple and (\<lambda>a. True)) s \<and> s' \<in> {s. target_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>target = thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> [] = []\<rbrace>} proof (prove)
goal:
No subgoals!