theory DetSchedDomainTime_AI

lemma schedule_domain_time_left:
  "\<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<rbrace>
   schedule
   \<lbrace>\<lambda>_ s. 0 < domain_time s \<rbrace>" (is "\<lbrace>?P\<rbrace> _ \<lbrace>\<lambda>_ . ?Q\<rbrace>") supply word_neq_0_conv[simp] apply (simp add: schedule_def) apply (wp|wpc)+ apply (wp hoare_drop_imp)[1] apply (wpsimp wp: gts_wp ethread_get_inv)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> schedule \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> schedule \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>\<lambda>fastfail s. (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s \<longrightarrow> valid_domain_list s) \<and> (\<not> (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> valid_domain_list s) \<and> (\<not> (runnable ct_st \<and> ct_prio = target_prio) \<longrightarrow> 0 < domain_time s))\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B31 ct ct_st x x2 y it target_prio\<rbrace>
 3. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B29 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B30 ct ct_st x x2 y it\<rbrace>
 4. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B29 ct ct_st x x2 y\<rbrace>
 5. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B28 ct ct_st x x2\<rbrace>
 6. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 7. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> 0 < domain_time s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 8. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 9. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 10. \<And>s. (valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (9 subgoals):
 1. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>\<lambda>ct_prio s. valid_domain_list s \<and> valid_domain_list s \<and> 0 < domain_time s\<rbrace>
 2. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B29 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B30 ct ct_st x x2 y it\<rbrace>
 3. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B29 ct ct_st x x2 y\<rbrace>
 4. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B28 ct ct_st x x2\<rbrace>
 5. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 6. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> 0 < domain_time s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 7. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 9. \<And>s. (valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s st. \<lbrakk>valid_domain_list s; domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> (runnable st \<longrightarrow> 0 < domain_time s) \<and> (cur_thread s = idle_thread s \<longrightarrow> 0 < domain_time s)) \<and> ((\<exists>x. scheduler_action s = switch_thread x) \<longrightarrow> 0 < domain_time s) proof (prove)
goal:
No subgoals!