theory Syscall_R

lemma handleReply_handleRecv_corres:
  "corres dc (einvs and ct_running)
             (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
         (do x \<leftarrow> handle_reply; handle_recv True od)
         (do x \<leftarrow> handleReply; handleRecv True od)" apply (rule corres_guard_imp) apply (rule corres_split_nor[OF handleReply_corres]) apply (rule handleRecv_isBlocking_corres') apply (wp handle_reply_nonz_cap_to_ct handleReply_sane
               handleReply_nonz_cap_to_ct handleReply_ct_not_ksQ handle_reply_valid_sched)+ apply (fastforce simp: ct_in_state_def ct_in_state'_def simple_sane_strg
                    elim!: st_tcb_weakenE st_tcb_ex_cap') apply (clarsimp simp: ct_in_state'_def) apply (frule(1) ct_not_ksQ) apply (fastforce elim: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and ct_running) (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do x <- handle_reply;
handle_recv True
od) (do x <- handleReply;
handleRecv True
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do x <- handle_reply;
handle_recv True
od) (do x <- handleReply;
handleRecv True
od)
 2. \<And>s. (einvs and ct_running) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. corres dc ?R4 ?R'4 (handle_recv True) (handleRecv True)
 2. \<lbrace>?Q4\<rbrace> handle_reply \<lbrace>\<lambda>x. ?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> handleReply \<lbrace>\<lambda>x. ?R'4\<rbrace>
 4. \<And>s. (einvs and ct_running) s \<Longrightarrow> (einvs and ct_running and ?Q4) s
 5. \<And>s. (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> (invs' and ct_running' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> handle_reply \<lbrace>\<lambda>x. einvs and ct_active and (\<lambda>s. ex_nonz_cap_to (cur_thread s) s)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> handleReply \<lbrace>\<lambda>x. 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)\<rbrace>
 3. \<And>s. (einvs and ct_running) s \<Longrightarrow> (einvs and ct_running and ?Q4) s
 4. \<And>s. (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> (invs' and ct_running' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and ct_running) s \<Longrightarrow> (einvs and ct_running and (\<lambda>s. invs s \<and> valid_list s \<and> (valid_sched and ct_active and invs) s \<and> (invs and ct_active) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at (cur_thread s) s)) s
 2. \<And>s. (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> (invs' and ct_running' and (\<lambda>s. (invs' and sch_act_simple) s \<and> ct_in_state' simple' s \<and> sch_act_sane s \<and> (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<and> (ct_active' and invs' and sch_act_simple) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> (invs' and ct_running' and (\<lambda>s. (invs' and sch_act_simple) s \<and> ct_in_state' simple' s \<and> sch_act_sane s \<and> (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<and> (ct_active' and invs' and sch_act_simple) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' active' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' active' (ksCurThread s) s proof (prove)
goal:
No subgoals!