theory ADT_IF_Refine

lemma kernel_entry_if_corres:
  "corres (prod_lift (dc \<oplus> dc))
     (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)
            and (\<lambda>s. scheduler_action s = resume_cur_thread)
            and (\<lambda>s. 0 < domain_time s) and valid_domain_list)
     (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s)
            and arch_extras
            and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
     (kernel_entry_if event tc) (kernelEntry_if event tc)" apply (simp add: kernel_entry_if_def kernelEntry_if_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split) apply simp apply (rule threadset_corresT) apply (erule arch_tcb_context_set_tcb_relation) apply (clarsimp simp: tcb_cap_cases_def) apply (rule allI[OF ball_tcb_cte_casesI]; clarsimp) apply (simp add: exst_same_def) apply (rule corres_split[OF handleEvent_corres_arch_extras]) apply (rule corres_stateAssert_assume_stronger[where Q=\<top> and
                        P="\<lambda>s. valid_domain_list s \<and>
                               (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and>
                               (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow>
                                 scheduler_action s = choose_new_thread)"]) apply (clarsimp simp: prod_lift_def) apply (clarsimp simp: state_relation_def) apply (wp hoare_TrueI threadSet_invs_trivial thread_set_invs_trivial thread_set_ct_running
                   threadSet_ct_running' thread_set_not_state_valid_sched hoare_vcg_const_imp_lift
                   handle_event_domain_time_inv handle_interrupt_valid_domain_time
                | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imps)+ apply (fastforce simp: invs_def cur_tcb_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (prod_lift (dc \<oplus> dc)) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (kernel_entry_if event tc) (kernelEntry_if event tc) proof (prove)
goal (1 subgoal):
 1. corres (prod_lift (dc \<oplus> dc)) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event event;
return (r, tc)
od) (do t <- getCurThread;
y <- threadSet (tcbArch_update (atcbContextSet tc)) t;
r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od) proof (prove)
goal (3 subgoals):
 1. corres (prod_lift (dc \<oplus> dc)) ?Q ?Q' (do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event event;
return (r, tc)
od) (do t <- getCurThread;
y <- threadSet (tcbArch_update (atcbContextSet tc)) t;
r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R4 t) (?R'4 ta) (do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event event;
return (r, tc)
od) (do y <- threadSet (tcbArch_update (atcbContextSet tc)) ta;
r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> corres (?r'8 t ta) (?P9 t) (?P'11 ta) (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t) (threadSet (tcbArch_update (atcbContextSet tc)) ta)
 2. \<And>t ta y ya. \<lbrakk>t = ta; ?r'8 t ta y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. ?P9 t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. ?P'11 ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t. corres (?r'8 t t) (?P9 t) (?P'11 t) (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t) (threadSet (tcbArch_update (atcbContextSet tc)) t)
 2. \<And>t ta y ya. \<lbrakk>t = ta; ?r'8 t ta y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. ?P9 t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. ?P'11 ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (11 subgoals):
 1. \<And>t tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) (tcbArch_update (atcbContextSet tc) tcb')
 2. \<And>t tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) = getF tcb
 3. \<And>t. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (atcbContextSet tc) tcb) = getF tcb
 4. \<And>t tcb'. exst_same tcb' (tcbArch_update (atcbContextSet tc) tcb')
 5. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 7. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 8. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>t tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) = getF tcb
 2. \<And>t. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (atcbContextSet tc) tcb) = getF tcb
 3. \<And>t tcb'. exst_same tcb' (tcbArch_update (atcbContextSet tc) tcb')
 4. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>t. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (atcbContextSet tc) tcb) = getF tcb
 2. \<And>t tcb'. exst_same tcb' (tcbArch_update (atcbContextSet tc) tcb')
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t tcb'. exst_same tcb' (tcbArch_update (atcbContextSet tc) tcb')
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R8 t ta y) (?R'8 t ta ya) (do r <- handle_event event;
return (r, tc)
od) (do r <- handleEvent event;
y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od)
 2. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>?R'8 t ta\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 6. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>t ta y ya r ra. \<lbrakk>t = ta; dc y ya; (dc \<oplus> dc) r ra\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (?R42 t ta y ya r) (?R'42 t ta y ya ra) (return (r, tc)) (do y <- stateAssert (\<lambda>s. valid_domain_list' s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (event = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (ra, tc)
od)
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t ta y\<rbrace> handle_event event \<lbrace>?R42 t ta y ya\<rbrace>
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'47 t ta ya\<rbrace> handleEvent event \<lbrace>?R'42 t ta y ya\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q45 t ta y\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras and ?Q'47 t ta ya\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>t ta y ya r ra. \<lbrakk>t = ta; dc y ya; (dc \<oplus> dc) r ra\<rbrakk> \<Longrightarrow> corres (prod_lift (dc \<oplus> dc)) (\<lambda>s. valid_domain_list s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and> (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) (\<lambda>_. True) (return (r, tc)) (return (ra, tc))
 2. \<And>t ta y ya r ra s s'. \<lbrakk>t = ta; dc y ya; (dc \<oplus> dc) r ra; (s, s') \<in> state_relation; valid_domain_list s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and> (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread); True\<rbrakk> \<Longrightarrow> valid_domain_list' s' \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s') \<and> (event = Interrupt \<longrightarrow> ksDomainTime s' = 0 \<longrightarrow> ksSchedulerAction s' = ChooseNewThread)
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t ta y\<rbrace> handle_event event \<lbrace>\<lambda>r s. valid_domain_list s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and> (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 4. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'47 t ta ya\<rbrace> handleEvent event \<lbrace>\<lambda>ra _. True\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q45 t ta y\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras and ?Q'47 t ta ya\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>t ta y ya r ra s s'. \<lbrakk>t = ta; dc y ya; (dc \<oplus> dc) r ra; (s, s') \<in> state_relation; valid_domain_list s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and> (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread); True\<rbrakk> \<Longrightarrow> valid_domain_list' s' \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s') \<and> (event = Interrupt \<longrightarrow> ksDomainTime s' = 0 \<longrightarrow> ksSchedulerAction s' = ChooseNewThread)
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t ta y\<rbrace> handle_event event \<lbrace>\<lambda>r s. valid_domain_list s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and> (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'47 t ta ya\<rbrace> handleEvent event \<lbrace>\<lambda>ra _. True\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q45 t ta y\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras and ?Q'47 t ta ya\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t ta y\<rbrace> handle_event event \<lbrace>\<lambda>r s. valid_domain_list s \<and> (event \<noteq> Interrupt \<longrightarrow> 0 < domain_time s) \<and> (event = Interrupt \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'47 t ta ya\<rbrace> handleEvent event \<lbrace>\<lambda>ra _. True\<rbrace>
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q45 t ta y\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (tcbArch_update (atcbContextSet tc)) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras and ?Q'47 t ta ya\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<Longrightarrow> tcb_at (cur_thread s) s \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> (event = Interrupt \<longrightarrow> domain_time s \<noteq> 0)
 2. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. (invs' sa \<and> tcb_at' (ksCurThread s) sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbArch_update (atcbContextSet tc) tcb)) \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko d p. ko_at' ko (ksCurThread s) sa \<and> inQ d p (tcbArch_update (atcbContextSet tc) ko) \<and> \<not> inQ d p ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbArch_update (atcbContextSet tc) tcb)) \<longrightarrow> ex_nonz_cap_to' (ksCurThread s) sa \<and> ksCurThread s \<noteq> ksCurThread sa) \<and> (\<forall>tcb. tcbQueued (tcbArch_update (atcbContextSet tc) tcb) \<and> ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> ksCurThread s \<noteq> ksCurThread sa)) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running' sa) \<and> ksSchedulerAction sa = ResumeCurrentThread \<and> arch_extras sa \<and> ?P'228 (ksCurThread s) sa)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. (invs' sa \<and> tcb_at' (ksCurThread s) sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbArch_update (atcbContextSet tc) tcb)) \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko d p. ko_at' ko (ksCurThread s) sa \<and> inQ d p (tcbArch_update (atcbContextSet tc) ko) \<and> \<not> inQ d p ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbArch_update (atcbContextSet tc) tcb)) \<longrightarrow> ex_nonz_cap_to' (ksCurThread s) sa \<and> ksCurThread s \<noteq> ksCurThread sa) \<and> (\<forall>tcb. tcbQueued (tcbArch_update (atcbContextSet tc) tcb) \<and> ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> ksCurThread s \<noteq> ksCurThread sa)) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running' sa) \<and> ksSchedulerAction sa = ResumeCurrentThread \<and> arch_extras sa \<and> ?P'228 (ksCurThread s) sa)) s)) s proof (prove)
goal:
No subgoals!