theory ArchIpc_AC

lemma lookup_ipc_buffer_ptr_range_in_ipc[Ipc_AC_assms]:
  "\<lbrace>valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st\<rbrace>
   lookup_ipc_buffer True thread
   \<lbrace>\<lambda>rv _. \<not> is_subject aag thread \<longrightarrow>
           (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st 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] integrity_tcb_in_ipc_def) apply (drule get_tcb_SomeD) apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def case_bool_if
                 split: if_split_asm) apply (erule tcb_in_ipc.cases; clarsimp simp: get_tcb_def vm_read_write_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st\<rbrace> lookup_ipc_buffer True thread \<lbrace>\<lambda>rv _. pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st\<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 _. pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st 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 _. pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)\<rbrace>
 2. \<And>s. (valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st) 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> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (cap = DomainCap \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (cap = IRQControlCap \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (x = ASIDControlCap \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st 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> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case Some $ xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd)) of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<not> (vm_read_write \<subseteq> xc \<or> vm_read_only \<subseteq> xc \<and> \<not> True) \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits))) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits)) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> (case None of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st 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; integrity_tcb_in_ipc aag X thread epptr tst st 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; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> auth_ipc_buffers st 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; integrity_tcb_in_ipc aag X thread epptr tst st 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; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> tcb_cnode_index 4 \<in> dom tcb_cap_cases
 2. \<And>s tcb xa xb xc xd xe. \<lbrakk>valid_objs s; integrity_tcb_in_ipc aag X thread epptr tst st 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; pasObjectAbs aag thread \<noteq> pasSubject aag; 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 st 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; integrity_tcb_in_ipc aag X thread epptr tst st 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; pasObjectAbs aag thread \<noteq> pasSubject aag; 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 st 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; pasObjectAbs aag thread \<noteq> pasSubject aag; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<Rightarrow> {} | _ \<Rightarrow> {}) then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag tst (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<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>valid_objs s; tcb_ipcframe tcb = ArchObjectCap (PageCap xa xb xc xd xe); vm_read_write \<subseteq> xc; pasObjectAbs aag thread \<noteq> pasSubject aag; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<Rightarrow> {} | _ \<Rightarrow> {}) then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag tst (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<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; pasObjectAbs aag thread \<noteq> pasSubject aag; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap xa xb xc xd xe)); pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<Rightarrow> {} | _ \<Rightarrow> {}) then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag tst (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); kheap s thread = Some (TCB tcb); valid_obj thread (TCB tcb) s\<rbrakk> \<Longrightarrow> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<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>integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<Rightarrow> {} | _ \<Rightarrow> {}) then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag tst (pasObjectAbs aag thread) epptr (kheap st thread) (Some (TCB tcb)); kheap s thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap False xb xc xd xe); vm_read_write \<subseteq> xc; pasObjectAbs aag thread \<noteq> pasSubject aag; caps_of_state s (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap False xb xc xd xe)); pas_refined aag st; \<not> xa; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state tcb) (getF tcb)); is_aligned (tcb_ipc_buffer tcb) msg_align_bits; valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> (case get_tcb thread st of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<Rightarrow> {} | _ \<Rightarrow> {}) = ptr_range (xb + (tcb_ipc_buffer tcb && mask (pageBitsForSize xd))) msg_align_bits proof (prove)
goal:
No subgoals!