theory Ipc_R

lemma lookupIPCBuffer_valid_ipc_buffer [wp]:
  "\<lbrace>valid_objs'\<rbrace> VSpace_H.lookupIPCBuffer b s \<lbrace>case_option \<top> valid_ipc_buffer_ptr'\<rbrace>" unfolding lookupIPCBuffer_def ARM_H.lookupIPCBuffer_def apply (simp add: Let_def getSlotCap_def getThreadBufferSlot_def
                   locateSlot_conv threadGet_def comp_def) apply (wp getCTE_wp getObject_tcb_wp | wpc)+ apply (clarsimp simp del: imp_disjL) apply (drule obj_at_ko_at') apply (clarsimp simp del: imp_disjL) apply (rule_tac x = ko in exI) apply (frule ko_at_cte_ipcbuffer) apply (clarsimp simp: cte_wp_at_ctes_of simp del: imp_disjL) apply (clarsimp simp: valid_ipc_buffer_ptr'_def) apply (frule (1) ko_at_valid_objs') apply (clarsimp simp: projectKO_opts_defs split: kernel_object.split_asm) apply (clarsimp simp add: valid_obj'_def valid_tcb'_def
                            isCap_simps cte_level_bits_def field_simps) apply (drule bspec [OF _ ranI [where a = "0x40"]]) apply simp apply (clarsimp simp add: valid_cap'_def) apply (rule conjI) apply (rule aligned_add_aligned) apply (clarsimp simp add: capAligned_def) apply assumption apply (erule is_aligned_andI1) apply (case_tac xd, simp_all add: msg_align_bits)[1] apply (clarsimp simp: capAligned_def) apply (drule_tac x =
    "(tcbIPCBuffer ko && mask (pageBitsForSize xd))  >> pageBits" in spec) apply (subst(asm) mult.commute mult.left_commute, subst(asm) shiftl_t2n[symmetric]) apply (simp add: shiftr_shiftl1) apply (subst (asm) mask_out_add_aligned) apply (erule is_aligned_weaken [OF _ pbfs_atleast_pageBits]) apply (erule mp) apply (rule shiftr_less_t2n) apply (clarsimp simp: pbfs_atleast_pageBits) apply (rule and_mask_less') apply (simp add: word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupIPCBuffer b s \<lbrace>case_option (\<lambda>_. True) valid_ipc_buffer_ptr'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do bufferPtr <- threadGet tcbIPCBuffer s;
bufferFrameSlot <- getThreadBufferSlot s;
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> b \<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 \<lbrace>case_option (\<lambda>_. True) valid_ipc_buffer_ptr'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do bufferPtr <- liftM tcbIPCBuffer (getObject s);
cte <- getCTE (s + 2 ^ cte_level_bits * tcbIPCBufferSlot);
case cteCap cte 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> b \<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 \<lbrace>case_option (\<lambda>_. True) valid_ipc_buffer_ptr'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. valid_objs' sa \<Longrightarrow> tcb_at' s sa \<longrightarrow> (\<exists>t. ko_at' t s sa \<and> ((\<lambda>bufferPtr sa. cte_wp_at' (\<lambda>_. True) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<and> (\<forall>x. cteCap cte = capability.ThreadCap x \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (cteCap cte = capability.NullCap \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x xa xb xc. cteCap cte = capability.NotificationCap x xa xb xc \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x. cteCap cte = capability.IRQHandlerCap x \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x xa xb xc xd xe. cteCap cte = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x xa xb. cteCap cte = capability.Zombie x xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = arch_capability.ASIDPoolCap xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (x = arch_capability.ASIDControlCap \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>xa xb xc xd xe. x = arch_capability.PageCap xa xb xc xd xe \<longrightarrow> (xa = True \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (xa = False \<longrightarrow> (xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly \<longrightarrow> (case Just (xb + PPtr (fromVPtr bufferPtr && mask (pageBitsForSize xd))) of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<not> (xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly) \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa))) \<and> (\<forall>xa xb. x = arch_capability.PageTableCap xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>xa xb. x = arch_capability.PageDirectoryCap xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa)) \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x xa xb xc. cteCap cte = capability.UntypedCap x xa xb xc \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (\<forall>x xa xb xc. cteCap cte = capability.CNodeCap x xa xb xc \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> (case Nothing of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) sa))) \<circ> tcbIPCBuffer) t sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>valid_objs' sa; tcb_at' s sa\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t s sa \<and> (cte_wp_at' (\<lambda>_. True) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb xc xd. (\<exists>xe. x = arch_capability.PageCap xa xb xc xd xe) \<longrightarrow> \<not> xa \<longrightarrow> xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly \<longrightarrow> valid_ipc_buffer_ptr' (xb + (tcbIPCBuffer t && mask (pageBitsForSize xd))) sa)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>valid_objs' sa; \<exists>ko. ko_at' ko s sa \<and> True\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t s sa \<and> (cte_wp_at' (\<lambda>_. True) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb xc xd. (\<exists>xe. x = arch_capability.PageCap xa xb xc xd xe) \<longrightarrow> \<not> xa \<longrightarrow> xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly \<longrightarrow> valid_ipc_buffer_ptr' (xb + (tcbIPCBuffer t && mask (pageBitsForSize xd))) sa)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko. \<lbrakk>valid_objs' sa; ko_at' ko s sa\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t s sa \<and> (cte_wp_at' (\<lambda>_. True) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb xc xd. (\<exists>xe. x = arch_capability.PageCap xa xb xc xd xe) \<longrightarrow> \<not> xa \<longrightarrow> xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly \<longrightarrow> valid_ipc_buffer_ptr' (xb + (tcbIPCBuffer t && mask (pageBitsForSize xd))) sa)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko. \<lbrakk>valid_objs' sa; ko_at' ko s sa\<rbrakk> \<Longrightarrow> ko_at' ko s sa \<and> (cte_wp_at' (\<lambda>_. True) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb xc xd. (\<exists>xe. x = arch_capability.PageCap xa xb xc xd xe) \<longrightarrow> \<not> xa \<longrightarrow> xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly \<longrightarrow> valid_ipc_buffer_ptr' (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) sa)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko. \<lbrakk>valid_objs' sa; ko_at' ko s sa; cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame ko) (s + tcbIPCBufferSlot * 0x10) sa\<rbrakk> \<Longrightarrow> ko_at' ko s sa \<and> (cte_wp_at' (\<lambda>_. True) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) sa \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb xc xd. (\<exists>xe. x = arch_capability.PageCap xa xb xc xd xe) \<longrightarrow> \<not> xa \<longrightarrow> xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly \<longrightarrow> valid_ipc_buffer_ptr' (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) sa)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko cte xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); ctes_of sa (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly\<rbrakk> \<Longrightarrow> valid_ipc_buffer_ptr' (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko cte xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); ctes_of sa (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa ko cte xa xb xc xd xe koa. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); ctes_of sa (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> injectKOS ko = koa
 2. \<And>sa ko cte xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); ctes_of sa (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_obj' (injectKOS ko) sa\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko cte xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); ctes_of sa (s + 2 ^ cte_level_bits * tcbIPCBufferSlot) = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_obj' (injectKOS ko) sa\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) sa; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority\<rbrakk> \<Longrightarrow> tcb_cte_cases 0x40 = Some (?x244 sa ko xa xb xc xd xe)
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; case ?x244 sa ko xa xb xc xd xe of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) sa\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; case (tcbIPCBufferFrame, tcbIPCBufferFrame_update) of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) sa\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits \<and> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd))) msg_align_bits
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (4 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> is_aligned xb (?n255 sa ko xa xb xc xd xe)
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (tcbIPCBuffer ko && mask (pageBitsForSize xd)) msg_align_bits
 3. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> msg_align_bits \<le> ?n255 sa ko xa xb xc xd xe
 4. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (4 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> is_aligned xb (?n255 sa ko False xb xc xd xe)
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (tcbIPCBuffer ko && mask (pageBitsForSize xd)) msg_align_bits
 3. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> msg_align_bits \<le> ?n255 sa ko xa xb xc xd xe
 4. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (3 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (tcbIPCBuffer ko && mask (pageBitsForSize xd)) msg_align_bits
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd
 3. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; capAligned (capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe)); xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) sa; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits < 2 ^ (pageBitsForSize xd - pageBits) \<longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits) * 2 ^ pageBits) sa\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits < 2 ^ (pageBitsForSize xd - pageBits) \<longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits << pageBits)) sa\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits < 2 ^ (pageBitsForSize xd - pageBits) \<longrightarrow> typ_at' UserDataT (xb + ((tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits)) sa\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> is_aligned xb pageBits
 2. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits < 2 ^ (pageBitsForSize xd - pageBits) \<longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits < 2 ^ (pageBitsForSize xd - pageBits) \<longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa\<rbrakk> \<Longrightarrow> typ_at' UserDataT (xb + (tcbIPCBuffer ko && mask (pageBitsForSize xd)) && ~~ mask pageBits) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> tcbIPCBuffer ko && mask (pageBitsForSize xd) >> pageBits < 2 ^ (pageBitsForSize xd - pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> tcbIPCBuffer ko && mask (pageBitsForSize xd) < 2 ^ (pageBits + (pageBitsForSize xd - pageBits)) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> tcbIPCBuffer ko && mask (pageBitsForSize xd) < 2 ^ pageBitsForSize xd proof (prove)
goal (1 subgoal):
 1. \<And>sa ko xa xb xc xd xe. \<lbrakk>valid_objs' sa; ko_at' ko s sa; ctes_of sa (s + tcbIPCBufferSlot * 0x10) = Some (tcbIPCBufferFrame ko); cteCap (tcbIPCBufferFrame ko) = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; xc = VMReadWrite \<or> \<not> b \<and> xc = VMReadOnly; valid_tcb_state' (tcbState ko) sa; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) sa; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority; xb \<noteq> 0; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits\<rbrakk> \<Longrightarrow> pageBitsForSize xd < LENGTH(32) proof (prove)
goal:
No subgoals!