theory Ipc_AC

lemma set_thread_state_running_respects:
  "\<lbrace>integrity aag X st and
    (\<lambda>s. \<exists>ep. aag_has_auth_to aag Receive ep \<and> st_tcb_at (send_blocked_on ep) sender s)\<rbrace>
   set_thread_state sender Running
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_wp) apply (erule integrity_trans) apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def integrity_asids_kh_upds) apply (clarsimp dest!: get_tcb_SomeD) apply (rule_tac new_st=Running in tro_tcb_receive) by (auto simp: tcb_bound_notification_reset_integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<exists>ep. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (send_blocked_on ep) sender s)\<rbrace> set_thread_state sender Running \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<exists>ep. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (send_blocked_on ep) sender s)\<rbrace> do tcb <- gets_the (get_tcb sender);
y <- set_object sender (TCB (tcb\<lparr>tcb_state := Running\<rparr>));
set_thread_state_ext sender
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ep y. \<lbrakk>integrity aag X st s; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; st_tcb_at (send_blocked_on ep) sender s; get_tcb sender s = Some y\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(sender \<mapsto> TCB (y\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ep y. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; st_tcb_at (send_blocked_on ep) sender s; get_tcb sender s = Some y\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := (kheap s)(sender \<mapsto> TCB (y\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ep y tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; get_tcb sender s = Some y; kheap s sender = Some (TCB tcb); send_blocked_on ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag sender) (Some (TCB tcb)) (Some (TCB (y\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag sender) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (6 subgoals):
 1. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB tcb) = Some (TCB (?tcb29 s ep tcb))
 2. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) = Some (TCB (?tcb'29 s ep tcb))
 3. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ?tcb'29 s ep tcb = ?tcb29 s ep tcb\<lparr>tcb_state := Running\<rparr>
 4. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Running = Running \<or> inactive Running \<and> call_blocked (?ep29 s ep tcb) (tcb_state (?tcb29 s ep tcb)) \<or> awaiting_reply Running \<and> allowed_call_blocked (?ep29 s ep tcb) (tcb_state (?tcb29 s ep tcb))
 5. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> send_blocked_on (?ep29 s ep tcb) (tcb_state (?tcb29 s ep tcb))
 6. \<And>s ep tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); kheap s sender = Some (TCB tcb)\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Receive (?ep29 s ep tcb)