theory ArchIpc_AC

lemma lookup_ipc_buffer_has_auth[Ipc_AC_assms, wp]:
  "\<lbrace>pas_refined aag and valid_objs\<rbrace>
   lookup_ipc_buffer True receiver
   \<lbrace>\<lambda>rv _. ipc_buffer_has_auth aag receiver 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_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 (rule conjI) apply (clarsimp simp: valid_cap_simps cap_aligned_def) 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 simp 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_write_def is_page_cap_def) apply (drule bspec) apply (erule (3) ipcframe_subset_page) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and valid_objs\<rbrace> lookup_ipc_buffer True receiver \<lbrace>\<lambda>rv _. ipc_buffer_has_auth aag receiver rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> lookup_ipc_buffer True receiver \<lbrace>\<lambda>rv _. ipc_buffer_has_auth aag receiver 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 receiver;
get_cap (receiver, 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 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 _. ipc_buffer_has_auth aag receiver 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) receiver s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (receiver, tcb_cnode_index 4) s \<longrightarrow> (cap = NullCap \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (cap = DomainCap \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (cap = IRQControlCap \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (x = ASIDControlCap \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> (vm_read_write \<subseteq> xc \<longrightarrow> ipc_buffer_has_auth aag receiver (Some (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))))) \<and> (\<not> vm_read_write \<subseteq> xc \<longrightarrow> ipc_buffer_has_auth aag receiver None)) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver None) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> ipc_buffer_has_auth aag receiver 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> 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 receiver, Write, 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<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 receiver, Write, 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<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 receiver, Write, 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> 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 receiver, Write, 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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; get_tcb receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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; valid_tcb receiver 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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\<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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); vm_read_write \<subseteq> xc; caps_of_state s (receiver, 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> \<forall>x\<in>ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits. (pasObjectAbs aag receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; caps_of_state s (receiver, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); s \<turnstile> 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 receiver, Write, 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe); aag_cap_auth aag (pasObjectAbs aag (fst (receiver, 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 receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe); x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; AllowRead \<in> xc; AllowWrite \<in> xc; \<forall>x\<in>ptr_range xb (pageBitsForSize xd). (pasObjectAbs aag receiver, Read, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasObjectAbs aag receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe); x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; AllowRead \<in> xc; AllowWrite \<in> xc; cap_links_asid_slot aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> ?x243 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 receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe); x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; AllowRead \<in> xc; AllowWrite \<in> xc; cap_links_asid_slot aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe)); (pasObjectAbs aag receiver, Read, pasObjectAbs aag (?x243 s tcb xa xb xc xd xe x)) \<in> pasPolicy aag \<and> (pasObjectAbs aag receiver, Write, pasObjectAbs aag (?x243 s tcb xa xb xc xd xe x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe x. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb receiver s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); s \<turnstile> ArchObjectCap (PageCap xa xb xc xd xe); x \<in> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits; AllowRead \<in> xc; AllowWrite \<in> xc; cap_links_asid_slot aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe)); cap_links_irq aag (pasObjectAbs aag receiver) (ArchObjectCap (PageCap xa xb xc xd xe)); (pasObjectAbs aag receiver, Read, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasObjectAbs aag receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!