kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_R

lemma valid_queues_no_bitmap_correct_queueI[intro]:
  "valid_queues_no_bitmap s \<Longrightarrow> correct_queue t s" unfolding correct_queue_def valid_queues_no_bitmap_def by (fastforce simp: obj_at'_def inQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues_no_bitmap s \<Longrightarrow> correct_queue t s proof (prove)
goal (1 subgoal):
 1. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []) \<Longrightarrow> \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s
theory Schedule_R

lemma tcbSchedDequeue_valid_queues:
  "\<lbrace>Invariants_H.valid_queues
    and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t
    and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t\<rbrace>
     tcbSchedDequeue t
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (rule hoare_pre, rule tcbSchedDequeue_valid_queues_weak) apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<Longrightarrow> (valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and correct_queue t and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t) s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedAppend_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' tcb\<rbrace>
    tcbSchedAppend tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>" apply (simp add: tcbSchedAppend_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> tcbSchedAppend 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 (queue @ [tcb]);
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 Schedule_R

lemma tcbSchedEnqueue_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedEnqueue_ksMachine) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. 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> tcbSchedEnqueue t \<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> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedEnqueue_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" apply (rule tcb_in_cur_domain'_lift) apply wp apply (clarsimp simp: tcbSchedEnqueue_def) apply (wpsimp simp: unless_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> do queued <- threadGet tcbQueued t;
unless 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>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedAppend_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedAppend_ksMachine) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. 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> tcbSchedAppend t \<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> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedAppend_tcbDomain[wp]:
  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>
     tcbSchedAppend t
   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>" apply (clarsimp simp: tcbSchedAppend_def) apply (wpsimp simp: unless_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedAppend_tcbPriority[wp]:
  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>
     tcbSchedAppend t
   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>" apply (clarsimp simp: tcbSchedAppend_def) apply (wpsimp simp: unless_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedAppend_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedAppend thread
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add:tcbSchedAppend_def bitmap_fun_defs) apply (wp unless_wp setQueue_sch_act threadGet_wp|simp)+ apply (fastforce simp:typ_at'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedAppend thread \<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> do queued <- threadGet tcbQueued thread;
unless queued (do tdom <- threadGet tcbDomain thread;
prio <- threadGet tcbPriority thread;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [thread]);
y <- when (null queue) (do y <- do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks tdom);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap ks)(tdom := l1 || 2 ^ prioToL1Index prio)\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (tdom, invertL1Index (prioToL1Index prio)));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap ks)((tdom, invertL1Index (prioToL1Index prio)) := l2 || 2 ^ unat (prio && mask wordRadix))\<rparr>)
od);
threadSet (tcbQueued_update (\<lambda>_. True)) thread
od)
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> tcb_at' thread s \<longrightarrow> (\<exists>tcb. (tcbQueued tcb \<longrightarrow> ko_at' tcb thread s) \<and> (\<not> tcbQueued tcb \<longrightarrow> ko_at' tcb thread s \<and> (\<exists>tcb. ko_at' tcb thread s))) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedEnqueue_invs'_not_ResumeCurrentThread:
  "\<lbrace>invs'
    and st_tcb_at' runnable' t
    and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
     tcbSchedEnqueue t
   \<lbrace>\<lambda>_. invs'\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. invs'\<rbrace>
theory Schedule_R

lemma tcbSchedAppend_invs'_not_ResumeCurrentThread:
  "\<lbrace>invs'
    and st_tcb_at' runnable' t
    and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
     tcbSchedAppend t
   \<lbrace>\<lambda>_. invs'\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. invs'\<rbrace>
theory Schedule_R

lemma tcb_at'_has_tcbDomain:
 "tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbDomain tcb = p) t s" by (clarsimp simp add: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbDomain tcb = p) t s
theory Schedule_R

lemma valid_queues'_ko_atD:
  "valid_queues' s \<Longrightarrow> ko_at' tcb t s \<Longrightarrow> tcbQueued tcb
    \<Longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb))" apply (simp add: valid_queues'_def) apply (elim allE, erule mp) apply normalise_obj_at' apply (simp add: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues' s; ko_at' tcb t s; tcbQueued tcb\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ko_at' tcb t s; tcbQueued tcb\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb t s; tcbQueued tcb\<rbrakk> \<Longrightarrow> obj_at' (inQ (tcbDomain tcb) (tcbPriority tcb)) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbQueued tcb; ko_at' tcb t s\<rbrakk> \<Longrightarrow> inQ (tcbDomain tcb) (tcbPriority tcb) tcb proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedDequeue_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedDequeue_ksMachine) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. 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> tcbSchedDequeue t \<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> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedDequeue_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" apply (rule tcb_in_cur_domain'_lift) apply wp apply (clarsimp simp: tcbSchedDequeue_def) apply (wp hoare_when_weak_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) 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>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedDequeue_tcbDomain[wp]:
  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>
     tcbSchedDequeue t
   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>" apply (clarsimp simp: tcbSchedDequeue_def) apply (wp hoare_when_weak_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) 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>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedDequeue_tcbPriority[wp]:
  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>
     tcbSchedDequeue t
   \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>" apply (clarsimp simp: tcbSchedDequeue_def) apply (wp hoare_when_weak_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) 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>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma setCurThread_corres:
  "corres dc \<top> \<top> (modify (cur_thread_update (\<lambda>_. t))) (setCurThread t)" apply (unfold setCurThread_def) apply (rule corres_modify) apply (simp add: state_relation_def swp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (modify (cur_thread_update (\<lambda>_. t))) (setCurThread t) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (modify (cur_thread_update (\<lambda>_. t))) (modify (ksCurThread_update (\<lambda>_. t))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>cur_thread := t\<rparr>, s'\<lparr>ksCurThread := t\<rparr>) \<in> state_relation proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma arch_switch_thread_tcb_at' [wp]: "\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>" by (unfold ARM_H.switchToThread_def, wp typ_at_lift_tcb')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
theory Schedule_R

lemma Arch_switchToThread_pred_tcb'[wp]:
  "\<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace>
   Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>" proof - have pos: "\<And>P t t'. \<lbrace>pred_tcb_at' proj P t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace>" apply (simp add:  pred_tcb_at'_def ARM_H.switchToThread_def) apply (rule hoare_seq_ext)+ apply (rule doMachineOp_obj_at) apply (rule setVMRoot_obj_at) done show ?thesis apply (rule P_bool_lift [OF pos]) by (rule lift_neg_pred_tcb_at' [OF ArchThreadDecls_H_ARM_H_switchToThread_typ_at' pos]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t t'. \<lbrace>pred_tcb_at' proj P t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t t'. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P t t' y. \<lbrace>?B P t t' y\<rbrace> doMachineOp ARM.clearExMonitor \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace>
 2. \<And>P t t'. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace> setVMRoot t \<lbrace>?B P t t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t t'. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t'\<rbrace> setVMRoot t \<lbrace>\<lambda>y. obj_at' (\<lambda>a. P (proj (tcb_to_itcb' a))) t'\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pred_tcb_at' proj ?P ?t'\<rbrace> Arch.switchToThread ?t \<lbrace>\<lambda>rv. pred_tcb_at' proj ?P ?t'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv s. P (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> Arch.switchToThread t \<lbrace>\<lambda>rv s. \<not> pred_tcb_at' proj P' t' s\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>

goal:
No subgoals!
theory Schedule_R

lemma arch_switch_thread_ksQ[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>" apply (simp add: ARM_H.switchToThread_def) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal:
No subgoals!