theory Finalise_R

lemma cancelAllSignals_ct_not_ksQ:
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   cancelAllSignals ntfnptr
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") apply (simp add: cancelAllSignals_def) apply (wp, wpc, wp+) apply (wps rescheduleRequired_ct') apply (wp rescheduleRequired_ksQ') apply clarsimp apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv) apply (wp hoare_lift_Pf2 [OF setNotification_ksQ setNotification_ksCurThread]) apply (wps setNotification_ksCurThread, wp) prefer 2 apply assumption apply (rule_tac Q="\<lambda>ep. ?PRE and ko_at' ep ntfnptr" in hoare_post_imp) apply ((clarsimp simp: invs'_def valid_state'_def sch_act_sane_def
          | drule(1) ct_not_in_ntfnQueue)+)[1] apply (wp get_ntfn_sp') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> cancelAllSignals ntfnptr \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<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 s. ksCurThread s \<notin> set (ksReadyQueues s p)\<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>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<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 ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 5. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn x3 x xa prev_s. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?P30 ntfn x3 x xa prev_s\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p)\<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>\<lambda>xa s. ?P30 ntfn x3 x xa s s\<rbrace>
 3. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 5. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<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. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<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. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>?B25 ntfn x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>\<lambda>a b. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set x3)) b \<and> sch_act_not (ksCurThread b) b\<rbrace>
 2. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 3. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?P'67 ntfn x3\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) \<lbrace>\<lambda>rv s. sch_act_not (ksCurThread s) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> ?P'67 ntfn x s)\<rbrace>
 3. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)\<rbrace>
 2. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s
 2. \<lbrace>?Q\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' rv ntfnptr) s \<Longrightarrow> (ntfnObj rv = Structures_H.ntfn.IdleNtfn \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj rv = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ntfnObj rv = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)
 2. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ep. invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ep ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ep. invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ep ntfnptr\<rbrace> proof (prove)
goal:
No subgoals!