theory Syscall_AC

lemma schedule_integrity:
  "\<lbrace>einvs and integrity aag X st and pas_refined aag and pas_cur_domain aag
          and (\<lambda>s. domain_time s \<noteq> 0) \<rbrace>
   schedule
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: schedule_def) apply (wpsimp wp: switch_to_thread_respects' guarded_switch_to_lift
                    switch_to_idle_thread_respects choose_thread_respects gts_wp hoare_drop_imps
                    set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued
                    tcb_sched_action_enqueue_valid_blocked_except tcb_sched_action_append_integrity'
         | simp add: allActiveTCBs_def schedule_choose_new_thread_def
         | rule hoare_pre_cont[where f=next_domain])+ apply (auto simp: obj_at_def st_tcb_at_def not_cur_thread_2_def valid_sched_def
                    valid_sched_action_def weak_valid_sched_action_def
                    valid_sched_action_switch_subject_thread) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0)\<rbrace> schedule \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and integrity aag X st and pas_refined aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0)\<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>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>invs s; valid_list s; valid_sched s; integrity aag X st s; pas_refined aag s; pas_cur_domain aag s; domain_time s \<noteq> 0\<rbrakk> \<Longrightarrow> (runnable sta \<longrightarrow> st_tcb_at ((=) sta) (cur_thread s) s \<longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable x s \<and> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s x))) \<and> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable x s \<and> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s x)))) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable (cur_thread s) s \<and> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s) \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) choose_new_thread (cur_thread s) \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s)) \<and> (\<not> runnable sta \<longrightarrow> st_tcb_at ((=) sta) (cur_thread s) s \<longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_queues s \<and> st_tcb_at runnable x s \<and> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s x))) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_queues s \<and> st_tcb_at runnable x s \<and> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s x)))) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> valid_queues s)) proof (prove)
goal:
No subgoals!