theory Syscall_R

lemma setDomain_invs':
  "\<lbrace>invs' and sch_act_simple and ct_active' and
  (tcb_at' ptr and
  (\<lambda>s. sch_act_not ptr s) and
  (\<lambda>y. domain \<le> maxDomain))\<rbrace>
  setDomain ptr domain \<lbrace>\<lambda>y. invs'\<rbrace>" apply (simp add:setDomain_def ) apply (wp add: when_wp hoare_weak_lift_imp hoare_weak_lift_imp_conj rescheduleRequired_all_invs_but_extra
    tcbSchedEnqueue_valid_action hoare_vcg_if_lift2) apply (rule_tac Q = "\<lambda>r s. all_invs_but_sch_extra s \<and> curThread = ksCurThread s
      \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)"
      in hoare_strengthen_post[rotated]) apply (clarsimp simp:invs'_def valid_state'_def st_tcb_at'_def[symmetric] valid_pspace'_def) apply (erule st_tcb_ex_cap'') apply simp apply (case_tac st,simp_all)[1] apply (rule hoare_strengthen_post[OF hoare_vcg_conj_lift]) apply (rule threadSet_all_invs_but_sch_extra) prefer 2 apply clarsimp apply assumption apply (wp hoare_weak_lift_imp threadSet_pred_tcb_no_state threadSet_not_curthread_ct_domain
               threadSet_tcbDomain_update_ct_not_inQ | simp)+ apply (rule_tac Q = "\<lambda>r s. invs' s \<and> curThread = ksCurThread s \<and> sch_act_simple s
                             \<and> domain \<le> maxDomain
                             \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_not ptr s)"
      in hoare_strengthen_post[rotated]) apply (clarsimp simp:invs'_def valid_state'_def) apply (wp hoare_vcg_imp_lift)+ apply (clarsimp simp:invs'_def valid_pspace'_def valid_state'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))\<rbrace> setDomain ptr domain \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))\<rbrace> do curThread <- getCurThread;
y <- tcbSchedDequeue ptr;
y <- threadSet (tcbDomain_update (\<lambda>_. domain)) ptr;
runnable <- isRunnable ptr;
y <- when runnable (tcbSchedEnqueue ptr);
when (ptr = curThread) rescheduleRequired
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curThread y. \<lbrace>?B2 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>ya s. (st_tcb_at' runnable' ptr s \<longrightarrow> (ptr = curThread \<longrightarrow> valid_pspace' s \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' ptr and valid_objs') s \<and> sym_refs (state_refs_of' s) \<and> (if_live_then_nonz_cap' and ex_nonz_cap_to' ptr) 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> untyped_ranges_zero' s \<and> (valid_queues' and st_tcb_at' runnable' ptr) 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> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> (ptr \<noteq> curThread \<longrightarrow> (invs' and st_tcb_at' runnable' ptr and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> ptr)) s)) \<and> (\<not> st_tcb_at' runnable' ptr s \<longrightarrow> (if ptr = curThread then \<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) else invs') s)\<rbrace>
 2. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>?B2 curThread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread y rv s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s) \<Longrightarrow> (st_tcb_at' runnable' ptr s \<longrightarrow> (ptr = curThread \<longrightarrow> valid_pspace' s \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' ptr and valid_objs') s \<and> sym_refs (state_refs_of' s) \<and> (if_live_then_nonz_cap' and ex_nonz_cap_to' ptr) 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> untyped_ranges_zero' s \<and> (valid_queues' and st_tcb_at' runnable' ptr) 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> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> (ptr \<noteq> curThread \<longrightarrow> (invs' and st_tcb_at' runnable' ptr and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> ptr)) s)) \<and> (\<not> st_tcb_at' runnable' ptr s \<longrightarrow> (if ptr = curThread then \<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) else invs') s)
 2. \<And>curThread y. \<lbrace>?B2 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>r s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>?B2 curThread\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' 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; untyped_ranges_zero' s; valid_queues' 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)); \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s; ptr = ksCurThread s; st_tcb_at' runnable' (ksCurThread s) s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 2. \<And>curThread y. \<lbrace>?B2 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>r s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>?B2 curThread\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' 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; untyped_ranges_zero' s; valid_queues' 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)); \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s; ptr = ksCurThread s\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap' s
 2. \<And>s st. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' 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; untyped_ranges_zero' s; valid_queues' 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)); \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s; ptr = ksCurThread s; runnable' st\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState
 3. \<And>curThread y. \<lbrace>?B2 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>r s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)\<rbrace>
 4. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>?B2 curThread\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 6. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>s st. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' 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; untyped_ranges_zero' s; valid_queues' 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)); \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s; ptr = ksCurThread s; runnable' st\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState
 2. \<And>curThread y. \<lbrace>?B2 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>r s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>?B2 curThread\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>curThread y. \<lbrace>?B2 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>r s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)\<rbrace>
 2. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>?B2 curThread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>curThread y. \<lbrace>?P113 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>?Q113 curThread y\<rbrace>
 2. \<And>curThread y. \<lbrace>?P'113 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>?Q'113 curThread y\<rbrace>
 3. \<And>curThread y rv s. ?Q113 curThread y rv s \<and> ?Q'113 curThread y rv s \<Longrightarrow> (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)
 4. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>y s. ?P113 curThread y s \<and> ?P'113 curThread y s\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 6. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread y. \<lbrace>?P'113 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>?Q'113 curThread y\<rbrace>
 2. \<And>curThread y rv s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> ?Q'113 curThread y rv s \<Longrightarrow> (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>y s. (tcb_at' ptr and (\<lambda>s. \<forall>p. ptr \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (domain \<le> maxDomain)) s \<and> ?P'113 curThread y s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread y rv s. (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> ?Q'113 curThread y rv s \<Longrightarrow> (valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)
 2. \<And>curThread y. \<lbrace>?P'113 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>?Q'113 curThread y\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>y s. (tcb_at' ptr and (\<lambda>s. \<forall>p. ptr \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (domain \<le> maxDomain)) s \<and> ?P'113 curThread y s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread s. \<lbrakk>valid_pspace' 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; untyped_ranges_zero' s; valid_queues' 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)); \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s; ?Q'113 curThread () () s\<rbrakk> \<Longrightarrow> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ct_idle_or_in_cur_domain' s)
 2. \<And>curThread y. \<lbrace>?P'113 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>?Q'113 curThread y\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>y s. (tcb_at' ptr and (\<lambda>s. \<forall>p. ptr \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (domain \<le> maxDomain)) s \<and> ?P'113 curThread y s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>curThread y. \<lbrace>?P'113 curThread y\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) ptr \<lbrace>\<lambda>a b. curThread = ksCurThread b \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ b \<and> sch_act_wf (ksSchedulerAction b) b \<and> ct_idle_or_in_cur_domain' b)\<rbrace>
 2. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>y s. (tcb_at' ptr and (\<lambda>s. \<forall>p. ptr \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (domain \<le> maxDomain)) s \<and> ?P'113 curThread y s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>curThread. \<lbrace>?P'190 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>rv s. 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> untyped_ranges_zero' s \<and> valid_queues' 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> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) \<and> sch_act_simple s \<and> domain \<le> maxDomain \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not ptr s \<and> ptr \<noteq> ksCurThread s \<and> ct_idle_or_in_cur_domain' s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>\<lambda>curThread s. tcb_at' ptr s \<and> (Invariants_H.valid_queues and tcb_at' ptr and K (ptr = ptr)) s \<and> valid_pspace' s \<and> ?P'190 curThread s\<rbrace>
 3. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>curThread rv s. invs' s \<and> curThread = ksCurThread s \<and> sch_act_simple s \<and> domain \<le> maxDomain \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_not ptr s) \<Longrightarrow> 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> untyped_ranges_zero' s \<and> valid_queues' 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> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) \<and> sch_act_simple s \<and> domain \<le> maxDomain \<and> curThread = ksCurThread s \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not ptr s \<and> ptr \<noteq> ksCurThread s \<and> ct_idle_or_in_cur_domain' s)
 2. \<And>curThread. \<lbrace>?P'190 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>r s. invs' s \<and> curThread = ksCurThread s \<and> sch_act_simple s \<and> domain \<le> maxDomain \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_not ptr s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>\<lambda>curThread s. tcb_at' ptr s \<and> (Invariants_H.valid_queues and tcb_at' ptr and K (ptr = ptr)) s \<and> valid_pspace' s \<and> ?P'190 curThread s\<rbrace>
 4. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>curThread. \<lbrace>?P'190 curThread\<rbrace> tcbSchedDequeue ptr \<lbrace>\<lambda>r s. invs' s \<and> curThread = ksCurThread s \<and> sch_act_simple s \<and> domain \<le> maxDomain \<and> (ptr \<noteq> curThread \<longrightarrow> ct_not_inQ s \<and> sch_act_not ptr s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>\<lambda>curThread s. tcb_at' ptr s \<and> (Invariants_H.valid_queues and tcb_at' ptr and K (ptr = ptr)) s \<and> valid_pspace' s \<and> ?P'190 curThread s\<rbrace>
 3. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and ct_active' and (tcb_at' ptr and sch_act_not ptr and (\<lambda>y. domain \<le> maxDomain))) s \<Longrightarrow> tcb_at' ptr s \<and> (Invariants_H.valid_queues and tcb_at' ptr and K (ptr = ptr)) s \<and> valid_pspace' s \<and> (invs' and tcb_at' ptr) s \<and> ksCurThread s = ksCurThread s \<and> sch_act_simple s \<and> domain \<le> maxDomain \<and> (\<not> ptr \<noteq> ksCurThread s \<or> ct_not_inQ s \<and> sch_act_not ptr s) proof (prove)
goal:
No subgoals!