theory IpcCancel_R

lemma cancelAllIPC_unlive:
  "\<lbrace>valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
      cancelAllIPC ep \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ep\<rbrace>" apply (simp add: cancelAllIPC_def ep'_Idle_case_helper) apply (rule hoare_seq_ext [OF _ get_ep_sp']) apply (rule hoare_pre) apply (wp cancelAll_unlive_helper setEndpoint_ko_wp_at'
             hoare_vcg_const_Ball_lift rescheduleRequired_unlive
             mapM_x_wp'
        | simp add: objBits_simps')+ apply (clarsimp simp: projectKO_opt_tcb) apply (frule(1) obj_at_valid_objs') apply (intro conjI impI) apply (clarsimp simp: valid_obj'_def valid_ep'_def projectKOs
                        obj_at'_def pred_tcb_at'_def ko_wp_at'_def
                 split: endpoint.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace> cancelAllIPC ep \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace> do epa <- getEndpoint ep;
if epa = Structures_H.endpoint.IdleEP then return () else 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 \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa. \<lbrace>valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and ko_at' epa ep\<rbrace> if epa = Structures_H.endpoint.IdleEP then return () else 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 \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ep\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>epa. \<lbrace>?Q4 epa\<rbrace> if epa = Structures_H.endpoint.IdleEP then return () else 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 \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ep\<rbrace>
 2. \<And>epa s. (valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and ko_at' epa ep) s \<Longrightarrow> ?Q4 epa s proof (prove)
goal (1 subgoal):
 1. \<And>epa s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> ko_at' epa ep s \<Longrightarrow> (epa = Structures_H.endpoint.IdleEP \<longrightarrow> ko_wp_at' (Not \<circ> live') ep s) \<and> (epa \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> (\<forall>x\<in>set (epQueue epa). tcb_at' x s) \<and> projectKO_opt (KOEndpoint Structures_H.endpoint.IdleEP) = None \<and> sch_act_not ep s) proof (prove)
goal (1 subgoal):
 1. \<And>epa s. \<lbrakk>valid_objs' s; sch_act_wf (ksSchedulerAction s) s; ko_at' epa ep s\<rbrakk> \<Longrightarrow> (epa = Structures_H.endpoint.IdleEP \<longrightarrow> ko_wp_at' (Not \<circ> live') ep s) \<and> (epa \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> (\<forall>x\<in>set (epQueue epa). tcb_at' x s) \<and> sch_act_not ep s) proof (prove)
goal (1 subgoal):
 1. \<And>epa s. \<lbrakk>valid_objs' s; sch_act_wf (ksSchedulerAction s) s; ko_at' epa ep s; \<exists>k. k = epa \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> (epa = Structures_H.endpoint.IdleEP \<longrightarrow> ko_wp_at' (Not \<circ> live') ep s) \<and> (epa \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> (\<forall>x\<in>set (epQueue epa). tcb_at' x s) \<and> sch_act_not ep s) proof (prove)
goal (3 subgoals):
 1. \<And>epa s. \<lbrakk>valid_objs' s; sch_act_wf (ksSchedulerAction s) s; ko_at' epa ep s; \<exists>k. k = epa \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s); epa = Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> ko_wp_at' (Not \<circ> live') ep s
 2. \<And>epa s. \<lbrakk>valid_objs' s; sch_act_wf (ksSchedulerAction s) s; ko_at' epa ep s; \<exists>k. k = epa \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s); epa \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (epQueue epa). tcb_at' x s
 3. \<And>epa s. \<lbrakk>valid_objs' s; sch_act_wf (ksSchedulerAction s) s; ko_at' epa ep s; \<exists>k. k = epa \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s); epa \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> sch_act_not ep s proof (prove)
goal:
No subgoals!