theory Schedule_R

lemma setCurThread_invs_no_cicd'_idle_thread:
  "\<lbrace>invs_no_cicd' and (\<lambda>s. t = ksIdleThread s) \<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have ct_not_inQ_ct: "\<And>s t . \<lbrakk> ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr> ksCurThread := t \<rparr>)" apply (simp add: ct_not_inQ_def o_def) done have idle'_activatable': "\<And> s t. st_tcb_at' idle' t s \<Longrightarrow> st_tcb_at' activatable' t s" apply (clarsimp simp: st_tcb_at'_def o_def obj_at'_def) done show ?thesis apply (simp add: setCurThread_def) apply wp apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def) apply (frule (2) idle'_not_tcbQueued'[simplified o_def]) apply (clarsimp simp add: ct_not_inQ_ct idle'_activatable'
                              invs'_def cur_tcb'_def valid_state'_def valid_idle'_def
                              sch_act_wf ct_in_state'_def state_refs_of'_def
                              ps_clear_def valid_irq_node'_def
                              ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
                              valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def valid_queues'_def
                              pred_tcb_at'_def
                        cong: option.case_cong) apply (clarsimp simp: obj_at'_def projectKOs idle_tcb'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>ct_not_inQ ?s; obj_at' (\<lambda>x. \<not> tcbQueued x) ?t ?s\<rbrakk> \<Longrightarrow> ct_not_inQ (?s\<lparr>ksCurThread := ?t\<rparr>)

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s t. st_tcb_at' idle' t s \<Longrightarrow> st_tcb_at' activatable' t s proof (prove)
goal:
No subgoals! proof (state)
this:
st_tcb_at' idle' ?t ?s \<Longrightarrow> st_tcb_at' activatable' ?t ?s

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)) s \<Longrightarrow> invs' (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; valid_machine_state' s; cur_tcb' s; valid_queues' s; ct_not_inQ s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; t = ksIdleThread s\<rbrakk> \<Longrightarrow> invs' (s\<lparr>ksCurThread := ksIdleThread s\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; valid_machine_state' s; cur_tcb' s; valid_queues' s; ct_not_inQ s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; t = ksIdleThread s; obj_at' (\<lambda>x. \<not> tcbQueued x) (ksIdleThread s) s\<rbrakk> \<Longrightarrow> invs' (s\<lparr>ksCurThread := ksIdleThread s\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sym_refs (\<lambda>x. case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s) = {} then refs_of' ko else {}); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_global_refs' s; valid_arch_state' s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; valid_machine_state' s; tcb_at' (ksCurThread s) s; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ct_not_inQ s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; t = idle_thread_ptr; obj_at' (\<lambda>x. \<not> tcbQueued x) idle_thread_ptr s; \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s; \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrakk> \<Longrightarrow> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) idle_thread_ptr s) \<and> tcb_at' idle_thread_ptr s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. t = ksIdleThread s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!