theory Ipc_R

lemma lookupExtraCaps_corres:
  "\<lbrakk> info' = message_info_map info; buffer = buffer'\<rbrakk> \<Longrightarrow>
  corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)))
   (valid_objs and pspace_aligned and tcb_at thread and (\<lambda>_. valid_message_info info))
   (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread
        and case_option \<top> valid_ipc_buffer_ptr' buffer')
   (lookup_extra_caps thread buffer info) (lookupExtraCaps thread buffer' info')" unfolding lookupExtraCaps_def lookup_extra_caps_def apply (rule corres_gen_asm) apply (cases "mi_extra_caps info = 0") apply (cases info) apply (simp add: Let_def returnOk_def getExtraCPtrs_def
                    liftE_bindE upto_enum_step_def mapM_def
                    sequence_def doMachineOp_return mapME_Nil
             split: option.split) apply (cases info) apply (rename_tac w1 w2 w3 w4) apply (simp add: Let_def liftE_bindE) apply (cases buffer') apply (simp add: getExtraCPtrs_def mapME_Nil) apply (rule corres_returnOk) apply simp apply (simp add: msgLengthBits_def msgMaxLength_def word_size field_simps
                   getExtraCPtrs_def upto_enum_step_def upto_enum_word
                   word_size_def msg_max_length_def liftM_def
                   Suc_unat_diff_1 word_le_sub1 mapM_map_simp
                   upt_lhs_sub_map[where x=buffer_cptr_index]
                   wordSize_def wordBits_def
              del: upt.simps) apply (rule corres_guard_imp) apply (rule corres_underlying_split) apply (rule_tac S = "\<lambda>x y. x = y \<and> x < unat w2"
               in corres_mapM_list_all2
         [where Q = "\<lambda>_. valid_objs and pspace_aligned and tcb_at thread" and r = "(=)"
            and Q' = "\<lambda>_. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread
              and case_option \<top> valid_ipc_buffer_ptr' buffer'" and r'="(=)" ]) apply simp apply simp apply simp apply (rule corres_guard_imp) apply (rule loadWordUser_corres') apply (clarsimp simp: buffer_cptr_index_def msg_max_length_def
                                   max_ipc_words valid_message_info_def
                                   msg_max_extra_caps_def word_le_nat_alt) apply (simp add: buffer_cptr_index_def msg_max_length_def) apply simp apply simp apply (simp add: load_word_offs_word_def) apply (wp | simp)+ apply (subst list_all2_same) apply (clarsimp simp: max_ipc_words field_simps) apply (simp add: mapME_def, fold mapME_def)[1] apply (rule corres_mapME [where S = Id and r'="(\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))"]) apply simp apply simp apply simp apply (rule corres_cap_fault [OF lookupCapAndSlot_corres]) apply simp apply simp apply (wp | simp)+ apply (simp add: set_zip_same Int_lower1) apply (wp mapM_wp [OF _ subset_refl] | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info' = message_info_map info; buffer = buffer'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread and (\<lambda>_. valid_message_info info)) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (lookup_extra_caps thread buffer info) (lookupExtraCaps thread buffer' info') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info' = message_info_map info; buffer = buffer'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread and (\<lambda>_. valid_message_info info)) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info = 0\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr))
 2. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info \<noteq> 0\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info = 0; info = Structures_A.message_info.MI x1 x2 x3 x4\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr))
 2. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info \<noteq> 0\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info \<noteq> 0\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info \<noteq> 0; info = Structures_A.message_info.MI x1 x2 x3 x4\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4. \<lbrakk>info' = message_info_map info; buffer = buffer'; valid_message_info info; mi_extra_caps info \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((liftE $ get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr)) ((withoutFailure $ getExtraCPtrs buffer' info') >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False $ lookupCapAndSlot thread cptr)) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = buffer'; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (get_extra_cptrs buffer' (Structures_A.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr))) (getExtraCPtrs buffer' (Types_H.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr))) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = buffer'; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = None\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (get_extra_cptrs buffer' (Structures_A.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr))) (getExtraCPtrs buffer' (Types_H.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)))
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = buffer'; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (get_extra_cptrs buffer' (Structures_A.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr))) (getExtraCPtrs buffer' (Types_H.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr))) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = None; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = None\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) (returnOk []) (returnOk [])
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = buffer'; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (get_extra_cptrs buffer' (Structures_A.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr))) (getExtraCPtrs buffer' (Types_H.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr))) proof (prove)
goal (2 subgoals):
 1. \<And>w1 w2 w3 w4 s s'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = None; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = None; (s, s') \<in> state_relation; (valid_objs and pspace_aligned and tcb_at thread) s; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) s'\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) [] []
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = buffer'; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (get_extra_cptrs buffer' (Structures_A.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr))) (getExtraCPtrs buffer' (Types_H.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr))) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = buffer'; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (get_extra_cptrs buffer' (Structures_A.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr))) (getExtraCPtrs buffer' (Types_H.message_info.MI w1 w2 w3 w4) >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr))) proof (prove)
goal (1 subgoal):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) (do x <- mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2];
mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)
od) (mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr))) proof (prove)
goal (3 subgoals):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q17 w1 w2 w3 w4 a) (?Q'17 w1 w2 w3 w4 a) (do x <- mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2];
mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)
od) (mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] >>= mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)))
 2. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> ?Q17 w1 w2 w3 w4 a s
 3. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> ?Q'17 w1 w2 w3 w4 a s proof (prove)
goal (6 subgoals):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> corres (?r'21 w1 w2 w3 w4 a) (?Q17 w1 w2 w3 w4 a) (?Q'17 w1 w2 w3 w4 a) (mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2]) (mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2])
 2. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; ?r'21 w1 w2 w3 w4 a x rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 w1 w2 w3 w4 a\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 4. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 w1 w2 w3 w4 a\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 5. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> ?Q17 w1 w2 w3 w4 a s
 6. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> ?Q'17 w1 w2 w3 w4 a s proof (prove)
goal (11 subgoals):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>w1 w2 w3 w4 a x xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; xs = ys; x = y\<rbrakk> \<Longrightarrow> x # xs = y # ys
 3. \<And>w1 w2 w3 w4 a x xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> corres (=) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((load_word_offs a \<circ> (+) buffer_cptr_index) x) ((loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y)
 4. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 5. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 7. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; xs = ys; x = y\<rbrakk> \<Longrightarrow> x # xs = y # ys
 2. \<And>w1 w2 w3 w4 a x xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> corres (=) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((load_word_offs a \<circ> (+) buffer_cptr_index) x) ((loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y)
 3. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 4. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 5. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 6. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (9 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> corres (=) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) ((load_word_offs a \<circ> (+) buffer_cptr_index) x) ((loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y)
 2. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 4. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (9 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> corres (=) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and valid_ipc_buffer_ptr' a) (load_word_offs a (buffer_cptr_index + x)) (loadWordUser (a + (0x1E8 + word_of_nat x * 4)))
 2. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 4. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (11 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> corres (=) (?Q28 w1 w2 w3 w4 a x xs ys) (?Q'28 w1 w2 w3 w4 a x xs ys) (load_word_offs a (buffer_cptr_index + x)) (loadWordUser (a + (0x1E8 + word_of_nat x * 4)))
 2. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> ?Q28 w1 w2 w3 w4 a x xs ys s
 3. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> ?Q'28 w1 w2 w3 w4 a x xs ys s
 4. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 5. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 7. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> buffer_cptr_index + x < unat max_ipc_words
 2. \<And>w1 w2 w3 w4 a x xs ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> 0x1E8 + word_of_nat x * 4 = word_of_nat (buffer_cptr_index + x) * 4
 3. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> True
 4. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_ptr' a s
 5. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 6. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 8. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 9. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 10. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys\<rbrakk> \<Longrightarrow> 0x1E8 + word_of_nat x * 4 = word_of_nat (buffer_cptr_index + x) * 4
 2. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> True
 3. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_ptr' a s
 4. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 5. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 7. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> True
 2. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_ptr' a s
 3. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 4. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 5. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 6. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (9 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs ys s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; list_all2 (\<lambda>x y. x = y \<and> x < unat w2) xs ys; (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_ptr' a s
 2. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 4. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (8 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> (load_word_offs a \<circ> (+) buffer_cptr_index) x \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 2. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 5. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (8 subgoals):
 1. \<And>w1 w2 w3 w4 a x xs. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x < unat w2; suffix (x # xs) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> load_word_offs a (buffer_cptr_index + x) \<lbrace>\<lambda>r. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 2. \<And>w1 w2 w3 w4 a x y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = y \<and> x < unat w2; suffix (y # ys) [0..<unat w2]\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) y \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 5. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (6 subgoals):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. x = y \<and> x < unat w2) [0..<unat w2] [0..<unat w2]
 2. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 4. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 5. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 6. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (6 subgoals):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0..<unat w2]. x = x \<and> x < unat w2
 2. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 4. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 5. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 6. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (5 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a x) (?Q'21 w1 w2 w3 w4 a rv') (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) (map to_bl x)) (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 4. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 5. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (5 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a rv') (?Q'21 w1 w2 w3 w4 a rv') (mapME ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) rv') (mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) rv')
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 4. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 5. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (11 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) [] []
 2. \<And>w1 w2 w3 w4 a x rv' xa xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) xs ys; cap_relation (fst xa) (fst y) \<and> snd y = cte_map (snd xa)\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (xa # xs) (y # ys)
 3. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a rv') (?Q'21 w1 w2 w3 w4 a rv') (((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa) (capFaultOnFailure y False (lookupCapAndSlot thread y))
 4. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 w1 w2 w3 w4 a rv'\<rbrace> ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa \<lbrace>\<lambda>rv. ?Q21 w1 w2 w3 w4 a rv'\<rbrace>
 5. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 w1 w2 w3 w4 a rv'\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. ?Q'21 w1 w2 w3 w4 a rv'\<rbrace>
 6. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 7. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv' xa xs y ys. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) xs ys; cap_relation (fst xa) (fst y) \<and> snd y = cte_map (snd xa)\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x)) (xa # xs) (y # ys)
 2. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a rv') (?Q'21 w1 w2 w3 w4 a rv') (((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa) (capFaultOnFailure y False (lookupCapAndSlot thread y))
 3. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 w1 w2 w3 w4 a rv'\<rbrace> ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa \<lbrace>\<lambda>rv. ?Q21 w1 w2 w3 w4 a rv'\<rbrace>
 4. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 w1 w2 w3 w4 a rv'\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. ?Q'21 w1 w2 w3 w4 a rv'\<rbrace>
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 6. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 10. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (9 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a rv') (?Q'21 w1 w2 w3 w4 a rv') (((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa) (capFaultOnFailure y False (lookupCapAndSlot thread y))
 2. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 w1 w2 w3 w4 a rv'\<rbrace> ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa \<lbrace>\<lambda>rv. ?Q21 w1 w2 w3 w4 a rv'\<rbrace>
 3. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 w1 w2 w3 w4 a rv'\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. ?Q'21 w1 w2 w3 w4 a rv'\<rbrace>
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (9 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; xa = y\<rbrakk> \<Longrightarrow> corres (fr \<oplus> (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))) (?Q21 w1 w2 w3 w4 a rv') (?Q'21 w1 w2 w3 w4 a rv') (cap_fault_on_failure y False (lookup_cap_and_slot thread (to_bl y))) (capFaultOnFailure y False (lookupCapAndSlot thread y))
 2. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 w1 w2 w3 w4 a rv'\<rbrace> ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa \<lbrace>\<lambda>rv. ?Q21 w1 w2 w3 w4 a rv'\<rbrace>
 3. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 w1 w2 w3 w4 a rv'\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. ?Q'21 w1 w2 w3 w4 a rv'\<rbrace>
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>?Q21 w1 w2 w3 w4 a\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>?Q'21 w1 w2 w3 w4 a\<rbrace>
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (9 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; xa = y\<rbrakk> \<Longrightarrow> to_bl y = to_bl y
 2. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 5. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 7. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 9. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (8 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> ((\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)) \<circ> to_bl) xa \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 2. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 5. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 7. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (8 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; xa = y\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> cap_fault_on_failure y False (lookup_cap_and_slot thread (to_bl y)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 2. \<And>w1 w2 w3 w4 a x rv' xa y. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'; (xa, y) \<in> Id\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace> capFaultOnFailure y False (lookupCapAndSlot thread y) \<lbrace>\<lambda>rv. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> length rv' = length rv'
 4. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 5. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 6. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 7. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 8. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (5 subgoals):
 1. \<And>w1 w2 w3 w4 a x rv'. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; x = rv'\<rbrakk> \<Longrightarrow> set (zip rv' rv') \<subseteq> Id
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 4. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 5. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (4 subgoals):
 1. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and tcb_at thread\<rbrace> mapM (load_word_offs a \<circ> (+) buffer_cptr_index) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs and pspace_aligned and tcb_at thread\<rbrace>
 2. \<And>w1 w2 w3 w4 a. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> mapM (loadWordUser \<circ> (\<lambda>x. a + (x * 4 + 0x1E4)) \<circ> ((\<lambda>x. x + 1) \<circ> word_of_nat)) [0..<unat w2] \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread\<rbrace>
 3. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs and pspace_aligned and tcb_at thread) s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at thread) s
 4. \<And>w1 w2 w3 w4 a s. \<lbrakk>info' = Types_H.message_info.MI w1 w2 w3 w4; buffer = Some a; valid_message_info (Structures_A.message_info.MI w1 w2 w3 w4); w2 \<noteq> 0; info = Structures_A.message_info.MI w1 w2 w3 w4; buffer' = Some a; (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' thread and (case buffer' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal:
No subgoals!