theory Syscall_R

lemma handleRecv_isBlocking_corres:
  "corres dc (einvs and ct_active)
             (invs' and ct_active' and sch_act_sane and
                    (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))
            (handle_recv isBlocking) (handleRecv isBlocking)" apply (rule corres_guard_imp) apply (rule handleRecv_isBlocking_corres') apply (clarsimp simp: ct_in_state_def) apply (fastforce elim!: st_tcb_weakenE st_tcb_ex_cap) apply (clarsimp simp: ct_in_state'_def invs'_def valid_state'_def) apply (frule(1) st_tcb_ex_cap'') apply (auto elim: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and ct_active) (invs' and ct_active' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) (handle_recv isBlocking) (handleRecv isBlocking) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (handle_recv isBlocking) (handleRecv isBlocking)
 2. \<And>s. (einvs and ct_active) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and ct_active' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and ct_active) s \<Longrightarrow> (einvs and ct_active and (\<lambda>s. ex_nonz_cap_to (cur_thread s) s)) s
 2. \<And>s. (invs' and ct_active' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs s; valid_list s; valid_sched s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s
 2. \<And>s. (invs' and ct_active' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_active' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; 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; cur_tcb' s; st_tcb_at' active' (ksCurThread s) s; sch_act_sane s; \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s st. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; 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; cur_tcb' s; st_tcb_at' active' (ksCurThread s) s; sch_act_sane s; \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)); active' st\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState
 2. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; 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; cur_tcb' s; st_tcb_at' active' (ksCurThread s) s; sch_act_sane s; \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)); ex_nonz_cap_to' (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s proof (prove)
goal:
No subgoals!