theory Syscall_R

lemma hinv_corres_assist:
  "\<lbrakk> info' = message_info_map info \<rbrakk>
       \<Longrightarrow> corres (fr \<oplus> (\<lambda>(p, cap, extracaps, buffer) (p', capa, extracapsa, buffera).
        p' = cte_map p \<and> cap_relation cap capa \<and> buffer = buffera \<and>
        list_all2
         (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))
         extracaps extracapsa))

           (invs and tcb_at thread and (\<lambda>_. valid_message_info info))
           (invs' and tcb_at' thread)
           (doE (cap, slot) \<leftarrow>
                cap_fault_on_failure cptr' False
                 (lookup_cap_and_slot thread (to_bl cptr'));
                do
                   buffer \<leftarrow> lookup_ipc_buffer False thread;
                   doE extracaps \<leftarrow> lookup_extra_caps thread buffer info;
                       returnOk (slot, cap, extracaps, buffer)
                   odE
                od
            odE)
           (doE (cap, slot) \<leftarrow> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr');
               do buffer \<leftarrow> VSpace_H.lookupIPCBuffer False thread;
                  doE extracaps \<leftarrow> lookupExtraCaps thread buffer info';
                      returnOk (slot, cap, extracaps, buffer)
                  odE
               od
            odE)" apply (clarsimp simp add: split_def) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF corres_cap_fault])
       \<comment> \<open>switched over to argument of corres_cap_fault\<close> apply (rule lookupCapAndSlot_corres, simp) apply (rule corres_split[OF lookupIPCBuffer_corres]) apply (rule corres_splitEE) apply (rule lookupExtraCaps_corres; simp) apply (rule corres_returnOkTT) apply (wp | simp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. info' = message_info_map info \<Longrightarrow> corres (fr \<oplus> (\<lambda>(p, cap, extracaps, buffer) (p', capa, extracapsa, buffera). p' = cte_map p \<and> cap_relation cap capa \<and> buffer = buffera \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) extracaps extracapsa)) (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) (invs' and tcb_at' thread) (doE (cap, slot) <- cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr'));
do buffer <- lookup_ipc_buffer False thread;
doE extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) (doE (cap, slot) <- capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr');
do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer info';
returnOk (slot, cap, extracaps, buffer)
odE
od
odE) proof (prove)
goal (1 subgoal):
 1. info' = message_info_map info \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) (invs' and tcb_at' thread) (doE p <- cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr'));
do buffer <- lookup_ipc_buffer False thread;
doE extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE
od
odE) (doE p <- capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr');
do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer (message_info_map info);
returnOk (snd p, fst p, extracaps, buffer)
odE
od
odE) proof (prove)
goal (3 subgoals):
 1. info' = message_info_map info \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) ?Q1 ?Q'1 (doE p <- cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr'));
do buffer <- lookup_ipc_buffer False thread;
doE extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE
od
odE) (doE p <- capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr');
do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer (message_info_map info);
returnOk (snd p, fst p, extracaps, buffer)
odE
od
odE)
 2. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. info' = message_info_map info \<Longrightarrow> corres (lfr \<oplus> ?r'5) ?P5 ?P'5 (lookup_cap_and_slot thread (to_bl cptr')) (lookupCapAndSlot thread cptr')
 2. \<And>p pa. \<lbrakk>info' = message_info_map info; ?r'5 p pa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) (?R5 p) (?R'5 pa) (do buffer <- lookup_ipc_buffer False thread;
doE extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE
od) (do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer (message_info_map info);
returnOk (snd pa, fst pa, extracaps, buffer)
odE
od)
 3. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q5\<rbrace> cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr')) \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q'5\<rbrace> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr') \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) (?R5 p) (?R'5 pa) (do buffer <- lookup_ipc_buffer False thread;
doE extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE
od) (do buffer <- lookupIPCBuffer False thread;
doE extracaps <- lookupExtraCaps thread buffer (message_info_map info);
returnOk (snd pa, fst pa, extracaps, buffer)
odE
od)
 2. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q5\<rbrace> cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr')) \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q'5\<rbrace> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr') \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 5. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) (?R13 p pa buffer) (?R'13 p pa buffera) (doE extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (doE extracaps <- lookupExtraCaps thread buffera (message_info_map info);
returnOk (snd pa, fst pa, extracaps, buffera)
odE)
 2. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 p\<rbrace> lookup_ipc_buffer False thread \<lbrace>?R13 p pa\<rbrace>
 3. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pa\<rbrace> lookupIPCBuffer False thread \<lbrace>?R'13 p pa\<rbrace>
 4. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q5\<rbrace> cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr')) \<lbrace>\<lambda>p. tcb_at thread and invs and ?Q16 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q'5\<rbrace> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr') \<lbrace>\<lambda>pa. tcb_at' thread and invs' and ?Q'18 pa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'5) s proof (prove)
goal (10 subgoals):
 1. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> corres (fr \<oplus> ?r'22 p pa buffer buffera) (?P23 p pa buffer) (?P'25 p pa buffera) (lookup_extra_caps thread buffer info) (lookupExtraCaps thread buffera (message_info_map info))
 2. \<And>p pa buffer buffera extracaps extracapsa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera; ?r'22 p pa buffer buffera extracaps extracapsa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) (?R22 p pa buffer buffera extracaps) (?R'22 p pa buffer buffera extracapsa) (returnOk (snd p, fst p, extracaps, buffer)) (returnOk (snd pa, fst pa, extracapsa, buffera))
 3. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 p pa buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>?R22 p pa buffer buffera\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 p pa buffera\<rbrace> lookupExtraCaps thread buffera (message_info_map info) \<lbrace>?R'22 p pa buffer buffera\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 p\<rbrace> lookup_ipc_buffer False thread \<lbrace>\<lambda>buffer. ?P23 p pa buffer and ?Q24 p pa buffer\<rbrace>
 6. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pa\<rbrace> lookupIPCBuffer False thread \<lbrace>\<lambda>buffera. ?P'25 p pa buffera and ?Q'26 p pa buffera\<rbrace>
 7. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q5\<rbrace> cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr')) \<lbrace>\<lambda>p. tcb_at thread and invs and ?Q16 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q'5\<rbrace> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr') \<lbrace>\<lambda>pa. tcb_at' thread and invs' and ?Q'18 pa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 10. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>p pa buffer buffera extracaps extracapsa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) extracaps extracapsa\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>p pa. fst pa = cte_map (fst p) \<and> cap_relation (fst (snd p)) (fst (snd pa)) \<and> snd (snd (snd p)) = snd (snd (snd pa)) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd p))) (fst (snd (snd pa))))) (?R22 p pa buffer buffera extracaps) (?R'22 p pa buffer buffera extracapsa) (returnOk (snd p, fst p, extracaps, buffer)) (returnOk (snd pa, fst pa, extracapsa, buffera))
 2. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 p pa buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>?R22 p pa buffer buffera\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 p pa buffera\<rbrace> lookupExtraCaps thread buffera (message_info_map info) \<lbrace>?R'22 p pa buffer buffera\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 p\<rbrace> lookup_ipc_buffer False thread \<lbrace>\<lambda>buffer. valid_objs and pspace_aligned and tcb_at thread and (\<lambda>_. valid_message_info info) and ?Q24 p pa buffer\<rbrace>
 5. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pa\<rbrace> lookupIPCBuffer False thread \<lbrace>\<lambda>buffera. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffera of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'26 p pa buffera\<rbrace>
 6. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q5\<rbrace> cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr')) \<lbrace>\<lambda>p. tcb_at thread and invs and ?Q16 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q'5\<rbrace> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr') \<lbrace>\<lambda>pa. tcb_at' thread and invs' and ?Q'18 pa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 9. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>p pa buffer buffera extracaps extracapsa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) extracaps extracapsa\<rbrakk> \<Longrightarrow> fst (snd pa, fst pa, extracapsa, buffera) = cte_map (fst (snd p, fst p, extracaps, buffer)) \<and> cap_relation (fst (snd (snd p, fst p, extracaps, buffer))) (fst (snd (snd pa, fst pa, extracapsa, buffera))) \<and> snd (snd (snd (snd p, fst p, extracaps, buffer))) = snd (snd (snd (snd pa, fst pa, extracapsa, buffera))) \<and> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (fst (snd (snd (snd p, fst p, extracaps, buffer)))) (fst (snd (snd (snd pa, fst pa, extracapsa, buffera))))
 2. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 p pa buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>\<lambda>extracaps _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>p pa buffer buffera. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p); buffer = buffera\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 p pa buffera\<rbrace> lookupExtraCaps thread buffera (message_info_map info) \<lbrace>\<lambda>extracapsa _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 p\<rbrace> lookup_ipc_buffer False thread \<lbrace>\<lambda>buffer. valid_objs and pspace_aligned and tcb_at thread and (\<lambda>_. valid_message_info info) and ?Q24 p pa buffer\<rbrace>
 5. \<And>p pa. \<lbrakk>info' = message_info_map info; cap_relation (fst p) (fst pa) \<and> snd pa = cte_map (snd p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pa\<rbrace> lookupIPCBuffer False thread \<lbrace>\<lambda>buffera. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffera of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'26 p pa buffera\<rbrace>
 6. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q5\<rbrace> cap_fault_on_failure cptr' False (lookup_cap_and_slot thread (to_bl cptr')) \<lbrace>\<lambda>p. tcb_at thread and invs and ?Q16 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. info' = message_info_map info \<Longrightarrow> \<lbrace>?Q'5\<rbrace> capFaultOnFailure cptr' False (lookupCapAndSlot thread cptr') \<lbrace>\<lambda>pa. tcb_at' thread and invs' and ?Q'18 pa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s. \<lbrakk>info' = message_info_map info; (invs and tcb_at thread and (\<lambda>_. valid_message_info info)) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread and ?Q5) s
 9. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>info' = message_info_map info; invs s \<and> tcb_at thread s \<and> valid_message_info info\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s
 2. \<And>s. \<lbrakk>info' = message_info_map info; (invs' and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (\<lambda>s. True \<and> (tcb_at' thread and invs' and (\<lambda>s. (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s \<and> valid_objs' s \<and> True \<and> True)) s)) s proof (prove)
goal:
No subgoals!