theory Syscall_C

lemma performInvocation_Reply_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple
             and ((Not o real_cte_at' slot) or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot)
             and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte))
                 slot and (\<lambda>s. ksCurThread s = sender))
       (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr receiver}
             \<inter> {s. slot_' s = cte_Ptr slot}
             \<inter> {s. canGrant_' s = from_bool grant}) []
     (liftE (doReplyTransfer sender receiver slot grant))
     (Call performInvocation_Reply_'proc)" apply cinit apply (ctac add: doReplyTransfer_ccorres) apply (simp add: return_returnOk) apply (rule ccorres_return_CE, simp+)[1] apply wp apply simp apply (vcg exspec=doReplyTransfer_modifies) apply (simp add: rf_sr_ksCurThread) apply (auto simp: isReply_def elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>) [] (liftE (doReplyTransfer sender receiver slot grant)) (Call performInvocation_Reply_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q10 ?Q'10 [SKIP] (do r <- doReplyTransfer sender receiver slot grant;
return (Inr ())
od) (CALL doReplyTransfer_'proc(\<acute>ksCurThread,\<acute>thread,\<acute>slot,\<acute>canGrant);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> ?Q10 s \<and> s' \<in> ?Q'10 proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q18 rv) (?Q'18 rv xfdc) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R18\<rbrace> doReplyTransfer sender receiver slot grant \<lbrace>?Q18\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL doReplyTransfer_'proc(\<acute>ksCurThread,\<acute>thread,\<acute>slot,\<acute>canGrant) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'18 rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' (Not \<circ> isReply) sender and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and ?R18) s \<and> s' \<in> {s. grant_'_update (\<lambda>_. canGrant_' s) (slot_'_update (\<lambda>_. slot_' s) (receiver_'_update (\<lambda>_. thread_' s) (sender_'_update (\<lambda>_. ksCurThread_' (globals s)) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>grant = from_bool grant\<rbrace>} \<inter> ?R'18 proof (prove)
goal (4 subgoals):
 1. \<And>xfdc. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q18 ()) (?Q'18 () xfdc) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R18\<rbrace> doReplyTransfer sender receiver slot grant \<lbrace>?Q18\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL doReplyTransfer_'proc(\<acute>ksCurThread,\<acute>thread,\<acute>slot,\<acute>canGrant) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'18 rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' (Not \<circ> isReply) sender and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and ?R18) s \<and> s' \<in> {s. grant_'_update (\<lambda>_. canGrant_' s) (slot_'_update (\<lambda>_. slot_' s) (receiver_'_update (\<lambda>_. thread_' s) (sender_'_update (\<lambda>_. ksCurThread_' (globals s)) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>grant = from_bool grant\<rbrace>} \<inter> ?R'18 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R18\<rbrace> doReplyTransfer sender receiver slot grant \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL doReplyTransfer_'proc(\<acute>ksCurThread,\<acute>thread,\<acute>slot,\<acute>canGrant) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc rv (K rv (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' (Not \<circ> isReply) sender and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and ?R18) s \<and> s' \<in> {s. grant_'_update (\<lambda>_. canGrant_' s) (slot_'_update (\<lambda>_. slot_' s) (receiver_'_update (\<lambda>_. thread_' s) (sender_'_update (\<lambda>_. ksCurThread_' (globals s)) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>grant = from_bool grant\<rbrace>} \<inter> ?R'18 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL doReplyTransfer_'proc(\<acute>ksCurThread,\<acute>thread,\<acute>slot,\<acute>canGrant) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc rv (K rv (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' (Not \<circ> isReply) sender and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. True)) s \<and> s' \<in> {s. grant_'_update (\<lambda>_. canGrant_' s) (slot_'_update (\<lambda>_. slot_' s) (receiver_'_update (\<lambda>_. thread_' s) (sender_'_update (\<lambda>_. ksCurThread_' (globals s)) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>grant = from_bool grant\<rbrace>} \<inter> ?R'18 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'18 CALL doReplyTransfer_'proc(\<acute>ksCurThread,\<acute>thread,\<acute>canGrant) UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' (Not \<circ> isReply) sender and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. True)) s \<and> s' \<in> {s. grant_'_update (\<lambda>_. canGrant_' s) (slot_'_update (\<lambda>_. slot_' s) (receiver_'_update (\<lambda>_. thread_' s) (sender_'_update (\<lambda>_. ksCurThread_' (globals s)) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>grant = from_bool grant\<rbrace>} \<inter> ?R'18 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. ksCurThread s = sender)) s; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>canGrant = from_bool grant\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' (Not \<circ> isReply) sender and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and (Not \<circ> real_cte_at' slot or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot and (\<lambda>s. True)) s \<and> s' \<in> {s. grant_'_update (\<lambda>_. canGrant_' s) (slot_'_update (\<lambda>_. slot_' s) (receiver_'_update (\<lambda>_. thread_' s) (sender_'_update (\<lambda>_. ksCurThread_' (globals s)) s))) \<in> UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>grant = from_bool grant\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s \<and> st_tcb_at' active' sender s \<and> sch_act_simple s \<and> (real_cte_at' slot s \<longrightarrow> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot s \<and> ksCurThread s = sender; thread_' s' = tcb_ptr_to_ctcb_ptr receiver \<and> slot_' s' = cte_Ptr slot \<and> canGrant_' s' = from_bool grant\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> isReply) sender s \<and> ksCurDomain s \<le> maxDomain proof (prove)
goal:
No subgoals!