kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma ct_in_state'_set:
  "\<lbrace>\<lambda>s. tcb_at' t s \<and> P st \<and> t = ksCurThread s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" apply (rule hoare_vcg_precond_imp) apply (rule ct_in_state'_decomp[where t=t]) apply (wp setThreadState_ct') apply (wp setThreadState_st_tcb) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<and> P st \<and> t = ksCurThread s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>
 2. \<And>s. tcb_at' t s \<and> P st \<and> t = ksCurThread s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. t = ksCurThread s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. t = ksCurThread s\<rbrace>
 2. \<lbrace>?Pre3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 3. \<And>s. tcb_at' t s \<and> P st \<and> t = ksCurThread s \<Longrightarrow> ?Pre3 s \<and> t = ksCurThread s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Pre3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 2. \<And>s. tcb_at' t s \<and> P st \<and> t = ksCurThread s \<Longrightarrow> ?Pre3 s \<and> t = ksCurThread s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<and> P st \<and> t = ksCurThread s \<Longrightarrow> P st \<and> t = ksCurThread s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_valid_idle'[wp]:
  "\<lbrace>valid_idle' and valid_pspace' and
    (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' ts)\<rbrace>
   setThreadState ts t
   \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: setThreadState_def) apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle' and valid_pspace' and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' ts)\<rbrace> setThreadState ts t \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle' and valid_pspace' and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' ts)\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. ts)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sbn_valid_idle'[wp]:
  "\<lbrace>valid_idle' and valid_pspace' and
    (\<lambda>s. t = ksIdleThread s \<longrightarrow> \<not>bound ntfn)\<rbrace>
   setBoundNotification ntfn t
   \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: setBoundNotification_def) apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle' and valid_pspace' and (\<lambda>s. t = ksIdleThread s \<longrightarrow> \<not> ntfn \<noteq> None)\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle' and valid_pspace' and (\<lambda>s. t = ksIdleThread s \<longrightarrow> ntfn = None)\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gbn_sp':
  "\<lbrace>P\<rbrace> getBoundNotification t \<lbrace>\<lambda>rv. bound_tcb_at' (\<lambda>st. st = rv) t and P\<rbrace>" apply (simp add: getBoundNotification_def threadGet_def) apply wp apply (simp add: o_def pred_tcb_at'_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getBoundNotification t \<lbrace>\<lambda>rv. bound_tcb_at' (\<lambda>st. st = rv) t and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> liftM tcbBoundNotification (getObject t) \<lbrace>\<lambda>rv. bound_tcb_at' (\<lambda>st. st = rv) t and P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>(\<lambda>rv s. bound_tcb_at' (\<lambda>st. st = rv) t s \<and> P s) \<circ> tcbBoundNotification\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>x s. obj_at' (\<lambda>ko. tcbBoundNotification ko = tcbBoundNotification x) t s \<and> P s\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> obj_at' (\<lambda>ko. tcbBoundNotification ko = tcbBoundNotification ta) t s \<and> P s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedDequeue_tcbState_obj_at'[wp]:
  "\<lbrace>obj_at' (P \<circ> tcbState) t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t'\<rbrace>" apply (simp add: tcbSchedDequeue_def) apply (wp | simp add: o_def split del: if_split cong: if_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t'\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setQueue_pred_tcb_at[wp]:
  "\<lbrace>\<lambda>s. P' (pred_tcb_at' proj P t s)\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. P' (pred_tcb_at' proj P t s)\<rbrace>" unfolding pred_tcb_at'_def apply (rule_tac P=P' in P_bool_lift) apply (rule setQueue_obj_at) apply (rule_tac Q="\<lambda>_ s. \<not>typ_at' TCBT t s \<or> obj_at' (Not \<circ> (P \<circ> proj \<circ> tcb_to_itcb')) t s"
           in hoare_post_imp, simp add: not_obj_at' o_def) apply (wp hoare_vcg_disj_lift) apply (clarsimp simp: not_obj_at' o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (pred_tcb_at' proj P t s)\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. P' (pred_tcb_at' proj P t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s)\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. P' (obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setQueue d p q \<lbrace>\<lambda>r. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s\<rbrace> setQueue d p q \<lbrace>\<lambda>r s. \<not> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s\<rbrace> setQueue d p q \<lbrace>\<lambda>r s. \<not> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s\<rbrace> setQueue d p q \<lbrace>\<lambda>_ s. \<not> typ_at' TCBT t s \<or> obj_at' (Not \<circ> (P \<circ> proj \<circ> tcb_to_itcb')) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s \<Longrightarrow> \<not> typ_at' TCBT t s \<or> obj_at' (Not \<circ> (P \<circ> proj \<circ> tcb_to_itcb')) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedDequeue_pred_tcb_at'[wp]:
  "\<lbrace>\<lambda>s. P' (pred_tcb_at' proj P t' s)\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. P' (pred_tcb_at' proj P t' s)\<rbrace>" apply (rule_tac P=P' in P_bool_lift) apply (simp add: tcbSchedDequeue_def) apply (wp threadSet_pred_tcb_no_state | clarsimp simp: tcb_to_itcb'_def)+ apply (simp add: tcbSchedDequeue_def) apply (wp threadSet_pred_tcb_no_state | clarsimp simp: tcb_to_itcb'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (pred_tcb_at' proj P t' s)\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. P' (pred_tcb_at' proj P t' s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>pred_tcb_at' proj P t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>r. pred_tcb_at' proj P t'\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P t' s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>pred_tcb_at' proj P t'\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>r. pred_tcb_at' proj P t'\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P t' s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj P t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P t' s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj P t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P t' s\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj P t' s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_st_tcb':
  "\<lbrace>if t = t' then K (P st) else st_tcb_at' P t\<rbrace>
  setThreadState st t'
  \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>" apply (cases "t = t'",
         simp_all add: setThreadState_def
                  split del: if_split) apply ((wp threadSet_pred_tcb_at_state | simp)+)[1] apply (wp threadSet_obj_at'_really_strongest
              | simp add: pred_tcb_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if t = t' then K (P st) else st_tcb_at' P t\<rbrace> setThreadState st t' \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>y. P st\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at' P t\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at' P t\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sbn_st_tcb':
  "\<lbrace>st_tcb_at' P t\<rbrace>
  setBoundNotification ntfn t'
  \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>" apply (cases "t = t'",
         simp_all add: setBoundNotification_def
                  split del: if_split) apply ((wp threadSet_pred_tcb_at_state | simp)+)[1] apply (wp threadSet_obj_at'_really_strongest
              | simp add: pred_tcb_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> setBoundNotification ntfn t' \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>st_tcb_at' P t'\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t' \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at' P t\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t' \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t = t'; st_tcb_at' P t' s\<rbrakk> \<Longrightarrow> tcb_at' t' s \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbState tcb)) t' s
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at' P t\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t' \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setThreadState_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (t := tcb_st_refs_of' st
                                 \<union> {r \<in> state_refs_of' s t. snd r = TCBBound}))\<rbrace>
     setThreadState st t
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" by (simp add: setThreadState_def fun_upd_def
        | wp threadSet_state_refs_of')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(t := tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound}))\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>
theory TcbAcc_R

lemma setBoundNotification_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (t := tcb_bound_refs' ntfn
                                 \<union> {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound}))\<rbrace>
     setBoundNotification ntfn t
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" by (simp add: setBoundNotification_def Un_commute fun_upd_def
        | wp threadSet_state_refs_of' )+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(t := tcb_bound_refs' ntfn \<union> {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound}))\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>
theory TcbAcc_R

lemma sts_cur_tcb'[wp]:
  "\<lbrace>cur_tcb'\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" by (wp cur_tcb_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>
theory TcbAcc_R

lemma sbn_cur_tcb'[wp]:
  "\<lbrace>cur_tcb'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" by (wp cur_tcb_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>
theory TcbAcc_R

lemma tcbSchedEnqueue_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' tcb\<rbrace>
    tcbSchedEnqueue tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp threadSet_iflive' hoare_drop_imps | simp add: crunch_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' tcb\<rbrace> tcbSchedEnqueue tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' tcb\<rbrace> do queued <- threadGet tcbQueued tcb;
when (\<not> queued) (do tdom <- threadGet tcbDomain tcb;
prio <- threadGet tcbPriority tcb;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (tcb # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) tcb
od)
od \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap'
        and (\<lambda>s. \<forall>t. ksSchedulerAction s = SwitchToThread t
                \<longrightarrow> st_tcb_at' runnable' t s)\<rbrace>
      rescheduleRequired
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp)+ apply (clarsimp simp: pred_tcb_at'_def obj_at'_real_def) apply (erule(1) if_live_then_nonz_capD') apply (fastforce simp: projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and (\<lambda>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s)\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and (\<lambda>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s) \<Longrightarrow> \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> ex_nonz_cap_to' x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> runnable' (tcbState obj)) x s; ksSchedulerAction s = SwitchToThread x\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' x s proof (prove)
goal (1 subgoal):
 1. \<And>s x obj. \<lbrakk>ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> runnable' (tcbState obj)) x s; ksSchedulerAction s = SwitchToThread x; \<exists>obja. projectKO_opt obj = Some obja \<and> runnable' (tcbState obja); ksPSpace s x = Some obj; is_aligned x (objBitsKO obj)\<rbrakk> \<Longrightarrow> live' obj proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sbn_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> (bound ntfn \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace>
     setBoundNotification ntfn t
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: setBoundNotification_def) apply (rule hoare_pre) apply (wp threadSet_iflive' | simp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (ntfn \<noteq> None \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ((\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. ntfn = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcb \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued tcb \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma st_tcb_ex_cap'':
  "\<lbrakk> st_tcb_at' P t s; if_live_then_nonz_cap' s;
     \<And>st. P st \<Longrightarrow> st \<noteq> Inactive \<and> \<not> idle' st \<rbrakk> \<Longrightarrow> ex_nonz_cap_to' t s" by (clarsimp simp: pred_tcb_at'_def obj_at'_real_def projectKOs
              elim!: ko_wp_at'_weakenE
                     if_live_then_nonz_capE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; if_live_then_nonz_cap' s; \<And>st. P st \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' t s
theory TcbAcc_R

lemma bound_tcb_ex_cap'':
  "\<lbrakk> bound_tcb_at' P t s; if_live_then_nonz_cap' s;
     \<And>ntfn. P ntfn \<Longrightarrow> bound ntfn \<rbrakk> \<Longrightarrow> ex_nonz_cap_to' t s" by (clarsimp simp: pred_tcb_at'_def obj_at'_real_def projectKOs
              elim!: ko_wp_at'_weakenE
                     if_live_then_nonz_capE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bound_tcb_at' P t s; if_live_then_nonz_cap' s; \<And>ntfn. P ntfn \<Longrightarrow> ntfn \<noteq> None\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' t s
theory TcbAcc_R

lemma sbn_ctes_of [wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_ctes_ofT | simp add: tcb_cte_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_global_reds' [wp]:
  "\<lbrace>valid_global_refs'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>" by (rule valid_global_refs_lift'; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>
theory TcbAcc_R

lemma sbn_global_reds' [wp]:
  "\<lbrace>valid_global_refs'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>" by (rule valid_global_refs_lift'; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>