theory Syscall_C

lemma deleteCallerCap_ccorres [corres]:
  "ccorres dc xfdc
       (\<lambda>s. invs' s \<and> tcb_at' receiver s)
       (UNIV \<inter> {s. receiver_' s = tcb_ptr_to_ctcb_ptr receiver})
       []
       (deleteCallerCap receiver)
       (Call deleteCallerCap_'proc)" apply (cinit lift: receiver_') apply (simp only: getThreadCallerSlot_def locateSlot_conv) apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ apply (rule_tac P="\<lambda>_. is_aligned receiver tcbBlockSizeBits" and r'="\<lambda> a c. cte_Ptr a = c"
                   and xf'="callerSlot_'" and P'=UNIV in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def word_sle_def) apply (frule is_aligned_neg_mask_eq) apply (simp add: mask_def tcbCallerSlot_def Kernel_C.tcbCaller_def
              cte_level_bits_def size_of_def) apply (drule ptr_val_tcb_ptr_mask2) apply (simp add: mask_def objBits_defs) apply ceqv apply (rule ccorres_symb_exec_l) apply (rule ccorres_symb_exec_l) apply (rule ccorres_symb_exec_r) apply (ctac add:  cteDeleteOne_ccorres[where w="ucast cap_reply_cap"]) apply vcg apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def
             gs_set_assn_Delete_cstate_relation[unfolded o_def]) apply (wp | simp)+ apply (simp add: getSlotCap_def) apply (wp getCTE_wp)+ apply clarsimp apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
                        ghost_assertion_data_set_def) apply (clarsimp simp: cte_wp_at_ctes_of cap_get_tag_isCap[symmetric]
                        cap_tag_defs tcb_cnode_index_defs word_sle_def
                        tcb_aligned') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. invs' s \<and> tcb_at' receiver s) (UNIV \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>) [] (deleteCallerCap receiver) (Call deleteCallerCap_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ccorres dc xfdc (?Q263 receivera) (?Q'263 receivera) [SKIP] (do callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne callerSlot
od) (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))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)))
 2. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q263 receivera s \<and> s' \<in> ?Q'263 receivera proof (prove)
goal (2 subgoals):
 1. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ccorres dc xfdc (?Q263 (tcb_ptr_to_ctcb_ptr receiver)) (?Q'263 (tcb_ptr_to_ctcb_ptr receiver)) [SKIP] (do callerSlot <- return (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
callerCap <- getSlotCap callerSlot;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne callerSlot
od) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>callerSlot :== cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)))
 2. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q263 receivera s \<and> s' \<in> ?Q'263 receivera proof (prove)
goal (2 subgoals):
 1. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ccorres dc xfdc (?A273 (tcb_ptr_to_ctcb_ptr receiver)) (?C'270 (tcb_ptr_to_ctcb_ptr receiver)) [SKIP] (do callerSlot <- return (receiver + 2 ^ cte_level_bits * tcbCallerSlot);
callerCap <- getSlotCap callerSlot;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne callerSlot
od) (\<acute>callerSlot :== cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)))
 2. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A273 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> ?C'270 receivera \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ccorres (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>_. is_aligned receiver tcbBlockSizeBits) UNIV [] (return (receiver + 2 ^ cte_level_bits * tcbCallerSlot)) (\<acute>callerSlot :== cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))))
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. is_aligned receiver tcbBlockSizeBits \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>callerSlot :== cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<exists>(rv, \<sigma>')\<in>fst (return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> cte_Ptr rv = callerSlot_' s}
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>receivera \<sigma>. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> {s. is_aligned receiver tcbBlockSizeBits \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<sigma>). (\<sigma>', callerSlot_'_update (\<lambda>_. cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) s) \<in> rf_sr \<and> cte_Ptr rv = cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))}
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned receiver tcbBlockSizeBits; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> receiver + 2 ^ cte_level_bits * tcbCallerSlot = (ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned receiver tcbBlockSizeBits; (\<sigma>, x) \<in> rf_sr; receiver && ~~ mask tcbBlockSizeBits = receiver\<rbrakk> \<Longrightarrow> receiver + 2 ^ cte_level_bits * tcbCallerSlot = (ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned receiver tcbBlockSizeBits; (\<sigma>, x) \<in> rf_sr; receiver && ~~ (2 ^ tcbBlockSizeBits - 1) = receiver\<rbrakk> \<Longrightarrow> receiver = ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>(\<sigma>, x) \<in> rf_sr; receiver && ~~ (2 ^ tcbBlockSizeBits - 1) = receiver; ptr_val (tcb_ptr_to_ctcb_ptr receiver) && ~~ mask tcbBlockSizeBits = receiver\<rbrakk> \<Longrightarrow> receiver = ptr_val (tcb_ptr_to_ctcb_ptr receiver) && 0xFFFFFE00
 2. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 6. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>receivera rv' t t'. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> ceqv \<Gamma> callerSlot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(\<acute>callerSlot)) (?d'276 receivera rv')
 2. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (?d'276 receivera rv')
 3. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 5. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q276 receivera rv) (?Q'276 receivera rv rv') [SKIP] (do callerCap <- getSlotCap rv;
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne rv
od) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(rv'))
 2. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 3. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (?Q'276 receivera)
 4. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q341 receivera rv rv' rva) (?Q'341 receivera rv rv' rva) [SKIP] (do y <- assert (isReplyCap rva \<or> rva = capability.NullCap);
cteDeleteOne rv
od) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(rv'))
 2. \<And>receivera rv rv' s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 receivera rv\<rbrace> getSlotCap rv \<lbrace>?Q341 receivera rv rv'\<rbrace>
 4. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 5. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 6. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q341 receivera rv rv' rva s \<longrightarrow> s' \<in> ?Q'341 receivera rv rv' rva})
 7. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>receivera rv rv' rva rvb. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q346 receivera rv rv' rva rvb) (?Q'346 receivera rv rv' rva rvb) [SKIP] (cteDeleteOne rv) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap));;
CALL cteDeleteOne_'proc(rv'))
 2. \<And>receivera rv rv' rva s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 receivera rv rv' rva\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>?Q346 receivera rv rv' rva\<rbrace>
 4. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (assert (isReplyCap rva \<or> rva = capability.NullCap))
 5. \<And>receivera rv rv' s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 receivera rv\<rbrace> getSlotCap rv \<lbrace>?Q341 receivera rv rv'\<rbrace>
 7. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 8. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 9. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q341 receivera rv rv' rva s \<longrightarrow> s' \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> ?Q346 receivera rv rv' rva rvb s \<longrightarrow> s' \<in> ?Q'346 receivera rv rv' rva rvb}})
 10. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>receivera rv rv' rva rvb. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q346 receivera rv rv' rva rvb) (?Q'351 receivera rv rv' rva rvb) [SKIP] (cteDeleteOne rv) (CALL cteDeleteOne_'proc(rv'))
 2. \<And>receivera rv rv' rva rvb. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'346 receivera rv rv' rva rvb) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (?Q'351 receivera rv rv' rva rvb)
 3. \<And>receivera rv rv' rva rvb s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'; ?Q346 receivera rv rv' rva rvb s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'346 receivera rv rv' rva rvb \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) {s'. (s, s') \<in> rf_sr}
 4. \<And>receivera rv rv' rva s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 receivera rv rv' rva\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>?Q346 receivera rv rv' rva\<rbrace>
 6. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (assert (isReplyCap rva \<or> rva = capability.NullCap))
 7. \<And>receivera rv rv' s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 receivera rv\<rbrace> getSlotCap rv \<lbrace>?Q341 receivera rv rv'\<rbrace>
 9. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 10. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>receivera rv rv' rva rvb. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'346 receivera rv rv' rva rvb) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) {s. slot_'_update (\<lambda>_. rv') s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = UCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>}
 2. \<And>receivera rv rv' rva rvb s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'; (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'346 receivera rv rv' rva rvb \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) {s'. (s, s') \<in> rf_sr}
 3. \<And>receivera rv rv' rva s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 receivera rv rv' rva\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>rvb. invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv\<rbrace>
 5. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (assert (isReplyCap rva \<or> rva = capability.NullCap))
 6. \<And>receivera rv rv' s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 receivera rv\<rbrace> getSlotCap rv \<lbrace>?Q341 receivera rv rv'\<rbrace>
 8. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 9. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 10. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q341 receivera rv rv' rva s \<longrightarrow> s' \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s \<longrightarrow> s' \<in> ?Q'346 receivera rv rv' rva rvb}})
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>receivera rv rv' rva rvb s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'; (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) {s'. (s, s') \<in> rf_sr}
 2. \<And>receivera rv rv' rva s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 receivera rv rv' rva\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>rvb. invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv\<rbrace>
 4. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (assert (isReplyCap rva \<or> rva = capability.NullCap))
 5. \<And>receivera rv rv' s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 receivera rv\<rbrace> getSlotCap rv \<lbrace>?Q341 receivera rv rv'\<rbrace>
 7. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 8. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 9. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q341 receivera rv rv' rva s \<longrightarrow> s' \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv\<rbrace>}})
 10. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>receivera rv rv' rva s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q341 receivera rv rv' rva\<rbrace> assert (isReplyCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>rvb. invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv\<rbrace>
 3. \<And>receivera rv rv' rva. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (assert (isReplyCap rva \<or> rva = capability.NullCap))
 4. \<And>receivera rv rv' s. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 receivera rv\<rbrace> getSlotCap rv \<lbrace>?Q341 receivera rv rv'\<rbrace>
 6. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 7. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 8. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> ?Q341 receivera rv rv' rva s \<longrightarrow> s' \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv\<rbrace>}})
 9. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 (tcb_ptr_to_ctcb_ptr receiver) rv\<rbrace> getSlotCap rv \<lbrace>\<lambda>rva s. (isReplyCap rva \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s) \<and> (rva = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s)\<rbrace>
 2. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 3. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (isReplyCap rva \<or> rva = capability.NullCap \<longrightarrow> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s) \<longrightarrow> s' \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv\<rbrace>}})
 5. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q276 (tcb_ptr_to_ctcb_ptr receiver) rv\<rbrace> do cte <- getCTE rv;
return (cteCap cte)
od \<lbrace>\<lambda>rva s. (isReplyCap rva \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s) \<and> (rva = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s)\<rbrace>
 2. \<And>receivera rv rv'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; cte_Ptr rv = rv'\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 3. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> \<lbrace>?R280 (tcb_ptr_to_ctcb_ptr receiver)\<rbrace> return (receiver + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q276 receivera\<rbrace>
 4. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (isReplyCap rva \<or> rva = capability.NullCap \<longrightarrow> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s) \<longrightarrow> s' \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv\<rbrace>}})
 5. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and ?R280 receivera and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>receivera. receivera = tcb_ptr_to_ctcb_ptr receiver \<Longrightarrow> guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (isReplyCap rva \<or> rva = capability.NullCap \<longrightarrow> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s) \<longrightarrow> s' \<in> {s'. \<forall>rva s. (s, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv) s \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv\<rbrace>}})
 2. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and (\<lambda>a. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<and> (isReplyCap (cteCap cte) \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a))) and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (2 subgoals):
 1. guard_is_UNIV (\<lambda>a. (=) (cte_Ptr a)) callerSlot_' (\<lambda>rv rv'. {s'. (\<exists>rva s. (s, s') \<in> rf_sr \<and> (isReplyCap rva \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s) \<and> (rva = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s)) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> invs' s \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) rv s) \<longrightarrow> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_reply_cap) (\<lambda>x. apsnd (apsnd x)) (ghost'state_' (globals s'))) = UCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> rv' = cte_Ptr rv})
 2. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and (\<lambda>a. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<and> (isReplyCap (cteCap cte) \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a))) and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>receivera s s'. \<lbrakk>receivera = tcb_ptr_to_ctcb_ptr receiver; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' receiver s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. is_aligned receiver tcbBlockSizeBits) and (\<lambda>a. cte_wp_at' (\<lambda>_. True) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a \<and> (isReplyCap (cteCap cte) \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. UCAST(32 signed \<rightarrow> 32) cap_reply_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = UCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (receiver + 2 ^ cte_level_bits * tcbCallerSlot) a))) and tcb_at' (ctcb_ptr_to_tcb_ptr receivera)) s \<and> s' \<in> UNIV \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCaller \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCaller + 1 | False \<Rightarrow> sint Kernel_C.tcbCaller) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal:
No subgoals!