kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_R

lemma corres_gets_queues_getReadyQueuesL1Bitmap:
  "corres (\<lambda>qs l1. ((l1 = 0) = (\<forall>p. qs p = []))) \<top> valid_queues
    (gets (\<lambda>s. ready_queues s d)) (getReadyQueuesL1Bitmap d)" unfolding state_relation_def valid_queues_def getReadyQueuesL1Bitmap_def by (clarsimp simp: bitmapL1_zero_ksReadyQueues ready_queues_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>qs l1. (l1 = 0) = (\<forall>p. qs p = [])) (\<lambda>_. True) Invariants_H.valid_queues (gets (\<lambda>s. ready_queues s d)) (getReadyQueuesL1Bitmap d) proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'} False True (\<lambda>qs l1. (l1 = 0) = (\<forall>p. qs p = [])) (\<lambda>_. True) (\<lambda>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s) (gets (\<lambda>s. ready_queues s d)) (gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d))
theory Schedule_R

lemma bitmap_lookup_queue_is_max_non_empty:
  "\<lbrakk> valid_queues s'; (s, s') \<in> state_relation; invs s;
     ksReadyQueuesL1Bitmap s' (ksCurDomain s') \<noteq> 0 \<rbrakk>
   \<Longrightarrow> ksReadyQueues s' (ksCurDomain s', lookupBitmapPriority (ksCurDomain s') s') =
        max_non_empty_queue (ready_queues s (cur_domain s))" unfolding all_invs_but_ct_idle_or_in_cur_domain'_def valid_queues_def by (clarsimp simp add: max_non_empty_queue_def lookupBitmapPriority_Max_eqI
                         state_relation_def ready_queues_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invariants_H.valid_queues s'; (s, s') \<in> state_relation; invs s; ksReadyQueuesL1Bitmap s' (ksCurDomain s') \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s' (ksCurDomain s', lookupBitmapPriority (ksCurDomain s') s') = max_non_empty_queue (ready_queues s (cur_domain s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues_no_bitmap s' \<and> valid_bitmapQ s' \<and> bitmapQ_no_L2_orphans s' \<and> bitmapQ_no_L1_orphans s'; (s, s') \<in> state_relation; invs s; ksReadyQueuesL1Bitmap s' (ksCurDomain s') \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s' (ksCurDomain s', lookupBitmapPriority (ksCurDomain s') s') = max_non_empty_queue (ready_queues s (cur_domain s))
theory Schedule_R

lemma ksReadyQueuesL1Bitmap_return_wp:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s d) s \<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>rv s. P rv s\<rbrace>" unfolding getReadyQueuesL1Bitmap_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s d) s\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s d) s\<rbrace> gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d) \<lbrace>P\<rbrace>
theory Schedule_R

lemma curDomain_or_return_0:
  "\<lbrakk> \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. Q rv s \<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain \<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv s. Q rv s \<rbrace>" apply (case_tac "1 < numDomains"; simp) apply (simp add: valid_def curDomain_def simpler_gets_def return_def maxDomain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> curDomain \<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> curDomain \<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain; \<not> Suc 0 < numDomains\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> return 0 \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma invs_no_cicd_ksCurDomain_maxDomain':
  "invs_no_cicd' s \<Longrightarrow> ksCurDomain s \<le> maxDomain" unfolding invs_no_cicd'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ksCurDomain s \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s \<Longrightarrow> ksCurDomain s \<le> maxDomain
theory Schedule_R

lemma thread_get_comm: "do x \<leftarrow> thread_get f p; y \<leftarrow> gets g; k x y od =
           do y \<leftarrow> gets g; x \<leftarrow> thread_get f p; k x y od" apply (rule ext) apply (clarsimp simp add: gets_the_def assert_opt_def
                   bind_def gets_def get_def return_def
                   thread_get_def
                   fail_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- thread_get f p;
gets g >>= k x
od = do y <- gets g;
x <- thread_get f p;
k x y
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- thread_get f p;
gets g >>= k x
od) x = (do y <- gets g;
x <- thread_get f p;
k x y
od) x proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma schact_bind_inside: "do x \<leftarrow> f; (case act of resume_cur_thread \<Rightarrow> f1 x
                     | switch_thread t \<Rightarrow> f2 t x
                     | choose_new_thread \<Rightarrow> f3 x) od
          = (case act of resume_cur_thread \<Rightarrow> (do x \<leftarrow> f; f1 x od)
                     | switch_thread t \<Rightarrow> (do x \<leftarrow> f; f2 t x od)
                     | choose_new_thread \<Rightarrow> (do x \<leftarrow> f; f3 x od))" apply (case_tac act,simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- f;
case act of resume_cur_thread \<Rightarrow> f1 x | switch_thread t \<Rightarrow> f2 t x | choose_new_thread \<Rightarrow> f3 x
od = (case act of resume_cur_thread \<Rightarrow> f >>= f1 | switch_thread t \<Rightarrow> f >>= f2 t | choose_new_thread \<Rightarrow> f >>= f3) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma getDomainTime_corres:
  "corres (=) \<top> \<top> (gets domain_time) getDomainTime" by (simp add: getDomainTime_def state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets domain_time) getDomainTime
theory Schedule_R

lemma nextDomain_corres:
  "corres dc \<top> \<top> next_domain nextDomain" apply (simp add: next_domain_def nextDomain_def) apply (rule corres_modify) apply (simp add: state_relation_def Let_def dschLength_def dschDomain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) next_domain nextDomain proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (modify (\<lambda>s. let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s)) (modify (\<lambda>ks. let ksDomScheduleIdx' = Suc (ksDomScheduleIdx ks) mod length (ksDomSchedule ks); next = ksDomSchedule ks ! ksDomScheduleIdx' in ks\<lparr>ksWorkUnitsCompleted := 0, ksDomScheduleIdx := ksDomScheduleIdx', ksCurDomain := dschDomain next, ksDomainTime := dschLength next\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s, let ksDomScheduleIdx' = Suc (ksDomScheduleIdx s') mod length (ksDomSchedule s'); next = ksDomSchedule s' ! ksDomScheduleIdx' in s'\<lparr>ksWorkUnitsCompleted := 0, ksDomScheduleIdx := ksDomScheduleIdx', ksCurDomain := dschDomain next, ksDomainTime := dschLength next\<rparr>) \<in> state_relation proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma next_domain_valid_sched[wp]:
  "\<lbrace> valid_sched and (\<lambda>s. scheduler_action s  = choose_new_thread)\<rbrace> next_domain \<lbrace> \<lambda>_. valid_sched \<rbrace>" apply (simp add: next_domain_def Let_def) apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def) apply (simp add:valid_blocked_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> next_domain \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> modify (\<lambda>s. trans_state (\<lambda>e. e\<lparr>domain_index_internal := Suc (domain_index s) mod length (domain_list s), cur_domain_internal := fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), domain_time_internal := snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), work_units_completed_internal := 0\<rparr>) s) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<and> DetSchedInvs_AI.valid_queues s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> ct_not_queued s) \<and> is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma nextDomain_invs_no_cicd':
  "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> nextDomain \<lbrace> \<lambda>_. invs_no_cicd' \<rbrace>" apply (simp add: nextDomain_def Let_def dschLength_def dschDomain_def) apply wp apply (clarsimp simp: invs'_def valid_state'_def valid_machine_state'_def
                        ct_not_inQ_def cur_tcb'_def ct_idle_or_in_cur_domain'_def dschDomain_def
                        all_invs_but_ct_idle_or_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> nextDomain \<lbrace>\<lambda>_. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := 0, ksDomScheduleIdx := Suc (ksDomScheduleIdx ks) mod length (ksDomSchedule ks), ksCurDomain := fst (ksDomSchedule ks ! (Suc (ksDomScheduleIdx ks) mod length (ksDomSchedule ks))), ksDomainTime := snd (ksDomSchedule ks ! (Suc (ksDomScheduleIdx ks) mod length (ksDomSchedule ks)))\<rparr>) \<lbrace>\<lambda>_. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' (s\<lparr>ksWorkUnitsCompleted := 0, ksDomScheduleIdx := Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s), ksCurDomain := fst (ksDomSchedule s ! (Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s))), ksDomainTime := snd (ksDomSchedule s ! (Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s)))\<rparr>) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma scheduleSwitchThreadFastfail_corres:
  "\<lbrakk> ct \<noteq> it \<longrightarrow> (tp = tp' \<and> cp = cp') ; ct = ct' ; it = it' \<rbrakk> \<Longrightarrow>
   corres ((=)) (is_etcb_at ct) (tcb_at' ct)
     (schedule_switch_thread_fastfail ct it cp tp)
     (scheduleSwitchThreadFastfail ct' it' cp' tp')" by (clarsimp simp: schedule_switch_thread_fastfail_def scheduleSwitchThreadFastfail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct \<noteq> it \<longrightarrow> tp = tp' \<and> cp = cp'; ct = ct'; it = it'\<rbrakk> \<Longrightarrow> corres (=) (is_etcb_at ct) (tcb_at' ct) (schedule_switch_thread_fastfail ct it cp tp) (scheduleSwitchThreadFastfail ct' it' cp' tp')
theory Schedule_R

lemma gets_is_highest_prio_expand:
  "gets (is_highest_prio d p) \<equiv> do
    q \<leftarrow> gets (\<lambda>s. ready_queues s d);
    return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)
   od" by (clarsimp simp: is_highest_prio_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets (is_highest_prio d p) \<equiv> do q <- gets (\<lambda>s. ready_queues s d);
return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)
od
theory Schedule_R

lemma setSchedulerAction_invs': (* not in wp set, clobbered by ssa_wp *)
  "\<lbrace>\<lambda>s. invs' s \<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>_. invs' \<rbrace>" by (wpsimp simp: invs'_def cur_tcb'_def valid_state'_def valid_irq_node'_def ct_not_inQ_def
                   valid_queues_def valid_queues_no_bitmap_def valid_queues'_def
                   ct_idle_or_in_cur_domain'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>_. invs'\<rbrace>
theory Schedule_R

lemma ethread_get_when_corres:
  assumes x: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> r (f etcb) (f' tcb')"
  shows      "corres (\<lambda>rv rv'. b \<longrightarrow> r rv rv') (is_etcb_at t) (tcb_at' t)
                (ethread_get_when b f t) (threadGet f' t)" apply (clarsimp simp: ethread_get_when_def) apply (rule conjI; clarsimp) apply (rule corres_guard_imp, rule ethreadget_corres; simp add: x) apply (clarsimp simp: threadGet_def) apply (rule corres_noop) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. b \<longrightarrow> r rv rv') (is_etcb_at t) (tcb_at' t) (ethread_get_when b f t) (threadGet f' t) proof (prove)
goal (1 subgoal):
 1. (b \<longrightarrow> corres r (is_etcb_at t) (tcb_at' t) (ethread_get f t) (threadGet f' t)) \<and> (\<not> b \<longrightarrow> corres (\<lambda>rv rv'. True) (is_etcb_at t) (tcb_at' t) (return undefined) (threadGet f' t)) proof (prove)
goal (2 subgoals):
 1. b \<Longrightarrow> corres r (is_etcb_at t) (tcb_at' t) (ethread_get f t) (threadGet f' t)
 2. \<not> b \<Longrightarrow> corres (\<lambda>rv rv'. True) (is_etcb_at t) (tcb_at' t) (return undefined) (threadGet f' t) proof (prove)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> corres (\<lambda>rv rv'. True) (is_etcb_at t) (tcb_at' t) (return undefined) (threadGet f' t) proof (prove)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> corres (\<lambda>x rv'. True) (is_etcb_at t) (tcb_at' t) (return undefined) (getObject t) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> b; is_etcb_at t s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> tcb_at' t s'\<rbrace> getObject t \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation \<and> True\<rbrace>
 2. \<And>s. \<lbrakk>\<not> b; is_etcb_at t s; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> tcb_at' t s') (getObject t) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma ssa_ct_not_inQ:
  "\<lbrace>\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
   setSchedulerAction sa \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>" by (simp add: setSchedulerAction_def ct_not_inQ_def, wp, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>
theory Schedule_R

lemma ssa_invs':
  "\<lbrace>invs' and sch_act_wf sa and
    (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) and
    (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace>
   setSchedulerAction sa \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (wp ssa_all_invs_but_ct_not_inQ'') apply (clarsimp simp add: invs'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_wf sa and (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) and (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_wf sa and (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) and (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)) s \<Longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> sch_act_wf sa s \<and> (sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) \<and> (sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma getDomainTime_wp[wp]: "\<lbrace>\<lambda>s. P (ksDomainTime s) s \<rbrace> getDomainTime \<lbrace> P \<rbrace>" unfolding getDomainTime_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomainTime s) s\<rbrace> getDomainTime \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomainTime s) s\<rbrace> gets ksDomainTime \<lbrace>P\<rbrace>
theory Schedule_R

lemma switchToThread_ct_not_queued_2:
  "\<lbrace>invs_no_cicd' and tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>"
  (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") apply (simp add: Thread_H.switchToThread_def) apply (wp) apply (simp add: ARM_H.switchToThread_def setCurThread_def) apply (wp tcbSchedDequeue_not_tcbQueued | simp )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t\<rbrace> do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrace>?B2 y ya\<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> tcbSchedDequeue t \<lbrace>?B2 y\<rbrace>
 3. \<lbrace>?Q\<rbrace> Arch.switchToThread t \<lbrace>?B1\<rbrace>
 4. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?B2 () ()\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> tcbSchedDequeue t \<lbrace>?B2 y\<rbrace>
 3. \<lbrace>?Q\<rbrace> Arch.switchToThread t \<lbrace>?B1\<rbrace>
 4. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma setCurThread_obj_at':
  "\<lbrace> obj_at' P t \<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s \<rbrace>" proof - show ?thesis apply (simp add: setCurThread_def) apply wp apply (simp add: ct_in_state'_def st_tcb_at'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> obj_at' P (ksCurThread (s\<lparr>ksCurThread := t\<rparr>)) (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>obj_at' P t\<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s\<rbrace>

goal:
No subgoals!