theory Ipc_R

lemma transferCaps_corres:
  "\<lbrakk> info' = message_info_map info;
    list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))
         caps caps' \<rbrakk>
  \<Longrightarrow>
   corres ((=) \<circ> message_info_map)
   (tcb_at receiver and valid_objs and
    pspace_aligned and pspace_distinct and valid_mdb
    and valid_list
    and (\<lambda>s. case ep of Some x \<Rightarrow> ep_at x s | _ \<Rightarrow> True)
    and case_option \<top> in_user_frame recv_buf
    and (\<lambda>s. valid_message_info info)
    and transfer_caps_srcs caps)
   (tcb_at' receiver and valid_objs' and
    pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'
    and (\<lambda>s. case ep of Some x \<Rightarrow> ep_at' x s | _ \<Rightarrow> True)
    and case_option \<top> valid_ipc_buffer_ptr' recv_buf
    and transferCaps_srcs caps'
    and (\<lambda>s. length caps' \<le> msgMaxExtraCaps))
   (transfer_caps info caps ep receiver recv_buf)
   (transferCaps info' caps' ep receiver recv_buf)" apply (simp add: transfer_caps_def transferCaps_def
                   getThreadCSpaceRoot) apply (rule corres_assume_pre) apply (rule corres_guard_imp) apply (rule corres_split[OF getReceiveSlots_corres]) apply (rule_tac x=recv_buf in option_corres) apply (rule_tac P=\<top> and P'=\<top> in corres_inst) apply (case_tac info, simp) apply simp apply (rule corres_rel_imp, rule transferCapsToSlots_corres,
             simp_all add: split_def)[1] apply (case_tac info, simp) apply (wp hoare_vcg_all_lift get_rs_cte_at hoare_weak_lift_imp
                | simp only: ball_conj_distrib)+ apply (simp add: cte_map_def tcb_cnode_index_def split_def) apply (clarsimp simp: valid_pspace'_def valid_ipc_buffer_ptr'_def2
                        split_def
                  cong: option.case_cong) apply (drule(1) bspec) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (frule(1) Invariants_AI.caps_of_state_valid) apply (fastforce simp:valid_cap_def) apply (cases info) apply (clarsimp simp: msg_max_extra_caps_def valid_message_info_def
                        max_ipc_words msg_max_length_def
                        msgMaxExtraCaps_def msgExtraCapBits_def
                        shiftL_nat valid_pspace'_def) apply (drule(1) bspec) apply (clarsimp simp:cte_wp_at_ctes_of) apply (case_tac cte,clarsimp) apply (frule(1) ctes_of_valid_cap') apply (fastforce simp:valid_cap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) (transfer_caps info caps ep receiver recv_buf) (transferCaps info' caps' ep receiver recv_buf) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) (do dest_slots <- get_receive_slots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))
od) (do destSlots <- getReceiveSlots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) (do dest_slots <- get_receive_slots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))
od) (do destSlots <- getReceiveSlots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info)))
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (?Q6 s s') (?Q'6 s s') (do dest_slots <- get_receive_slots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))
od) (do destSlots <- getReceiveSlots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info)))
od)
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> ?Q6 s s' sa
 3. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> ?Q'6 s s' sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (?R10 s s' dest_slots) (?R'10 s s' destSlots) (case recv_buf of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 2. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>?R10 s s'\<rbrace>
 3. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>?R'10 s s'\<rbrace>
 4. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 5. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; recv_buf = None; recv_buf = None\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (?P23 s s' dest_slots) (?P'21 s s' destSlots) (case None of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (case None of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 2. \<And>s s' dest_slots destSlots z z'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; recv_buf = Some z; recv_buf = Some z'\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (\<lambda>a. ?Q22 s s' dest_slots a z) (\<lambda>a. ?Q'20 s s' destSlots a z') (case Some z of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (case Some z' of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 3. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> (recv_buf = None) = (recv_buf = None)
 4. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> ?P23 s s' a aa) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q22 s s' a aa z)\<rbrace>
 5. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> ?P'21 s s' a aa) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q'20 s s' a aa z)\<rbrace>
 6. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 7. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; recv_buf = None; recv_buf = None\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (\<lambda>_. True) (\<lambda>_. True) (case None of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (case None of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 2. \<And>s s' dest_slots destSlots z z'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; recv_buf = Some z; recv_buf = Some z'\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (\<lambda>a. ?Q22 s s' dest_slots a z) (\<lambda>a. ?Q'20 s s' destSlots a z') (case Some z of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (case Some z' of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 3. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> (recv_buf = None) = (recv_buf = None)
 4. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q22 s s' a aa z)\<rbrace>
 5. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q'20 s s' a aa z)\<rbrace>
 6. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 7. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' dest_slots destSlots z z'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; recv_buf = Some z; recv_buf = Some z'\<rbrakk> \<Longrightarrow> corres ((=) \<circ> message_info_map) (\<lambda>a. ?Q22 s s' dest_slots a z) (\<lambda>a. ?Q'20 s s' destSlots a z') (case Some z of None \<Rightarrow> return (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (case Some z' of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps' destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 2. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> (recv_buf = None) = (recv_buf = None)
 3. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q22 s s' a aa z)\<rbrace>
 4. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q'20 s s' a aa z)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 6. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' dest_slots destSlots z z'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; tcb_at receiver s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_mdb s \<and> valid_list s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) \<and> in_user_frame z s \<and> valid_message_info info \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s); tcb_at' receiver s' \<and> valid_objs' s' \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> no_0_obj' s' \<and> valid_mdb' s' \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s') \<and> valid_ipc_buffer_ptr' z s' \<and> (\<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s') \<and> length caps' \<le> msgMaxExtraCaps; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; z' = z; recv_buf = Some z\<rbrakk> \<Longrightarrow> corres (\<lambda>a. (=) (message_info_map a)) (\<lambda>a. ?Q22 s s' dest_slots a z) (\<lambda>a. ?Q'20 s s' (map cte_map dest_slots) a z) (transfer_caps_loop ep z 0 caps dest_slots (Structures_A.message_info.MI (mi_length info) 0 0 (mi_label info))) (transferCapsToSlots ep z 0 caps' (map cte_map dest_slots) (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info))))
 2. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> (recv_buf = None) = (recv_buf = None)
 3. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q22 s s' a aa z)\<rbrace>
 4. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> ?Q'20 s s' a aa z)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 6. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' dest_slots destSlots z z'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; tcb_at receiver s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_mdb s \<and> valid_list s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) \<and> in_user_frame z s \<and> valid_message_info info \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s); tcb_at' receiver s' \<and> valid_objs' s' \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> no_0_obj' s' \<and> valid_mdb' s' \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s') \<and> valid_ipc_buffer_ptr' z s' \<and> (\<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s') \<and> length caps' \<le> msgMaxExtraCaps; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots; z' = z; recv_buf = Some z\<rbrakk> \<Longrightarrow> msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (message_info_map info)) = Types_H.message_info.MI (mi_length info) 0 0 (mi_label info)
 2. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> (recv_buf = None) = (recv_buf = None)
 3. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> valid_objs aa \<and> pspace_aligned aa \<and> pspace_distinct aa \<and> valid_mdb aa \<and> valid_list aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x aa) \<and> (\<forall>x\<in>set a. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x aa \<and> real_cte_at x aa) \<and> (\<forall>a\<in>set caps. case a of (cap, slot) \<Rightarrow> aa \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot aa) \<and> distinct a \<and> in_user_frame z aa)\<rbrace>
 4. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> valid_pspace' aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x aa) \<and> (\<forall>x\<in>set a. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x aa \<and> real_cte_at' x aa) \<and> distinct a \<and> valid_ipc_buffer_ptr' z aa \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap aa \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot aa) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 6. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' dest_slots destSlots. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; destSlots = map cte_map dest_slots\<rbrakk> \<Longrightarrow> (recv_buf = None) = (recv_buf = None)
 2. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s s'\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> valid_objs aa \<and> pspace_aligned aa \<and> pspace_distinct aa \<and> valid_mdb aa \<and> valid_list aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x aa) \<and> (\<forall>x\<in>set a. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x aa \<and> real_cte_at x aa) \<and> (\<forall>a\<in>set caps. case a of (cap, slot) \<Rightarrow> aa \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot aa) \<and> distinct a \<and> in_user_frame z aa)\<rbrace>
 3. \<And>s s'. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 s s'\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>a aa. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>z. recv_buf = Some z \<longrightarrow> valid_pspace' aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x aa) \<and> (\<forall>x\<in>set a. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x aa \<and> real_cte_at' x aa) \<and> distinct a \<and> valid_ipc_buffer_ptr' z aa \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap aa \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot aa) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words)\<rbrace>
 4. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and ?Q10 s s') sa
 5. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'10 s s') sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set caps. real_cte_at (snd x) s))) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set caps. real_cte_at (snd x) s))) sa\<rbrakk> \<Longrightarrow> (tcb_at receiver and valid_objs and pspace_aligned and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_mdb s \<and> valid_list s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) \<and> True \<and> valid_objs s \<and> (\<forall>a\<in>set caps. case a of (cap, slot) \<Rightarrow> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> True \<and> in_user_frame x s))) sa
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = fst (snd x) + of_bl (snd (snd x)) * 2 ^ cte_level_bits) caps caps'; tcb_at receiver s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_mdb s \<and> valid_list s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_message_info info \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set caps. real_cte_at (snd x) s); tcb_at' receiver s' \<and> valid_objs' s' \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> no_0_obj' s' \<and> valid_mdb' s' \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s') \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) s' \<and> (\<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s') \<and> length caps' \<le> msgMaxExtraCaps; (s, s') \<in> state_relation; tcb_at receiver sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> pspace_distinct sa \<and> valid_mdb sa \<and> valid_list sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) sa \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) sa) \<and> (\<forall>x\<in>set caps. real_cte_at (snd x) sa)\<rbrakk> \<Longrightarrow> \<forall>x. recv_buf = Some x \<longrightarrow> (\<forall>x\<in>set caps. sa \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp'. fst x \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> fst x \<longrightarrow> cp' = masked_as_full (fst x) (fst x)) (snd x) sa) \<and> in_user_frame x sa
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa x a aa b. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = fst (snd x) + of_bl (snd (snd x)) * 2 ^ cte_level_bits) caps caps'; (s, s') \<in> state_relation; tcb_at receiver s; tcb_at' receiver s'; tcb_at receiver sa; valid_objs s; valid_objs' s'; valid_objs sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct sa; valid_mdb s; no_0_obj' s'; valid_mdb sa; valid_list s; valid_mdb' s'; valid_list sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa; in_user_frame x s; in_user_frame x sa; valid_message_info info; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s'; length caps' \<le> msgMaxExtraCaps; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) sa; \<forall>x\<in>set caps. real_cte_at (snd x) sa; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s; \<forall>x\<in>set caps. real_cte_at (snd x) s; recv_buf = Some x; (a, aa, b) \<in> set caps; is_aligned x msg_align_bits; typ_at' UserDataT (x && ~~ mask pageBits) s'\<rbrakk> \<Longrightarrow> sa \<turnstile> a \<and> cte_wp_at (\<lambda>cp'. a \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> a \<longrightarrow> cp' = masked_as_full a a) (aa, b) sa
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa x a aa b. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = fst (snd x) + of_bl (snd (snd x)) * 2 ^ cte_level_bits) caps caps'; (s, s') \<in> state_relation; tcb_at receiver s; tcb_at' receiver s'; tcb_at receiver sa; valid_objs s; valid_objs' s'; valid_objs sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct sa; valid_mdb s; no_0_obj' s'; valid_mdb sa; valid_list s; valid_mdb' s'; valid_list sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa; in_user_frame x s; in_user_frame x sa; valid_message_info info; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s'; length caps' \<le> msgMaxExtraCaps; \<forall>x\<in>set caps. real_cte_at (snd x) sa; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s; \<forall>x\<in>set caps. real_cte_at (snd x) s; recv_buf = Some x; (a, aa, b) \<in> set caps; is_aligned x msg_align_bits; typ_at' UserDataT (x && ~~ mask pageBits) s'; cte_wp_at (\<lambda>cp. fst (a, aa, b) \<noteq> cap.NullCap \<longrightarrow> cp = fst (a, aa, b)) (snd (a, aa, b)) sa\<rbrakk> \<Longrightarrow> sa \<turnstile> a \<and> cte_wp_at (\<lambda>cp'. a \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> a \<longrightarrow> cp' = masked_as_full a a) (aa, b) sa
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa x a aa b cap. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = fst (snd x) + of_bl (snd (snd x)) * 2 ^ cte_level_bits) caps caps'; (s, s') \<in> state_relation; tcb_at receiver s; tcb_at' receiver s'; tcb_at receiver sa; valid_objs s; valid_objs' s'; valid_objs sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct sa; valid_mdb s; no_0_obj' s'; valid_mdb sa; valid_list s; valid_mdb' s'; valid_list sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa; in_user_frame x s; in_user_frame x sa; valid_message_info info; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s'; length caps' \<le> msgMaxExtraCaps; \<forall>x\<in>set caps. real_cte_at (snd x) sa; \<forall>x\<in>set caps. \<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> cap.NullCap \<longrightarrow> cap = fst x); \<forall>x\<in>set caps. real_cte_at (snd x) s; recv_buf = Some x; (a, aa, b) \<in> set caps; is_aligned x msg_align_bits; typ_at' UserDataT (x && ~~ mask pageBits) s'; caps_of_state sa (aa, b) = Some cap; a \<noteq> cap.NullCap \<longrightarrow> cap = a\<rbrakk> \<Longrightarrow> sa \<turnstile> a
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa x a aa b cap. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = fst (snd x) + of_bl (snd (snd x)) * 2 ^ cte_level_bits) caps caps'; (s, s') \<in> state_relation; tcb_at receiver s; tcb_at' receiver s'; tcb_at receiver sa; valid_objs s; valid_objs' s'; valid_objs sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct sa; valid_mdb s; no_0_obj' s'; valid_mdb sa; valid_list s; valid_mdb' s'; valid_list sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa; in_user_frame x s; in_user_frame x sa; valid_message_info info; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s'; length caps' \<le> msgMaxExtraCaps; \<forall>x\<in>set caps. real_cte_at (snd x) sa; \<forall>x\<in>set caps. \<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> cap.NullCap \<longrightarrow> cap = fst x); \<forall>x\<in>set caps. real_cte_at (snd x) s; recv_buf = Some x; (a, aa, b) \<in> set caps; is_aligned x msg_align_bits; typ_at' UserDataT (x && ~~ mask pageBits) s'; caps_of_state sa (aa, b) = Some cap; a \<noteq> cap.NullCap \<longrightarrow> cap = a; sa \<turnstile> cap\<rbrakk> \<Longrightarrow> sa \<turnstile> a
 2. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa x1 x2 x3 x4. \<lbrakk>info' = message_info_map info; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and valid_list and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (\<lambda>s. valid_message_info info) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) s'; (s, s') \<in> state_relation; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (\<lambda>s. \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length caps' \<le> msgMaxExtraCaps)) sa; info = Structures_A.message_info.MI x1 x2 x3 x4\<rbrakk> \<Longrightarrow> (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. (recv_buf = None \<longrightarrow> True) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> valid_pspace' s \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) \<and> True \<and> valid_objs' s \<and> True \<and> valid_ipc_buffer_ptr' x s \<and> (\<forall>a\<in>set caps'. case a of (cap, slot) \<Rightarrow> valid_cap' cap s \<and> cte_wp_at' (\<lambda>cte. cap \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> cap \<longrightarrow> cteCap cte = maskedAsFull cap cap) slot s) \<and> 2 + msg_max_length + 0 + length caps' < unat max_ipc_words))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa x1 x2 x3 x4 x a b. \<lbrakk>info' = Types_H.message_info.MI x1 x2 x3 x4; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (s, s') \<in> state_relation; info = Structures_A.message_info.MI x1 x2 x3 x4; tcb_at receiver s; tcb_at' receiver s'; tcb_at' receiver sa; valid_objs s; valid_objs' s'; valid_objs' sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned' sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct' sa; valid_mdb s; no_0_obj' s'; no_0_obj' sa; valid_list s; valid_mdb' s'; valid_mdb' sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x sa; in_user_frame x s; valid_ipc_buffer_ptr' x s'; valid_ipc_buffer_ptr' x sa; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) sa; x1 \<le> 0x78; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s'; length caps' \<le> 3; x2 \<le> 3; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s; recv_buf = Some x; (a, b) \<in> set caps'\<rbrakk> \<Longrightarrow> valid_cap' a sa \<and> cte_wp_at' (\<lambda>cte. a \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> a \<longrightarrow> cteCap cte = maskedAsFull a a) b sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa x1 x2 x3 x4 x a b. \<lbrakk>info' = Types_H.message_info.MI x1 x2 x3 x4; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (s, s') \<in> state_relation; info = Structures_A.message_info.MI x1 x2 x3 x4; tcb_at receiver s; tcb_at' receiver s'; tcb_at' receiver sa; valid_objs s; valid_objs' s'; valid_objs' sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned' sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct' sa; valid_mdb s; no_0_obj' s'; no_0_obj' sa; valid_list s; valid_mdb' s'; valid_mdb' sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x sa; in_user_frame x s; valid_ipc_buffer_ptr' x s'; valid_ipc_buffer_ptr' x sa; x1 \<le> 0x78; \<forall>x\<in>set caps'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s'; length caps' \<le> 3; x2 \<le> 3; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s; recv_buf = Some x; (a, b) \<in> set caps'; cte_wp_at' (\<lambda>cte. fst (a, b) \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst (a, b)) (snd (a, b)) sa\<rbrakk> \<Longrightarrow> valid_cap' a sa \<and> cte_wp_at' (\<lambda>cte. a \<noteq> capability.NullCap \<longrightarrow> cteCap cte \<noteq> a \<longrightarrow> cteCap cte = maskedAsFull a a) b sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa x1 x2 x3 x4 x a b cte. \<lbrakk>info' = Types_H.message_info.MI x1 x2 x3 x4; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (s, s') \<in> state_relation; info = Structures_A.message_info.MI x1 x2 x3 x4; tcb_at receiver s; tcb_at' receiver s'; tcb_at' receiver sa; valid_objs s; valid_objs' s'; valid_objs' sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned' sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct' sa; valid_mdb s; no_0_obj' s'; no_0_obj' sa; valid_list s; valid_mdb' s'; valid_mdb' sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x sa; in_user_frame x s; valid_ipc_buffer_ptr' x s'; valid_ipc_buffer_ptr' x sa; x1 \<le> 0x78; \<forall>x\<in>set caps'. \<exists>cte. ctes_of s' (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x); length caps' \<le> 3; x2 \<le> 3; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s; recv_buf = Some x; (a, b) \<in> set caps'; ctes_of sa b = Some cte; a \<noteq> capability.NullCap \<longrightarrow> cteCap cte = a\<rbrakk> \<Longrightarrow> valid_cap' a sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa x1 x2 x3 x4 x a b x1a x2a. \<lbrakk>info' = Types_H.message_info.MI x1 x2 x3 x4; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (s, s') \<in> state_relation; info = Structures_A.message_info.MI x1 x2 x3 x4; tcb_at receiver s; tcb_at' receiver s'; tcb_at' receiver sa; valid_objs s; valid_objs' s'; valid_objs' sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned' sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct' sa; valid_mdb s; no_0_obj' s'; no_0_obj' sa; valid_list s; valid_mdb' s'; valid_mdb' sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x sa; in_user_frame x s; valid_ipc_buffer_ptr' x s'; valid_ipc_buffer_ptr' x sa; x1 \<le> 0x78; \<forall>x\<in>set caps'. \<exists>cte. ctes_of s' (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x); length caps' \<le> 3; x2 \<le> 3; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s; recv_buf = Some x; (a, b) \<in> set caps'; ctes_of sa b = Some (CTE x1a x2a); a \<noteq> capability.NullCap \<longrightarrow> x1a = a\<rbrakk> \<Longrightarrow> valid_cap' a sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa x1 x2 x3 x4 x a b x1a x2a. \<lbrakk>info' = Types_H.message_info.MI x1 x2 x3 x4; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) caps caps'; (s, s') \<in> state_relation; info = Structures_A.message_info.MI x1 x2 x3 x4; tcb_at receiver s; tcb_at' receiver s'; tcb_at' receiver sa; valid_objs s; valid_objs' s'; valid_objs' sa; pspace_aligned s; pspace_aligned' s'; pspace_aligned' sa; pspace_distinct s; pspace_distinct' s'; pspace_distinct' sa; valid_mdb s; no_0_obj' s'; no_0_obj' sa; valid_list s; valid_mdb' s'; valid_mdb' sa; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s'; case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x sa; in_user_frame x s; valid_ipc_buffer_ptr' x s'; valid_ipc_buffer_ptr' x sa; x1 \<le> 0x78; \<forall>x\<in>set caps'. \<exists>cte. ctes_of s' (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x); length caps' \<le> 3; x2 \<le> 3; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s; recv_buf = Some x; (a, b) \<in> set caps'; ctes_of sa b = Some (CTE x1a x2a); a \<noteq> capability.NullCap \<longrightarrow> x1a = a; valid_cap' x1a sa\<rbrakk> \<Longrightarrow> valid_cap' a sa proof (prove)
goal:
No subgoals!