theory Ipc_AC

lemma integrity_tcb_in_fault_reply_refl:
  "\<lbrakk> st_tcb_at awaiting_reply receiver s; fault_tcb_at (flip (\<noteq>) None) receiver s;
     aag_has_auth_to aag Reply receiver; \<not> is_subject aag receiver; pas_refined aag s \<rbrakk>
     \<Longrightarrow> integrity_tcb_in_fault_reply aag X receiver TRFContext s s" unfolding integrity_tcb_in_fault_reply_def apply (clarsimp elim!: pred_tcb_atE) apply (rule tifr_context[OF refl refl]) apply (rule tcb_context_no_change) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at awaiting_reply receiver s; fault_tcb_at (swp (\<noteq>) None) receiver s; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s\<rbrakk> \<Longrightarrow> integrity_tcb_in_fault_reply aag X receiver TRFContext s s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at awaiting_reply receiver s; fault_tcb_at (swp (\<noteq>) None) receiver s; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag s \<and> integrity aag X s (s\<lparr>kheap := (kheap s)(receiver := kheap s receiver)\<rparr>) \<and> tcb_in_fault_reply aag TRFContext (pasObjectAbs aag receiver) (kheap s receiver) (kheap s receiver) proof (prove)
goal (1 subgoal):
 1. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag TRFContext (pasObjectAbs aag receiver) (Some (TCB tcb)) (Some (TCB tcb)) proof (prove)
goal (5 subgoals):
 1. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> \<exists>ctxt'. tcb = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>
 2. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag
 3. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> awaiting_reply (tcb_state tcb)
 4. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> tcb_fault tcb = Some (?fault5 tcb y)
 5. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> TRFContext = TRFContext proof (prove)
goal (4 subgoals):
 1. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag
 2. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> awaiting_reply (tcb_state tcb)
 3. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> tcb_fault tcb = Some (?fault5 tcb y)
 4. \<And>tcb y. \<lbrakk>(pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; awaiting_reply (tcb_state tcb); kheap s receiver = Some (TCB tcb); tcb_fault tcb = Some y\<rbrakk> \<Longrightarrow> TRFContext = TRFContext proof (prove)
goal:
No subgoals!