theory ArchDetSchedDomainTime_AI

lemma timer_tick_valid_domain_time:
  "\<lbrace> \<lambda>s :: det_ext state. 0 < domain_time s \<rbrace>
   timer_tick
   \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" (is "\<lbrace> ?dtnot0 \<rbrace> _ \<lbrace> _ \<rbrace>") unfolding timer_tick_def supply if_split[split del] supply ethread_get_wp[wp del] supply if_apply_def2[simp] apply (wpsimp
           wp: reschedule_required_valid_domain_time hoare_vcg_const_imp_lift gts_wp
               (* unless we hit dec_domain_time we know ?dtnot0 holds on the state, so clean up the
                  postcondition once we hit thread_set_time_slice *)
               hoare_post_imp[where Q="\<lambda>_. ?dtnot0" and R="\<lambda>_ s. domain_time s = 0 \<longrightarrow> X s"
                                and a="thread_set_time_slice t ts" for X t ts]
               hoare_drop_imp[where f="ethread_get t f" for t f]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> timer_tick \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do cur <- gets cur_thread;
state <- get_thread_state cur;
case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (1 < numDomains) (do dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do cur <- gets cur_thread;
state <- get_thread_state cur;
case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (1 < numDomains) (do dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do cur <- gets cur_thread;
state <- get_thread_state cur;
case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (1 < numDomains) (do dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do cur <- gets cur_thread;
state <- get_thread_state cur;
case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (1 < numDomains) (do dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s st. \<lbrakk>0 < domain_time s; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> (inactive st \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> (st = Restart \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> ((\<exists>x xa. st = BlockedOnReceive x xa) \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> ((\<exists>x xa. st = BlockedOnSend x xa) \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> (awaiting_reply st \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> ((\<exists>x. st = BlockedOnNotification x) \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> (idle st \<longrightarrow> \<not> Suc 0 < numDomains \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) proof (prove)
goal:
No subgoals!