theory Ipc_AC

lemma as_user_set_register_respects:
  "\<lbrace>integrity aag X st and st_tcb_at ((=) Running) thread and
    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st) \<and>
       (aag_has_auth_to aag SyncSend ep \<or> aag_has_auth_to aag Notify ep))\<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) apply (rule send_upd_ctxintegrity [OF disjI1, unfolded fun_upd_def]) apply (auto simp: direct_send_def st_tcb_def2) done

(* 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_on ep) thread st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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_on ep) thread st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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_on ep) thread st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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_on ep) thread st; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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_on ep) thread st; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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_on ep) thread st; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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_on ep) thread st; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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; get_tcb thread st = Some tcba; receive_blocked_on ep (tcb_state tcba)\<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. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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; get_tcb thread st = Some tcba; receive_blocked_on ep (tcb_state tcba)\<rbrakk> \<Longrightarrow> direct_send {pasSubject aag} aag (?ep35 s y tcb a b tcba) (?tcb35 s y tcb a b tcba)
 2. \<And>s y tcb a b tcba. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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; get_tcb thread st = Some tcba; receive_blocked_on ep (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity aag X st s
 3. \<And>s y tcb a b tcba. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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; get_tcb thread st = Some tcba; receive_blocked_on ep (tcb_state tcba)\<rbrakk> \<Longrightarrow> st_tcb_at ((=) Running) thread s
 4. \<And>s y tcb a b tcba. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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; get_tcb thread st = Some tcba; receive_blocked_on ep (tcb_state tcba)\<rbrakk> \<Longrightarrow> get_tcb thread st = Some (?tcb35 s y tcb a b tcba)
 5. \<And>s y tcb a b tcba. \<lbrakk>integrity aag X st s; Running = tcb_state y; (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<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; get_tcb thread st = Some tcba; receive_blocked_on ep (tcb_state tcba)\<rbrakk> \<Longrightarrow> get_tcb thread s = Some y proof (prove)
goal:
No subgoals!