theory Ipc_AC

lemma set_thread_state_blocked_on_reply_respects:
  "\<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread and
    pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread and
    K (aag_has_auth_to aag Receive ep)\<rbrace>
   set_thread_state thread BlockedOnReply
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (simp add: set_thread_state_def set_object_def get_object_def) apply wp apply clarsimp apply (erule integrity_trans) apply (clarsimp simp: integrity_def integrity_asids_kh_upds
                 dest!: get_tcb_SomeD elim!: pred_tcb_atE) apply (rule tro_tcb_receive[where new_st=BlockedOnReply]) by fastforce+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread and K ((pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag)\<rbrace> set_thread_state thread BlockedOnReply \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread\<rbrace> set_thread_state thread BlockedOnReply \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_thread_state thread BlockedOnReply \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (integrity aag X st and st_tcb_at (send_blocked_on ep) thread and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q2\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh thread = Some y);
return (the (kh thread))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>)
od;
set_thread_state_ext thread
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (integrity aag X st and st_tcb_at (send_blocked_on ep) thread and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (integrity aag X st and st_tcb_at (send_blocked_on ep) thread and pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread) s\<rbrakk> \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> (\<exists>y. kheap s thread = Some y) \<longrightarrow> a_type (the (kheap s thread)) = ATCB \<longrightarrow> integrity_once_ts_upd thread BlockedOnReply aag X st s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; integrity aag X st s; st_tcb_at (send_blocked_on ep) thread s; pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread s; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; st_tcb_at (send_blocked_on ep) thread s; pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread s; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>))) proof (prove)
goal (6 subgoals):
 1. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB tcb) = Some (TCB (?tcb47 s tcb))
 2. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>)) = Some (TCB (?tcb'47 s tcb))
 3. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ?tcb'47 s tcb = ?tcb47 s tcb\<lparr>tcb_state := BlockedOnReply\<rparr>
 4. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> BlockedOnReply = Running \<or> inactive BlockedOnReply \<and> call_blocked (?ep47 s tcb) (tcb_state (?tcb47 s tcb)) \<or> awaiting_reply BlockedOnReply \<and> allowed_call_blocked (?ep47 s tcb) (tcb_state (?tcb47 s tcb))
 5. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> send_blocked_on (?ep47 s tcb) (tcb_state (?tcb47 s tcb))
 6. \<And>s tcb. \<lbrakk>(pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; send_blocked_on ep (tcb_state tcb); allowed_call_blocked ep (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Receive (?ep47 s tcb)