theory ArchAccess_AC

lemma ipcframe_subset_page:
  "\<lbrakk> valid_objs s; get_tcb p s = Some tcb;
     tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx);
     x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits \<rbrakk>
     \<Longrightarrow> x \<in> ptr_range p' (pageBitsForSize vms)" apply (frule (1) valid_tcb_objs) apply (clarsimp simp add: valid_tcb_def ran_tcb_cap_cases) apply (erule set_mp[rotated]) apply (rule ptr_range_subset) apply (simp add: valid_cap_def cap_aligned_def) apply (simp add: valid_tcb_def valid_ipc_buffer_cap_def is_aligned_andI1 split:bool.splits) apply (rule order_trans [OF _ pbfs_atleast_pageBits]) apply (simp add: msg_align_bits pageBits_def) apply (rule and_mask_less') apply (simp add: pbfs_less_wb' [unfolded word_bits_conv]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits\<rbrakk> \<Longrightarrow> x \<in> ptr_range p' (pageBitsForSize vms) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits; valid_tcb p tcb s\<rbrakk> \<Longrightarrow> x \<in> ptr_range p' (pageBitsForSize vms) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits; s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> x \<in> ptr_range p' (pageBitsForSize vms) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits \<subseteq> ptr_range p' (pageBitsForSize vms) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> is_aligned p' (pageBitsForSize vms)
 2. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb && mask (pageBitsForSize vms)) msg_align_bits
 3. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize vms
 4. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize vms) < 2 ^ pageBitsForSize vms proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb && mask (pageBitsForSize vms)) msg_align_bits
 2. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize vms
 3. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize vms) < 2 ^ pageBitsForSize vms proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize vms
 2. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize vms) < 2 ^ pageBitsForSize vms proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits
 2. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize vms) < 2 ^ pageBitsForSize vms proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> tcb_ipc_buffer tcb && mask (pageBitsForSize vms) < 2 ^ pageBitsForSize vms proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb p s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap d p' R vms xx); s \<turnstile> tcb_ctable tcb; s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = p \<and> AllowGrant \<in> cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = NullCap; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); s \<turnstile> ArchObjectCap (PageCap d p' R vms xx); is_nondevice_page_cap (ArchObjectCap (PageCap d p' R vms xx)); valid_ipc_buffer_cap (ArchObjectCap (PageCap d p' R vms xx)) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_fault x2; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> pageBitsForSize vms < LENGTH(32) proof (prove)
goal:
No subgoals!