theory IpcCancel_R

lemma cancelAllSignals_unlive:
  "\<lbrace>\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
      \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s\<rbrace>
      cancelAllSignals ntfnptr \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace>" apply (simp add: cancelAllSignals_def) apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) apply (case_tac "ntfnObj ntfn", simp_all add: setNotification_def) apply wp apply (fastforce simp: obj_at'_real_def projectKOs
                     dest: obj_at_conj'
                     elim: ko_wp_at'_weakenE) apply wp apply (fastforce simp: obj_at'_real_def projectKOs
                    dest: obj_at_conj'
                    elim: ko_wp_at'_weakenE) apply (wp rescheduleRequired_unlive) apply (wp cancelAll_unlive_helper) apply ((wp mapM_x_wp' setObject_ko_wp_at' hoare_vcg_const_Ball_lift)+,
          simp_all add: objBits_simps', simp_all) apply (fold setNotification_def, wp) apply (intro conjI[rotated]) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs) apply (clarsimp simp: projectKOs projectKO_opt_tcb) apply (fastforce simp: ko_wp_at'_def valid_obj'_def valid_ntfn'_def
                         obj_at'_def projectKOs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s\<rbrace> cancelAllSignals ntfnptr \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s\<rbrace> do ntfn <- getNotification ntfnptr;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn. ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> return () \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace>
 2. \<And>ntfn x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> return () \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace>
 3. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> do y <- setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.IdleNtfn; ((\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr) s\<rbrakk> \<Longrightarrow> ko_wp_at' (Not \<circ> live') ntfnptr s
 2. \<And>ntfn x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> return () \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace>
 3. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> do y <- setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x2. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> return () \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> do y <- setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x2 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2; ((\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr) s\<rbrakk> \<Longrightarrow> ko_wp_at' (Not \<circ> live') ntfnptr s
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> do y <- setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr\<rbrace> do y <- setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') ntfnptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3 y. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B35 ntfn x3 y\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3 \<lbrace>\<lambda>ya s. ko_wp_at' (Not \<circ> live') ntfnptr s \<and> sch_act_not ntfnptr s\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?Q34 ntfn x3\<rbrace> setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B35 ntfn x3\<rbrace>
 3. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ((\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr) s\<rbrakk> \<Longrightarrow> ?Q34 ntfn x3 s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3 y. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?P'39 ntfn x3 y\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3 \<lbrace>\<lambda>rv. sch_act_not ntfnptr\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?Q34 ntfn x3\<rbrace> setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>\<lambda>y s. ((\<forall>x\<in>set x3. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) ntfnptr s) \<and> ?P'39 ntfn x3 y s\<rbrace>
 3. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ((\<lambda>s. valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s) and ko_at' ntfn ntfnptr) s\<rbrakk> \<Longrightarrow> ?Q34 ntfn x3 s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?P'53 ntfn x3\<rbrace> setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>\<lambda>rv. sch_act_not ntfnptr\<rbrace>
 2. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x3. tcb_at' x s) \<and> ntfnBoundTCB ntfn = None \<and> projectKO_opt (KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn)) = None \<and> ?P'53 ntfn x3 s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x3. tcb_at' x s) \<and> ntfnBoundTCB ntfn = None \<and> projectKO_opt (KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn)) = None \<and> sch_act_not ntfnptr s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> sch_act_not ntfnptr s
 2. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> projectKO_opt (KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn)) = None
 3. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> ntfnBoundTCB ntfn = None
 4. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x3. tcb_at' x s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> projectKO_opt (KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn)) = None
 2. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> ntfnBoundTCB ntfn = None
 3. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x3. tcb_at' x s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> ntfnBoundTCB ntfn = None
 2. \<And>ntfn x3 s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None) ntfnptr s \<and> ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x3. tcb_at' x s proof (prove)
goal:
No subgoals!