theory Ipc_C

lemma lookupIPCBuffer_aligned:
  "\<lbrace>valid_objs'\<rbrace> lookupIPCBuffer r t \<lbrace>\<lambda>rv. K (case_option True (\<lambda>x. is_aligned x msg_align_bits) rv)\<rbrace>" apply (simp add: lookupIPCBuffer_def ARM_H.lookupIPCBuffer_def
                   getThreadBufferSlot_def locateSlot_conv
                   Let_def getSlotCap_def cong: if_cong) apply (rule hoare_pre) apply (wp getCTE_wp' threadGet_wp | wpc)+ apply clarsimp apply (drule (1) ctes_of_valid) apply (drule (1) ko_at_valid_objs', simp add: projectKOs) apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def valid_obj'_def valid_tcb'_def) apply (auto elim: aligned_add_aligned intro: is_aligned_andI1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupIPCBuffer r t \<lbrace>\<lambda>rv. K (case rv of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do bufferPtr <- threadGet tcbIPCBuffer t;
cte <- getCTE (t + 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 = vmrights.VMReadWrite \<or> \<not> r \<and> rights = vmrights.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>\<lambda>rv y. case rv of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do bufferPtr <- threadGet tcbIPCBuffer t;
cte <- getCTE (t + 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 = vmrights.VMReadWrite \<or> \<not> r \<and> rights = vmrights.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>\<lambda>rv y. case rv of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<Longrightarrow> \<forall>tcb. ko_at' tcb t s \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) s \<longrightarrow> (\<forall>x. cteCap cte = capability.ThreadCap x \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (cteCap cte = capability.NullCap \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x xa xb xc. cteCap cte = capability.NotificationCap x xa xb xc \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x. cteCap cte = capability.IRQHandlerCap x \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x xa xb xc xd xe. cteCap cte = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x xa xb. cteCap cte = capability.Zombie x xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = arch_capability.ASIDPoolCap xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (x = arch_capability.ASIDControlCap \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<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> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (xa = False \<longrightarrow> (xc = vmrights.VMReadWrite \<or> \<not> r \<and> xc = vmrights.VMReadOnly \<longrightarrow> (case Just (xb + PPtr (fromVPtr (tcbIPCBuffer tcb) && mask (pageBitsForSize xd))) of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<not> (xc = vmrights.VMReadWrite \<or> \<not> r \<and> xc = vmrights.VMReadOnly) \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)))) \<and> (\<forall>xa xb. x = arch_capability.PageTableCap xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>xa xb. x = arch_capability.PageDirectoryCap xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits))) \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x xa xb xc. cteCap cte = capability.UntypedCap x xa xb xc \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (\<forall>x xa xb xc. cteCap cte = capability.CNodeCap x xa xb xc \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits)) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> (case Nothing of None \<Rightarrow> True | Some x \<Rightarrow> is_aligned x msg_align_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb cte xa xb xc xd xe. \<lbrakk>valid_objs' s; ko_at' tcb t s; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) s; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa\<rbrakk> \<Longrightarrow> (xc = vmrights.VMReadWrite \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (\<not> r \<and> xc = vmrights.VMReadOnly \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb cte xa xb xc xd xe. \<lbrakk>valid_objs' s; ko_at' tcb t s; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> (xc = vmrights.VMReadWrite \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (\<not> r \<and> xc = vmrights.VMReadOnly \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb cte xa xb xc xd xe. \<lbrakk>valid_objs' s; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; valid_cap' (cteCap cte) s; valid_obj' (injectKOS tcb) s\<rbrakk> \<Longrightarrow> (xc = vmrights.VMReadWrite \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (\<not> r \<and> xc = vmrights.VMReadOnly \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb cte xa xb xc xd xe. \<lbrakk>valid_objs' s; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap False xb xc xd xe); \<not> xa; is_aligned xb (pageBitsForSize xd); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> is_aligned (global.capUntypedPtr (cteCap (getF tcb))) (capBits (cteCap (getF tcb))) \<and> capBits (cteCap (getF tcb)) < word_bits \<and> (case cteCap (getF tcb) of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> local.maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageTableCap ref mapdata) \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref mapdata) \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True); pageBitsForSize xd < word_bits; valid_tcb_state' (tcbState tcb) s; xb \<noteq> 0; is_aligned (tcbIPCBuffer tcb) msg_align_bits; \<forall>p<2 ^ (pageBitsForSize xd - pageBits). typ_at' UserDataT (xb + p * 2 ^ pageBits) s; case xe of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref xd \<and> ref < pptrBase; valid_bound_ntfn' (tcbBoundNotification tcb) s; tcbDomain tcb \<le> maxDomain; tcbPriority tcb \<le> maxPriority; tcbMCP tcb \<le> maxPriority\<rbrakk> \<Longrightarrow> (xc = vmrights.VMReadWrite \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (\<not> r \<and> xc = vmrights.VMReadOnly \<longrightarrow> is_aligned (xb + (tcbIPCBuffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal:
No subgoals!