theory Ipc_R

lemma cancelAllSignals_not_rct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>
   cancelAllSignals epptr
   \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>" apply (simp add: cancelAllSignals_def) apply (wp | wpc)+ apply (rule hoare_post_imp [OF _ rescheduleRequired_notresume], simp) apply simp apply (rule mapM_x_wp_inv) apply (wp)+ apply (wp hoare_vcg_all_lift hoare_drop_imp) apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> cancelAllSignals epptr \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> do ntfn <- getNotification epptr;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification epptr (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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn x3 x xa. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B27 ntfn x3 x xa\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ntfn x3 x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B25 ntfn x3 x\<rbrace> forM_x x3 (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>?B27 ntfn x3 x\<rbrace>
 3. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification epptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification epptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 5. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x3 x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B25 ntfn x3 x\<rbrace> forM_x x3 (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>\<lambda>xa s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification epptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification epptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B25 ntfn x3 ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3 \<lbrace>\<lambda>xa s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification epptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification epptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x3 x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>\<lambda>a. ksSchedulerAction a \<noteq> ResumeCurrentThread\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>xa a. ksSchedulerAction a \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification epptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>\<lambda>a b. ksSchedulerAction b \<noteq> ResumeCurrentThread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification epptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification epptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
 2. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<and> (\<forall>x. ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ksSchedulerAction s \<noteq> ResumeCurrentThread) proof (prove)
goal:
No subgoals!