kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma addToBitmap_ksMachine[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>" unfolding bitmap_fun_defs by (wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
theory TcbAcc_R

lemma removeFromBitmap_ksMachine[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>" unfolding bitmap_fun_defs by (wp|simp add: bitmap_fun_defs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
(\<lambda>f. do l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), f l2)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
when (l2 = 0) $ (\<lambda>f. do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, f l1)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
theory TcbAcc_R

lemma tcbSchedEnqueue_ksMachine[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> tcbSchedEnqueue x \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>" by (simp add: tcbSchedEnqueue_def unless_def setQueue_def | wp)+

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

lemma setThreadState_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setThreadState F t \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> setThreadState F t \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> setThreadState F t \<lbrace>\<lambda>rv s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma ct_not_inQ_addToBitmap[wp]:
  "\<lbrace> ct_not_inQ \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. ct_not_inQ \<rbrace>" unfolding bitmap_fun_defs by (wp, clarsimp simp: ct_not_inQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>
theory TcbAcc_R

lemma ct_not_inQ_removeFromBitmap[wp]:
  "\<lbrace> ct_not_inQ \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. ct_not_inQ \<rbrace>" unfolding bitmap_fun_defs by (wp|simp add: bitmap_fun_defs ct_not_inQ_def comp_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
(\<lambda>f. do l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), f l2)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
when (l2 = 0) $ (\<lambda>f. do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, f l1)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>
theory TcbAcc_R

lemma setBoundNotification_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setSchedulerAction_direct:
  "\<lbrace>\<top>\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>_ s. ksSchedulerAction s = sa\<rbrace>" by (wpsimp simp: setSchedulerAction_def)

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

lemma rescheduleRequired_ct_not_inQ:
  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: rescheduleRequired_def ct_not_inQ_def) apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = ChooseNewThread"
           in hoare_post_imp, clarsimp) apply (wp setSchedulerAction_direct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. ct_not_inQ\<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>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread 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>_ s. ksSchedulerAction s = ChooseNewThread\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_sa_cnt[wp]:
  "\<lbrace>\<lambda>s. True \<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>" unfolding rescheduleRequired_def setSchedulerAction_def by wpsimp

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

lemma possibleSwitchTo_ct_not_inQ:
  "\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
    possibleSwitchTo t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") apply (simp add: possibleSwitchTo_def curDomain_def) apply (wpsimp wp: hoare_weak_lift_imp rescheduleRequired_ct_not_inQ tcbSchedEnqueue_ct_not_inQ
                    threadGet_wp
       | (rule hoare_post_imp[OF _ rescheduleRequired_sa_cnt], fastforce))+ apply (fastforce simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction $ SwitchToThread t
od \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ct_not_inQ s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>tcb. ko_at' tcb t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setThreadState_ct_not_inQ:
  "\<lbrace>ct_not_inQ\<rbrace> setThreadState st t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") including no_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_ct_not_inQ) apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_post_imp, clarsimp) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> setThreadState st t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> setThreadState st t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<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>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then \<lambda>_. True else ct_not_inQ) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_ct_not_inQ:
  "\<lbrace>ct_not_inQ\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") by (simp add: setBoundNotification_def, wp)

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

lemma setThreadState_not_st:
  "(\<And>tcb st qd. P (tcb\<lparr>tcbState := st, tcbQueued := qd\<rparr>) \<longleftrightarrow> P tcb)
     \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace>" apply (simp add: setThreadState_def rescheduleRequired_def) apply (wp hoare_vcg_conj_lift tcbSchedEnqueue_not_st
          | wpc
          | rule hoare_drop_imps
          | simp)+ apply (clarsimp simp: obj_at'_def) apply (case_tac obj) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb) \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb) \<Longrightarrow> \<lbrace>obj_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) (do action <- getSchedulerAction;
y <- case action of SwitchToThread x \<Rightarrow> tcbSchedEnqueue x | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od)
od \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb; obj_at' P t' s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>obj. (t = t' \<longrightarrow> P (tcbState_update (\<lambda>_. st) obj)) \<and> (t \<noteq> t' \<longrightarrow> P obj)) t' s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj. \<lbrakk>\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb; ksPSpace s t' = Some ko; is_aligned t' (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear t' (objBitsKO ko) s; t = t'\<rbrakk> \<Longrightarrow> P (tcbState_update (\<lambda>_. st) obj) proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb; ksPSpace s t' = Some ko; is_aligned t' (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear t' (objBitsKO ko) s; t = t'; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> P (tcbState_update (\<lambda>_. st) obj) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma addToBitmap_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace> ct_idle_or_in_cur_domain' \<rbrace> addToBitmap d p \<lbrace> \<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift| rule obj_at_setObject2
           | clarsimp simp: updateObject_default_def in_monad setNotification_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> addToBitmap d p \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>da a t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. da = tcbDomain tcb) t s\<rbrace> addToBitmap d p \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. da = tcbDomain tcb) t s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma removeFromBitmap_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace> ct_idle_or_in_cur_domain' \<rbrace> removeFromBitmap d p \<lbrace> \<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift| rule obj_at_setObject2
           | clarsimp simp: updateObject_default_def in_monad setNotification_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>da a t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. da = tcbDomain tcb) t s\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. da = tcbDomain tcb) t s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedEnqueue_ksDomSchedule[wp]:
  "\<lbrace> \<lambda>s. P (ksDomSchedule s)\<rbrace> tcbSchedEnqueue tptr \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply wpsimp done

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

lemma tcbSchedEnqueue_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> tcbSchedEnqueue tptr \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp threadSet_ct_idle_or_in_cur_domain' | simp)+ done

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

lemma setSchedulerAction_spec:
  "\<lbrace>\<top>\<rbrace>setSchedulerAction ChooseNewThread
  \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>" apply (simp add:setSchedulerAction_def) apply wp apply (simp add:ct_idle_or_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> modify (ksSchedulerAction_update (\<lambda>_. ChooseNewThread)) \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ct_idle_or_in_cur_domain' (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp setSchedulerAction_spec) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<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. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_ksCurDomain[wp]:
  "\<lbrace> \<lambda>s. P (ksCurDomain s) \<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksCurDomain s) \<rbrace>" apply (simp add: rescheduleRequired_def) apply wpsimp done

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

lemma rescheduleRequired_ksDomSchedule[wp]:
  "\<lbrace> \<lambda>s. P (ksDomSchedule s) \<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>" by (simp add: rescheduleRequired_def) wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>
theory TcbAcc_R

lemma setThreadState_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setThreadState st tptr \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>" apply (simp add: setThreadState_def) apply (wp threadSet_ct_idle_or_in_cur_domain' hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setThreadState st tptr \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) tptr;
runnable <- isRunnable tptr;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = tptr \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal:
No subgoals!