kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma setQueue_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> setQueue d p xs \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>" apply (simp add: setQueue_def tcb_in_cur_domain'_def) apply wp apply (simp add: ps_clear_def projectKOs obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> setQueue d p xs \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := xs)\<rparr>) \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := xs)\<rparr>) = tcbDomain tcb) t (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := xs)\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setQueue_sch_act:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  setQueue d p xs
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp sch_act_wf_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> setQueue d p xs \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma setQueue_valid_bitmapQ_except[wp]:
  "\<lbrace> valid_bitmapQ_except d p \<rbrace>
  setQueue d p ts
  \<lbrace>\<lambda>_. valid_bitmapQ_except d p \<rbrace>" unfolding setQueue_def bitmapQ_defs by (wp, clarsimp simp: bitmapQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> setQueue d p ts \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>_ s. \<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])\<rbrace>
theory TcbAcc_R

lemma setQueue_valid_queues':
  "\<lbrace>valid_queues' and (\<lambda>s. \<forall>t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set ts)\<rbrace>
    setQueue d p ts \<lbrace>\<lambda>_. valid_queues'\<rbrace>" by (wp | simp add: valid_queues'_def setQueue_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and (\<lambda>s. \<forall>t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set ts)\<rbrace> setQueue d p ts \<lbrace>\<lambda>_. valid_queues'\<rbrace>
theory TcbAcc_R

lemma setQueue_cur:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv s. cur_tcb' s\<rbrace>" unfolding setQueue_def cur_tcb'_def by (wp, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>rv s. tcb_at' (ksCurThread s) s\<rbrace>
theory TcbAcc_R

lemma ssa_sch_act[wp]:
  "\<lbrace>sch_act_wf sa\<rbrace> setSchedulerAction sa
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (simp add: setSchedulerAction_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_wf sa\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma threadSet_pred_tcb_at_state:
  "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t
        then obj_at' (\<lambda>tcb. P (proj (tcb_to_itcb' (f tcb)))) t s
        else pred_tcb_at' proj P p s)\<rbrace>
  threadSet f t \<lbrace>\<lambda>_. pred_tcb_at' proj P p\<rbrace>" apply (rule hoare_chain) apply (rule threadSet_obj_at'_really_strongest) prefer 2 apply (simp add: pred_tcb_at'_def) apply (clarsimp split: if_splits simp: pred_tcb_at'_def o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (proj (tcb_to_itcb' (f tcb)))) t s else pred_tcb_at' proj P p s)\<rbrace> threadSet f t \<lbrace>\<lambda>_. pred_tcb_at' proj P p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> threadSet f t \<lbrace>?Q\<rbrace>
 2. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (proj (tcb_to_itcb' (f tcb)))) t s else pred_tcb_at' proj P p s) \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> pred_tcb_at' proj P p s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (proj (tcb_to_itcb' (f tcb)))) t s else pred_tcb_at' proj P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ?t'4 then ?P4 (f obj) else ?P4 obj) ?t'4 s
 2. \<And>rv s. obj_at' ?P4 ?t'4 s \<Longrightarrow> pred_tcb_at' proj P p s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. obj_at' ?P4 ?t'4 s \<Longrightarrow> pred_tcb_at' proj P p s
 2. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (proj (tcb_to_itcb' (f tcb)))) t s else pred_tcb_at' proj P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ?t'4 then ?P4 (f obj) else ?P4 obj) ?t'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (proj (tcb_to_itcb' (f tcb)))) t s else pred_tcb_at' proj P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = p then P (proj (tcb_to_itcb' (f obj))) else P (proj (tcb_to_itcb' obj))) p s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_tcbDomain_triv':
  "\<lbrace>tcb_in_cur_domain' t' and K (t \<noteq> t')\<rbrace> threadSet f t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace>" apply (simp add: tcb_in_cur_domain'_def) apply (rule hoare_assume_pre) apply simp apply (rule_tac f="ksCurDomain" in hoare_lift_Pf) apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t' and K (t \<noteq> t')\<rbrace> threadSet f t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s) and (\<lambda>y. t \<noteq> t')\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s) and (\<lambda>y. t \<noteq> t')) s \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s) and (\<lambda>y. t \<noteq> t')\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<and> t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s x. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<and> t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> threadSet f t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace>
 2. \<And>s P. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<and> t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_sch_act'[wp]:
  "\<lbrace>\<top>\<rbrace>
      rescheduleRequired
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_queued_pred_tcb_at'[wp]:
  "\<lbrace>pred_tcb_at' proj P t' and obj_at' ((=) tcb) t\<rbrace>
    setObject t (tcbQueued_update f tcb)
   \<lbrace>\<lambda>_. pred_tcb_at' proj P t'\<rbrace>" apply (simp add: pred_tcb_at'_def) apply (rule hoare_pre) apply (wp setObject_tcb_strongest) apply (clarsimp simp: obj_at'_def tcb_to_itcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t' and obj_at' ((=) tcb) t\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>_. pred_tcb_at' proj P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t' and obj_at' ((=) tcb) t\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>_. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>_. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace>
 2. \<And>s. (obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t' and obj_at' ((=) tcb) t) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t' and obj_at' ((=) tcb) t) s \<Longrightarrow> if t = t' then P (proj (tcb_to_itcb' (tcbQueued_update f tcb))) else obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t' s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setObject_queued_ct_activatable'[wp]:
  "\<lbrace>ct_in_state' activatable' and obj_at' ((=) tcb) t\<rbrace>
    setObject t (tcbQueued_update f tcb)
   \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>" apply (clarsimp simp: ct_in_state'_def pred_tcb_at'_def) apply (rule hoare_pre) apply (wps setObject_ct_inv) apply (wp setObject_tcb_strongest) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' activatable' and obj_at' ((=) tcb) t\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s) and obj_at' ((=) tcb) t\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s\<rbrace>
 2. \<And>s. ((\<lambda>s. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s) and obj_at' ((=) tcb) t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> setObject t (tcbQueued_update f tcb) \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. ((\<lambda>s. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s) and obj_at' ((=) tcb) t) s \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s) and obj_at' ((=) tcb) t) s \<Longrightarrow> if t = ksCurThread s then activatable' (tcbState (tcbQueued_update f tcb)) else obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedEnqueue_pred_tcb_at'[wp]:
  "\<lbrace>\<lambda>s. pred_tcb_at' proj P' t' s \<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. pred_tcb_at' proj P' t' s\<rbrace>" apply (simp add: tcbSchedEnqueue_def when_def unless_def) apply (wp threadSet_pred_tcb_no_state crunch_wps | clarsimp simp: tcb_to_itcb'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P' t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. pred_tcb_at' proj P' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P' t'\<rbrace> do queued <- threadGet tcbQueued t;
if \<not> queued then do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od else return ()
od \<lbrace>\<lambda>_. pred_tcb_at' proj P' t'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedDequeue_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
    tcbSchedDequeue t
   \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" unfolding tcbSchedDequeue_def by (wp setQueue_sch_act | wp sch_act_wf_lift | simp add: if_apply_def2)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> do queued <- threadGet tcbQueued t;
when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od
od \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma sbn_sch_act':
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  setBoundNotification ntfn t  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_sch_act | simp)+ done

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

lemma ssa_sch_act_simple[wp]:
  "sa = ResumeCurrentThread \<or> sa = ChooseNewThread \<Longrightarrow>
   \<lbrace>\<top>\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" unfolding setSchedulerAction_def sch_act_simple_def by (wp | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sa = ResumeCurrentThread \<or> sa = ChooseNewThread \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. sa = ResumeCurrentThread \<or> sa = ChooseNewThread \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> modify (ksSchedulerAction_update (\<lambda>_. sa)) \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrace>
theory TcbAcc_R

lemma rescheduleRequired_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (simp add: setThreadState_def) apply (wp hoare_drop_imps | rule sch_act_simple_lift | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<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>rv. sch_act_simple\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setQueue_after:
  "(setQueue d p q >>= (\<lambda>rv. threadSet f t)) =
   (threadSet f t >>= (\<lambda>rv. setQueue d p q))" apply (simp add: setQueue_def) apply (rule oblivious_modify_swap) apply (simp add: threadSet_def getObject_def setObject_def
                   loadObject_default_def
                   split_def projectKO_def2 alignCheck_assert
                   magnitudeCheck_assert updateObject_default_def) apply (intro oblivious_bind, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do rv <- setQueue d p q;
threadSet f t
od = do rv <- threadSet f t;
setQueue d p q
od proof (prove)
goal (1 subgoal):
 1. do rv <- modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>);
threadSet f t
od = do rv <- threadSet f t;
modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>)
od proof (prove)
goal (1 subgoal):
 1. oblivious (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>) (threadSet f t) proof (prove)
goal (1 subgoal):
 1. oblivious (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>) (do tcb <- do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t map));
y <- assert (t = fst p);
val <- assert_opt (projectKO_opt (snd p));
y <- assert (is_aligned t (objBits val));
y <- assert (case snd (lookupAround2 t map) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits val \<le> z - t);
return val
od;
ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- do y <- assert (t = fst p);
_ <- assert_opt (projectKO_opt (snd p));
y <- assert (is_aligned t (objBits (f tcb)));
y <- assert (case snd (lookupAround2 t ps) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits (f tcb) \<le> z - t);
return (KOTCB (f tcb))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedEnqueue_sch_act[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
    tcbSchedEnqueue t
   \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (simp add: tcbSchedEnqueue_def unless_def)
     (wp setQueue_sch_act | wp sch_act_wf_lift  | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma tcbSchedEnqueue_weak_sch_act[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
    tcbSchedEnqueue t
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp setQueue_sch_act threadSet_weak_sch_act_wf | clarsimp)+ done

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

lemma threadGet_wp: "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> P (f tcb) s)\<rbrace> threadGet f t \<lbrace>P\<rbrace>" apply (simp add: threadGet_def) apply (wp getObject_tcb_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> P (f tcb) s)\<rbrace> threadGet f t \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> P (f tcb) s)\<rbrace> liftM f (getObject t) \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> P (f tcb) s) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (P \<circ> f) ta s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadGet_const:
  "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (P \<circ> f) t s\<rbrace> threadGet f t \<lbrace>\<lambda>rv s. P (rv)\<rbrace>" apply (simp add: threadGet_def liftM_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (P \<circ> f) t s\<rbrace> threadGet f t \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (P \<circ> f) t s\<rbrace> do x <- getObject t;
return (f x)
od \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<longrightarrow> obj_at' (P \<circ> f) t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> P (f ta)) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma prioToL1Index_size [simp]:
  "prioToL1Index w < l2BitmapSize" unfolding prioToL1Index_def wordRadix_def l2BitmapSize_def' by (fastforce simp: shiftr_div_2n' nat_divide_less_eq
                intro: order_less_le_trans[OF unat_lt2p])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prioToL1Index w < l2BitmapSize proof (prove)
goal (1 subgoal):
 1. (fromIntegral $ w `~shiftR~` wordSizeCase 5 6) < 8
theory TcbAcc_R

lemma prioToL1Index_bit_set:
  "((2 :: 32 word) ^ prioToL1Index p) !! prioToL1Index p" using l2BitmapSize_def' by (fastforce simp: nth_w2p_same intro: order_less_le_trans[OF prioToL1Index_size])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 ^ prioToL1Index p) !! prioToL1Index p proof (prove)
using this:
l2BitmapSize = 8

goal (1 subgoal):
 1. (2 ^ prioToL1Index p) !! prioToL1Index p