theory Ipc_AC

lemma integrity_tcb_in_ipc_no_call:
  "integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s
   \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinal st s" unfolding integrity_tcb_in_ipc_def tcb_in_ipc.simps by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinal st s proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> (is_subject aag receiver \<or> (\<exists>tcb tcb'. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> can_receive_ipc (tcb_state tcb) \<and> (\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>) \<and> TRFinalOrCall = TRContext) \<or> (\<exists>tcb tcb'. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> receive_blocked_on epptr (tcb_state tcb) \<and> (\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (TRFinalOrCall = TRFinal \<or> TRFinalOrCall = TRFinalOrCall)) \<or> (\<exists>tcb tcb' caller R. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> ep_recv_blocked epptr (tcb_state tcb) \<and> (\<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>) \<and> is_subject aag caller \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> TRFinalOrCall = TRFinal) \<or> (\<exists>tcb tcb'. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> (\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>) \<and> (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag \<and> awaiting_reply (tcb_state tcb) \<and> TRFinalOrCall = TRFinal)) \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> (is_subject aag receiver \<or> (\<exists>tcb tcb'. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> can_receive_ipc (tcb_state tcb) \<and> (\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>) \<and> TRFinal = TRContext) \<or> (\<exists>tcb tcb'. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> receive_blocked_on epptr (tcb_state tcb) \<and> (\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (TRFinal = TRFinal \<or> TRFinal = TRFinalOrCall)) \<or> (\<exists>tcb tcb' caller R. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> ep_recv_blocked epptr (tcb_state tcb) \<and> (\<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>) \<and> is_subject aag caller \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> TRFinal = TRFinal) \<or> (\<exists>tcb tcb'. kheap st receiver = Some (TCB tcb) \<and> kheap s receiver = Some (TCB tcb') \<and> (\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := Running\<rparr>) \<and> (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag \<and> awaiting_reply (tcb_state tcb) \<and> TRFinal = TRFinal))