theory Syscall_R

lemma handleYield_corres:
  "corres dc einvs (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) handle_yield handleYield" apply (clarsimp simp: handle_yield_def handleYield_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply simp apply (rule corres_split[OF tcbSchedDequeue_corres]) apply (rule corres_split[OF tcbSchedAppend_corres]) apply (rule rescheduleRequired_corres) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues | simp add: )+ apply (simp add: invs_def valid_sched_def valid_sched_action_def
                cur_tcb_def tcb_at_is_etcb_at) apply clarsimp apply (frule ct_active_runnable') apply (clarsimp simp: invs'_def valid_state'_def ct_in_state'_def sch_act_wf_weak cur_tcb'_def
                        valid_pspace_valid_objs' valid_objs'_maxDomain tcb_in_cur_domain'_def) apply (erule(1) valid_objs_valid_tcbE[OF valid_pspace_valid_objs']) apply (simp add:valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc einvs (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) handle_yield handleYield proof (prove)
goal (1 subgoal):
 1. corres dc einvs (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
y <- tcb_sched_action tcb_sched_dequeue thread;
y <- tcb_sched_action tcb_sched_append thread;
reschedule_required
od) (do thread <- getCurThread;
y <- tcbSchedDequeue thread;
y <- tcbSchedAppend thread;
rescheduleRequired
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q1 ?Q'1 (do thread <- gets cur_thread;
y <- tcb_sched_action tcb_sched_dequeue thread;
y <- tcb_sched_action tcb_sched_append thread;
reschedule_required
od) (do thread <- getCurThread;
y <- tcbSchedDequeue thread;
y <- tcbSchedAppend thread;
rescheduleRequired
od)
 2. \<And>s. einvs s \<Longrightarrow> ?Q1 s
 3. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q'1 s proof (prove)
goal (5 subgoals):
 1. \<And>thread threada. thread = threada \<Longrightarrow> corres dc (?R5 thread) (?R'5 threada) (do y <- tcb_sched_action tcb_sched_dequeue thread;
y <- tcb_sched_action tcb_sched_append thread;
reschedule_required
od) (do y <- tcbSchedDequeue threada;
y <- tcbSchedAppend threada;
rescheduleRequired
od)
 2. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>?R5\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>?R'5\<rbrace>
 4. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>thread. corres dc (?R5 thread) (?R'5 thread) (do y <- tcb_sched_action tcb_sched_dequeue thread;
y <- tcb_sched_action tcb_sched_append thread;
reschedule_required
od) (do y <- tcbSchedDequeue thread;
y <- tcbSchedAppend thread;
rescheduleRequired
od)
 2. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>?R5\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>?R'5\<rbrace>
 4. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>thread y ya. dc y ya \<Longrightarrow> corres dc (?R9 thread y) (?R'9 thread ya) (do y <- tcb_sched_action tcb_sched_append thread;
reschedule_required
od) (do y <- tcbSchedAppend thread;
rescheduleRequired
od)
 2. \<And>thread. \<lbrace>?Q9 thread\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>?R9 thread\<rbrace>
 3. \<And>thread. \<lbrace>?Q'9 thread\<rbrace> tcbSchedDequeue thread \<lbrace>?R'9 thread\<rbrace>
 4. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. is_etcb_at thread and ?Q9 thread\<rbrace>
 5. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and Invariants_H.valid_queues and ?Q'9 thread\<rbrace>
 6. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 7. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>thread y ya yb yc. \<lbrakk>dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres dc (?R14 thread y ya yb) (?R'14 thread y ya yc) reschedule_required rescheduleRequired
 2. \<And>thread y ya. dc y ya \<Longrightarrow> \<lbrace>?Q17 thread y\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>?R14 thread y ya\<rbrace>
 3. \<And>thread y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'19 thread ya\<rbrace> tcbSchedAppend thread \<lbrace>?R'14 thread y ya\<rbrace>
 4. \<And>thread. \<lbrace>?Q9 thread\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>y. is_etcb_at thread and ?Q17 thread y\<rbrace>
 5. \<And>thread. \<lbrace>?Q'9 thread\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>ya. tcb_at' thread and Invariants_H.valid_queues and valid_queues' and ?Q'19 thread ya\<rbrace>
 6. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. is_etcb_at thread and ?Q9 thread\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and Invariants_H.valid_queues and ?Q'9 thread\<rbrace>
 8. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 9. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>thread y ya. dc y ya \<Longrightarrow> \<lbrace>?Q17 thread y\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>yb. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>thread y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'19 thread ya\<rbrace> tcbSchedAppend thread \<lbrace>\<lambda>yc. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>thread. \<lbrace>?Q9 thread\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>y. is_etcb_at thread and ?Q17 thread y\<rbrace>
 4. \<And>thread. \<lbrace>?Q'9 thread\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>ya. tcb_at' thread and Invariants_H.valid_queues and valid_queues' and ?Q'19 thread ya\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. is_etcb_at thread and ?Q9 thread\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and Invariants_H.valid_queues and ?Q'9 thread\<rbrace>
 7. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<Longrightarrow> is_etcb_at (cur_thread s) s \<and> weak_valid_sched_action s \<and> valid_etcbs s
 2. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and Invariants_H.valid_queues and (\<lambda>sa. tcb_at' (ksCurThread s) sa \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s)) sa \<and> (valid_queues' and tcb_at' (ksCurThread s)) sa \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s)) sa \<and> st_tcb_at' runnable' (ksCurThread s) sa \<and> valid_objs' sa \<and> (valid_queues' and tcb_at' (ksCurThread s)) sa \<and> tcb_at' (ksCurThread s) sa \<and> weak_sch_act_wf (ksSchedulerAction sa) sa)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_active' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and Invariants_H.valid_queues and (\<lambda>sa. tcb_at' (ksCurThread s) sa \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s)) sa \<and> (valid_queues' and tcb_at' (ksCurThread s)) sa \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s)) sa \<and> st_tcb_at' runnable' (ksCurThread s) sa \<and> valid_objs' sa \<and> (valid_queues' and tcb_at' (ksCurThread s)) sa \<and> tcb_at' (ksCurThread s) sa \<and> weak_sch_act_wf (ksSchedulerAction sa) sa)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_active' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s) s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s) s \<and> st_tcb_at' runnable' (ksCurThread s) s \<and> valid_objs' s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> weak_sch_act_wf ResumeCurrentThread s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_active' s; ksSchedulerAction s = ResumeCurrentThread; ct_in_state' runnable' s\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s) s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) (ksCurThread s) s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s) s \<and> st_tcb_at' runnable' (ksCurThread s) s \<and> valid_objs' s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> weak_sch_act_wf ResumeCurrentThread s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at' active' (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; st_tcb_at' runnable' (ksCurThread s) s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread 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; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' 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; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>st_tcb_at' active' (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; st_tcb_at' runnable' (ksCurThread s) s; st_tcb_at' activatable' (ksCurThread 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; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' 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; tcb_at' (ksCurThread s) s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcbPriority tcb \<le> maxPriority proof (prove)
goal:
No subgoals!