theory ArchSyscall_AC

lemma set_thread_state_restart_to_running_respects[Syscall_AC_assms]:
  "\<lbrace>integrity aag X st and st_tcb_at ((=) Restart) thread and K (pasMayActivate aag)\<rbrace>
   do pc \<leftarrow> as_user thread getRestartPC;
            as_user thread $ setNextPC pc;
            set_thread_state thread Structures_A.thread_state.Running
   od
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_thread_state_def as_user_def split_def setNextPC_def
                   getRestartPC_def setRegister_def bind_assoc getRegister_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: in_monad fun_upd_def[symmetric] cong: if_cong) apply (cases "is_subject aag thread") apply (cut_tac aag=aag in integrity_update_autarch, simp+) apply (erule integrity_trans) apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def) apply (clarsimp dest!: get_tcb_SomeD) apply (rule_tac tro_tcb_activate[OF refl refl]) apply (simp add: tcb_bound_notification_reset_integrity_def ctxt_IP_update_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at ((=) Restart) thread and K (pasMayActivate aag)\<rbrace> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and st_tcb_at ((=) Restart) thread and (\<lambda>y. pasMayActivate aag)\<rbrace> do x <- gets_the (get_tcb thread);
xa <- select_f (gets (\<lambda>uc. uc FaultIP) (arch_tcb_context_get (tcb_arch x)));
y <- set_object thread (TCB (x\<lparr>tcb_arch := arch_tcb_context_set (snd xa) (tcb_arch x)\<rparr>));
x <- gets_the (get_tcb thread);
xa <- select_f (modify (\<lambda>uc. uc(NextIP := fst xa)) (arch_tcb_context_get (tcb_arch x)));
y <- set_object thread (TCB (x\<lparr>tcb_arch := arch_tcb_context_set (snd xa) (tcb_arch x)\<rparr>));
tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := Running\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b y ba ya yb. \<lbrakk>integrity_subjects {pasSubject aag} aag True X st s; st_tcb_at ((=) Restart) thread s; pasMayActivate aag; (a, b) \<in> fst (gets (\<lambda>uc. uc FaultIP) (arch_tcb_context_get (tcb_arch y))); get_tcb thread s = Some y; ((), ba) \<in> fst (modify (\<lambda>uc b. if b = NextIP then a else uc b) (arch_tcb_context_get (tcb_arch ya))); get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>))\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch ya)\<rparr>)) else kheap s a\<rparr>) = Some yb\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} aag True X st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (yb\<lparr>tcb_state := Running\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya yb. \<lbrakk>integrity_subjects {pasSubject aag} aag True X st s; st_tcb_at ((=) Restart) thread s; pasMayActivate aag; get_tcb thread s = Some y; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB y)\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch y) FaultIP)) (tcb_arch ya)\<rparr>))\<rparr>) = Some yb\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} aag True X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (yb\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y ya yb. \<lbrakk>integrity_subjects {pasSubject aag} aag True X st s; st_tcb_at ((=) Restart) thread s; pasMayActivate aag; get_tcb thread s = Some y; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB y)\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch y) FaultIP)) (tcb_arch ya)\<rparr>))\<rparr>) = Some yb; is_subject aag thread\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} aag True X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (yb\<lparr>tcb_state := Running\<rparr>))\<rparr>)
 2. \<And>s y ya yb. \<lbrakk>integrity_subjects {pasSubject aag} aag True X st s; st_tcb_at ((=) Restart) thread s; pasMayActivate aag; get_tcb thread s = Some y; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB y)\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch y) FaultIP)) (tcb_arch ya)\<rparr>))\<rparr>) = Some yb; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} aag True X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (yb\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya yb. \<lbrakk>integrity_subjects {pasSubject aag} aag True X st s; st_tcb_at ((=) Restart) thread s; pasMayActivate aag; get_tcb thread s = Some y; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB y)\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch y) FaultIP)) (tcb_arch ya)\<rparr>))\<rparr>) = Some yb; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} aag True X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (yb\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya yb. \<lbrakk>st_tcb_at ((=) Restart) thread s; pasMayActivate aag; get_tcb thread s = Some y; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB y)\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch y) FaultIP)) (tcb_arch ya)\<rparr>))\<rparr>) = Some yb; pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} aag True X s (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (yb\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya yb tcb. \<lbrakk>pasMayActivate aag; get_tcb thread s = Some y; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB y)\<rparr>) = Some ya; get_tcb thread (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch y) FaultIP)) (tcb_arch ya)\<rparr>))\<rparr>) = Some yb; pasObjectAbs aag thread \<noteq> pasSubject aag; kheap s thread = Some (TCB tcb); Restart = tcb_state tcb\<rbrakk> \<Longrightarrow> integrity_obj aag True {pasSubject aag} (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (yb\<lparr>tcb_state := Running\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ya. \<lbrakk>pasMayActivate aag; pasObjectAbs aag thread \<noteq> pasSubject aag; Restart = tcb_state ya; kheap s thread = Some (TCB ya)\<rbrakk> \<Longrightarrow> integrity_obj aag True {pasSubject aag} (pasObjectAbs aag thread) (Some (TCB ya)) (Some (TCB (ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch ya) FaultIP)) (tcb_arch ya), tcb_state := Running\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>s ya. \<lbrakk>pasMayActivate aag; pasObjectAbs aag thread \<noteq> pasSubject aag; Restart = tcb_state ya; kheap s thread = Some (TCB ya)\<rbrakk> \<Longrightarrow> ya\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch ya))(NextIP := arch_tcb_context_get (tcb_arch ya) FaultIP)) (tcb_arch ya), tcb_state := Running\<rparr> = ya\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch ya))) (tcb_arch ya), tcb_state := Running\<rparr>
 2. \<And>s ya. \<lbrakk>pasMayActivate aag; pasObjectAbs aag thread \<noteq> pasSubject aag; Restart = tcb_state ya; kheap s thread = Some (TCB ya)\<rbrakk> \<Longrightarrow> tcb_state ya = Restart
 3. \<And>s ya. \<lbrakk>pasMayActivate aag; pasObjectAbs aag thread \<noteq> pasSubject aag; Restart = tcb_state ya; kheap s thread = Some (TCB ya)\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!