theory Tcb_C

lemma invokeTCB_NotificationControl_unbind_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
    (invs' and tcb_inv_wf' (tcbinvocation.NotificationControl t None))
    (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. ntfnPtr_' s = NULL}) []
    (invokeTCB (tcbinvocation.NotificationControl t None))
    (Call invokeTCB_NotificationControl_'proc)" apply (cinit lift: tcb_' ntfnPtr_') apply (clarsimp simp add: option_to_0_def liftE_def) apply (ctac(no_vcg) add: unbindNotification_ccorres) apply (rule ccorres_return_CE[unfolded returnOk_def, simplified]) apply simp apply simp apply simp apply wp apply (clarsimp simp: option_to_0_def) 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_inv_wf' (tcbinvocation.NotificationControl t None)) (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>) [] (invokeTCB (tcbinvocation.NotificationControl t None)) (Call invokeTCB_NotificationControl_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr tcb. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q161 ntfnPtr tcb) (?Q'161 ntfnPtr tcb) [SKIP] (liftE (do y <- unbindNotification t;
return []
od)) (IF ntfnPtr \<noteq> NULL THEN
  CALL bindNotification_'proc(tcb,ntfnPtr)
ELSE
  CALL unbindNotification_'proc(tcb)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q161 ntfnPtr tcb s \<and> s' \<in> ?Q'161 ntfnPtr tcb proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q161 NULL (tcb_ptr_to_ctcb_ptr t)) (?Q'161 NULL (tcb_ptr_to_ctcb_ptr t)) [SKIP] (do y <- unbindNotification t;
return (Inr [])
od) (CALL unbindNotification_'proc(tcb_ptr_to_ctcb_ptr t);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q161 ntfnPtr tcb s \<and> s' \<in> ?Q'161 ntfnPtr tcb 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_') (?Q179 rv) (?Q'179 rv xfdc) [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R188 NULL (tcb_ptr_to_ctcb_ptr t)\<rbrace> unbindNotification t \<lbrace>?Q179\<rbrace>
 3. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R188 ntfnPtr tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'185 ntfnPtr tcb t rv}
flex-flex pairs:
?Q'185 NULL (tcb_ptr_to_ctcb_ptr t) \<equiv>\<^sup>? \<lambda>t rv. ?Q'179 rv (xfdc t) proof (prove)
goal (5 subgoals):
 1. \<And>rv xfdc s f. dc rv xfdc \<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>rv xfdc s f. dc rv xfdc \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 3. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> wfhandlers [SKIP]
 4. \<lbrace>?R188 NULL (tcb_ptr_to_ctcb_ptr t)\<rbrace> unbindNotification t \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R188 ntfnPtr tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<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 (4 subgoals):
 1. \<And>rv xfdc s f. dc rv xfdc \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 2. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> wfhandlers [SKIP]
 3. \<lbrace>?R188 NULL (tcb_ptr_to_ctcb_ptr t)\<rbrace> unbindNotification t \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R188 ntfnPtr tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<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 (3 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> wfhandlers [SKIP]
 2. \<lbrace>?R188 NULL (tcb_ptr_to_ctcb_ptr t)\<rbrace> unbindNotification t \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R188 ntfnPtr tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<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 (2 subgoals):
 1. \<lbrace>?R188 NULL (tcb_ptr_to_ctcb_ptr t)\<rbrace> unbindNotification t \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R188 ntfnPtr tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<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>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = NULL; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>a. True)) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<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!