theory Ipc_AC

lemma integrity_tcb_in_ipc_final:
  "integrity_tcb_in_ipc aag X thread epptr TRFinal st s \<Longrightarrow> integrity aag X st s" unfolding integrity_tcb_in_ipc_def apply clarsimp apply (erule integrity_trans) apply (clarsimp simp: integrity_def) apply (rule conjI) apply (erule tcb_in_ipc.cases; simp) apply (fastforce intro!: tro_tcb_send simp: direct_send_def) apply (fastforce intro!: tro_tcb_call simp: direct_call_def) apply clarsimp apply (fastforce intro!: tro_tcb_reply tcb.equality simp: direct_reply_def) apply (rule conjI) prefer 2 apply (clarsimp) apply (erule tcb_in_ipc.cases; clarsimp simp: integrity_asids_kh_upds' split: if_splits)
  \<comment> \<open>rm\<close> apply clarsimp apply (cases "is_subject aag thread") apply (rule trm_write) apply (solves\<open>simp\<close>)
  \<comment> \<open>doesn't own\<close> apply (erule tcb_in_ipc.cases, simp_all)[1] apply clarsimp apply (rule trm_ipc [where p' = thread]) apply (simp add: tcb_states_of_state_def get_tcb_def) apply (simp add: tcb_states_of_state_def get_tcb_def) apply (fastforce elim: auth_ipc_buffers_kheap_update) apply simp apply clarsimp apply (rule trm_ipc [where p' = thread]) apply (simp add: tcb_states_of_state_def get_tcb_def split: thread_state.splits) apply (simp add: tcb_states_of_state_def get_tcb_def) apply (fastforce elim: auth_ipc_buffers_kheap_update) apply simp apply clarsimp apply (rule trm_ipc [where p' = thread]) apply (simp add: tcb_states_of_state_def get_tcb_def split: thread_state.splits) apply (simp add: tcb_states_of_state_def get_tcb_def) apply (fastforce elim: auth_ipc_buffers_kheap_update) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_tcb_in_ipc aag X thread epptr TRFinal st s \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag thread \<noteq> pasSubject aag \<and> pas_refined aag st \<and> 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> auth_ipc_buffers st thread then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread) \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; 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> auth_ipc_buffers st thread then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity aag X (s\<lparr>kheap := (kheap s)(thread := kheap st thread), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st thread then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (kheap s thread) \<and> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (kheap s thread)
 2. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (4 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); receive_blocked_on epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))
 2. \<And>tcb tcb' caller R. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))
 3. \<And>tcb tcb'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))
 4. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcb' caller R. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))
 2. \<And>tcb tcb'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))
 3. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))
 2. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ctxt'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)))
 2. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 2. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s
 2. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s
 2. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> auth_ipc_buffers st thread \<longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); x \<in> auth_ipc_buffers st thread\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); x \<in> auth_ipc_buffers st thread; is_subject aag thread\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 2. \<And>x. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); x \<in> auth_ipc_buffers st thread; is_subject aag thread\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Write x
 2. \<And>x. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRFinal (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); receive_blocked_on epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 2. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 3. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 2. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 3. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (6 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> case tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
 2. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> tcb_states_of_state s thread = Some Running
 3. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 4. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 5. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 6. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (5 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> tcb_states_of_state s thread = Some Running
 2. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 3. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 4. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 5. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (4 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 2. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 3. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 4. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 2. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 3. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<And>x tcb tcb' caller R. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); ep_recv_blocked epptr (tcb_state tcb); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 2. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)
 2. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (5 subgoals):
 1. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> case tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
 2. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> tcb_states_of_state s thread = Some Running
 3. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 4. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 5. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (4 subgoals):
 1. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> tcb_states_of_state s thread = Some Running
 2. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 3. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 4. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 2. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 3. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<And>x tcb caller R ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); ep_recv_blocked epptr (tcb_state tcb); is_subject aag caller; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag}
 2. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (1 subgoal):
 1. \<And>x tcb tcb'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (1 subgoal):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (tcb_states_of_state s) (auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>)) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x) proof (prove)
goal (4 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> case tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
 2. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_states_of_state s thread = Some Running
 3. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 4. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag} proof (prove)
goal (3 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_states_of_state s thread = Some Running
 2. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 3. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag} proof (prove)
goal (2 subgoals):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
 2. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag} proof (prove)
goal (1 subgoal):
 1. \<And>x tcb ctxt'. \<lbrakk>pas_refined aag st; x \<in> auth_ipc_buffers st thread; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>)); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<notin> {pasSubject aag} proof (prove)
goal:
No subgoals!