theory Syscall_AI

lemma schedule_choose_new_thread_ct_activatable[wp]:
  "\<lbrace> invs \<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. ct_in_state activatable \<rbrace>" proof - have P: "\<And>t s. ct_in_state activatable (cur_thread_update (\<lambda>_. t) s) = st_tcb_at activatable t s" by (fastforce simp: ct_in_state_def st_tcb_at_def intro: obj_at_pspaceI) show ?thesis unfolding schedule_choose_new_thread_def choose_thread_def guarded_switch_to_def apply (simp add: P set_scheduler_action_def guarded_switch_to_def choose_thread_def
                             next_domain_def Let_def tcb_sched_action_def set_tcb_queue_def
                             get_tcb_queue_def ethread_get_def bind_assoc) apply (wpsimp wp: stt_activatable stit_activatable gts_wp)+ apply (force simp: ct_in_state_def pred_tcb_at_def obj_at_def invs_def valid_state_def
                       valid_idle_def split: if_split_asm)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t s. ct_in_state activatable (s\<lparr>cur_thread := t\<rparr>) = st_tcb_at activatable t s proof (state)
this:
ct_in_state activatable (?s\<lparr>cur_thread := ?t\<rparr>) = st_tcb_at activatable ?t ?s

goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (max_non_empty_queue queues));
assert (runnable ts);
switch_to_thread (hd (max_non_empty_queue queues))
od
od;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do dom_time <- gets domain_time;
y <- when (dom_time = 0) (modify (\<lambda>s. trans_state (\<lambda>e. e\<lparr>domain_index_internal := Suc (domain_index s) mod length (domain_list s), cur_domain_internal := fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), domain_time_internal := snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), work_units_completed_internal := 0\<rparr>) s));
x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
y <- if \<forall>prio. x prio = [] then switch_to_idle_thread else do ts <- get_thread_state (hd (max_non_empty_queue x));
y <- assert (runnable ts);
switch_to_thread (hd (max_non_empty_queue x))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> (domain_time s = 0 \<longrightarrow> (\<exists>prio. ready_queues s (fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s)))) prio \<noteq> []) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))))))) s \<longrightarrow> runnable st \<longrightarrow> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))))))) s)) \<and> (domain_time s \<noteq> 0 \<longrightarrow> (\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s \<longrightarrow> runnable st \<longrightarrow> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>invs\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. ct_in_state activatable\<rbrace>

goal:
No subgoals!