theory Intent_DR

lemma get_ipc_buffer_words:
  "\<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf))\<rbrace>
    mapM (load_word_offs (buf)) (ls)
   \<lbrace>\<lambda>buf_mrs s. buf_mrs = get_ipc_buffer_words (machine_state sa) obj (ls)\<rbrace>" apply (simp add: pred_conj_aci get_ipc_buffer_words_def) apply (rule wp_spec) apply clarsimp apply (drule lookup_ipc_buffer_SomeB_evalMonad) apply (clarsimp simp:obj_at_def cte_wp_at_cases) apply (drule sym[where t = "tcb_ipcframe obj"]) apply clarsimp apply (rule weak_det_spec_ret) apply (rule weak_det_spec_mapM) apply (rule weak_det_spec_load_word_offs) apply simp apply (clarsimp simp: mapM_load_word_offs_do_machine_op mapM_map_simp) apply (rule arg_cong[where f = the]) apply (rule evalMonad_do_machine_op) apply (rule weak_det_spec_mapM) apply clarsimp apply (rule weak_det_spec_loadWord) apply (rule empty_when_fail_mapM) apply (rule conjI) apply (clarsimp simp: weak_det_spec_loadWord empty_when_fail_loadWord)+ apply (rule empty_when_fail_mapM) apply (clarsimp simp:weak_det_spec_load_word_offs empty_when_fail_load_word_offs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf))\<rbrace> mapM (load_word_offs buf) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = get_ipc_buffer_words (machine_state sa) obj ls\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) sa and (ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf)))\<rbrace> mapM (load_word_offs buf) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (case tcb_ipcframe obj of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ls) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. (ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf))) sa \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (case tcb_ipcframe obj of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ls) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB obj) thread sa; evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (case tcb_ipcframe obj of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ls) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB obj) thread sa; \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at thread b rs sz sa \<and> ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs buf) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (case tcb_ipcframe obj of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ls) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe obj\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (case tcb_ipcframe obj of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ls) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (case tcb_ipcframe obj of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) ls) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (machine_state sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls \<lbrace>\<lambda>buf_mrs s. buf_mrs = the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) ls)) (machine_state sa))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec ((=) sa) (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> ?g17 b rs sz mapdata dev sa = mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls sa
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) ls)) (machine_state sa)) = the (evalMonad (?g17 b rs sz mapdata dev) sa)
 4. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (4 subgoals):
 1. \<And>b rs sz mapdata dev r P. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) r)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> ?g17 b rs sz mapdata dev sa = mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls sa
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) ls)) (machine_state sa)) = the (evalMonad (?g17 b rs sz mapdata dev) sa)
 4. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (3 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> ?g17 b rs sz mapdata dev sa = mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls sa
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) ls)) (machine_state sa)) = the (evalMonad (?g17 b rs sz mapdata dev) sa)
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (2 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size) ls)) (machine_state sa)) = the (evalMonad (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) sa)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (2 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls) (machine_state sa)) = the (evalMonad (do_machine_op (mapM (loadWord \<circ> (\<lambda>offs. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size)) ls)) sa)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (2 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> evalMonad (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls) (machine_state sa) = evalMonad (do_machine_op (mapM (loadWord \<circ> (\<lambda>offs. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat offs * word_of_nat word_size)) ls)) sa
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (3 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec ((=) (machine_state sa)) (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls)
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (3 subgoals):
 1. \<And>b rs sz mapdata dev r P. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P ((loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) r)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls)
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (3 subgoals):
 1. \<And>b rs sz mapdata dev r P. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P (loadWord (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat r * word_of_nat word_size))
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls)
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (2 subgoals):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) ls)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (2 subgoals):
 1. \<And>b rs sz mapdata dev P l. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P ((loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) l) \<and> empty_when_fail ((loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) l)
 2. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (3 subgoals):
 1. \<And>b rs sz mapdata dev P l. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P ((loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) l)
 2. \<And>b rs sz mapdata dev P l. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail ((loadWord \<circ> (\<lambda>n. b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat n * word_of_nat word_size)) l)
 3. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata dev. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) ls) proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata dev P l. \<lbrakk>kheap sa thread = Some (TCB obj); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> weak_det_spec P (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) l) \<and> empty_when_fail (load_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) l) proof (prove)
goal:
No subgoals!