theory Ipc_R

lemma setupCallerCap_corres:
  "corres dc
     (st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and
      st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and
      valid_objs and pspace_distinct and pspace_aligned and valid_mdb
      and valid_list and
      valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3))
     (tcb_at' sender and tcb_at' receiver and valid_pspace'
                and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
     (setup_caller_cap sender receiver grant)
     (setupCallerCap sender receiver grant)" supply if_split[split del] apply (simp add: setup_caller_cap_def setupCallerCap_def
                   getThreadReplySlot_def locateSlot_conv
                   getThreadCallerSlot_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split_nor) apply (rule setThreadState_corres) apply (simp split: option.split) apply (rule corres_symb_exec_r) apply (rule_tac F="\<exists>r. cteCap masterCTE = capability.ReplyCap sender True r
                             \<and> mdbNext (cteMDBNode masterCTE) = nullPointer"
                      in corres_gen_asm2, clarsimp simp add: isCap_simps) apply (rule corres_symb_exec_r) apply (rule_tac F="rv = capability.NullCap"
                         in corres_gen_asm2, simp) apply (rule cteInsert_corres) apply (simp split: if_splits) apply (simp add: cte_map_def tcbReplySlot_def
                              tcb_cnode_index_def cte_level_bits_def) apply (simp add: cte_map_def tcbCallerSlot_def
                             tcb_cnode_index_def cte_level_bits_def) apply (rule_tac R="\<lambda>rv. cte_at' (receiver + 2 ^ cte_level_bits * tcbCallerSlot)"
                    in hoare_post_add) apply (wp, (wp getSlotCap_wp)+) apply blast apply (rule no_fail_pre, wp) apply (clarsimp simp: cte_wp_at'_def cte_at'_def) apply (rule_tac R="\<lambda>rv. cte_at' (sender + 2 ^ cte_level_bits * tcbReplySlot)"
                     in hoare_post_add) apply (wp, (wp getCTE_wp')+) apply blast apply (rule no_fail_pre, wp) apply (clarsimp simp: cte_wp_at_ctes_of) apply (wp sts_valid_pspace_hangers
                 | simp add: cte_wp_at_ctes_of)+ apply (clarsimp simp: valid_tcb_state_def st_tcb_at_reply_cap_valid
                         st_tcb_at_tcb_at st_tcb_at_caller_cap_null
                  split: option.split) apply (clarsimp simp: valid_tcb_state'_def valid_cap'_def capAligned_reply_tcbI) apply (frule(1) st_tcb_at_reply_cap_valid, simp, clarsimp) apply (clarsimp simp: cte_wp_at_ctes_of cte_wp_at_caps_of_state) apply (drule pspace_relation_cte_wp_at[rotated, OF caps_of_state_cteD],
         erule valid_pspace'_splits, clarsimp+)+ apply (clarsimp simp: cte_wp_at_ctes_of cte_map_def tcbReplySlot_def
                        tcbCallerSlot_def tcb_cnode_index_def
                        is_cap_simps) apply (auto intro: reply_no_descendants_mdbNext_null[OF not_waiting_reply_slot_no_descendants]
               simp: cte_index_repair) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (setup_caller_cap sender receiver grant) (setupCallerCap sender receiver grant) proof (prove)
goal (1 subgoal):
 1. corres dc (st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (setup_caller_cap sender receiver grant) (setupCallerCap sender receiver grant) proof (prove)
goal (1 subgoal):
 1. corres dc (st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (do y <- set_thread_state sender Structures_A.thread_state.BlockedOnReply;
cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od) (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);
callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q1 ?Q'1 (do y <- set_thread_state sender Structures_A.thread_state.BlockedOnReply;
cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od) (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);
callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q'1 s' proof (prove)
goal (6 subgoals):
 1. corres dc ?P5 ?P'5 (set_thread_state sender Structures_A.thread_state.BlockedOnReply) (setThreadState Structures_H.thread_state.BlockedOnReply sender)
 2. corres dc ?R5 ?R'5 (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (do 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);
callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 3. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s' proof (prove)
goal (6 subgoals):
 1. thread_state_relation Structures_A.thread_state.BlockedOnReply Structures_H.thread_state.BlockedOnReply
 2. corres dc ?R5 ?R'5 (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (do 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);
callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 3. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 6. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (5 subgoals):
 1. corres dc ?R5 ?R'5 (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (do 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);
callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 4. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 5. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (8 subgoals):
 1. \<And>masterCTE. corres dc ?R5 (?Q'12 masterCTE) (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (do y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>?Q'12\<rbrace>
 3. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 5. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 7. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 8. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (8 subgoals):
 1. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> corres dc ?R5 (?P'17 masterCTE) (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (do callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 3. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 5. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 7. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 8. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (11 subgoals):
 1. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> corres dc ?R5 (?Q'22 masterCTE r rv) (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (do y <- assert (rv = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q'22 masterCTE r\<rbrace>
 3. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 5. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 6. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 8. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 9. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 10. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> corres dc ?R5 (?P'27 masterCTE r capability.NullCap) (cap_insert (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)) (cteInsert (capability.ReplyCap sender False grant) (sender + 2 ^ cte_level_bits * tcbReplySlot) (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 2. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rv. ?P'27 masterCTE r rv and (\<lambda>s. rv = capability.NullCap)\<rbrace>
 3. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 5. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 6. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 8. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. ?R5\<rbrace>
 9. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 10. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> cap_relation (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (capability.ReplyCap sender False grant)
 2. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> sender + 2 ^ cte_level_bits * tcbReplySlot = cte_map (sender, tcb_cnode_index 2)
 3. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> receiver + 2 ^ cte_level_bits * tcbCallerSlot = cte_map (receiver, tcb_cnode_index 3)
 4. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rv. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant) and cte_wp_at' (\<lambda>c. cteCap c = rv) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) and (\<lambda>s. rv = capability.NullCap)\<rbrace>
 5. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 7. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 8. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 10. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> sender + 2 ^ cte_level_bits * tcbReplySlot = cte_map (sender, tcb_cnode_index 2)
 2. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> receiver + 2 ^ cte_level_bits * tcbCallerSlot = cte_map (receiver, tcb_cnode_index 3)
 3. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rv. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant) and cte_wp_at' (\<lambda>c. cteCap c = rv) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) and (\<lambda>s. rv = capability.NullCap)\<rbrace>
 4. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 6. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 7. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 9. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 10. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>masterCTE r rv. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; rv = capability.NullCap\<rbrakk> \<Longrightarrow> receiver + 2 ^ cte_level_bits * tcbCallerSlot = cte_map (receiver, tcb_cnode_index 3)
 2. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rv. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant) and cte_wp_at' (\<lambda>c. cteCap c = rv) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) and (\<lambda>s. rv = capability.NullCap)\<rbrace>
 3. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 5. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 6. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 8. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 9. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 10. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rv. pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant) and cte_wp_at' (\<lambda>c. cteCap c = rv) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) and (\<lambda>s. rv = capability.NullCap)\<rbrace>
 2. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 4. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 5. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 7. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 8. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 9. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 10. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (10 subgoals):
 1. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 masterCTE\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant) and cte_wp_at' (\<lambda>c. cteCap c = r) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) and (\<lambda>s. r = capability.NullCap)) s\<rbrace>
 2. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; ?P'17 masterCTE s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (?P'17 masterCTE) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 4. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. ?P'17 masterCTE and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 5. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 7. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 8. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 9. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 10. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (9 subgoals):
 1. \<And>masterCTE r s sa. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap); s = sa\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) sa \<and> s = sa
 2. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 3. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. (\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 4. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 6. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 8. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 9. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (8 subgoals):
 1. \<And>masterCTE r. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) (getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot))
 2. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. (\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 3. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 5. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 7. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 8. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (8 subgoals):
 1. \<And>masterCTE r s. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; cteCap masterCTE = capability.ReplyCap sender True r; True; valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s
 2. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. (\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 3. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 5. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 7. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 8. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (7 subgoals):
 1. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE. (\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) and (\<lambda>s. \<exists>r. cteCap masterCTE = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode masterCTE) = nullPointer)\<rbrace>
 2. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 4. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 5. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 6. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 7. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (7 subgoals):
 1. \<lbrace>?R'5\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> ((\<lambda>s. valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) and (\<lambda>s. \<exists>ra. cteCap r = capability.ReplyCap sender True ra \<and> mdbNext (cteMDBNode r) = nullPointer)) s\<rbrace>
 2. \<And>s. ?R'5 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail ?R'5 (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 4. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 5. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x. ?R'5\<rbrace>
 6. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 7. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (6 subgoals):
 1. \<And>s sa. \<lbrakk>cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer)); s = sa\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) sa \<longrightarrow> s = sa
 2. True \<Longrightarrow> no_fail (\<lambda>s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))) (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 3. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 4. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))\<rbrace>
 5. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 6. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (5 subgoals):
 1. True \<Longrightarrow> no_fail (\<lambda>s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))) (getCTE (sender + 2 ^ cte_level_bits * tcbReplySlot))
 2. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))\<rbrace>
 4. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 5. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>True; cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s
 2. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))\<rbrace>
 4. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 5. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q5\<rbrace> set_thread_state sender Structures_A.thread_state.BlockedOnReply \<lbrace>\<lambda>x. valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K ((sender, tcb_cnode_index 2) \<noteq> (receiver, tcb_cnode_index 3)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) and (\<lambda>s. cte_wp_at (is_derived (cdt s) (sender, tcb_cnode_index 2) (cap.ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite}))) (sender, tcb_cnode_index 2) s)\<rbrace>
 2. \<lbrace>?Q'5\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (valid_objs' s \<and> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' (capability.ReplyCap sender False grant)) s \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> cap = capability.NullCap)) \<and> (\<forall>cte. cte_wp_at' ((=) cte) (sender + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r \<and> mdbNext (cteMDBNode cte) = nullPointer))\<rbrace>
 3. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q5) s
 4. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'5) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>st_tcb_at (Not \<circ> halted) sender s \<and> tcb_at receiver s \<and> st_tcb_at (Not \<circ> awaiting_reply) sender s \<and> valid_reply_caps s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_mdb s \<and> valid_list s \<and> valid_reply_masters s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) s; tcb_at' sender s' \<and> tcb_at' receiver s' \<and> valid_pspace' s' \<and> weak_sch_act_wf (ksSchedulerAction s') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at sender s \<and> valid_tcb_state Structures_A.thread_state.BlockedOnReply s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s) \<and> cte_wp_at (\<lambda>a. is_master_reply_cap a \<and> obj_ref_of a = sender) (sender, tcb_cnode_index 2) s
 2. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) 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 \<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 \<and> valid_cap' (capability.ReplyCap sender False grant) s \<and> (\<exists>cte. ctes_of s (receiver + 2 ^ cte_level_bits * tcbCallerSlot) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r) \<and> mdbNext (cteMDBNode cte) = nullPointer))) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(st_tcb_at (Not \<circ> halted) sender and tcb_at receiver and st_tcb_at (Not \<circ> awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and valid_reply_masters and cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) s; (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' sender and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) 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 \<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 \<and> valid_cap' (capability.ReplyCap sender False grant) s \<and> (\<exists>cte. ctes_of s (receiver + 2 ^ cte_level_bits * tcbCallerSlot) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r) \<and> mdbNext (cteMDBNode cte) = nullPointer))) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; st_tcb_at (Not \<circ> halted) sender s; tcb_at' sender s'; tcb_at receiver s; tcb_at' receiver s'; st_tcb_at (Not \<circ> awaiting_reply) sender s; valid_pspace' s'; weak_sch_act_wf (ksSchedulerAction s') s'; valid_reply_caps s; valid_objs s; pspace_distinct s; pspace_aligned s; valid_mdb s; valid_list s; valid_reply_masters s; cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s' \<and> (\<exists>cte. ctes_of s' (receiver + 2 ^ cte_level_bits * tcbCallerSlot) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s' (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r) \<and> mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; st_tcb_at (Not \<circ> halted) sender s; tcb_at' sender s'; tcb_at receiver s; tcb_at' receiver s'; st_tcb_at (Not \<circ> awaiting_reply) sender s; valid_pspace' s'; weak_sch_act_wf (ksSchedulerAction s') s'; valid_reply_caps s; valid_objs s; pspace_distinct s; pspace_aligned s; valid_mdb s; valid_list s; valid_reply_masters s; cte_wp_at (\<lambda>c. c = cap.NullCap) (receiver, tcb_cnode_index 3) s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sender) (sender, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (sender + 2 ^ cte_level_bits * tcbReplySlot) s' \<and> (\<exists>cte. ctes_of s' (receiver + 2 ^ cte_level_bits * tcbCallerSlot) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s' (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r) \<and> mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cap. \<lbrakk>(s, s') \<in> state_relation; st_tcb_at (Not \<circ> halted) (obj_ref_of cap) s; tcb_at' (obj_ref_of cap) s'; tcb_at receiver s; tcb_at' receiver s'; st_tcb_at (Not \<circ> awaiting_reply) (obj_ref_of cap) s; valid_pspace' s'; weak_sch_act_wf (ksSchedulerAction s') s'; valid_reply_caps s; valid_objs s; pspace_distinct s; pspace_aligned s; valid_mdb s; valid_list s; valid_reply_masters s; caps_of_state s (receiver, tcb_cnode_index 3) = Some cap.NullCap; caps_of_state s (obj_ref_of cap, tcb_cnode_index 2) = Some cap; is_master_reply_cap cap; sender = obj_ref_of cap\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s' (obj_ref_of cap + 2 ^ cte_level_bits * tcbReplySlot) = Some cte) \<and> (\<exists>cte. ctes_of s' (receiver + 2 ^ cte_level_bits * tcbCallerSlot) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s' (obj_ref_of cap + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap (obj_ref_of cap) True r) \<and> mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cap. \<lbrakk>(s, s') \<in> state_relation; st_tcb_at (Not \<circ> halted) (obj_ref_of cap) s; tcb_at' (obj_ref_of cap) s'; tcb_at receiver s; tcb_at' receiver s'; st_tcb_at (Not \<circ> awaiting_reply) (obj_ref_of cap) s; valid_pspace' s'; weak_sch_act_wf (ksSchedulerAction s') s'; valid_reply_caps s; valid_objs s; pspace_distinct s; pspace_aligned s; valid_mdb s; valid_list s; valid_reply_masters s; is_master_reply_cap cap; sender = obj_ref_of cap; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (receiver, tcb_cnode_index 3)) s'; cte_wp_at' (\<lambda>cte. cap_relation cap (cteCap cte)) (cte_map (obj_ref_of cap, tcb_cnode_index 2)) s'\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s' (obj_ref_of cap + 2 ^ cte_level_bits * tcbReplySlot) = Some cte) \<and> (\<exists>cte. ctes_of s' (receiver + 2 ^ cte_level_bits * tcbCallerSlot) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s' (obj_ref_of cap + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap (obj_ref_of cap) True r) \<and> mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte ctea R. \<lbrakk>(s, s') \<in> state_relation; st_tcb_at (Not \<circ> halted) sender s; tcb_at' sender s'; tcb_at receiver s; tcb_at' receiver s'; st_tcb_at (Not \<circ> awaiting_reply) sender s; valid_pspace' s'; weak_sch_act_wf (ksSchedulerAction s') s'; valid_reply_caps s; valid_objs s; pspace_distinct s; pspace_aligned s; valid_mdb s; valid_list s; valid_reply_masters s; ctes_of s' (receiver + 3 * 2 ^ cte_level_bits) = Some cte; cteCap cte = capability.NullCap; ctes_of s' (sender + 2 * 2 ^ cte_level_bits) = Some ctea; cteCap ctea = capability.ReplyCap sender True (AllowGrant \<in> R)\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s' (sender + 2 ^ cte_level_bits * 2) = Some cte) \<and> (\<exists>cte. ctes_of s' (receiver + 2 ^ cte_level_bits * 3) = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<forall>cte. ctes_of s' (sender + 2 ^ cte_level_bits * 2) = Some cte \<longrightarrow> (\<exists>r. cteCap cte = capability.ReplyCap sender True r) \<and> mdbNext (cteMDBNode cte) = nullPointer) proof (prove)
goal:
No subgoals!