theory Ipc_AC

lemma integrity_tcb_in_fault_reply_final:
  "integrity_tcb_in_fault_reply aag X thread TRFFinal st s \<Longrightarrow> integrity aag X st s" unfolding integrity_tcb_in_fault_reply_def apply clarsimp apply (erule integrity_trans) apply (clarsimp simp: integrity_def) apply (erule tcb_in_fault_reply.cases; clarsimp) apply (rule conjI) apply (fastforce intro!: tcb.equality tro_tcb_reply) apply (clarsimp simp: integrity_asids_kh_upds') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_tcb_in_fault_reply aag X thread TRFFinal st s \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. 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)\<rparr>) \<and> tcb_in_fault_reply aag TRFFinal (pasObjectAbs aag thread) (kheap st thread) (kheap s thread) \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>); tcb_in_fault_reply aag TRFFinal (pasObjectAbs aag thread) (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_fault_reply aag TRFFinal (pasObjectAbs aag thread) (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> integrity aag X (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; tcb_in_fault_reply aag TRFFinal (pasObjectAbs aag thread) (kheap st thread) (kheap s thread)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (kheap s thread) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb new_st fault ctxt'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := new_st\<rparr>)); new_st = Restart \<or> inactive new_st; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := new_st\<rparr>))) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb new_st fault ctxt'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := new_st\<rparr>)); new_st = Restart \<or> inactive new_st; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := new_st\<rparr>)))
 2. \<And>tcb new_st fault ctxt'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := new_st\<rparr>)); new_st = Restart \<or> inactive new_st; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb new_st fault ctxt'. \<lbrakk>pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := new_st\<rparr>)); new_st = Restart \<or> inactive new_st; (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) s proof (prove)
goal:
No subgoals!