theory Ipc_AC

lemma set_thread_state_respects_in_fault_reply:
  "tst = Restart \<or> tst = Inactive \<Longrightarrow>
   \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>
   set_thread_state thread tst
   \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\<rbrace>" apply (simp add: set_thread_state_def) apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp) apply (clarsimp simp: integrity_tcb_in_fault_reply_def) apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD) apply (rule tifr_reply[OF refl refl]) apply (intro exI tcb.equality; simp) by fastforce+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tst = Restart \<or> inactive tst \<Longrightarrow> \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace> set_thread_state thread tst \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. tst = Restart \<or> inactive tst \<Longrightarrow> \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := tst\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tst = Restart \<or> inactive tst; integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st s\<rbrakk> \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> integrity_tcb_in_fault_reply aag X thread TRFFinal st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (the (get_tcb thread s)\<lparr>tcb_state := tst\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>tst = Restart \<or> inactive tst; 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 TRFRemoveFault (pasObjectAbs aag thread) (kheap st thread) (kheap s thread); get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag TRFFinal (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (y\<lparr>tcb_state := tst\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag TRFFinal (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 := tst\<rparr>))) proof (prove)
goal (6 subgoals):
 1. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>ctxt'a. tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None, tcb_state := tst\<rparr> = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt'a (tcb_arch tcb), tcb_fault := None, tcb_state := ?new_st31 s tcb fault ctxt'\<rparr>
 2. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> ?new_st31 s tcb fault ctxt' = Restart \<or> inactive (?new_st31 s tcb fault ctxt')
 3. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag
 4. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> awaiting_reply (tcb_state tcb)
 5. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> tcb_fault tcb = Some (?fault31 s tcb fault ctxt')
 6. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> TRFFinal = TRFFinal proof (prove)
goal (5 subgoals):
 1. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> tst = Restart \<or> inactive tst
 2. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag
 3. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> awaiting_reply (tcb_state tcb)
 4. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> tcb_fault tcb = Some (?fault31 s tcb fault ctxt')
 5. \<And>s tcb fault ctxt'. \<lbrakk>tst = Restart \<or> inactive tst; pasObjectAbs aag thread \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>); kheap st thread = Some (TCB tcb); (pasSubject aag, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag; awaiting_reply (tcb_state tcb); tcb_fault tcb = Some fault; kheap s thread = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_fault := None\<rparr>))\<rbrakk> \<Longrightarrow> TRFFinal = TRFFinal