theory Ipc_AC

lemma set_thread_state_respects_in_signalling:
  "\<lbrace>\<lambda>s. integrity aag X st s \<and> aag_has_auth_to aag Notify ntfnptr \<and>
        (is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s)\<rbrace>
   set_thread_state thread Running
   \<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 (cases "is_subject aag thread") apply (erule(1) integrity_update_autarch [unfolded fun_upd_def]) apply (erule integrity_trans) apply (drule get_tcb_SomeD) apply (clarsimp simp: integrity_def st_tcb_def2 integrity_asids_kh_upds) apply (clarsimp dest!: get_tcb_SomeD) apply (rule tro_tcb_send [OF refl refl]) apply (rule tcb.equality; simp; rule arch_tcb_context_set_eq[symmetric]) apply (auto simp: indirect_send_def direct_send_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s)\<rbrace> set_thread_state thread Running \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s)\<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 := Running\<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 s \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread 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 aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (the (get_tcb thread s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>integrity aag X st s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) 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 := Running\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb. \<lbrakk>integrity aag X st s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); is_subject aag thread\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := Running\<rparr>)) else kheap s a\<rparr>)
 2. \<And>s y tcb. \<lbrakk>integrity aag X st s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := Running\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>integrity aag X st s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := Running\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := Running\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; is_subject aag thread \<or> st_tcb_at (receive_blocked_on ntfnptr) thread s; kheap s thread = Some (TCB tcb); pasObjectAbs aag thread \<noteq> pasSubject aag; kheap s thread = Some (TCB y)\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_state := Running\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb tcba. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap s thread = Some (TCB tcb); get_tcb thread s = Some tcba; receive_blocked_on ntfnptr (tcb_state tcba)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; pasObjectAbs aag thread \<noteq> pasSubject aag; receive_blocked_on ntfnptr (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 := Running\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; pasObjectAbs aag thread \<noteq> pasSubject aag; receive_blocked_on ntfnptr (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> tcb\<lparr>tcb_state := Running\<rparr> = tcb\<lparr>tcb_arch := arch_tcb_context_set (?ctxt'45 s tcb) (tcb_arch tcb), tcb_state := Running\<rparr>
 2. \<And>s tcb. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; pasObjectAbs aag thread \<noteq> pasSubject aag; receive_blocked_on ntfnptr (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> direct_send {pasSubject aag} aag (?ep45 s tcb) tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) (?ep45 s tcb) tcb proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; pasObjectAbs aag thread \<noteq> pasSubject aag; receive_blocked_on ntfnptr (tcb_state tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> direct_send {pasSubject aag} aag (?ep45 s tcb) tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) (?ep45 s tcb) tcb proof (prove)
goal:
No subgoals!