theory Tcb_C

lemma invokeTCB_NotificationControl_bind_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
    (invs' and tcb_inv_wf' (tcbinvocation.NotificationControl t (Some a)))
    (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. ntfnPtr_' s = ntfn_Ptr a}) []
    (invokeTCB (tcbinvocation.NotificationControl t (Some a)))
    (Call invokeTCB_NotificationControl_'proc)" apply (cinit lift: tcb_' ntfnPtr_') apply (clarsimp simp: option_to_0_def liftE_def) apply (rule ccorres_cond_true_seq) apply (ctac(no_vcg) add: bindNotification_ccorres) apply (rule ccorres_return_CE[unfolded returnOk_def, simplified]) apply simp apply simp apply simp apply wp apply (case_tac "a = 0", auto) 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 (Some a))) (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr a\<rbrace>) [] (invokeTCB (tcbinvocation.NotificationControl t (Some a))) (Call invokeTCB_NotificationControl_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr tcb. \<lbrakk>ntfnPtr = ntfn_Ptr a; 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 <- bindNotification t a;
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 = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) 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 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)) (?Q'161 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)) [SKIP] (do y <- bindNotification t a;
return (Inr [])
od) (Cond (if a \<noteq> 0 then UNIV else {}) (CALL bindNotification_'proc(tcb_ptr_to_ctcb_ptr t,ntfn_Ptr a)) (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 = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) 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 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)) (?R'173 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)) [SKIP] (do y <- bindNotification t a;
return (Inr [])
od) (CALL bindNotification_'proc(tcb_ptr_to_ctcb_ptr t,ntfn_Ptr a);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q161 ntfnPtr tcb s \<and> s' \<in> ?R'173 ntfnPtr tcb \<inter> (if a \<noteq> 0 then UNIV else {}) 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_') (?Q177 rv) (?Q'177 rv xfdc) [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R186 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)\<rbrace> bindNotification t a \<lbrace>?Q177\<rbrace>
 3. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and ?R186 ntfnPtr tcb) s \<and> s' \<in> {s. ntfnPtr_'_update (\<lambda>_. ntfnPtr) (tcb_'_update (\<lambda>_. tcb) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfnPtr\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'183 ntfnPtr tcb t rv} \<inter> (if a \<noteq> 0 then UNIV else {})
flex-flex pairs:
?Q'183 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t) \<equiv>\<^sup>? \<lambda>t rv. ?Q'177 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>?R186 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)\<rbrace> bindNotification t a \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and ?R186 ntfnPtr tcb) s \<and> s' \<in> {s. ntfnPtr_'_update (\<lambda>_. ntfnPtr) (tcb_'_update (\<lambda>_. tcb) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfnPtr\<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>} \<inter> (if a \<noteq> 0 then UNIV else {}) 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>?R186 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)\<rbrace> bindNotification t a \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and ?R186 ntfnPtr tcb) s \<and> s' \<in> {s. ntfnPtr_'_update (\<lambda>_. ntfnPtr) (tcb_'_update (\<lambda>_. tcb) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfnPtr\<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>} \<inter> (if a \<noteq> 0 then UNIV else {}) proof (prove)
goal (3 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> wfhandlers [SKIP]
 2. \<lbrace>?R186 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)\<rbrace> bindNotification t a \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and ?R186 ntfnPtr tcb) s \<and> s' \<in> {s. ntfnPtr_'_update (\<lambda>_. ntfnPtr) (tcb_'_update (\<lambda>_. tcb) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfnPtr\<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>} \<inter> (if a \<noteq> 0 then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R186 (ntfn_Ptr a) (tcb_ptr_to_ctcb_ptr t)\<rbrace> bindNotification t a \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and ?R186 ntfnPtr tcb) s \<and> s' \<in> {s. ntfnPtr_'_update (\<lambda>_. ntfnPtr) (tcb_'_update (\<lambda>_. tcb) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfnPtr\<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>} \<inter> (if a \<noteq> 0 then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr tcb s s'. \<lbrakk>ntfnPtr = ntfn_Ptr a; tcb = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and (tcb_at' t and ex_nonz_cap_to' t and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) t))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and (\<lambda>a. True)) s \<and> s' \<in> {s. ntfnPtr_'_update (\<lambda>_. ntfnPtr) (tcb_'_update (\<lambda>_. tcb) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfnPtr\<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>} \<inter> (if a \<noteq> 0 then UNIV else {}) proof (prove)
goal:
No subgoals!