theory ArchIpc_IF

lemma lookup_ipc_buffer_ptr_range'[Ipc_IF_assms]:
  "\<lbrace>valid_objs\<rbrace>
   lookup_ipc_buffer True thread
   \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits\<rbrace>" unfolding lookup_ipc_buffer_def apply (rule hoare_pre) 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 (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric]) apply (drule(1) valid_tcb_objs) apply (drule get_tcb_SomeD)+ apply (simp add: vm_read_write_def valid_tcb_def valid_ipc_buffer_cap_def split: bool.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do buffer_ptr <- thread_get tcb_ipc_buffer thread;
buffer_frame_slot <- return (thread, tcb_cnode_index 4);
buffer_cap <- get_cap buffer_frame_slot;
case buffer_cap of ArchObjectCap (PageCap x p R vms xa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> True then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None
od \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do buffer_ptr <- thread_get tcb_ipc_buffer thread;
buffer_frame_slot <- return (thread, tcb_cnode_index 4);
buffer_cap <- get_cap buffer_frame_slot;
case buffer_cap of ArchObjectCap (PageCap x p R vms xa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> True then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None
od \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. 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> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (cap = DomainCap \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (cap = IRQControlCap \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (x = ASIDControlCap \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<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> True \<longrightarrow> (Some $ xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<not> (vm_read_write \<subseteq> xc \<or> vm_read_only \<subseteq> xc \<and> \<not> True) \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> None = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>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)); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))\<rbrakk> \<Longrightarrow> auth_ipc_buffers s thread = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>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)); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))\<rbrakk> \<Longrightarrow> tcb_cnode_index 4 \<in> dom tcb_cap_cases
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>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)); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)); caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<rbrakk> \<Longrightarrow> auth_ipc_buffers s thread = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>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)); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)); caps_of_state s (thread, tcb_cnode_index 4) = Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 4))) tcb)\<rbrakk> \<Longrightarrow> auth_ipc_buffers s thread = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe))\<rbrakk> \<Longrightarrow> (AllowWrite \<in> xc \<longrightarrow> (case xa of True \<Rightarrow> {} | False \<Rightarrow> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (AllowWrite \<notin> xc \<longrightarrow> (case xa of True \<Rightarrow> {} | _ \<Rightarrow> {}) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>get_tcb thread s = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> (AllowWrite \<in> xc \<longrightarrow> (case xa of True \<Rightarrow> {} | False \<Rightarrow> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (AllowWrite \<notin> xc \<longrightarrow> (case xa of True \<Rightarrow> {} | _ \<Rightarrow> {}) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb xc xd xe. \<lbrakk>tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; buf' = xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)); caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); valid_tcb thread tcb s; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (AllowWrite \<in> xc \<longrightarrow> (case xa of True \<Rightarrow> {} | False \<Rightarrow> ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) \<and> (AllowWrite \<notin> xc \<longrightarrow> (case xa of True \<Rightarrow> {} | _ \<Rightarrow> {}) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits) proof (prove)
goal:
No subgoals!