theory Ipc_R

lemma setupCallerCap_vp[wp]:
  "\<lbrace>valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace>
   setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (simp add: valid_pspace'_def setupCallerCap_def getThreadCallerSlot_def
                   getThreadReplySlot_def locateSlot_conv getSlotCap_def) apply (wp getCTE_wp) apply (rule_tac Q="\<lambda>_. valid_pspace' and
                         tcb_at' sender and tcb_at' rcvr"
                  in hoare_post_imp) apply (clarsimp simp: valid_cap'_def o_def cte_wp_at_ctes_of isCap_simps
                         valid_pspace'_def) apply (frule(1) ctes_of_valid', simp add: valid_cap'_def capAligned_def) apply clarsimp apply (wp | simp add: valid_pspace'_def valid_tcb_state'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace> setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' sender and tcb_at' rcvr\<rbrace> do y <- setThreadState Structures_H.thread_state.BlockedOnReply sender;
masterCTE <- getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot);
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
cte <- getCTE (rcvr + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot)
od \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>y s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (cteCap cte = capability.NullCap \<longrightarrow> (valid_objs' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. sender + 2 ^ cte_level_bits * tcbReplySlot \<noteq> rcvr + 2 ^ cte_level_bits * tcbCallerSlot) and K (capAligned (capability.ReplyCap sender False grant)) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) (sender + 2 ^ cte_level_bits * tcbReplySlot) (capability.ReplyCap sender False grant) \<circ> cteCap) (sender + 2 ^ cte_level_bits * tcbReplySlot) s)) s))))\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' sender and tcb_at' rcvr) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (valid_pspace' and tcb_at' sender and tcb_at' rcvr) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (cteCap cte = capability.NullCap \<longrightarrow> (valid_objs' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. sender + 2 ^ cte_level_bits * tcbReplySlot \<noteq> rcvr + 2 ^ cte_level_bits * tcbCallerSlot) and K (capAligned (capability.ReplyCap sender False grant)) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) (sender + 2 ^ cte_level_bits * tcbReplySlot) (capability.ReplyCap sender False grant) \<circ> cteCap) (sender + 2 ^ cte_level_bits * tcbReplySlot) s)) s))))
 2. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>_. valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace>
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' sender and tcb_at' rcvr) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>s cte v1 v2 ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcb_at' sender s; tcb_at' rcvr s; ctes_of s (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; cteCap cte = capability.ReplyCap sender True v2; v1; mdbNext (cteMDBNode cte) = nullPointer; ctes_of s (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> capAligned (capability.ReplyCap sender False grant) \<and> sender + 2 ^ cte_level_bits * tcbReplySlot \<noteq> rcvr + 2 ^ cte_level_bits * tcbCallerSlot \<and> capAligned (capability.ReplyCap sender False grant)
 2. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>_. valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace>
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' sender and tcb_at' rcvr) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>s cte v1 v2 ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcb_at' sender s; tcb_at' rcvr s; ctes_of s (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; cteCap cte = capability.ReplyCap sender True v2; v1; mdbNext (cteMDBNode cte) = nullPointer; ctes_of s (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) = Some ctea; cteCap ctea = capability.NullCap; is_aligned sender (objBits undefined) \<and> objBits undefined < word_bits\<rbrakk> \<Longrightarrow> sender + 2 ^ cte_level_bits * tcbReplySlot \<noteq> rcvr + 2 ^ cte_level_bits * tcbCallerSlot
 2. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>_. valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace>
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' sender and tcb_at' rcvr) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>_. valid_pspace' and tcb_at' sender and tcb_at' rcvr\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' sender and tcb_at' rcvr) s \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!