theory Tcb_C

lemma invokeTCB_Suspend_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
     (invs' and sch_act_simple and tcb_at' t and ex_nonz_cap_to' t)
     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) []
   (invokeTCB (Suspend t)) (Call invokeTCB_Suspend_'proc)" apply (cinit lift: thread_') apply (simp add: liftE_def return_returnOk) apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres]) apply (rule ccorres_return_CE, simp+)[1] apply wp apply clarsimp apply (auto simp: invs'_def valid_state'_def global'_no_ex_cap) 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 sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>) [] (invokeTCB (tcbinvocation.Suspend t)) (Call invokeTCB_Suspend_'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.suspend t;
return []
od)) (CALL suspend_'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 sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) 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.suspend t;
returnOk []
od) (CALL suspend_'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 sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) 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.suspend t \<lbrace>?Q67\<rbrace>
 3. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s) 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.suspend 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 sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s) 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 sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s) 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 (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; sch_act_simple s; tcb_at' (ksIdleThread s) s; ex_nonz_cap_to' (ksIdleThread s) s; t = ksIdleThread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!