theory Refine_C

lemma threadSet_all_invs_triv':
  "\<lbrace>all_invs' e and (\<lambda>s. t = ksCurThread s)\<rbrace>
  threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. all_invs' e\<rbrace>" unfolding all_invs'_def apply (rule hoare_pre) apply (rule wp_from_corres_unit) apply (rule threadset_corresT [where f="tcb_arch_update (arch_tcb_context_set f)"]) apply (simp add: tcb_relation_def arch_tcb_context_set_def
                         atcbContextSet_def arch_tcb_relation_def) apply (simp add: tcb_cap_cases_def) apply (simp add: tcb_cte_cases_def) apply (simp add: exst_same_def) apply (wp thread_set_invs_trivial thread_set_ct_running thread_set_not_state_valid_sched
              threadSet_invs_trivial threadSet_ct_running' hoare_weak_lift_imp
              thread_set_ct_in_state
           | simp add: tcb_cap_cases_def tcb_arch_ref_def
           | rule threadSet_ct_in_state'
           | wp (once) hoare_vcg_disj_lift)+ apply clarsimp apply (rule exI, rule conjI, assumption) apply (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def) apply (simp add: state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs' e and (\<lambda>s. t = ksCurThread s)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. all_invs' e\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 2. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. corres_underlying state_relation ?nf3 ?nf'3 ?r3 ?G3 ?G'3 ?f3 (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t)
 2. \<lbrace>?P3\<rbrace> ?f3 \<lbrace>\<lambda>_ s. einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 3. \<lbrace>?P'3\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 4. ?nf3 \<Longrightarrow> no_fail ?P3 ?f3
 5. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> ?P3 sa \<and> ?G3 sa \<and> ?P'3 s \<and> ?G'3 s proof (prove)
goal (8 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (tcb_arch_update (arch_tcb_context_set f) tcb) (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb')) tcb')
 2. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb_arch_update (arch_tcb_context_set f) tcb) = getF tcb
 3. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) = getF tcb
 4. \<And>tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb')) tcb')
 5. \<lbrace>?P3\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 6. \<lbrace>?P'3\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 7. False \<Longrightarrow> no_fail ?P3 (thread_set (tcb_arch_update (arch_tcb_context_set f)) t)
 8. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> ?P3 sa \<and> tcb_at t sa \<and> ?P'3 s \<and> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb_arch_update (arch_tcb_context_set f) tcb) = getF tcb
 2. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) = getF tcb
 3. \<And>tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb')) tcb')
 4. \<lbrace>?P3\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 5. \<lbrace>?P'3\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 6. False \<Longrightarrow> no_fail ?P3 (thread_set (tcb_arch_update (arch_tcb_context_set f)) t)
 7. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> ?P3 sa \<and> tcb_at t sa \<and> ?P'3 s \<and> tcb_at' t s proof (prove)
goal (6 subgoals):
 1. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) = getF tcb
 2. \<And>tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb')) tcb')
 3. \<lbrace>?P3\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 4. \<lbrace>?P'3\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 5. False \<Longrightarrow> no_fail ?P3 (thread_set (tcb_arch_update (arch_tcb_context_set f)) t)
 6. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> ?P3 sa \<and> tcb_at t sa \<and> ?P'3 s \<and> tcb_at' t s proof (prove)
goal (5 subgoals):
 1. \<And>tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb')) tcb')
 2. \<lbrace>?P3\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 3. \<lbrace>?P'3\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 4. False \<Longrightarrow> no_fail ?P3 (thread_set (tcb_arch_update (arch_tcb_context_set f)) t)
 5. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> ?P3 sa \<and> tcb_at t sa \<and> ?P'3 s \<and> tcb_at' t s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P3\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 2. \<lbrace>?P'3\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s'. invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace>
 3. False \<Longrightarrow> no_fail ?P3 (thread_set (tcb_arch_update (arch_tcb_context_set f)) t)
 4. \<And>s. ((\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s) \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) and (\<lambda>s. t = ksCurThread s)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> ?P3 sa \<and> tcb_at t sa \<and> ?P'3 s \<and> tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread) \<and> t = ksCurThread s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> tcb_at (ksCurThread s) sa \<and> invs' s \<and> tcb_at' (ksCurThread s) s \<and> vs_valid_duplicates' (ksPSpace s) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> (ct_running' s \<or> ct_idle' s) \<and> ksDomainTime s \<noteq> 0 \<and> ksSchedulerAction s = ResumeCurrentThread \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>t = ksCurThread s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> tcb_at (ksCurThread s) sa \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>t = ksCurThread s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa \<and> tcb_at (ksCurThread s) sa \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>t = ksCurThread s; (sa, s) \<in> state_relation; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread; valid_state sa; tcb_at (cur_thread sa) sa; valid_state' s; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> tcb_at (ksCurThread s) sa proof (prove)
goal:
No subgoals!