theory CNode_AC

lemma sts_respects_restart_ep:
  "\<lbrace>integrity aag X st and
    (\<lambda>s. \<exists>ep. aag_has_auth_to aag Reset ep \<and> st_tcb_at (blocked_on ep) thread s)\<rbrace>
   set_thread_state thread Restart
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_wp) apply (erule integrity_trans) apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def get_tcb_def integrity_asids_kh_upds) apply (rule_tac tro_tcb_restart [OF refl refl]) apply (fastforce dest!: get_tcb_SomeD) apply (fastforce dest!: get_tcb_SomeD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<exists>ep. (pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (blocked_on ep) thread s)\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<exists>ep. (pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (blocked_on ep) thread s)\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := Restart\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ep y. \<lbrakk>integrity aag X st s; (pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; st_tcb_at (blocked_on ep) thread s; get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (y\<lparr>tcb_state := Restart\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; st_tcb_at (blocked_on ep) thread s; get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (y\<lparr>tcb_state := Restart\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB y)) (Some (TCB (y\<lparr>tcb_state := Restart\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> y\<lparr>tcb_state := Restart\<rparr> = y\<lparr>tcb_state := Restart\<rparr>
 2. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> blocked_on (?ep28 s ep y) (tcb_state y)
 3. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset (?ep28 s ep y) proof (prove)
goal (2 subgoals):
 1. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> blocked_on (?ep28 s ep y) (tcb_state y)
 2. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset (?ep28 s ep y) proof (prove)
goal (1 subgoal):
 1. \<And>s ep y. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s thread = Some (TCB y); blocked_on ep (tcb_state y)\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset ep proof (prove)
goal:
No subgoals!