theory Scheduler_IF

lemma timer_tick_reads_respects_scheduler_cur_domain:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l
           (reads_scheduler_cur_domain aag l 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 (wp when_ev reschedule_required_reads_respects_scheduler
            ethread_set_reads_respects_scheduler
            get_thread_state_reads_respects_scheduler gts_wp
         | wpc | wp (once) hoare_drop_imps)+ apply (fastforce simp: invs_def valid_state_def valid_idle_def pred_tcb_at_def obj_at_def
                         guarded_pas_domain_def scheduler_equiv_def domain_fields_equiv_def
                         valid_sched_def valid_sched_action_def
                  split: option.splits
                   dest: domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (reads_scheduler_cur_domain aag l 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) (reads_scheduler_cur_domain 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) (reads_scheduler_cur_domain 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) (reads_scheduler_cur_domain 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. \<And>s. (reads_scheduler_cur_domain aag l and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s \<Longrightarrow> reads_scheduler_cur_domain aag l s \<and> ((\<lambda>sa. st_tcb_at (\<lambda>_. True) (cur_thread s) sa \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l \<or> cur_thread s = idle_thread sa) and valid_idle) s \<and> (\<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> ((st = Running \<longrightarrow> K (pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) s \<and> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l \<and> pas_refined aag s \<and> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_etcbs s \<and> valid_sched_action s)) (cur_thread s) s) \<and> (inactive st \<longrightarrow> True) \<and> (st = Restart \<longrightarrow> True) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> True) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply st \<longrightarrow> True) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> True) \<and> (idle st \<longrightarrow> True)) \<and> (st = Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> 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> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> 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> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (st = Restart \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> 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> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> 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> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (awaiting_reply st \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s) \<and> (idle st \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s)) proof (prove)
goal:
No subgoals!