theory Ipc_C

lemma setupCallerCap_ccorres [corres]:
  "ccorres dc xfdc (valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p)))
                    and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender
                    and tcb_at' sender and tcb_at' receiver
                    and tcb_at' sender and tcb_at' receiver)
        (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>canGrant = from_bool canGrant\<rbrace>) hs
        (setupCallerCap sender receiver canGrant)
        (Call setupCallerCap_'proc)" apply (rule ccorres_gen_asm_state, rule ccorres_gen_asm_state) apply (frule_tac p=sender in is_aligned_tcb_ptr_to_ctcb_ptr) apply (cinit lift: sender_' receiver_' canGrant_') apply (clarsimp simp: word_sle_def
                         tcb_cnode_index_defs[THEN ptr_add_assertion_positive[OF ptr_add_assertion_positive_helper]]) apply ccorres_remove_UNIV_guard apply (ctac(no_vcg)) apply (rule ccorres_move_array_assertion_tcb_ctes) apply (simp only: getThreadReplySlot_def getThreadCallerSlot_def) apply (ctac(no_vcg)) apply (rename_tac replySlot replySlot') apply (simp del: Collect_const) apply (rule ccorres_getCTE_cte_at) apply (rule ccorres_move_c_guard_cte) apply (ctac(no_vcg) add:  getSlotCap_h_val_ccorres[unfolded getSlotCap_def fun_app_def,
                                                         folded liftM_def, simplified ccorres_liftM_simp]) apply (rule ccorres_assert2)+ apply (simp add: ccorres_seq_skip locateSlot_conv
                         ) apply (rule ccorres_move_array_assertion_tcb_ctes) apply csymbr apply (rule ccorres_getSlotCap_cte_at) apply (rule ccorres_move_c_guard_cte) apply (ctac(no_vcg)) apply (rule ccorres_assert) apply (simp only: ccorres_seq_skip) apply csymbr apply (ctac add: cteInsert_ccorres) apply simp apply (wp getSlotCap_cte_wp_at) apply (clarsimp simp: ccap_relation_def cap_lift_reply_cap
                             cap_to_H_simps cap_reply_cap_lift_def
                             tcbSlots Kernel_C.tcbCaller_def
                             size_of_def cte_level_bits_def ctcb_size_bits_def) apply (simp add: is_aligned_neg_mask) apply (wp getCTE_wp') apply (simp add: tcbSlots Kernel_C.tcbCaller_def
                       size_of_def cte_level_bits_def
                       ptr_add_assertion_positive Collect_const_mem
                       tcb_cnode_index_defs) apply simp apply (rule_tac Q="\<lambda>rv. valid_pspace' and tcb_at' receiver" in hoare_post_imp) apply (auto simp: cte_wp_at_ctes_of isCap_simps
                        tcbSlots Kernel_C.tcbCaller_def size_of_def
                        cte_level_bits_def)[1] apply (case_tac cte,clarsimp) apply (drule ctes_of_valid_cap') apply fastforce apply (simp add:valid_cap'_def capAligned_def) apply (simp add: locateSlot_conv) apply wp apply (clarsimp simp: ccap_rights_relation_def allRights_def
                          mask_def cap_rights_to_H_def tcbCallerSlot_def
                          Kernel_C.tcbCaller_def) apply simp apply wp apply (clarsimp simp: Kernel_C.ThreadState_BlockedOnReply_def mask_def
                        valid_pspace'_def tcbReplySlot_def
                        valid_tcb_state'_def Collect_const_mem
                        tcb_cnode_index_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver and tcb_at' sender and tcb_at' receiver) (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>canGrant = from_bool canGrant\<rbrace>) hs (setupCallerCap sender receiver canGrant) (Call setupCallerCap_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) (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>canGrant = from_bool canGrant\<rbrace>) hs (setupCallerCap sender receiver canGrant) (Call setupCallerCap_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) (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>canGrant = from_bool canGrant\<rbrace>) hs (setupCallerCap sender receiver canGrant) (Call setupCallerCap_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>s sa canGranta receivera sendera. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1196 s sa canGranta receivera sendera) (?Q'1196 s sa canGranta receivera sendera) (SKIP # hs) (do y <- setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (CALL setThreadState_'proc(sendera,SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply);;
(Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val sendera && 0xFFFFFE00)) (sint Kernel_C.tcbReply) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>replySlot :== cte_Ptr ((ptr_val sendera && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot_' s} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val receivera && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr ((ptr_val receivera && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(UCAST(32 \<rightarrow> 32) canGranta,SCAST(32 signed \<rightarrow> 32) false,UCAST(32 \<rightarrow> 32) (ptr_val sendera));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,\<acute>replySlot,\<acute>callerSlot)))))))
 2. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1196 s sa canGranta receivera sendera sb \<and> s' \<in> ?Q'1196 s sa canGranta receivera sendera proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1196 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (?Q'1196 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (SKIP # hs) (do y <- setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply);;
(Guard MemorySafety \<lbrace>Kernel_C.tcbReply = 0 \<or> array_assertion (cte_Ptr sender) (nat (sint Kernel_C.tcbReply)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>replySlot :== cte_Ptr (sender + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot_' s} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,\<acute>replySlot,\<acute>callerSlot)))))))
 2. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1196 s sa canGranta receivera sendera sb \<and> s' \<in> ?Q'1196 s sa canGranta receivera sendera proof (prove)
goal (2 subgoals):
 1. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1196 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (?G'1208 s sa rv') (SKIP # hs) (do y <- setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply);;
(Guard MemorySafety \<lbrace>Kernel_C.tcbReply = 0 \<or> array_assertion (cte_Ptr sender) (nat (sint Kernel_C.tcbReply)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>replySlot :== cte_Ptr (sender + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot_' s} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,\<acute>replySlot,\<acute>callerSlot)))))))
 2. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1196 s sa canGranta receivera sendera sb \<and> s' \<in> {sb. sb \<in> ?G'1211 s sa canGranta receivera sendera}
flex-flex pairs:
\<lambda>s sa. ?G'1211 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) \<equiv>\<^sup>? \<lambda>s sa. ?G'1208 s sa () proof (prove)
goal (3 subgoals):
 1. \<And>s sa rv' rv xfdca. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1266 s sa rv' rv) (?Q'1266 s sa rv' rv xfdca) (SKIP # hs) (do replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (Guard MemorySafety \<lbrace>Kernel_C.tcbReply = 0 \<or> array_assertion (cte_Ptr sender) (nat (sint Kernel_C.tcbReply)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>replySlot :== cte_Ptr (sender + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot_' s} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,\<acute>replySlot,\<acute>callerSlot))))))
 2. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>?Q1266 s sa rv'\<rbrace>
 3. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {sb. sb \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'1276 s sa canGranta receivera sendera t rv}}
flex-flex pairs:
\<lambda>s sa. ?Q'1276 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) \<equiv>\<^sup>? \<lambda>s sa t rv. ?Q'1266 s sa () rv (xfdc t) proof (prove)
goal (3 subgoals):
 1. \<And>s sa rv' rv xfdca. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1310 s sa rv' rv) (?C'1306 s sa rv' rv xfdca) (SKIP # hs) (do replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (\<acute>replySlot :== cte_Ptr (sender + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot_' s} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,\<acute>replySlot,\<acute>callerSlot))))))
 2. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. ?A1310 s sa rv' a and tcb_at' sender\<rbrace>
 3. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {sb. sb \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?C'1308 s sa canGranta receivera sendera t rv \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}}
flex-flex pairs:
\<lambda>s sa. ?C'1308 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) \<equiv>\<^sup>? \<lambda>s sa t rv. ?C'1306 s sa () rv (xfdc t) proof (prove)
goal (3 subgoals):
 1. \<And>s sa rv' rv xfdca. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1310 s sa rv' rv) (?C'1306 s sa rv' rv xfdca) (SKIP # hs) (do replySlot <- locateSlotTCB sender tcbReplySlot;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (\<acute>replySlot :== cte_Ptr (sender + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot_' s} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,\<acute>replySlot,\<acute>callerSlot))))))
 2. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. ?A1310 s sa rv' a and tcb_at' sender\<rbrace>
 3. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {sb. sb \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?C'1308 s sa canGranta receivera sendera t rv \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}}
flex-flex pairs:
\<lambda>s sa. ?C'1308 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) \<equiv>\<^sup>? \<lambda>s sa t rv. ?C'1306 s sa () rv (xfdc t) proof (prove)
goal (5 subgoals):
 1. \<And>s sa rv' rv xfdca rva replySlot. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdca; replySlot = cte_Ptr rva\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1315 s sa rv' rv xfdca rva) (?Q'1315 s sa rv' rv xfdca rva replySlot) (SKIP # hs) (do masterCTE <- getCTE rva;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) rva callerSlot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,replySlot,\<acute>callerSlot)))))
 2. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>?Q1315 s sa rv' rv xfdc\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1315 s sa rv' rv xfdc rva (replySlot_' sb)
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa rv' rv xfdca replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdca; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1315 s sa rv' rv xfdca replySlot) (?Q'1315 s sa rv' rv xfdca replySlot replySlot') (SKIP # hs) (do masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c replySlot'} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(replySlot'\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,replySlot',\<acute>callerSlot)))))
 2. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>?Q1315 s sa rv' rv xfdc\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1315 s sa rv' rv xfdc rva (replySlot_' sb)
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa xfdca replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1315 s sa () () xfdca replySlot) (?Q'1315 s sa () () xfdca replySlot (cte_Ptr replySlot)) (SKIP # hs) (do masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr replySlot} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot)))))
 2. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>?Q1315 s sa rv' rv xfdc\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1315 s sa rv' rv xfdc rva (replySlot_' sb)
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa xfdca replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1464 s sa () () xfdca replySlot) (?Q'1315 s sa () () xfdca replySlot (cte_Ptr replySlot)) (SKIP # hs) (do a <- getCTE replySlot;
y <- assert (isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender);
y <- assert (mdbNext (cteMDBNode a) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr replySlot} (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr replySlot\<rightarrow>[''cap_C''])));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot)))))
 2. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ?P1464 s sa rv' rv xfdc a b\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1315 s sa rv' rv xfdc rva (replySlot_' sb)
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa xfdca replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1472 s sa () () xfdca replySlot) (?C'1469 s sa () () xfdca replySlot (cte_Ptr replySlot)) (SKIP # hs) (do a <- getCTE replySlot;
y <- assert (isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender);
y <- assert (mdbNext (cteMDBNode a) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (\<acute>masterCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr replySlot\<rightarrow>[''cap_C'']));;
(Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot)))))
 2. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> (?A1472 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> ?C'1469 s sa rv' rv xfdc rva (replySlot_' sb) \<inter> \<lbrace>True\<rbrace>
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv masterCap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1479 s sa xfdca replySlot replySlot' rv) (?Q'1479 s sa xfdca replySlot replySlot' rv masterCap) (SKIP # hs) (do y <- assert (isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender);
y <- assert (mdbNext (cteMDBNode rv) = nullPointer);
callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>?Q1479 s sa xfdc replySlot replySlot'\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1479 s sa xfdc replySlot replySlot' rv (masterCap_' sb)
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G1609 s sa xfdca replySlot replySlot' rv) (?G'1607 s sa xfdca replySlot replySlot' rv masterCap) (SKIP # hs) (do callerSlot <- locateSlotTCB receiver tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot callerSlot
od) (Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ?G1609 s sa xfdc replySlot replySlot' a b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> sc \<in> {sc. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> sc \<in> ?G'1607 s sa xfdc replySlot replySlot' rv (masterCap_' sb)}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G1609 s sa xfdca replySlot (cte_Ptr replySlot) rv) (?G'1607 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap) (SKIP # hs) (do callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) (Guard MemorySafety \<lbrace>Kernel_C.tcbCaller = 0 \<or> array_assertion (cte_Ptr receiver) (nat (sint Kernel_C.tcbCaller)) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ?G1609 s sa xfdc replySlot replySlot' a b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> sc \<in> {sc. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> sc \<in> ?G'1607 s sa xfdc replySlot replySlot' rv (masterCap_' sb)}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1620 s sa xfdca replySlot (cte_Ptr replySlot) rv) (?C'1617 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap) (SKIP # hs) (do callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) (\<acute>callerSlot :== cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c callerSlot_' s} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>callerSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,\<acute>callerSlot))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> (?A1620 s sa xfdc replySlot replySlot' a and tcb_at' receiver) b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> sc \<in> {sc. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> sc \<in> ?C'1617 s sa xfdc replySlot replySlot' rv (masterCap_' sb) \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1620 s sa xfdca replySlot (cte_Ptr replySlot) rv) (?G'1631 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap) (SKIP # hs) (do callerCap <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> (?A1620 s sa xfdc replySlot replySlot' a and tcb_at' receiver) b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> sc \<in> {sc. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> sc \<in> {sc. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) sc \<in> ?G'1631 s sa xfdc replySlot replySlot' rv (masterCap_' sb)} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G1723 s sa xfdca replySlot (cte_Ptr replySlot) rv) (?G'1631 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap) (SKIP # hs) (do a <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (a = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))} (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ?G1723 s sa xfdc replySlot replySlot' a b) and tcb_at' receiver) b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> sc \<in> {sc. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> sc \<in> {sc. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) sc \<in> ?G'1631 s sa xfdc replySlot replySlot' rv (masterCap_' sb)} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A1731 s sa xfdca replySlot (cte_Ptr replySlot) rv) (?C'1728 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap) (SKIP # hs) (do a <- getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (a = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) (\<acute>callerCap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']));;
(\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))))))
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> (?A1731 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> sc \<in> {sc. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> sc \<in> {sc. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) sc \<in> ?C'1728 s sa xfdc replySlot replySlot' rv (masterCap_' sb) \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap rva callerCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva callerCap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1738 s sa xfdca replySlot replySlot' rv masterCap rva) (?Q'1738 s sa xfdca replySlot replySlot' rv masterCap rva callerCap) (SKIP # hs) (do y <- assert (rva = capability.NullCap);
cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)
od) (\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))
 2. \<And>s sa xfdc replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1743 s sa xfdc replySlot (cte_Ptr replySlot) rv\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q1738 s sa xfdc replySlot replySlot' rv masterCap\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1738 s sa xfdc replySlot replySlot' rv masterCap rva (callerCap_' sb)
 4. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ((\<lambda>a. True) and ?R1743 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 5. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 6. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 7. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 8. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 9. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap rva callerCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva callerCap; rva = capability.NullCap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1738 s sa xfdca replySlot replySlot' rv masterCap rva) (?Q'1738 s sa xfdca replySlot replySlot' rv masterCap rva callerCap) (SKIP # hs) (cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)) (\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))
 2. \<And>s sa xfdc replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1743 s sa xfdc replySlot (cte_Ptr replySlot) rv\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q1738 s sa xfdc replySlot replySlot' rv masterCap\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1738 s sa xfdc replySlot replySlot' rv masterCap rva (callerCap_' sb)
 4. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ((\<lambda>a. True) and ?R1743 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 5. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 6. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 7. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 8. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 9. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap rva callerCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation capability.NullCap callerCap; rva = capability.NullCap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1738 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap capability.NullCap) (?Q'1738 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap capability.NullCap callerCap) (SKIP # hs) (cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)) (\<acute>ret__struct_cap_C :== CALL cap_reply_cap_new_'proc(from_bool canGrant,SCAST(32 signed \<rightarrow> 32) false,ptr_val (tcb_ptr_to_ctcb_ptr sender));;
CALL cteInsert_'proc(\<acute>ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))
 2. \<And>s sa xfdc replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1743 s sa xfdc replySlot (cte_Ptr replySlot) rv\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q1738 s sa xfdc replySlot replySlot' rv masterCap\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> ?Q'1738 s sa xfdc replySlot replySlot' rv masterCap rva (callerCap_' sb)
 4. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ((\<lambda>a. True) and ?R1743 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 5. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 6. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 7. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 8. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 9. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>s sa xfdca replySlot replySlot' rv masterCap rva callerCap ret__struct_cap_C. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation capability.NullCap callerCap; rva = capability.NullCap; cap_reply_cap_lift ret__struct_cap_C = \<lparr>capReplyCanGrant_CL = from_bool canGrant, capReplyMaster_CL = SCAST(32 signed \<rightarrow> 32) false, capTCBPtr_CL = ptr_val (tcb_ptr_to_ctcb_ptr sender) && ~~ mask 6\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1738 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap capability.NullCap) (?G'1830 s sa xfdca replySlot (cte_Ptr replySlot) rv masterCap capability.NullCap callerCap ret__struct_cap_C) (SKIP # hs) (cteInsert (capability.ReplyCap sender False canGrant) replySlot (receiver + 2 ^ cte_level_bits * tcbCallerSlot)) (CALL cteInsert_'proc(ret__struct_cap_C,cte_Ptr replySlot,cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))
 2. \<And>s sa xfdc replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1743 s sa xfdc replySlot (cte_Ptr replySlot) rv\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q1738 s sa xfdc replySlot replySlot' rv masterCap\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {sc. \<forall>v. cap_reply_cap_lift v = \<lparr>capReplyCanGrant_CL = capReplyCanGrant_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) sc))) && mask 1, capReplyMaster_CL = capReplyMaster_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) sc))) && mask 1, capTCBPtr_CL = capTCBPtr_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) sc))) && ~~ mask 6\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> sc\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> ?G'1830 s sa xfdc replySlot replySlot' rv masterCap rva (callerCap_' sb) v}
 4. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ((\<lambda>a. True) and ?R1743 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 5. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 6. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 7. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 8. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 9. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (8 subgoals):
 1. \<And>s sa xfdc replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1743 s sa xfdc replySlot (cte_Ptr replySlot) rv\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (capability.ReplyCap sender False canGrant) \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) replySlot and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' (capability.ReplyCap sender False canGrant) and cte_wp_at' (\<lambda>c. True) replySlot\<rbrace>
 2. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. \<forall>v. cap_reply_cap_lift v = \<lparr>capReplyCanGrant_CL = capReplyCanGrant_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && mask 1, capReplyMaster_CL = capReplyMaster_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && mask 1, capTCBPtr_CL = capTCBPtr_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && ~~ mask 6\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) (srcSlot_'_update (\<lambda>_. replySlot') (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = replySlot'\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap sender False canGrant) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = replySlot'\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap sender False canGrant) \<acute>newCap\<rbrace>}}
 3. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ((\<lambda>a. True) and ?R1743 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 4. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 5. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 6. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 7. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 8. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (8 subgoals):
 1. \<And>s sa xfdc replySlot replySlot' rv masterCap. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1743 s sa xfdc replySlot (cte_Ptr replySlot) rv\<rbrace> getSlotCap (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) replySlot b \<and> valid_mdb' b \<and> valid_objs' b \<and> pspace_aligned' b \<and> valid_cap' (capability.ReplyCap sender False canGrant) b \<and> cte_wp_at' (\<lambda>c. True) replySlot b\<rbrace>
 2. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. \<forall>v. cap_reply_cap_lift v = \<lparr>capReplyCanGrant_CL = capReplyCanGrant_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && mask 1, capReplyMaster_CL = capReplyMaster_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && mask 1, capTCBPtr_CL = capTCBPtr_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && ~~ mask 6\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) (srcSlot_'_update (\<lambda>_. replySlot') (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = replySlot'\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap sender False canGrant) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = replySlot'\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap sender False canGrant) \<acute>newCap\<rbrace>}}
 3. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>b. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> ((\<lambda>a. True) and ?R1743 s sa xfdc replySlot replySlot' a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) b) and tcb_at' receiver) b\<rbrace>
 4. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 5. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 6. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 7. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 8. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s sa xfdc replySlot replySlot' rv masterCap sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; ccap_relation (cteCap rv) masterCap; isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender; mdbNext (cteMDBNode rv) = nullPointer; ccap_relation rva (callerCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. \<forall>v. cap_reply_cap_lift v = \<lparr>capReplyCanGrant_CL = capReplyCanGrant_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && mask 1, capReplyMaster_CL = capReplyMaster_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && mask 1, capTCBPtr_CL = capTCBPtr_' (capTCBPtr_'_update (\<lambda>_. ptr_val (tcb_ptr_to_ctcb_ptr sender)) (capReplyMaster_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (capReplyCanGrant_'_update (\<lambda>_. from_bool canGrant) s))) && ~~ mask 6\<rparr> \<and> cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. destSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) (srcSlot_'_update (\<lambda>_. replySlot') (newCap_'_update (\<lambda>_. v) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = replySlot'\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap sender False canGrant) \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = replySlot'\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap sender False canGrant) \<acute>newCap\<rbrace>}}
 2. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>a. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) replySlot a \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> valid_cap' (capability.ReplyCap sender False canGrant) a \<and> cte_wp_at' (\<lambda>c. True) replySlot a) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) a) and tcb_at' receiver) b\<rbrace>
 3. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 4. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 5. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 6. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 7. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> ((\<lambda>a. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) replySlot a \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> valid_cap' (capability.ReplyCap sender False canGrant) a \<and> cte_wp_at' (\<lambda>c. True) replySlot a) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))))) a) and tcb_at' receiver) b\<rbrace>
 2. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 3. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 4. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 5. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 6. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>s sa xfdc replySlot replySlot'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot\<rbrakk> \<Longrightarrow> \<lbrace>?R1484 s sa () () xfdc replySlot\<rbrace> getCTE replySlot \<lbrace>\<lambda>a b. isReplyCap (cteCap a) \<and> capReplyMaster (cteCap a) \<and> capTCBPtr (cteCap a) = sender \<longrightarrow> mdbNext (cteMDBNode a) = nullPointer \<longrightarrow> (cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) replySlot b \<and> valid_mdb' b \<and> valid_objs' b \<and> pspace_aligned' b \<and> valid_cap' (capability.ReplyCap sender False canGrant) b \<and> cte_wp_at' (\<lambda>c. True) replySlot b \<and> cte_wp_at' (\<lambda>_. True) (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) b) \<and> tcb_at' receiver b\<rbrace>
 2. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 3. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and ?R1484 s sa rv' rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 4. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 5. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 6. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa xfdc replySlot replySlot' sb rv. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; replySlot' = cte_Ptr replySlot; (ccap_relation \<circ> cteCap) rv (masterCap_' sb)\<rbrakk> \<Longrightarrow> sb \<in> {s. isReplyCap (cteCap rv) \<and> capReplyMaster (cteCap rv) \<and> capTCBPtr (cteCap rv) = sender \<longrightarrow> s \<in> {s. mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> s \<in> {s. callerSlot_'_update (\<lambda>_. cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s \<in> \<lbrace>cte_Ptr (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (receiver + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace> \<inter> \<lbrace>True\<rbrace>} \<inter> \<lbrace>nat (sint Kernel_C.tcbCaller) \<le> unat tcbCNodeEntries\<rbrace>}}
 2. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and (\<lambda>b. \<forall>cte. cte_wp_at' ((=) cte) a b \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) a b \<and> valid_mdb' b \<and> valid_objs' b \<and> pspace_aligned' b \<and> valid_cap' (capability.ReplyCap sender False canGrant) b \<and> cte_wp_at' (\<lambda>c. True) a b \<and> cte_wp_at' (\<lambda>_. True) (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) b) \<and> tcb_at' receiver b) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>s sa rv' rv xfdc. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa rv' rv\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> ((\<lambda>a. True) and (\<lambda>b. \<forall>cte. cte_wp_at' ((=) cte) a b \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) a b \<and> valid_mdb' b \<and> valid_objs' b \<and> pspace_aligned' b \<and> valid_cap' (capability.ReplyCap sender False canGrant) b \<and> cte_wp_at' (\<lambda>c. True) a b \<and> cte_wp_at' (\<lambda>_. True) (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) b) \<and> tcb_at' receiver b) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))) b\<rbrace>
 2. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 3. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 4. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>a b. cte_wp_at' (\<lambda>_. True) a b \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) a b \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) b \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) a b \<and> valid_mdb' b \<and> valid_objs' b \<and> pspace_aligned' b \<and> valid_cap' (capability.ReplyCap sender False canGrant) b \<and> cte_wp_at' (\<lambda>_. True) (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) b) \<and> tcb_at' receiver b)\<rbrace>
 2. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 3. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 4. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa rv sb. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; (valid_pspace' and tcb_at' receiver) sb\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) rv sb \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) rv sb \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<and> capTCBPtr (cteCap cte) = sender \<longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) sb \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capability.ReplyCap sender True True \<or> is_simple_cap' (capability.ReplyCap sender False canGrant)) rv sb \<and> valid_mdb' sb \<and> valid_objs' sb \<and> pspace_aligned' sb \<and> valid_cap' (capability.ReplyCap sender False canGrant) sb \<and> cte_wp_at' (\<lambda>_. True) (receiver + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) sb) \<and> tcb_at' receiver sb)
 2. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa rv sb cte v1 v2 cteb. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; valid_pspace' sb; tcb_at' receiver sb; ctes_of sb rv = Some cte; cteCap cte = capability.ReplyCap sender True v2; v1; mdbNext (cteMDBNode cte) = nullPointer; ctes_of sb (receiver + 0x30) = Some cteb\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap sender False canGrant) sb
 2. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa rv sb v1 v2 cteb x2. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; valid_pspace' sb; tcb_at' receiver sb; ctes_of sb rv = Some (CTE (capability.ReplyCap sender True v2) x2); v1; mdbNext x2 = nullPointer; ctes_of sb (receiver + 0x30) = Some cteb\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap sender False canGrant) sb
 2. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>s sa rv sb v1 v2 cteb x2. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; valid_pspace' sb; tcb_at' receiver sb; v1; mdbNext x2 = nullPointer; ctes_of sb (receiver + 0x30) = Some cteb\<rbrakk> \<Longrightarrow> valid_objs' sb
 2. \<And>s sa rv sb v1 v2 cteb x2. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; valid_pspace' sb; tcb_at' receiver sb; v1; mdbNext x2 = nullPointer; ctes_of sb (receiver + 0x30) = Some cteb; valid_cap' (capability.ReplyCap sender True v2) sb\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap sender False canGrant) sb
 3. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 4. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 5. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 6. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>s sa rv sb v1 v2 cteb x2. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; valid_pspace' sb; tcb_at' receiver sb; v1; mdbNext x2 = nullPointer; ctes_of sb (receiver + 0x30) = Some cteb; valid_cap' (capability.ReplyCap sender True v2) sb\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap sender False canGrant) sb
 2. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 3. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 4. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 5. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> locateSlotTCB sender tcbReplySlot \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 2. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 3. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 4. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1320 s sa () ()\<rbrace> return (sender + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>rv. valid_pspace' and tcb_at' receiver\<rbrace>
 2. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 3. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1320 s sa rv' a and tcb_at' sender\<rbrace>
 4. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>s sa rv' rv xfdc sb rva. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; dc rv xfdc; replySlot_' sb = cte_Ptr rva\<rbrakk> \<Longrightarrow> sb \<in> \<lbrace>\<^bsup>sb\<^esup>replySlot = \<^bsup>sb\<^esup>replySlot\<rbrace> \<inter> \<lbrace>True\<rbrace>
 2. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and (valid_pspace' and tcb_at' receiver) and tcb_at' sender\<rbrace>
 3. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>s sa rv'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a. (\<lambda>a. True) and (valid_pspace' and tcb_at' receiver) and tcb_at' sender\<rbrace>
 2. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R1272 s sa (from_bool canGrant) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>a b. valid_pspace' b \<and> tcb_at' receiver b \<and> tcb_at' sender b\<rbrace>
 2. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1272 s sa canGranta receivera sendera) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>s sa canGranta receivera sendera sb s'. \<lbrakk>tcb_at' receiver s; tcb_at' sender sa; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr sender)) ctcb_size_bits; canGranta = from_bool canGrant; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (sb, s') \<in> rf_sr; (Invariants_H.valid_queues and valid_pspace' and (\<lambda>s. \<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))) and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and sch_act_not sender and tcb_at' sender and tcb_at' receiver) sb; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. tcb_at' sender a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.BlockedOnReply a \<and> (ksSchedulerAction a = SwitchToThread sender \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> (\<forall>p. sender \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (valid_pspace' and tcb_at' sender and valid_tcb_state' Structures_H.thread_state.BlockedOnReply) a \<and> tcb_at' receiver a \<and> tcb_at' sender a)) sb \<and> s' \<in> {s. s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply) (tptr_'_update (\<lambda>_. sendera) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.BlockedOnReply (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = sendera\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>sender = sender \<and> tcbReplySlot = SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbReply\<rbrace> \<inter> \<lbrace>nat (sint Kernel_C.tcbReply) \<le> unat tcbCNodeEntries\<rbrace>}} proof (prove)
goal:
No subgoals!