theory ArchIpc_IF

lemma lookup_ipc_buffer_has_read_auth[Ipc_IF_assms]:
  "\<lbrace>pas_refined aag and valid_objs\<rbrace>
   lookup_ipc_buffer is_receiver thread
   \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace>" apply (rule hoare_pre) apply (simp add: lookup_ipc_buffer_def) apply (wp get_cap_wp thread_get_wp' | wpc)+ apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_read_auth_def get_tcb_ko_at[symmetric]) apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) apply (simp add: dom_tcb_cap_cases) apply (frule (1) caps_of_state_valid_cap) apply (clarsimp simp: vm_read_only_def vm_read_write_def) apply (rule_tac Q="AllowRead \<in> xc" in conj_imp) apply (clarsimp simp: valid_cap_simps cap_aligned_def) apply (rule conjI) apply (erule aligned_add_aligned) apply (rule is_aligned_andI1) apply (drule (1) valid_tcb_objs) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def
                     split: if_splits) apply (rule order_trans [OF _ pbfs_atleast_pageBits]) apply (simp add: msg_align_bits pageBits_def) apply (drule (1) cap_auth_caps_of_state) apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def
                          vspace_cap_rights_to_auth_def vm_read_only_def) apply (drule bspec) apply (erule (3) ipcframe_subset_page) apply (clarsimp split: if_split_asm simp: vspace_cap_rights_to_auth_def is_page_cap_def) apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and valid_objs\<rbrace> lookup_ipc_buffer is_receiver thread \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> lookup_ipc_buffer is_receiver thread \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace>
 2. \<And>s. (pas_refined aag and valid_objs) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do buffer_ptr <- thread_get tcb_ipc_buffer thread;
get_cap (thread, 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> is_receiver then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace>
 2. \<And>s. (pas_refined aag and valid_objs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and valid_objs) s \<Longrightarrow> \<forall>tcb. ko_at (TCB tcb) thread s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (thread, tcb_cnode_index 4) s \<longrightarrow> (cap = NullCap \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (cap = DomainCap \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (cap = IRQControlCap \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (x = ASIDControlCap \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> (vm_read_write \<subseteq> xc \<or> vm_read_only \<subseteq> xc \<and> \<not> is_receiver \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) (Some $ xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)))) \<and> (\<not> (vm_read_write \<subseteq> xc \<or> vm_read_only \<subseteq> xc \<and> \<not> is_receiver) \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None)) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) None))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (vm_read_only \<subseteq> xc \<and> \<not> is_receiver \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> tcb_cnode_index 4 \<in> dom tcb_cap_cases
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (vm_read_only \<subseteq> xc \<and> \<not> is_receiver \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (vm_read_only \<subseteq> xc \<and> \<not> is_receiver \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (vm_read_only \<subseteq> xc \<and> \<not> is_receiver \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> (AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> (AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)) proof (prove)
goal (3 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (3 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits \<and> (\<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag)
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (4 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> is_aligned (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (5 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 5. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (5 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 5. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (5 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc; valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> is_aligned (tcb_ipc_buffer tcb) msg_align_bits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 5. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (4 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBitsForSize xd
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (4 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (3 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (3 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc; aag_cap_auth aag (pasObjectAbs aag (fst (thread, tcb_cnode_index 4))) (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (3 subgoals):
 1. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc; x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; \<forall>x\<in>ptr_range xb (pageBitsForSize xd). (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (\<forall>auth\<in>if AllowWrite \<in> xc then {Write} else {}. (pasObjectAbs aag thread, auth, pasObjectAbs aag x) \<in> pasPolicy aag); cap_links_asid_slot aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (4 subgoals):
 1. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc; x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; cap_links_asid_slot aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> ?x244 s tcb xa xb xc xd xe x \<in> ptr_range xb (pageBitsForSize xd)
 2. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc; x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; cap_links_asid_slot aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe)); (pasObjectAbs aag thread, Read, pasObjectAbs aag (?x244 s tcb xa xb xc xd xe x)) \<in> pasPolicy aag \<and> (\<forall>auth\<in>if AllowWrite \<in> xc then {Write} else {}. (pasObjectAbs aag thread, auth, pasObjectAbs aag (?x244 s tcb xa xb xc xd xe x)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 4. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (3 subgoals):
 1. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); is_aligned xb (pageBitsForSize xd); pageBitsForSize xd < word_bits; if xa then typ_at (AArch (ADeviceData xd)) xb s else typ_at (AArch (AUserData xd)) xb s; xc \<in> valid_vm_rights; 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 < kernel_base; AllowRead \<in> xc; x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; cap_links_asid_slot aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap xa xb xc xd xe)); (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (\<forall>auth\<in>if AllowWrite \<in> xc then {Write} else {}. (pasObjectAbs aag thread, auth, pasObjectAbs aag x) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 3. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> AllowWrite \<in> xc \<longrightarrow> AllowRead \<in> xc
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe)\<rbrakk> \<Longrightarrow> AllowRead \<in> xc \<and> \<not> is_receiver \<longrightarrow> AllowRead \<in> xc proof (prove)
goal:
No subgoals!