theory ArchArch_IF

lemma auth_ipc_buffers_mem_Write':
  "\<lbrakk> x \<in> auth_ipc_buffers s thread; pas_refined aag s; valid_objs s \<rbrakk>
     \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag" apply (clarsimp simp add: auth_ipc_buffers_member_def) apply (drule (1) cap_auth_caps_of_state) apply simp 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
                 split: if_split_asm) apply (auto dest: ipcframe_subset_page) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> auth_ipc_buffers s thread; pas_refined aag s; valid_objs s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb p' R vms xx. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap False p' R vms xx)); AllowWrite \<in> R; x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb p' R vms xx. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx); AllowWrite \<in> R; x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits; aag_cap_auth aag (pasObjectAbs aag (fst (thread, tcb_cnode_index 4))) (ArchObjectCap (PageCap False p' R vms xx))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb p' R vms xx. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx); AllowWrite \<in> R; x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits; aag_cap_auth aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap False p' R vms xx))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>tcb p' R vms xx. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx); AllowWrite \<in> R; x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits; AllowRead \<in> R; \<forall>x\<in>ptr_range p' (pageBitsForSize vms). (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasObjectAbs aag thread, Read, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap False p' R vms xx)); cap_links_irq aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap False p' R vms xx))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>tcb p' R vms xx. \<lbrakk>pas_refined aag s; valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx); AllowWrite \<in> R; x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits; AllowRead \<notin> R; \<forall>x\<in>ptr_range p' (pageBitsForSize vms). (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap False p' R vms xx)); cap_links_irq aag (pasObjectAbs aag thread) (ArchObjectCap (PageCap False p' R vms xx))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!