theory Ipc_DR

lemma evalMonad_get_extra_cptrs:
  "\<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf);get_tcb thread s = Some tcb;
    (evalMonad (Ipc_A.get_extra_cptrs (Some buf) (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) s) = Some a
    \<rbrakk>
  \<Longrightarrow> a = (map (to_bl) (cdl_intent_extras $ transform_full_intent (machine_state s) thread tcb))" including no_pre apply (clarsimp simp:get_extra_cptrs_def) apply (clarsimp simp:liftM_def) apply (subst (asm) evalMonad_compose) apply (rule empty_when_fail_mapM) apply (simp add:weak_det_spec_load_word_offs empty_when_fail_load_word_offs) apply (rule weak_det_spec_mapM) apply (simp add:weak_det_spec_load_word_offs) apply (wp mapM_wp,fastforce) apply (clarsimp split:option.splits) apply (rule_tac x = x2 in arg_cong) apply (clarsimp simp:transform_full_intent_def Let_def) apply (clarsimp simp:get_ipc_buffer_words_def) apply (drule lookup_ipc_buffer_SomeB_evalMonad) apply (clarsimp simp:cte_wp_at_cases obj_at_def dest!: get_tcb_SomeD) apply (drule sym[where t = "tcb_ipcframe tcb"]) apply clarsimp apply (simp add:mapM_load_word_offs_do_machine_op) apply (subst (asm) evalMonad_do_machine_op[symmetric]) apply (rule weak_det_spec_mapM[OF weak_det_spec_loadWord]) apply (rule empty_when_fail_mapM) apply (clarsimp simp:empty_when_fail_loadWord weak_det_spec_loadWord) apply (clarsimp simp:get_tcb_message_info_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (get_extra_cptrs (Some buf) (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) s = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras $ transform_full_intent (machine_state s) thread tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (get_extra_cptrs (Some buf) (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) s = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras $ transform_full_intent (machine_state s) thread tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (liftM (map to_bl) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])) s = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (do x <- mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))];
return (map to_bl x)
od) s = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; (case evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (map to_bl r)) s) = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (4 subgoals):
 1. \<And>P l. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec P (load_word_offs buf l) \<and> empty_when_fail (load_word_offs buf l)
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; (case evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (map to_bl r)) s) = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; (case evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (map to_bl r)) s) = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (3 subgoals):
 1. \<And>r P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec P (load_word_offs buf r)
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; (case evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (map to_bl r)) s) = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; (case evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (map to_bl r)) s) = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; (case evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (map to_bl r)) s) = Some a\<rbrakk> \<Longrightarrow> a = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2\<rbrakk> \<Longrightarrow> map to_bl x2 = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2\<rbrakk> \<Longrightarrow> x2 = cdl_intent_extras (transform_full_intent (machine_state s) thread tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2\<rbrakk> \<Longrightarrow> x2 = get_ipc_buffer_words (machine_state s) tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some buf); get_tcb thread s = Some tcb; evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))]) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>get_tcb thread s = Some tcb; evalMonad (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2; \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> False \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at thread b rs sz s \<and> ko_at (TCB obj) thread s \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))]) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM (load_word_offs (b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)))) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2; AllowRead \<in> rs; ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe tcb; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))]) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM (load_word_offs (b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)))) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))]) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM (load_word_offs (b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)))) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]) s = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))])) (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (do_machine_op (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]))) s = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))])) (machine_state s)) proof (prove)
goal (3 subgoals):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec ((=) (machine_state s)) (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]))
 2. \<And>x2 b rs sz mapdata dev. \<lbrakk>a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]))
 3. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])) (machine_state s) = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))])) (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))]))
 2. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])) (machine_state s) = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))])) (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 b rs sz mapdata dev P l. \<lbrakk>a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P (loadWord l) \<and> empty_when_fail (loadWord l)
 2. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])) (machine_state s) = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))])) (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 b rs sz mapdata dev. \<lbrakk>evalMonad (mapM loadWord (map (\<lambda>offs. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))])) (machine_state s) = Some x2; a = map to_bl x2; AllowRead \<in> rs; kheap s thread = Some (TCB tcb); buf = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> x2 = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))])) (machine_state s)) proof (prove)
goal:
No subgoals!