theory Ipc_AC

lemma update_tcb_state_in_ipc:
  "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s;
     receive_blocked_on epptr (tcb_state tcb); aag_has_auth_to aag SyncSend epptr;
     get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr> \<rbrakk>
     \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRFinalOrCall st
                              (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)" unfolding integrity_tcb_in_ipc_def apply (elim conjE) apply (intro conjI) apply assumption+ apply (erule integrity_trans) apply (simp cong: if_cong) apply clarsimp apply (erule tcb_in_ipc.cases, simp_all) apply (drule get_tcb_SomeD) apply (rule tii_final[OF refl refl]) apply (solves\<open>clarsimp\<close>) apply (elim exE, intro exI tcb.equality; solves \<open>simp\<close>) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_tcb_in_ipc aag X thread epptr TRContext st s; receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>\<rbrakk> \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRFinalOrCall st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread); receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb'), kheap := (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>))(thread := kheap st thread), machine_state := machine_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)\<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\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) thread) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb'), kheap := (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>))(thread := kheap st thread), machine_state := machine_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)\<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\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) thread) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<noteq> pasSubject aag
 2. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> pas_refined aag st
 3. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb'), kheap := (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>))(thread := kheap st thread), machine_state := machine_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)\<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\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)) p\<rparr>\<rparr>)
 4. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) thread) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb'), kheap := (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>))(thread := kheap st thread), machine_state := machine_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)\<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\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)) p\<rparr>\<rparr>)
 2. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) thread) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (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\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb'), kheap := (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>))(thread := kheap st thread), machine_state := machine_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)\<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\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)) p\<rparr>\<rparr>)
 2. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) thread) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (kheap (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) thread) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; 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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (kheap st thread) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (Some (TCB tcba)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag thread) epptr (Some (TCB tcba)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (4 subgoals):
 1. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> receive_blocked_on epptr (tcb_state tcba)
 2. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>ctxt'. tcb\<lparr>tcb_state := Running\<rparr> = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running\<rparr>
 3. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag
 4. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> TRFinalOrCall = TRFinal \<or> TRFinalOrCall = TRFinalOrCall proof (prove)
goal (3 subgoals):
 1. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>ctxt'. tcb\<lparr>tcb_state := Running\<rparr> = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running\<rparr>
 2. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag
 3. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> TRFinalOrCall = TRFinal \<or> TRFinalOrCall = TRFinalOrCall proof (prove)
goal (2 subgoals):
 1. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag
 2. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> TRFinalOrCall = TRFinal \<or> TRFinalOrCall = TRFinalOrCall proof (prove)
goal (1 subgoal):
 1. \<And>tcba tcb'a. \<lbrakk>receive_blocked_on epptr (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; tcb' = tcb\<lparr>tcb_state := Running\<rparr>; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcba), 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>); kheap st thread = Some (TCB tcba); kheap s thread = Some (TCB tcb'a); can_receive_ipc (tcb_state tcba); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba)\<rparr>; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> TRFinalOrCall = TRFinal \<or> TRFinalOrCall = TRFinalOrCall proof (prove)
goal:
No subgoals!