theory Ipc_AC

lemma as_user_respects_in_fault_reply:
  "as_user thread m \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>" apply (simp add: as_user_def) apply (wpsimp wp: 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_context[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> as_user thread m \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFContext 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);
(a, uc') <- select_f (m (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa. \<lbrakk>integrity_tcb_in_fault_reply aag X thread TRFContext st s; (x, xa) \<in> fst (m (arch_tcb_context_get (tcb_arch y))); get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> integrity_tcb_in_fault_reply aag X thread TRFContext st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa. \<lbrakk>(x, xa) \<in> fst (m (arch_tcb_context_get (tcb_arch y))); get_tcb thread s = Some y; 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)\<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag TRFContext (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa tcb fault ctxt'. \<lbrakk>(x, xa) \<in> fst (m ctxt'); 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 TRFContext (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch tcb)\<rparr>))) proof (prove)
goal (5 subgoals):
 1. \<And>s x xa tcb fault ctxt'. \<lbrakk>(x, xa) \<in> fst (m ctxt'); 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'. tcb\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch tcb)\<rparr> = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>
 2. \<And>s x xa tcb fault ctxt'. \<lbrakk>(x, xa) \<in> fst (m ctxt'); 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 x xa tcb fault ctxt'. \<lbrakk>(x, xa) \<in> fst (m ctxt'); 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 x xa tcb fault ctxt'. \<lbrakk>(x, xa) \<in> fst (m ctxt'); 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 (?fault57 s x xa tcb fault ctxt')
 5. \<And>s x xa tcb fault ctxt'. \<lbrakk>(x, xa) \<in> fst (m ctxt'); 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> TRFContext = TRFContext