theory Scheduler_IF

lemma timer_tick_reads_respects_scheduler_unobservable:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l
           ((\<lambda>s. \<not>reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag
                                                      and pas_refined aag and valid_sched)
           timer_tick" apply (simp add: timer_tick_def) apply (subst Let_def) apply (subst thread_set_time_slice_def)+ apply (simp add: bind_assoc[symmetric]) apply (rule bind_ev_pre) apply (simp add: bind_assoc) apply (rule timer_tick_snippit[OF domains_distinct]) apply (rule_tac P=\<top> and P'="(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and
                                 guarded_pas_domain aag and pas_refined aag and valid_sched"
                 in reads_respects_scheduler_unobservable'') apply (rule hoare_pre) apply (rule scheduler_equiv_lift) apply (wp gts_wp tcb_sched_action_unobservable
                      scheduler_equiv_lift| wpc | simp)+ apply (clarsimp simp: etcb_at_def split: option.splits) apply (intro impI conjI allI) apply (fastforce dest!: cur_thread_cur_domain)+ apply ((clarsimp simp add: st_tcb_at_def obj_at_def valid_sched_def)+)[3] apply (fastforce dest!: cur_thread_cur_domain) apply force apply (wp gts_wp | wpc)+ apply (clarsimp simp: etcb_at_def valid_sched_def st_tcb_at_def
                        obj_at_def valid_sched_action_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) timer_tick proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- 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 (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then thread_set_time_slice cur (ts - 1) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (do y <- do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od;
when (Suc 0 < numDomains) (do dom_time <- do y <- dec_domain_time;
gets domain_time
od;
when (dom_time = 0) reschedule_required
od)
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q1 rv) (when (Suc 0 < numDomains) (do dom_time <- do y <- dec_domain_time;
gets domain_time
od;
when (dom_time = 0) reschedule_required
od))
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'1 (do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od)
 3. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>?Q1\<rbrace>
 4. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q1 ()) (when (Suc 0 < numDomains) (do x <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od))
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'1 (do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od)
 3. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>?Q1\<rbrace>
 4. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'1 (do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od)
 2. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 3. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (5 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 4. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 5. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (6 subgoals):
 1. \<And>st. \<lbrace>?Q8 st\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st s. ((\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q8 st s
 3. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 5. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 6. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (11 subgoals):
 1. \<And>st sta. \<lbrace>globals_equiv_scheduler sta\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. \<lbrace>\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>silc_dom_equiv aag sta\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st s. ((\<lambda>_. True) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> scheduler_equiv aag st s
 8. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 10. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
A total of 11 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>st s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<Longrightarrow> st_tcb_at ((=) Running) (cur_thread s) s \<longrightarrow> etcb_at (\<lambda>t. (Suc 0 < tcb_time_slice t \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (\<not> Suc 0 < tcb_time_slice t \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_etcbs s \<and> valid_sched_action s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l)) (cur_thread s) s
 2. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 3. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 4. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (4 subgoals):
 1. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s\<rbrakk> \<Longrightarrow> (Suc 0 < tcb_time_slice x2 \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (\<not> Suc 0 < tcb_time_slice x2 \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_etcbs s \<and> valid_sched_action s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l)
 2. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 3. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 4. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (9 subgoals):
 1. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 2. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> valid_queues s
 3. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 4. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> valid_etcbs s
 5. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> valid_sched_action s
 6. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 7. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 8. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 9. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (7 subgoals):
 1. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> valid_sched_action s
 4. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 5. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 6. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 7. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (4 subgoals):
 1. \<And>st s x2. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ekheap s (cur_thread s) = Some x2; st_tcb_at ((=) Running) (cur_thread s) s; \<not> Suc 0 < tcb_time_slice x2\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 2. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 3. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 4. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (3 subgoals):
 1. \<And>s. ?P'1 s \<Longrightarrow> True \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 2. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 3. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> ?P'1 s \<and> ?P''1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''1\<rbrace> do cur <- gets cur_thread;
get_thread_state cur >>= case_thread_state (do ts <- ethread_get tcb_time_slice cur;
if 0 < ts - 1 then ethread_set (tcb_time_slice_update (\<lambda>_. ts - 1)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (return ()) (return ()) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())
od \<lbrace>\<lambda>a. pas_refined aag and valid_queues and valid_etcbs and valid_sched_action\<rbrace>
 2. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s) \<and> ?P''1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s) \<and> (\<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (st = Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> weak_valid_sched_action s \<and> valid_etcbs s \<and> True)) (cur_thread s) s) \<and> (inactive st \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (st = Restart \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (awaiting_reply st \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (idle st \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s)) proof (prove)
goal:
No subgoals!