theory Intent_DR

lemma get_ipc_buffer_words_helper:
  "\<lbrakk>valid_objs s;
    get_tcb thread s = Some tcb_type;
    ipc_frame_ptr_at obuf thread s;ipc_frame_sz_at osz thread s;
    ko_at (ArchObj (DataPage dev sz)) buf s;
    is_aligned ptr 2;
    pspace_aligned s; pspace_distinct s;
    within_page buf ptr sz;
    \<forall>x \<in> set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) +of_nat x* of_nat word_size) osz;
    obuf \<noteq> buf\<rbrakk> \<Longrightarrow>
    get_ipc_buffer_words (storeWord_ms ptr b ms) tcb_type xs= get_ipc_buffer_words ms tcb_type xs" apply (clarsimp dest!:get_tcb_SomeD simp:get_ipc_buffer_words_def split:cap.splits arch_cap.splits) apply (frule ipc_frame_ptr_at_frame_at[where buf = obuf],simp+) apply (frule valid_tcb_obj_ipc_align_etc[where buf = obuf],simp+) apply (erule get_tcb_rev) apply (rule arg_cong[where f = the]) apply (rule evalMonad_mapM) defer apply (simp_all add:empty_when_fail_loadWord weak_det_spec_loadWord) apply (wp loadWord_inv)+ apply (clarsimp simp:obj_at_def ipc_frame_wp_at_def) apply (drule_tac x = r in bspec,simp) apply (clarsimp simp:evalMonad_loadWord get_tcb_SomeD | rule conjI)+ apply (rule arg_cong[where f = word_rcat]) apply clarsimp apply (clarsimp simp:|rule conjI) apply (rule underlying_memory_storeWord) apply simp_all apply (rule aligned_add_aligned)+ apply simp+ apply (rule is_aligned_after_mask) apply simp+ apply (rule ipc_buffer_within_frame[where buf =obuf and buf'=buf]) apply (simp add:obj_at_def get_tcb_SomeD within_page_def add.assoc)+ apply (rule conjI) apply (subst add.assoc[symmetric])+ apply (rule underlying_memory_storeWord) apply (simp_all) apply (rule aligned_add_aligned)+ apply simp+ apply (subst is_aligned_after_mask) apply simp+ apply (rule ipc_buffer_within_frame[where buf = obuf and buf' = buf]) apply (simp add:obj_at_def get_tcb_SomeD within_page_def add.assoc)+ apply (rule conjI) apply (subst add.assoc[symmetric])+ apply (rule underlying_memory_storeWord) apply (simp_all) apply (rule aligned_add_aligned)+ apply simp+ apply (subst is_aligned_after_mask) apply simp+ apply (rule ipc_buffer_within_frame[where buf = obuf and buf' = buf]) apply (simp add:obj_at_def get_tcb_SomeD within_page_def add.assoc)+ apply (subst add.assoc[symmetric])+ apply (rule underlying_memory_storeWord[where n = 0,simplified]) apply (simp_all) apply (rule aligned_add_aligned)+ apply simp+ apply (subst is_aligned_after_mask) apply simp+ apply (rule ipc_buffer_within_frame[where buf = obuf and buf' = buf]) by ((simp add:obj_at_def get_tcb_SomeD within_page_def add.assoc)+)[7]

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb_type; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (storeWord_ms ptr b ms) tcb_type xs = get_ipc_buffer_words ms tcb_type xs proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) (storeWord_ms ptr b ms)) = the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) ms) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) (storeWord_ms ptr b ms)) = the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) ms) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s\<rbrakk> \<Longrightarrow> get_tcb thread s = Some (?tcb39 x31 x32 x33 x34 x35)
 2. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer (?tcb39 x31 x32 x33 x34 x35)) msg_align_bits \<and> is_aligned (tcb_ipc_buffer (?tcb39 x31 x32 x33 x34 x35)) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) (storeWord_ms ptr b ms)) = the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) ms) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) (storeWord_ms ptr b ms)) = the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) ms) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) (storeWord_ms ptr b ms) = evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs)) ms proof (prove)
goal (7 subgoals):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs). evalMonad (loadWord r) (storeWord_ms ptr b ms) = evalMonad (loadWord r) ms
 2. \<And>x31 x32 x33 x34 x35 sa r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> loadWord r \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 sa r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> loadWord r \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>x31 x32 x33 x34 x35 r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> empty_when_fail (loadWord r)
 5. \<And>x31 x32 x33 x34 x35 r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> empty_when_fail (loadWord r)
 6. \<And>x31 x32 x33 x34 x35 r P. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> weak_det_spec P (loadWord r)
 7. \<And>x31 x32 x33 x34 x35 r P. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> weak_det_spec P (loadWord r) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x32 x33 x34 x35 sa r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> loadWord r \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 sa r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> loadWord r \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> empty_when_fail (loadWord r)
 4. \<And>x31 x32 x33 x34 x35 r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> empty_when_fail (loadWord r)
 5. \<And>x31 x32 x33 x34 x35 r P. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> weak_det_spec P (loadWord r)
 6. \<And>x31 x32 x33 x34 x35 r P. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> weak_det_spec P (loadWord r)
 7. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<forall>r\<in>set (map (\<lambda>n. x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xs). evalMonad (loadWord r) (storeWord_ms ptr b ms) = evalMonad (loadWord r) ms proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 sa r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> loadWord r \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 sa r. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> loadWord r \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<forall>r\<in>set xs. evalMonad (loadWord (x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat r * word_of_nat word_size)) (storeWord_ms ptr b ms) = evalMonad (loadWord (x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat r * word_of_nat word_size)) ms proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>valid_objs s; ipc_frame_ptr_at obuf thread s; ipc_frame_sz_at osz thread s; ako_at (DataPage dev sz) buf s; is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 x32 x33 x34 x35); ako_at (DataPage False osz) obuf s; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits \<and> is_aligned (tcb_ipc_buffer tcb_type) 2 \<and> is_aligned obuf (pageBitsForSize osz) \<and> is_aligned obuf 2\<rbrakk> \<Longrightarrow> \<forall>r\<in>set xs. evalMonad (loadWord (x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat r * word_of_nat word_size)) (storeWord_ms ptr b ms) = evalMonad (loadWord (x32 + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize x34)) + word_of_nat r * word_of_nat word_size)) ms proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; \<forall>x\<in>set xs. within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat x * word_of_nat word_size) osz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2\<rbrakk> \<Longrightarrow> evalMonad (loadWord (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) (storeWord_ms ptr b ms) = evalMonad (loadWord (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) ms proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz\<rbrakk> \<Longrightarrow> evalMonad (loadWord (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) (storeWord_ms ptr b ms) = evalMonad (loadWord (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) ms proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> word_rcat [underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3), underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2), underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1), underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)] = word_rcat [underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3), underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2), underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1), underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)] proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> [underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3), underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2), underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1), underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)] = [underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3), underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2), underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1), underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)] proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 3)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> 3 \<le> 3
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned obuf (?n92 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n88 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n88 x31 x33 x35 r \<le> ?n92 x31 x33 x35 r
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n88 x31 x33 x35 r
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n88 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n88 x31 x33 x35 r \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n88 x31 x33 x35 r
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type) (?n88 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n88 x31 x33 x35 r \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n88 x31 x33 x35 r \<le> pageBitsForSize osz
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n88 x31 x33 x35 r
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (8 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_aligned (?s99 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_distinct (?s99 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev99 x31 x33 x35 r) (?sz99 x31 x33 x35 r)) obuf (?s99 x31 x33 x35 r)
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev'99 x31 x33 x35 r) (?sz'99 x31 x33 x35 r)) buf (?s99 x31 x33 x35 r)
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && ~~ mask (pageBitsForSize (?sz99 x31 x33 x35 r)) = obuf
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask (pageBitsForSize (?sz'99 x31 x33 x35 r)) = buf
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf \<noteq> buf
 8. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; within_page buf ptr sz; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; within_page obuf (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) osz; obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 2))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 2))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 2))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 2)))
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 2)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> 3
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned obuf (?n136 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n132 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n132 x31 x33 x35 r \<le> ?n136 x31 x33 x35 r
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n132 x31 x33 x35 r
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n132 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n132 x31 x33 x35 r \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n132 x31 x33 x35 r
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (8 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type) (?n141 x31 x33 x35 r (?x31.141 x31 x33 x35 r) (?x33.141 x31 x33 x35 r) (?x35.141 x31 x33 x35 r) (?r141 x31 x33 x35 r))
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n141 x31 x33 x35 r (?x31.141 x31 x33 x35 r) (?x33.141 x31 x33 x35 r) (?x35.141 x31 x33 x35 r) (?r141 x31 x33 x35 r) \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> True
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n141 x31 x33 x35 r (?x31.141 x31 x33 x35 r) (?x33.141 x31 x33 x35 r) (?x35.141 x31 x33 x35 r) (?r141 x31 x33 x35 r) \<le> pageBitsForSize osz
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n141 x31 x33 x35 r (?x31.141 x31 x33 x35 r) (?x33.141 x31 x33 x35 r) (?x35.141 x31 x33 x35 r) (?r141 x31 x33 x35 r)
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 8. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (8 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_aligned (?s143 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_distinct (?s143 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev143 x31 x33 x35 r) (?sz143 x31 x33 x35 r)) obuf (?s143 x31 x33 x35 r)
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev'143 x31 x33 x35 r) (?sz'143 x31 x33 x35 r)) buf (?s143 x31 x33 x35 r)
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && ~~ mask (pageBitsForSize (?sz143 x31 x33 x35 r)) = obuf
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask (pageBitsForSize (?sz'143 x31 x33 x35 r)) = buf
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf \<noteq> buf
 8. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) \<and> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1))) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + (word_of_nat r * word_of_nat word_size + 1)))
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size + 1)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 1 \<le> 3
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned obuf (?n180 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n176 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n176 x31 x33 x35 r \<le> ?n180 x31 x33 x35 r
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n176 x31 x33 x35 r
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n176 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n176 x31 x33 x35 r \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n176 x31 x33 x35 r
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (8 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type) (?n185 x31 x33 x35 r (?x31.185 x31 x33 x35 r) (?x33.185 x31 x33 x35 r) (?x35.185 x31 x33 x35 r) (?r185 x31 x33 x35 r))
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n185 x31 x33 x35 r (?x31.185 x31 x33 x35 r) (?x33.185 x31 x33 x35 r) (?x35.185 x31 x33 x35 r) (?r185 x31 x33 x35 r) \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> True
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n185 x31 x33 x35 r (?x31.185 x31 x33 x35 r) (?x33.185 x31 x33 x35 r) (?x35.185 x31 x33 x35 r) (?r185 x31 x33 x35 r) \<le> pageBitsForSize osz
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n185 x31 x33 x35 r (?x31.185 x31 x33 x35 r) (?x33.185 x31 x33 x35 r) (?x35.185 x31 x33 x35 r) (?r185 x31 x33 x35 r)
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 8. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (8 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_aligned (?s187 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_distinct (?s187 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev187 x31 x33 x35 r) (?sz187 x31 x33 x35 r)) obuf (?s187 x31 x33 x35 r)
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev'187 x31 x33 x35 r) (?sz'187 x31 x33 x35 r)) buf (?s187 x31 x33 x35 r)
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && ~~ mask (pageBitsForSize (?sz187 x31 x33 x35 r)) = obuf
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask (pageBitsForSize (?sz'187 x31 x33 x35 r)) = buf
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf \<noteq> buf
 8. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) = underlying_memory ms (obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size)) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) = underlying_memory ms (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr proof (prove)
goal (2 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) 2
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr proof (prove)
goal (6 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned obuf (?n210 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n206 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n206 x31 x33 x35 r \<le> ?n210 x31 x33 x35 r
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n206 x31 x33 x35 r
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr proof (prove)
goal (5 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) (?n206 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n206 x31 x33 x35 r \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n206 x31 x33 x35 r
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr proof (prove)
goal (7 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb_type) (?n215 x31 x33 x35 r (?x31.215 x31 x33 x35 r) (?x33.215 x31 x33 x35 r) (?x35.215 x31 x33 x35 r) (?r215 x31 x33 x35 r))
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n215 x31 x33 x35 r (?x31.215 x31 x33 x35 r) (?x33.215 x31 x33 x35 r) (?x35.215 x31 x33 x35 r) (?r215 x31 x33 x35 r) \<le> pageBitsForSize osz
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> True
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ?n215 x31 x33 x35 r (?x31.215 x31 x33 x35 r) (?x33.215 x31 x33 x35 r) (?x35.215 x31 x33 x35 r) (?r215 x31 x33 x35 r) \<le> pageBitsForSize osz
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat r * word_of_nat word_size) 2
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> 2 \<le> ?n215 x31 x33 x35 r (?x31.215 x31 x33 x35 r) (?x33.215 x31 x33 x35 r) (?x35.215 x31 x33 x35 r) (?r215 x31 x33 x35 r)
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr proof (prove)
goal (1 subgoal):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size \<noteq> ptr proof (prove)
goal (7 subgoals):
 1. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_aligned (?s217 x31 x33 x35 r)
 2. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> pspace_distinct (?s217 x31 x33 x35 r)
 3. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev217 x31 x33 x35 r) (?sz217 x31 x33 x35 r)) obuf (?s217 x31 x33 x35 r)
 4. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ako_at (DataPage (?dev'217 x31 x33 x35 r) (?sz'217 x31 x33 x35 r)) buf (?s217 x31 x33 x35 r)
 5. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf + (tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size && ~~ mask (pageBitsForSize (?sz217 x31 x33 x35 r)) = obuf
 6. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask (pageBitsForSize (?sz'217 x31 x33 x35 r)) = buf
 7. \<And>x31 x33 x35 r. \<lbrakk>valid_objs s; kheap s buf = Some (ArchObj (DataPage dev sz)); is_aligned ptr 2; pspace_aligned s; pspace_distinct s; ptr && ~~ mask (pageBitsForSize sz) = buf; obuf \<noteq> buf; kheap s thread = Some (TCB tcb_type); AllowRead \<in> x33; tcb_ipcframe tcb_type = ArchObjectCap (PageCap x31 obuf x33 osz x35); kheap s obuf = Some (ArchObj (DataPage False osz)); r \<in> set xs; is_aligned (tcb_ipc_buffer tcb_type) msg_align_bits; is_aligned (tcb_ipc_buffer tcb_type) 2; is_aligned obuf (pageBitsForSize osz); is_aligned obuf 2; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && ~~ mask (pageBitsForSize osz) = obuf; obuf + ((tcb_ipc_buffer tcb_type && mask (pageBitsForSize osz)) + word_of_nat r * word_of_nat word_size) && mask 2 = 0\<rbrakk> \<Longrightarrow> obuf \<noteq> buf