theory IpcCancel_R

lemma ep_cancel_corres:
  "corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep)
             (cancel_all_ipc ep) (cancelAllIPC ep)" proof - have P:
    "\<And>list.
     corres dc (\<lambda>s. (\<forall>t \<in> set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s
                        \<and> valid_etcbs s \<and> weak_valid_sched_action s)
               (\<lambda>s. (\<forall>t \<in> set list. tcb_at' t s) \<and> valid_pspace' s
                         \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s
                         \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s)
               (do x \<leftarrow> set_endpoint ep Structures_A.IdleEP;
                   x \<leftarrow> mapM_x (\<lambda>t. do
                        y \<leftarrow> set_thread_state t Structures_A.Restart;
                        tcb_sched_action tcb_sched_enqueue t
                     od) list;
                   reschedule_required
               od)
               (do x \<leftarrow> setEndpoint ep IdleEP;
                   x \<leftarrow> mapM_x (\<lambda>t. do
                        y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                        tcbSchedEnqueue t
                     od) list;
                   rescheduleRequired
                od)" apply (rule corres_underlying_split) apply (rule corres_guard_imp [OF setEndpoint_corres]) apply (simp add: ep_relation_def)+ apply (rule corres_split[OF _ rescheduleRequired_corres]) apply (rule ep_cancel_corres_helper) apply (rule mapM_x_wp') apply (wp weak_sch_act_wf_lift_linear set_thread_state_runnable_weak_valid_sched_action | simp)+ apply (rule_tac R="\<lambda>_ s. \<forall>x\<in>set list. tcb_at' x s \<and> valid_objs' s"
                   in hoare_post_add) apply (rule mapM_x_wp') apply (rule hoare_name_pre_state) apply ((wp hoare_vcg_const_Ball_lift mapM_x_wp'
                sts_valid_queues setThreadState_not_st sts_st_tcb' tcbSchedEnqueue_not_st
           | clarsimp
           | fastforce elim: obj_at'_weakenE simp: valid_tcb_state'_def)+)[2] apply (rule hoare_name_pre_state) apply (wp hoare_vcg_const_Ball_lift set_ep_valid_objs'
        | (clarsimp simp: valid_ep'_def)
        | (drule (1) bspec, clarsimp simp: valid_pspace'_def valid_tcb'_def valid_ep'_def elim!: valid_objs_valid_tcbE))+ done show ?thesis apply (simp add: cancel_all_ipc_def cancelAllIPC_def) apply (rule corres_underlying_split [OF _ _ get_simple_ko_sp get_ep_sp']) apply (rule corres_guard_imp [OF getEndpoint_corres], simp+) apply (case_tac epa, simp_all add: ep_relation_def
                                       get_ep_queue_def) apply (rule corres_guard_imp [OF P]
             | clarsimp simp: valid_obj_def valid_ep_def
                              valid_obj'_def valid_ep'_def
                              invs_valid_pspace projectKOs
                              valid_sched_def valid_sched_action_def
             | erule obj_at_valid_objsE
             | drule ko_at_valid_objs'
             | rule conjI | clarsimp simp: invs'_def valid_state'_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (cancel_all_ipc ep) (cancelAllIPC ep) proof (state)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (cancel_all_ipc ep) (cancelAllIPC ep) proof (prove)
goal (1 subgoal):
 1. \<And>list. corres dc (\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s) (\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) (do x <- set_endpoint ep Structures_A.endpoint.IdleEP;
x <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) (do x <- setEndpoint ep Structures_H.endpoint.IdleEP;
x <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list;
rescheduleRequired
od) proof (prove)
goal (4 subgoals):
 1. \<And>list. corres (?r' list) (\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s) (\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) (set_endpoint ep Structures_A.endpoint.IdleEP) (setEndpoint ep Structures_H.endpoint.IdleEP)
 2. \<And>list x xa. ?r' list x xa \<Longrightarrow> corres dc (?Q list x) (?Q' list xa) (do x <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) (do x <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list;
rescheduleRequired
od)
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>?Q list\<rbrace>
 4. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>?Q' list\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>list. ep_relation Structures_A.endpoint.IdleEP Structures_H.endpoint.IdleEP
 2. \<And>list s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s \<Longrightarrow> ep_at ep s
 3. \<And>list s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ep_at' ep s
 4. \<And>list x xa. dc x xa \<Longrightarrow> corres dc (?Q list x) (?Q' list xa) (do x <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) (do x <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list;
rescheduleRequired
od)
 5. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>?Q list\<rbrace>
 6. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>?Q' list\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>list. corres dc (?Q list ()) (?Q' list ()) (do x <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) (do x <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list;
rescheduleRequired
od)
 2. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>?Q list\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>?Q' list\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>list. corres (?r'10 list) (?P19 list ()) (?P'17 list ()) (mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list) (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list)
 2. \<And>list. \<lbrace>?Q18 list ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>
 3. \<And>list. \<lbrace>?Q'16 list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>x. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 4. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. ?P19 list a and ?Q18 list a\<rbrace>
 5. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. ?P'17 list a and ?Q'16 list a\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>list. \<lbrace>?Q18 list ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>list. \<lbrace>?Q'16 list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>x. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs and ?Q18 list a\<rbrace>
 4. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'16 list a\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>list x. x \<in> set list \<Longrightarrow> \<lbrace>weak_valid_sched_action and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>list. \<lbrace>?Q'16 list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>x. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 4. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'16 list a\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrace>?Q'16 list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>x s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'16 list a\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrace>?Q'16 list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>r s. (\<forall>x\<in>set list. tcb_at' x s \<and> valid_objs' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'16 list a\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>list x. x \<in> set list \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>r a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a\<rbrace>
 2. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>list x s. \<lbrakk>x \<in> set list; (\<forall>x\<in>set list. tcb_at' x s \<and> valid_objs' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>r a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a\<rbrace>
 2. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s\<rbrace> set_endpoint ep Structures_A.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrace>\<lambda>s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>list s. (\<forall>t\<in>set list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> setEndpoint ep Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. (\<forall>x\<in>set list. tcb_at' x a \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (\<lambda>s. (\<forall>t\<in>set ?list. tcb_at t s) \<and> valid_pspace s \<and> ep_at ep s \<and> valid_etcbs s \<and> weak_valid_sched_action s) (\<lambda>s. (\<forall>t\<in>set ?list. tcb_at' t s) \<and> valid_pspace' s \<and> ep_at' ep s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) (do x <- set_endpoint ep Structures_A.endpoint.IdleEP;
x <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) ?list;
reschedule_required
od) (do x <- setEndpoint ep Structures_H.endpoint.IdleEP;
x <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ?list;
rescheduleRequired
od)

goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (cancel_all_ipc ep) (cancelAllIPC ep) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (cancel_all_ipc ep) (cancelAllIPC ep) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (do epa <- get_endpoint ep;
case epa of Structures_A.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue epa;
set_endpoint ep Structures_A.endpoint.IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od
od) (do epa <- getEndpoint ep;
case epa of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint ep Structures_H.endpoint.IdleEP;
forM_x (epQueue epa) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od
od) proof (prove)
goal (2 subgoals):
 1. corres ?r' (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (get_endpoint ep) (getEndpoint ep)
 2. \<And>epa epaa. ?r' epa epaa \<Longrightarrow> corres dc (ko_at (Endpoint epa) ep and (invs and valid_sched and ep_at ep)) (invs' and ep_at' ep and ko_at' epaa ep) (case epa of Structures_A.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue epa;
set_endpoint ep Structures_A.endpoint.IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od) (case epaa of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint ep Structures_H.endpoint.IdleEP;
forM_x (epQueue epaa) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od) proof (prove)
goal (1 subgoal):
 1. \<And>epa epaa. ep_relation epa epaa \<Longrightarrow> corres dc (ko_at (Endpoint epa) ep and (invs and valid_sched and ep_at ep)) (invs' and ep_at' ep and ko_at' epaa ep) (case epa of Structures_A.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue epa;
set_endpoint ep Structures_A.endpoint.IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od) (case epaa of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint ep Structures_H.endpoint.IdleEP;
forM_x (epQueue epaa) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od) proof (prove)
goal (2 subgoals):
 1. \<And>epa epaa x2. \<lbrakk>epaa = Structures_H.endpoint.SendEP x2; epa = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) ep and (invs and valid_sched and ep_at ep)) (invs' and ep_at' ep and ko_at' (Structures_H.endpoint.SendEP x2) ep) (do y <- set_endpoint ep Structures_A.endpoint.IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od) (do y <- setEndpoint ep Structures_H.endpoint.IdleEP;
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2;
rescheduleRequired
od)
 2. \<And>epa epaa x3. \<lbrakk>epaa = Structures_H.endpoint.RecvEP x3; epa = Structures_A.endpoint.RecvEP x3\<rbrakk> \<Longrightarrow> corres dc (ko_at (Endpoint (Structures_A.endpoint.RecvEP x3)) ep and (invs and valid_sched and ep_at ep)) (invs' and ep_at' ep and ko_at' (Structures_H.endpoint.RecvEP x3) ep) (do y <- set_endpoint ep Structures_A.endpoint.IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x3;
reschedule_required
od) (do y <- setEndpoint ep Structures_H.endpoint.IdleEP;
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od) proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) (cancel_all_ipc ep) (cancelAllIPC ep)

goal:
No subgoals!