theory Ipc_AC

lemma update_tcb_context_in_ipc:
  "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s; get_tcb thread s = Some tcb;
     tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr> \<rbrakk>
     \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRContext 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 (auto intro!: tii_context[OF refl refl] dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_tcb_in_ipc aag X thread epptr TRContext st s; get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>\<rbrakk> \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRContext 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); get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (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>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (pasObjectAbs aag thread) epptr (kheap st thread) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>tcba tcb'a. \<lbrakk>get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<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 TRContext (pasObjectAbs aag thread) epptr (Some (TCB tcba)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>))) proof (prove)
goal:
No subgoals!