theory Ipc_AC

lemma set_object_respects_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_subject aag ptr)\<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" apply (simp add: integrity_tcb_in_ipc_def) apply (rule hoare_pre, wp) apply (wpsimp wp: set_object_wp) apply (simp only: pred_conj_def) apply (elim conjE) apply (intro conjI ; (solves \<open>simp\<close>)?) apply (erule integrity_trans) apply (clarsimp simp: integrity_def) apply (clarsimp simp: fun_upd_def) apply (rule integrity_asids_kh_update[simplified fun_upd_def]) apply (cut_tac integrity_asids_update_autarch) apply (auto simp: fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_subject aag ptr)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. 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> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and (\<lambda>y. is_subject aag ptr)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_ s. 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> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'6\<rbrace> set_object ptr obj \<lbrace>\<lambda>rv s. 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> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace>
 2. \<And>s. ((\<lambda>s. 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> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and (\<lambda>y. is_subject aag ptr)) s \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> ?P'6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. 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> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and (\<lambda>y. is_subject aag ptr)) s \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj), kheap := (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)\<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\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. (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> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) \<and> is_subject aag ptr \<Longrightarrow> \<not> False \<and> True \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj), kheap := (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)\<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\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; 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>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> \<not> False \<and> True \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj), kheap := (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)\<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\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; 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>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj), kheap := (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)\<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\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)) p\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> integrity aag X (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>) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj), kheap := (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)\<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\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)) p\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) (s\<lparr>kheap := \<lambda>a. if a = receiver then kheap st receiver else if a = ptr then Some obj else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>) (s\<lparr>kheap := \<lambda>a. if a = receiver then kheap st receiver else if a = ptr then Some obj else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := kheap s\<rparr>) (s\<lparr>kheap := \<lambda>x. if x = ptr then Some obj else kheap s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x a. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>xa aa. integrity_asids (?aag60 s x a) {pasSubject (?aag60 s x a)} xa aa (?s60 s x a) (?s'60 s x a\<lparr>kheap := (kheap (?s'60 s x a))(?ptr60 s x a \<mapsto> ?obj60 s x a)\<rparr>)\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := kheap s\<rparr>) (s\<lparr>kheap := \<lambda>x. if x = ptr then Some obj else kheap s x\<rparr>)
 2. \<And>s x a. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> \<forall>xa aa. integrity_asids (?aag60 s x a) {pasSubject (?aag60 s x a)} xa aa (?s60 s x a) (?s'60 s x a)
 3. \<And>s x a. \<lbrakk>is_subject aag ptr; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> is_subject (?aag60 s x a) (?ptr60 s x a) proof (prove)
goal:
No subgoals!