theory TcbAcc_R

lemma lookupIPCBuffer_corres':
  "corres (=) (tcb_at t and valid_objs and pspace_aligned)
               (tcb_at' t and valid_objs' and pspace_aligned'
                and pspace_distinct' and no_0_obj')
               (lookup_ipc_buffer w t) (lookupIPCBuffer w t)" apply (simp add: lookup_ipc_buffer_def ARM_H.lookupIPCBuffer_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF threadGet_corres]) apply (simp add: tcb_relation_def) apply (simp add: getThreadBufferSlot_def locateSlot_conv) apply (rule corres_split[OF getSlotCap_corres]) apply (simp add: cte_map_def tcb_cnode_index_def cte_level_bits_def tcbIPCBufferSlot_def) apply (rule_tac F="valid_ipc_buffer_cap rv buffer_ptr"
                     in corres_gen_asm) apply (rule_tac P="valid_cap rv" and Q="no_0_obj'"
                  in corres_assume_pre) apply (simp add: Let_def split: cap.split arch_cap.split
                       split del: if_split cong: if_cong) apply (safe, simp_all add: isCap_simps valid_ipc_buffer_cap_simps split:bool.split_asm)[1] apply (rename_tac word rights vmpage_size option) apply (subgoal_tac "word + (buffer_ptr &&
                                    mask (pageBitsForSize vmpage_size)) \<noteq> 0") apply (simp add: cap_aligned_def
                          valid_ipc_buffer_cap_def
                          vmrights_map_def vm_read_only_def vm_read_write_def) apply auto[1] apply (subgoal_tac "word \<noteq> 0") apply (subgoal_tac "word \<le> word + (buffer_ptr &&
                               mask (pageBitsForSize vmpage_size))") apply fastforce apply (rule_tac b="2 ^ (pageBitsForSize vmpage_size) - 1"
                      in word_plus_mono_right2) apply (clarsimp simp: valid_cap_def cap_aligned_def
                        intro!: is_aligned_no_overflow') apply (clarsimp simp: word_bits_def
                       intro!: word_less_sub_1 and_mask_less') apply (case_tac vmpage_size, simp_all)[1] apply (drule state_relation_pspace_relation) apply (clarsimp simp: valid_cap_def obj_at_def no_0_obj_kheap
                             obj_relation_cuts_def3 no_0_obj'_def split:if_split_asm) apply (wp get_cap_valid_ipc get_cap_aligned)+ apply (wp thread_get_obj_at_eq)+ apply (clarsimp elim!: tcb_at_cte_at) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t and valid_objs and pspace_aligned) (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') (lookup_ipc_buffer w t) (lookupIPCBuffer w t) proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t and valid_objs and pspace_aligned) (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') (do buffer_ptr <- thread_get tcb_ipc_buffer t;
get_cap (t, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) (do bufferPtr <- threadGet tcbIPCBuffer t;
bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz x) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz x) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr bufferPtr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do buffer_ptr <- thread_get tcb_ipc_buffer t;
get_cap (t, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) (do bufferPtr <- threadGet tcbIPCBuffer t;
bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz x) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz x) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr bufferPtr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od)
 2. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_ipc_buffer tcb = tcbIPCBuffer tcb'
 2. \<And>buffer_ptr. corres (=) (?R4 buffer_ptr) (?R'4 buffer_ptr) (get_cap (t, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) (do bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz x) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz x) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od)
 3. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>?R'4\<rbrace>
 5. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>buffer_ptr. corres (=) (?R4 buffer_ptr) (?R'4 buffer_ptr) (get_cap (t, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) (do bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz x) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz x) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od)
 2. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>buffer_ptr. corres (=) (?R4 buffer_ptr) (?R'4 buffer_ptr) (get_cap (t, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) (getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) >>= case_capability (\<lambda>word. return None) (return None) (\<lambda>word1 word2 bool1 bool2. return None) (\<lambda>word. return None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. return None) (return None) (\<lambda>word zombie_type nat. return None) (case_arch_capability (\<lambda>word1 word2. return None) (return None) (\<lambda>bool baseptr rights sz x. case bool of True \<Rightarrow> return Nothing | False \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od) (\<lambda>word option. return None) (\<lambda>word option. return None)) (\<lambda>word bool1 bool2. return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 nat1 word2 nat2. return None) (return None))
 2. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>buffer_ptr. t + 2 ^ cte_level_bits * tcbIPCBufferSlot = cte_map (t, tcb_cnode_index 4)
 2. \<And>buffer_ptr rv rv'. cap_relation rv rv' \<Longrightarrow> corres (=) (?R10 buffer_ptr rv) (?R'10 buffer_ptr rv') (case rv of cap.ArchObjectCap (arch_cap.PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | cap.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)
 3. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>?R10 buffer_ptr\<rbrace>
 4. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>?R'10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 7. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv rv'. cap_relation rv rv' \<Longrightarrow> corres (=) (?R10 buffer_ptr rv) (?R'10 buffer_ptr rv') (case rv of cap.ArchObjectCap (arch_cap.PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | cap.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>?R10 buffer_ptr\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>?R'10 buffer_ptr\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv rv'. \<lbrakk>cap_relation rv rv'; valid_ipc_buffer_cap rv buffer_ptr\<rbrakk> \<Longrightarrow> corres (=) (?P17 buffer_ptr rv) (?R'10 buffer_ptr rv') (case rv of cap.ArchObjectCap (arch_cap.PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | cap.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. ?P17 buffer_ptr rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>?R'10 buffer_ptr\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv rv' s s'. \<lbrakk>cap_relation rv rv'; valid_ipc_buffer_cap rv buffer_ptr; s \<turnstile> rv; no_0_obj' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres (=) (valid_cap rv) no_0_obj' (case rv of cap.ArchObjectCap (arch_cap.PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> w then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | cap.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv rv' s s'. \<lbrakk>cap_relation rv rv'; valid_ipc_buffer_cap rv buffer_ptr; s \<turnstile> rv; no_0_obj' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> corres (=) (valid_cap cap.NullCap) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x21 x22 x23 x24. rv = cap.UntypedCap x21 x22 x23 x24 \<longrightarrow> corres (=) (valid_cap (cap.UntypedCap x21 x22 x23 x24)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x31 x32 x33. rv = cap.EndpointCap x31 x32 x33 \<longrightarrow> corres (=) (valid_cap (cap.EndpointCap x31 x32 x33)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x41 x42 x43. rv = cap.NotificationCap x41 x42 x43 \<longrightarrow> corres (=) (valid_cap (cap.NotificationCap x41 x42 x43)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x51 x52 x53. rv = cap.ReplyCap x51 x52 x53 \<longrightarrow> corres (=) (valid_cap (cap.ReplyCap x51 x52 x53)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x61 x62 x63. rv = cap.CNodeCap x61 x62 x63 \<longrightarrow> corres (=) (valid_cap (cap.CNodeCap x61 x62 x63)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x7. rv = cap.ThreadCap x7 \<longrightarrow> corres (=) (valid_cap (cap.ThreadCap x7)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (rv = cap.DomainCap \<longrightarrow> corres (=) (valid_cap cap.DomainCap) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (rv = cap.IRQControlCap \<longrightarrow> corres (=) (valid_cap cap.IRQControlCap) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x10. rv = cap.IRQHandlerCap x10 \<longrightarrow> corres (=) (valid_cap (cap.IRQHandlerCap x10)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x111 x112 x113. rv = cap.Zombie x111 x112 x113 \<longrightarrow> corres (=) (valid_cap (cap.Zombie x111 x112 x113)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x12. (\<forall>x11 x12a. x12 = arch_cap.ASIDPoolCap x11 x12a \<longrightarrow> rv = cap.ArchObjectCap (arch_cap.ASIDPoolCap x11 x12a) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.ASIDPoolCap x11 x12a))) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (x12 = arch_cap.ASIDControlCap \<longrightarrow> rv = cap.ArchObjectCap arch_cap.ASIDControlCap \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap arch_cap.ASIDControlCap)) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x31 x32 x33 x34 x35. x12 = arch_cap.PageCap x31 x32 x33 x34 x35 \<longrightarrow> rv = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35))) no_0_obj' (if vm_read_write \<subseteq> x33 \<or> vm_read_only \<subseteq> x33 \<and> \<not> w then return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34)))) else return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x41 x42. x12 = arch_cap.PageTableCap x41 x42 \<longrightarrow> rv = cap.ArchObjectCap (arch_cap.PageTableCap x41 x42) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageTableCap x41 x42))) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)) \<and> (\<forall>x51 x52. x12 = arch_cap.PageDirectoryCap x51 x52 \<longrightarrow> rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) no_0_obj' (return None) (case rv' of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr buffer_ptr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)))
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv' s s' x31 x32 x33 x34 x35. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35); no_0_obj' s'; (s, s') \<in> state_relation; rv' = capability.ArchObjectCap (arch_capability.PageCap False x32 (vmrights_map x33) x34 x35); \<not> x31; is_aligned buffer_ptr msg_align_bits\<rbrakk> \<Longrightarrow> (vmrights_map x33 = VMReadOnly \<longrightarrow> (\<not> w \<longrightarrow> (vm_read_write \<subseteq> x33 \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35))) no_0_obj' (return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))) (do y <- assert (x32 + (buffer_ptr && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))
od)) \<and> (vm_read_only \<subseteq> x33 \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35))) no_0_obj' (return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))) (do y <- assert (x32 + (buffer_ptr && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))
od)) \<and> (\<not> vm_read_write \<subseteq> x33 \<and> \<not> vm_read_only \<subseteq> x33 \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35))) no_0_obj' (return None) (do y <- assert (x32 + (buffer_ptr && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))
od))) \<and> (w \<longrightarrow> vm_read_write \<subseteq> x33 \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation)))) \<and> (vmrights_map x33 \<noteq> VMReadOnly \<longrightarrow> (vmrights_map x33 = VMReadWrite \<longrightarrow> (vm_read_write \<subseteq> x33 \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35))) no_0_obj' (return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))) (do y <- assert (x32 + (buffer_ptr && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))
od)) \<and> (vm_read_only \<subseteq> x33 \<and> \<not> w \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35))) no_0_obj' (return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))) (do y <- assert (x32 + (buffer_ptr && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))
od)) \<and> (\<not> vm_read_write \<subseteq> x33 \<and> (vm_read_only \<subseteq> x33 \<longrightarrow> w) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35))) no_0_obj' (return None) (do y <- assert (x32 + (buffer_ptr && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (buffer_ptr && mask (pageBitsForSize x34))))
od))) \<and> (vmrights_map x33 \<noteq> VMReadWrite \<longrightarrow> (vm_read_write \<subseteq> x33 \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation))) \<and> (vm_read_only \<subseteq> x33 \<and> \<not> w \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False x32 x33 x34 x35) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation)))))
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv' s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; rv' = capability.ArchObjectCap (arch_capability.PageCap False word (vmrights_map rights) vmpage_size option); \<not> x31; is_aligned buffer_ptr msg_align_bits\<rbrakk> \<Longrightarrow> (vmrights_map rights = VMReadOnly \<longrightarrow> (\<not> w \<longrightarrow> (vm_read_write \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (vm_read_only \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (\<not> vm_read_write \<subseteq> rights \<and> \<not> vm_read_only \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return None) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od))) \<and> (w \<longrightarrow> vm_read_write \<subseteq> rights \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation)))) \<and> (vmrights_map rights \<noteq> VMReadOnly \<longrightarrow> (vmrights_map rights = VMReadWrite \<longrightarrow> (vm_read_write \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (vm_read_only \<subseteq> rights \<and> \<not> w \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (\<not> vm_read_write \<subseteq> rights \<and> (vm_read_only \<subseteq> rights \<longrightarrow> w) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return None) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od))) \<and> (vmrights_map rights \<noteq> VMReadWrite \<longrightarrow> (vm_read_write \<subseteq> rights \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation))) \<and> (vm_read_only \<subseteq> rights \<and> \<not> w \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation)))))
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>buffer_ptr rv' s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; rv' = capability.ArchObjectCap (arch_capability.PageCap False word (vmrights_map rights) vmpage_size option); \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0\<rbrakk> \<Longrightarrow> (vmrights_map rights = VMReadOnly \<longrightarrow> (\<not> w \<longrightarrow> (vm_read_write \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (vm_read_only \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (\<not> vm_read_write \<subseteq> rights \<and> \<not> vm_read_only \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return None) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od))) \<and> (w \<longrightarrow> vm_read_write \<subseteq> rights \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation)))) \<and> (vmrights_map rights \<noteq> VMReadOnly \<longrightarrow> (vmrights_map rights = VMReadWrite \<longrightarrow> (vm_read_write \<subseteq> rights \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (vm_read_only \<subseteq> rights \<and> \<not> w \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od)) \<and> (\<not> vm_read_write \<subseteq> rights \<and> (vm_read_only \<subseteq> rights \<longrightarrow> w) \<longrightarrow> corres (=) (valid_cap (cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option))) no_0_obj' (return None) (do y <- assert (word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0);
return (Some (word + (buffer_ptr && mask (pageBitsForSize vmpage_size))))
od))) \<and> (vmrights_map rights \<noteq> VMReadWrite \<longrightarrow> (vm_read_write \<subseteq> rights \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation))) \<and> (vm_read_only \<subseteq> rights \<and> \<not> w \<longrightarrow> (\<forall>s. s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option) \<longrightarrow> (\<forall>s'. no_0_obj' s' \<longrightarrow> (s, s') \<notin> state_relation)))))
 2. \<And>buffer_ptr rv' s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; rv' = capability.ArchObjectCap (arch_capability.PageCap False word (vmrights_map rights) vmpage_size option); \<not> x31; is_aligned buffer_ptr msg_align_bits\<rbrakk> \<Longrightarrow> word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0
 3. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 4. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 7. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr rv' s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; rv' = capability.ArchObjectCap (arch_capability.PageCap False word (vmrights_map rights) vmpage_size option); \<not> x31; is_aligned buffer_ptr msg_align_bits\<rbrakk> \<Longrightarrow> word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) \<noteq> 0
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 3. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 4. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 7. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0; word \<le> word + (buffer_ptr && mask (pageBitsForSize vmpage_size))\<rbrakk> \<Longrightarrow> False
 2. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> word \<le> word + (buffer_ptr && mask (pageBitsForSize vmpage_size))
 3. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 4. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 5. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 8. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 9. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> word \<le> word + (buffer_ptr && mask (pageBitsForSize vmpage_size))
 2. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 3. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 4. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 7. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1)
 2. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> buffer_ptr && mask (pageBitsForSize vmpage_size) \<le> 2 ^ pageBitsForSize vmpage_size - 1
 3. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 4. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 5. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 8. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 9. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> buffer_ptr && mask (pageBitsForSize vmpage_size) \<le> 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 3. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 4. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 7. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; word \<noteq> 0\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size < 32
 2. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 3. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 4. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 7. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; (s, s') \<in> state_relation; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0\<rbrakk> \<Longrightarrow> word \<noteq> 0
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>buffer_ptr s s' x31 word rights vmpage_size option. \<lbrakk>s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False word rights vmpage_size option); no_0_obj' s'; \<not> x31; is_aligned buffer_ptr msg_align_bits; word + (buffer_ptr && mask (pageBitsForSize vmpage_size)) = 0; pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> word \<noteq> 0
 2. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 3. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 6. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>buffer_ptr. \<lbrace>?Q10 buffer_ptr\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv. valid_cap rv and (\<lambda>s. valid_ipc_buffer_cap rv buffer_ptr)\<rbrace>
 2. \<And>buffer_ptr. \<lbrace>?Q'10 buffer_ptr\<rbrace> getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv'. no_0_obj'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>buffer_ptr. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) and ?Q10 buffer_ptr\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and ?Q'10 buffer_ptr\<rbrace>
 5. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'182\<rbrace> thread_get tcb_ipc_buffer t \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = rv) t\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>buffer_ptr. pspace_distinct' and pspace_aligned' and no_0_obj'\<rbrace>
 3. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and (\<lambda>s. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) s \<and> valid_objs s \<and> valid_objs s \<and> ?P'182 s)) s
 4. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> (tcb_at t and (\<lambda>s. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 4) s \<and> valid_objs s \<and> valid_objs s \<and> True)) s
 2. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and (pspace_distinct' and pspace_aligned' and no_0_obj')) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (tcb_at' t and (pspace_distinct' and pspace_aligned' and no_0_obj')) s proof (prove)
goal:
No subgoals!