theory Ipc_R

lemma setupCallerCap_urz[wp]:
  "\<lbrace>untyped_ranges_zero' and valid_pspace' and tcb_at' sender\<rbrace>
    setupCallerCap sender t g \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: setupCallerCap_def getSlotCap_def
                   getThreadCallerSlot_def getThreadReplySlot_def
                   locateSlot_conv) apply (wp getCTE_wp') apply (rule_tac Q="\<lambda>_. untyped_ranges_zero' and valid_mdb' and valid_objs'" in hoare_post_imp) apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def untyped_derived_eq_def
                         isCap_simps) apply (wp sts_valid_pspace_hangers) apply (clarsimp simp: valid_tcb_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_pspace' and tcb_at' sender\<rbrace> setupCallerCap sender t g \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_pspace' and tcb_at' sender\<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 (t + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap sender False g) (sender + 2 ^ cte_level_bits * tcbReplySlot) (t + 2 ^ cte_level_bits * tcbCallerSlot)
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>y s. \<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> (untyped_ranges_zero' and (\<lambda>s. sender + 2 ^ cte_level_bits * tcbReplySlot \<noteq> t + 2 ^ cte_level_bits * tcbCallerSlot) and valid_mdb' and valid_objs' and cte_wp_at' (untyped_derived_eq (capability.ReplyCap sender False g) \<circ> cteCap) (sender + 2 ^ cte_level_bits * tcbReplySlot)) s)\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and valid_pspace' and tcb_at' sender) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (untyped_ranges_zero' and valid_mdb' and valid_objs') s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> (untyped_ranges_zero' and (\<lambda>s. sender + 2 ^ cte_level_bits * tcbReplySlot \<noteq> t + 2 ^ cte_level_bits * tcbCallerSlot) and valid_mdb' and valid_objs' and cte_wp_at' (untyped_derived_eq (capability.ReplyCap sender False g) \<circ> cteCap) (sender + 2 ^ cte_level_bits * tcbReplySlot)) s)
 2. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>_. untyped_ranges_zero' and valid_mdb' and valid_objs'\<rbrace>
 3. \<And>s. (untyped_ranges_zero' and valid_pspace' and tcb_at' sender) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>_. untyped_ranges_zero' and valid_mdb' and valid_objs'\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and valid_pspace' and tcb_at' sender) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (untyped_ranges_zero' and valid_pspace' and tcb_at' sender) s \<Longrightarrow> untyped_ranges_zero' s \<and> (valid_pspace' and tcb_at' sender and valid_tcb_state' Structures_H.thread_state.BlockedOnReply) s \<and> (valid_pspace' and tcb_at' sender and valid_tcb_state' Structures_H.thread_state.BlockedOnReply) s proof (prove)
goal:
No subgoals!