theory Ipc_R

lemma doNormalTransfer_corres:
  "corres dc
  (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \<Rightarrow> bool)
   and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct
   and (\<lambda>s. case ep of Some x \<Rightarrow> ep_at x s | _ \<Rightarrow> True)
   and case_option \<top> in_user_frame send_buf
   and case_option \<top> in_user_frame recv_buf)
  (tcb_at' sender and tcb_at' receiver and valid_objs'
   and pspace_aligned' and pspace_distinct' and cur_tcb'
   and valid_mdb' and no_0_obj'
   and (\<lambda>s. case ep of Some x \<Rightarrow> ep_at' x s | _ \<Rightarrow> True)
   and case_option \<top> valid_ipc_buffer_ptr' send_buf
   and case_option \<top> valid_ipc_buffer_ptr' recv_buf)
  (do_normal_transfer sender send_buf ep badge can_grant receiver recv_buf)
  (doNormalTransfer sender send_buf ep badge can_grant receiver recv_buf)" apply (simp add: do_normal_transfer_def doNormalTransfer_def) apply (rule corres_guard_imp) apply (rule corres_split_mapr[OF getMessageInfo_corres]) apply (rule_tac F="valid_message_info mi" in corres_gen_asm) apply (rule_tac r'="list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))"
                  in corres_split) apply (rule corres_if[OF refl]) apply (rule corres_split_catch) apply (rule lookupExtraCaps_corres; simp) apply (rule corres_trivial, simp) apply wp+ apply (rule corres_trivial, simp) apply simp apply (rule corres_split_eqr[OF copyMRs_corres]) apply (rule corres_split) apply (rule transferCaps_corres; simp) apply (rename_tac mi' mi'') apply (rule_tac F="mi_label mi' = mi_label mi"
                      in corres_gen_asm) apply (rule corres_split_nor[OF setMessageInfo_corres]) apply (case_tac mi', clarsimp) apply (simp add: badge_register_def badgeRegister_def) apply (fold dc_def) apply (rule asUser_setRegister_corres) apply wp apply simp+ apply ((wp valid_case_option_post_wp hoare_vcg_const_Ball_lift
                      hoare_case_option_wp
                      hoare_valid_ipc_buffer_ptr_typ_at' copyMRs_typ_at'
                      hoare_vcg_const_Ball_lift lookupExtraCaps_length
                    | simp add: if_apply_def2)+) apply (wp hoare_weak_lift_imp | strengthen valid_msg_length_strengthen)+ apply clarsimp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do_normal_transfer sender send_buf ep badge can_grant receiver recv_buf) (doNormalTransfer sender send_buf ep badge can_grant receiver recv_buf) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do mi <- get_message_info sender;
caps <- if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do tag <- getMessageInfo sender;
caps <- if can_grant then lookupExtraCaps sender send_buf tag <catch> const (return []) else return [];
msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength tag);
tag' <- transferCaps tag caps ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q4 ?Q'4 (do mi <- get_message_info sender;
caps <- if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do tag <- getMessageInfo sender;
caps <- if can_grant then lookupExtraCaps sender send_buf tag <catch> const (return []) else return [];
msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength tag);
tag' <- transferCaps tag caps ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> ?Q4 s
 3. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>mi. corres dc (?R8 mi) (?R'8 (message_info_map mi)) (do caps <- if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do caps <- if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) caps ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>?R'8\<rbrace>
 4. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 5. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>mi. valid_message_info mi \<Longrightarrow> corres dc (?P13 mi) (?R'8 (message_info_map mi)) (do caps <- if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do caps <- if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) caps ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. ?P13 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>?R'8\<rbrace>
 4. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 5. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?P14 mi) (?P'20 (message_info_map mi)) (if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return []) (if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [])
 2. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 3. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 4. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 5. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. ?P14 mi and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. ?P'20 a and ?Q'19 a\<rbrace>
 7. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 8. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?P21 mi) (?P'26 (message_info_map mi)) (lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return [])) (lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []))
 2. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 mi) (?Q'25 (message_info_map mi)) (return []) (return [])
 3. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 4. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 5. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 6. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then ?P21 mi else ?Q21 mi) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then ?P'26 a else ?Q'25 a) and ?Q'19 a\<rbrace>
 8. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 9. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (12 subgoals):
 1. \<And>mi. valid_message_info mi \<Longrightarrow> corres (?f29 mi \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?P29 mi) (?P'33 (message_info_map mi)) (lookup_extra_caps sender send_buf mi) (lookupExtraCaps sender send_buf (message_info_map mi))
 2. \<And>mi ft ft'. \<lbrakk>valid_message_info mi; ?f29 mi ft ft'\<rbrakk> \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?E29 mi ft) (?E'29 mi ft') (return []) (const (return []) ft')
 3. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q29 mi\<rbrace> lookup_extra_caps sender send_buf mi \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E29 mi\<rbrace>
 4. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'32 (message_info_map mi)\<rbrace> lookupExtraCaps sender send_buf (message_info_map mi) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'29 mi\<rbrace>
 5. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 mi) (?Q'25 (message_info_map mi)) (return []) (return [])
 6. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 8. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 9. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then ?P29 mi and ?Q29 mi else ?Q21 mi) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 10. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then ?P'33 a and ?Q'32 a else ?Q'25 a) and ?Q'19 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>mi ft ft'. \<lbrakk>valid_message_info mi; fr ft ft'\<rbrakk> \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?E29 mi ft) (?E'29 mi ft') (return []) (const (return []) ft')
 2. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q29 mi\<rbrace> lookup_extra_caps sender send_buf mi \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E29 mi\<rbrace>
 3. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'32 (message_info_map mi)\<rbrace> lookupExtraCaps sender send_buf (message_info_map mi) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'29 mi\<rbrace>
 4. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 mi) (?Q'25 (message_info_map mi)) (return []) (return [])
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 8. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and ?Q29 mi else ?Q21 mi) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and ?Q'32 a else ?Q'25 a) and ?Q'19 a\<rbrace>
 10. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q29 mi\<rbrace> lookup_extra_caps sender send_buf mi \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft _. True\<rbrace>
 2. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'32 (message_info_map mi)\<rbrace> lookupExtraCaps sender send_buf (message_info_map mi) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft' _. True\<rbrace>
 3. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 mi) (?Q'25 (message_info_map mi)) (return []) (return [])
 4. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 5. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 7. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and ?Q29 mi else ?Q21 mi) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 8. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and ?Q'32 a else ?Q'25 a) and ?Q'19 a\<rbrace>
 9. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 10. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>mi. valid_message_info mi \<Longrightarrow> corres (list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 mi) (?Q'25 (message_info_map mi)) (return []) (return [])
 2. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 3. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 4. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 5. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else ?Q21 mi) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else ?Q'25 a) and ?Q'19 a\<rbrace>
 7. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 8. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength (message_info_map mi));
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 3. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 4. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 6. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 7. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R14 mi rv) (?R'14 mi rv') (do mrs_transferred <- copy_mrs sender send_buf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do msgTransferred <- copyMRs sender send_buf receiver recv_buf (mi_length mi);
tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?R14 mi\<rbrace>
 3. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>?R'14 mi\<rbrace>
 4. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 6. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 7. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R65 mi rv rv' rva) (?R'65 mi rv rv' rva) (do mi' <- transfer_caps mi rv ep receiver recv_buf;
y <- set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do tag' <- transferCaps (message_info_map mi) rv' ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. rva) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>?R65 mi rv rv'\<rbrace>
 3. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>?R'65 mi rv rv'\<rbrace>
 4. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 5. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 6. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 8. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
 9. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (12 subgoals):
 1. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> corres (?r'81 mi rv rv' rva) (?P81 mi rv rv' rva) (?P'81 mi rv rv' rva) (transfer_caps mi rv ep receiver recv_buf) (transferCaps (message_info_map mi) rv' ep receiver recv_buf)
 2. \<And>mi rv rv' rva rvb rv'a. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ?r'81 mi rv rv' rva rvb rv'a\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R81 mi rv rv' rva rvb) (?R'81 mi rv rv' rva rv'a) (do y <- set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps rvb) (mi_caps_unwrapped rvb) (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do y <- setMessageInfo receiver (msgLength_update (\<lambda>_. rva) rv'a);
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>?R81 mi rv rv' rva\<rbrace>
 4. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>?R'81 mi rv rv' rva\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. ?P81 mi rv rv' rva and ?Q81 mi rv rv' rva\<rbrace>
 6. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. ?P'81 mi rv rv' rva and ?Q'81 mi rv rv' rva\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 8. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 9. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 10. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>mi rv rv' rva rvb rv'a. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) rvb rv'a\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R81 mi rv rv' rva rvb) (?R'81 mi rv rv' rva rv'a) (do y <- set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps rvb) (mi_caps_unwrapped rvb) (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do y <- setMessageInfo receiver (msgLength_update (\<lambda>_. rva) rv'a);
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>?R81 mi rv rv' rva\<rbrace>
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>?R'81 mi rv rv' rva\<rbrace>
 4. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 8. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 10. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R81 mi rv rv' rva mi') (?R'81 mi rv rv' rva mi'') (do y <- set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do y <- setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>?R81 mi rv rv' rva\<rbrace>
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>?R'81 mi rv rv' rva\<rbrace>
 4. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 8. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 10. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?P96 mi rv rv' rva mi') (?R'81 mi rv rv' rva mi'') (do y <- set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user receiver (setRegister badge_register badge)
od) (do y <- setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. ?P96 mi rv rv' rva mi' and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>?R'81 mi rv rv' rva\<rbrace>
 4. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 8. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 10. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> msgLength_update (\<lambda>_. rva) mi'' = message_info_map (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi))
 2. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R97 mi rv rv' rva mi' mi'') (?R'97 mi rv rv' rva mi' mi'') (as_user receiver (setRegister badge_register badge)) (asUser receiver (setRegister Notification_H.badgeRegister badge))
 3. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 mi rv rv' rva mi'\<rbrace> set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi)) \<lbrace>\<lambda>x. ?R97 mi rv rv' rva mi' mi''\<rbrace>
 4. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. ?R'97 mi rv rv' rva mi' mi''\<rbrace>
 5. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and ?Q100 mi rv rv' rva mi' and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 6. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 7. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 8. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 9. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 10. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R97 mi rv rv' rva mi' mi'') (?R'97 mi rv rv' rva mi' mi'') (as_user receiver (setRegister badge_register badge)) (asUser receiver (setRegister Notification_H.badgeRegister badge))
 2. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 mi rv rv' rva mi'\<rbrace> set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi)) \<lbrace>\<lambda>x. ?R97 mi rv rv' rva mi' mi''\<rbrace>
 3. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. ?R'97 mi rv rv' rva mi' mi''\<rbrace>
 4. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and ?Q100 mi rv rv' rva mi' and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 5. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 6. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 7. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 8. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 9. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 10. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; message_info_map mi' = mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R97 mi rv rv' rva mi' mi'') (?R'97 mi rv rv' rva mi' mi'') (as_user receiver (setRegister ARM.badgeRegister badge)) (asUser receiver (setRegister ARM.badgeRegister badge))
 2. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 mi rv rv' rva mi'\<rbrace> set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi)) \<lbrace>\<lambda>x. ?R97 mi rv rv' rva mi' mi''\<rbrace>
 3. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. ?R'97 mi rv rv' rva mi' mi''\<rbrace>
 4. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and ?Q100 mi rv rv' rva mi' and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 5. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 6. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 7. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 8. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 9. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 10. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; message_info_map mi' = mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> corres dc (?R97 mi rv rv' rva mi' mi'') (?R'97 mi rv rv' rva mi' mi'') (as_user receiver (setRegister ARM.badgeRegister badge)) (asUser receiver (setRegister ARM.badgeRegister badge))
 2. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 mi rv rv' rva mi'\<rbrace> set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi)) \<lbrace>\<lambda>x. ?R97 mi rv rv' rva mi' mi''\<rbrace>
 3. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. ?R'97 mi rv rv' rva mi' mi''\<rbrace>
 4. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and ?Q100 mi rv rv' rva mi' and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 5. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 6. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 7. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 8. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 9. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 10. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q100 mi rv rv' rva mi'\<rbrace> set_message_info receiver (Structures_A.message_info.MI rva (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi)) \<lbrace>\<lambda>x. tcb_at receiver\<rbrace>
 2. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. tcb_at' receiver\<rbrace>
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and ?Q100 mi rv rv' rva mi' and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 4. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 6. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 8. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 9. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 10. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; ((=) \<circ> message_info_map) mi' mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. tcb_at' receiver\<rbrace>
 2. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and tcb_at receiver and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 4. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 8. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 10. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>mi rv rv' rva mi' mi''. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'; message_info_map mi' = mi''; mi_label mi' = mi_label mi\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 mi rv rv' rva mi''\<rbrace> setMessageInfo receiver (msgLength_update (\<lambda>_. rva) mi'') \<lbrace>\<lambda>x. tcb_at' receiver\<rbrace>
 2. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q81 mi rv rv' rva\<rbrace> transfer_caps mi rv ep receiver recv_buf \<lbrace>\<lambda>mi'. tcb_at receiver and tcb_at receiver and (\<lambda>s. mi_label mi' = mi_label mi)\<rbrace>
 3. \<And>mi rv rv' rva. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 mi rv rv' rva\<rbrace> transferCaps (message_info_map mi) rv' ep receiver recv_buf \<lbrace>\<lambda>mi''. tcb_at' receiver and ?Q'102 mi rv rv' rva mi''\<rbrace>
 4. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 mi rv\<rbrace> copy_mrs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 mi) and (\<lambda>s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and ?Q81 mi rv rv' rva\<rbrace>
 5. \<And>mi rv rv'. \<lbrakk>valid_message_info mi; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 mi rv'\<rbrace> copyMRs sender send_buf receiver recv_buf (mi_length mi) \<lbrace>\<lambda>rva. 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 rv'. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) and (\<lambda>s. length rv' \<le> msgMaxExtraCaps) and ?Q'81 mi rv rv' rva\<rbrace>
 6. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q14 mi\<rbrace> if can_grant then lookup_extra_caps sender send_buf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>rv. tcb_at sender and tcb_at receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and K (unat (mi_length mi) \<le> msg_max_length) and ?Q72 mi rv\<rbrace>
 7. \<And>mi. valid_message_info mi \<Longrightarrow> \<lbrace>?Q'19 (message_info_map mi)\<rbrace> if can_grant then lookupExtraCaps sender send_buf (message_info_map mi) <catch> const (return []) else return [] \<lbrace>\<lambda>rv'. tcb_at' sender and tcb_at' receiver and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'77 mi rv'\<rbrace>
 8. \<lbrace>?Q8\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. (if can_grant then valid_objs and pspace_aligned and tcb_at sender and (\<lambda>_. valid_message_info mi) and (\<lambda>s. True \<and> True) else (\<lambda>_. True)) and ?Q14 mi and (\<lambda>s. valid_message_info mi)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and ?Q'19 a\<rbrace>
 10. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'602\<rbrace> get_message_info sender \<lbrace>\<lambda>mi s. (can_grant \<longrightarrow> valid_message_info mi) \<and> (can_grant \<longrightarrow> tcb_at sender s \<and> tcb_at receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> unat (mi_length mi) \<le> msg_max_length \<and> 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>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_message_info mi \<and> tcb_at receiver s \<and> tcb_at sender s \<and> tcb_at receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> unat (mi_length mi) \<le> msg_max_length \<and> 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>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_message_info mi \<and> valid_objs s \<and> tcb_at receiver s) \<and> (\<not> can_grant \<longrightarrow> tcb_at sender s \<and> tcb_at receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> unat (mi_length mi) \<le> msg_max_length \<and> 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>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_message_info mi \<and> tcb_at receiver s) \<and> valid_message_info mi\<rbrace>
 2. \<lbrace>?Q'8\<rbrace> getMessageInfo sender \<lbrace>\<lambda>a. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) and (\<lambda>aa. (can_grant \<longrightarrow> tcb_at' sender aa \<and> tcb_at' receiver aa \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> tcb_at' receiver aa \<and> valid_objs' aa \<and> pspace_aligned' aa \<and> pspace_distinct' aa \<and> no_0_obj' aa \<and> valid_mdb' aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x aa) \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) aa) \<and> length [] \<le> msgMaxExtraCaps \<and> tcb_at' receiver aa \<and> tcb_at' sender aa \<and> tcb_at' receiver aa \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> tcb_at' receiver aa \<and> valid_objs' aa \<and> pspace_aligned' aa \<and> pspace_distinct' aa \<and> no_0_obj' aa \<and> valid_mdb' aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x aa) \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> True \<and> unat (msgExtraCaps a) \<le> msgMaxExtraCaps \<and> tcb_at' receiver aa \<and> tcb_at' receiver aa) \<and> (\<not> can_grant \<longrightarrow> tcb_at' sender aa \<and> tcb_at' receiver aa \<and> (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> tcb_at' receiver aa \<and> valid_objs' aa \<and> pspace_aligned' aa \<and> pspace_distinct' aa \<and> no_0_obj' aa \<and> valid_mdb' aa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x aa) \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) aa \<and> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) aa) \<and> length [] \<le> msgMaxExtraCaps \<and> tcb_at' receiver aa \<and> tcb_at' receiver aa))\<rbrace>
 3. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ((\<lambda>s. can_grant \<longrightarrow> valid_objs s) and ((\<lambda>s. can_grant \<longrightarrow> pspace_aligned s) and ((\<lambda>s. can_grant \<longrightarrow> tcb_at sender s) and ?P'602)))) s
 4. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at sender and tcb_at receiver and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> (tcb_at sender and ((\<lambda>s. can_grant \<longrightarrow> valid_objs s) and ((\<lambda>s. can_grant \<longrightarrow> pspace_aligned s) and ((\<lambda>s. can_grant \<longrightarrow> tcb_at sender s) and (\<lambda>s. (can_grant \<longrightarrow> valid_mdb s) \<and> (can_grant \<longrightarrow> tcb_at sender s \<and> tcb_at receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_mdb s \<and> 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>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_mdb s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> tcb_at receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_mdb s \<and> 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>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at receiver s) \<and> (\<not> can_grant \<longrightarrow> tcb_at sender s \<and> tcb_at receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_mdb s \<and> 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>a. True | Some x2 \<Rightarrow> in_user_frame x2) s \<and> valid_mdb s \<and> tcb_at receiver s) \<and> valid_mdb s))))) s
 2. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and (\<lambda>s. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) s \<and> (can_grant \<longrightarrow> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> 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>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<and> length [] \<le> msgMaxExtraCaps \<and> tcb_at' receiver s \<and> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> 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>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> True \<and> True \<and> tcb_at' receiver s \<and> tcb_at' receiver s) \<and> (\<not> can_grant \<longrightarrow> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> 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>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<and> length [] \<le> msgMaxExtraCaps \<and> tcb_at' receiver s \<and> tcb_at' receiver s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' sender and tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2) and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> (tcb_at' sender and (\<lambda>s. (if can_grant then valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' sender and (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (\<lambda>a. True \<and> True) else (\<lambda>a. True)) s \<and> (can_grant \<longrightarrow> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> 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>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<and> length [] \<le> msgMaxExtraCaps \<and> tcb_at' receiver s \<and> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> 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>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> True \<and> True \<and> tcb_at' receiver s \<and> tcb_at' receiver s) \<and> (\<not> can_grant \<longrightarrow> tcb_at' sender s \<and> tcb_at' receiver s \<and> (case send_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> 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>a. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) s \<and> (\<forall>x\<in>set []. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<and> length [] \<le> msgMaxExtraCaps \<and> tcb_at' receiver s \<and> tcb_at' receiver s))) s proof (prove)
goal:
No subgoals!