theory Ipc_AC

lemma as_user_set_register_respects_indirect:
  "\<lbrace>integrity aag X st and st_tcb_at ((=) Running) thread and
    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at receive_blocked thread st
                                  \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st) \<and>
       (aag_has_auth_to aag Notify ntfnptr))\<rbrace>
   as_user thread (set_register r v)
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: as_user_def split_def set_object_def get_object_def) apply wp apply (clarsimp simp: in_monad ) apply (cases "is_subject aag thread") apply (erule (1) integrity_update_autarch [unfolded fun_upd_def]) apply (clarsimp simp: st_tcb_def2 receive_blocked_def) apply (simp split: thread_state.split_asm) apply (rule send_upd_ctxintegrity [OF disjI2, unfolded fun_upd_def]) by (auto simp: st_tcb_def2 indirect_send_def pred_tcb_def2 dest: sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at ((=) Running) thread and K ((pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> as_user thread (set_register r v) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at ((=) Running) thread and (\<lambda>y. (pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> do tcb <- gets_the (get_tcb thread);
p <- select_f (set_register r v (arch_tcb_context_get (tcb_arch tcb)));
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_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and st_tcb_at ((=) Running) thread and (\<lambda>y. (pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (set_register r v (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). (\<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_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb thread s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a b. \<lbrakk>integrity aag X st s; st_tcb_at ((=) Running) thread s; pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb a b. \<lbrakk>integrity aag X st s; st_tcb_at ((=) Running) thread s; pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); is_subject aag thread\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s a\<rparr>)
 2. \<And>s y tcb a b. \<lbrakk>integrity aag X st s; st_tcb_at ((=) Running) thread s; pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); 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_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a b. \<lbrakk>integrity aag X st s; st_tcb_at ((=) Running) thread s; pasObjectAbs aag thread \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked thread st \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); 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_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a b tcba. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; case tcb_state tcba of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a b tcba x41 x42. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; tcb_state tcba = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s y tcb a b tcba x41 x42. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; tcb_state tcba = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> indirect_send {pasSubject aag} aag (the (tcb_bound_notification (?tcb70 s y tcb a b tcba x41 x42))) (?ep70 s y tcb a b tcba x41 x42) (?tcb70 s y tcb a b tcba x41 x42)
 2. \<And>s y tcb a b tcba x41 x42. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; tcb_state tcba = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> integrity aag X st s
 3. \<And>s y tcb a b tcba x41 x42. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; tcb_state tcba = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> st_tcb_at ((=) Running) thread s
 4. \<And>s y tcb a b tcba x41 x42. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; tcb_state tcba = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> get_tcb thread st = Some (?tcb70 s y tcb a b tcba x41 x42)
 5. \<And>s y tcb a b tcba x41 x42. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb thread s = Some y; kheap s thread = Some (TCB tcb); (a, b) \<in> fst (set_register r v (arch_tcb_context_get (tcb_arch y))); pasObjectAbs aag thread \<noteq> pasSubject aag; bound_tcb_at ((=) (Some ntfnptr)) thread st; get_tcb thread st = Some tcba; tcb_state tcba = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> get_tcb thread s = Some y