theory Ipc_AC

lemma sts_receive_Inactive_respects:
  "\<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread and
    (\<lambda>s. \<forall>tcb. get_tcb thread s = Some tcb \<longrightarrow> call_blocked ep (tcb_state tcb)) and
    K (aag_has_auth_to aag Receive ep)\<rbrace>
   set_thread_state thread Inactive
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 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) apply (drule get_tcb_SomeD) apply (rule_tac new_st=Inactive in tro_tcb_receive, simp_all) apply (fastforce simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread and (\<lambda>s. \<forall>tcb. get_tcb thread s = Some tcb \<longrightarrow> call_blocked ep (tcb_state tcb)) and K ((pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag)\<rbrace> set_thread_state thread Inactive \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread and (\<lambda>s. \<forall>tcb. get_tcb thread s = Some tcb \<longrightarrow> call_blocked ep (tcb_state tcb)) and (\<lambda>y. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag)\<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 := Inactive\<rparr>))\<rparr>)
od;
set_thread_state_ext thread
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and st_tcb_at (send_blocked_on ep) thread and (\<lambda>s. \<forall>tcb. get_tcb thread s = Some tcb \<longrightarrow> call_blocked ep (tcb_state tcb)) and (\<lambda>y. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag)) s \<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 Inactive aag X st s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>integrity aag X st s; st_tcb_at (send_blocked_on ep) thread s; call_blocked ep (tcb_state y); (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; 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 := Inactive\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>st_tcb_at (send_blocked_on ep) thread s; call_blocked ep (tcb_state y); (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; 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 := Inactive\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>st_tcb_at (send_blocked_on ep) thread s; call_blocked ep (tcb_state y); (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (y\<lparr>tcb_state := Inactive\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>st_tcb_at (send_blocked_on ep) thread s; call_blocked ep (tcb_state y); (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB tcb); kheap s thread = Some (TCB y)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (y\<lparr>tcb_state := Inactive\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>st_tcb_at (send_blocked_on ep) thread s; call_blocked ep (tcb_state tcb); (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; y = tcb; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> send_blocked_on ep (tcb_state tcb) proof (prove)
goal:
No subgoals!