theory Ipc_AC

lemma thread_set_no_fault_respects_in_fault_reply:
  "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
   thread_set (\<lambda>tcb. tcb \<lparr> tcb_fault := None \<rparr>) thread
   \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>" apply (simp add: thread_set_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_remove_fault[OF refl refl]) by fastforce+

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