kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma rescheduleRequired_ksQ:
  "\<lbrace>\<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p)\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>" including no_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\<lambda>rv s. (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)
                            \<and> P (ksReadyQueues s p)" in hoare_seq_ext) apply wpsimp apply (case_tac x; simp) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p)\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p)\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. (x = ResumeCurrentThread \<or> x = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> do y <- case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>
 2. \<lbrace>\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. (rv = ResumeCurrentThread \<or> rv = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. (x = ResumeCurrentThread \<or> x = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y s. P (ksReadyQueues s p)\<rbrace>
 2. \<lbrace>\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. (rv = ResumeCurrentThread \<or> rv = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. (rv = ResumeCurrentThread \<or> rv = ChooseNewThread) \<and> P (ksReadyQueues s p)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setSchedulerAction_ksQ[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setSchedulerAction act \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>" by (wp, simp)

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

lemma threadSet_ksQ[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>" by (simp add: threadSet_def | wp updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>
theory TcbAcc_R

lemma sbn_ksQ:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. P (ksReadyQueues s p)\<rbrace>" by (simp add: setBoundNotification_def, wp)

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

lemma sts_ksQ:
  "\<lbrace>\<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p)\<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_ksQ) apply (rule_tac Q="\<lambda>_ s. P (ksReadyQueues s p)" in hoare_post_imp) apply (clarsimp simp: sch_act_simple_def)+ apply (wp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p)\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p)\<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>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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>s. sch_act_simple s \<and> P (ksReadyQueues s p) else (\<lambda>s. P (ksReadyQueues s p))) s\<rbrace>
 2. \<And>s. sch_act_simple s \<and> P (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. P (ksReadyQueues s p) \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then \<lambda>s. sch_act_simple s \<and> P (ksReadyQueues s p) else (\<lambda>s. P (ksReadyQueues s p))) s
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>
 3. \<And>s. sch_act_simple s \<and> P (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>
 2. \<And>s. sch_act_simple s \<and> P (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma tcbSchedEnqueue_ksQ:
  "\<lbrace>\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> t' \<noteq> t \<rbrace>
   tcbSchedEnqueue t \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wpsimp wp: hoare_vcg_imp_lift threadGet_wp) apply (drule obj_at_ko_at') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> t' \<noteq> t\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> t' \<noteq> t\<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. t' \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t' \<notin> set (ksReadyQueues s p); t' \<noteq> t; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>tcb. (\<not> tcbQueued tcb \<longrightarrow> ko_at' tcb t s \<and> (\<exists>tcb. ko_at' tcb t s \<and> (\<exists>tcba. (p = (tcbDomain tcb, tcbPriority tcba) \<longrightarrow> ko_at' tcba t s \<and> t' \<notin> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcba))) \<and> (p \<noteq> (tcbDomain tcb, tcbPriority tcba) \<longrightarrow> ko_at' tcba t s)))) \<and> (tcbQueued tcb \<longrightarrow> ko_at' tcb t s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t' \<notin> set (ksReadyQueues s p); t' \<noteq> t; \<exists>ko. ko_at' ko t s \<and> True\<rbrakk> \<Longrightarrow> \<exists>tcb. (\<not> tcbQueued tcb \<longrightarrow> ko_at' tcb t s \<and> (\<exists>tcb. ko_at' tcb t s \<and> (\<exists>tcba. (p = (tcbDomain tcb, tcbPriority tcba) \<longrightarrow> ko_at' tcba t s \<and> t' \<notin> set (ksReadyQueues s (tcbDomain tcb, tcbPriority tcba))) \<and> (p \<noteq> (tcbDomain tcb, tcbPriority tcba) \<longrightarrow> ko_at' tcba t s)))) \<and> (tcbQueued tcb \<longrightarrow> ko_at' tcb t s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_ksQ':
  "\<lbrace>\<lambda>s. t \<notin> set (ksReadyQueues s p) \<and> sch_act_not t s \<rbrace>
   rescheduleRequired \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wpsimp wp: tcbSchedEnqueue_ksQ) done

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

lemma threadSet_tcbState_st_tcb_at':
  "\<lbrace>\<lambda>s. P st \<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>" apply (simp add: threadSet_def pred_tcb_at'_def) apply (wpsimp wp: setObject_tcb_strongest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P st\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P st\<rbrace> do tcb <- getObject t;
setObject t (tcbState_update (\<lambda>_. st) tcb)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>ko. P (tcbState ko)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma isRunnable_const:
  "\<lbrace>st_tcb_at' runnable' t\<rbrace> isRunnable t \<lbrace>\<lambda>runnable _. runnable \<rbrace>" by (rule isRunnable_wp)

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

lemma in_user_frame_eq:
  assumes y: "y < unat max_ipc_words"
  and    al: "is_aligned a msg_align_bits"
  shows "in_user_frame (a + of_nat y * 4) s = in_user_frame a s" proof - have "\<And>sz. (a + of_nat y * 4) && ~~ mask (pageBitsForSize sz) =
             a && ~~ mask (pageBitsForSize sz)" apply (rule mask_out_first_mask_some [where n = msg_align_bits]) apply (rule is_aligned_add_helper [OF al, THEN conjunct2]) apply (rule word_less_power_trans_ofnat [where k = 2, simplified]) apply (rule order_less_le_trans [OF y]) apply (simp add: msg_align_bits max_ipc_words) apply (simp add: msg_align_bits) apply (simp add: msg_align_bits pageBits_def) apply (case_tac sz, simp_all add: msg_align_bits) done thus ?thesis by (simp add: in_user_frame_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. in_user_frame (a + word_of_nat y * 4) s = in_user_frame a s proof (state)
goal (1 subgoal):
 1. in_user_frame (a + word_of_nat y * 4) s = in_user_frame a s proof (prove)
goal (1 subgoal):
 1. \<And>sz. a + word_of_nat y * 4 && ~~ mask (pageBitsForSize sz) = a && ~~ mask (pageBitsForSize sz) proof (prove)
goal (2 subgoals):
 1. \<And>sz. a + word_of_nat y * 4 && ~~ mask msg_align_bits = a
 2. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. \<And>sz. word_of_nat y * 4 < 2 ^ msg_align_bits
 2. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (4 subgoals):
 1. \<And>sz. y < 2 ^ (msg_align_bits - 2)
 2. \<And>sz. 2 \<le> msg_align_bits
 3. \<And>sz. msg_align_bits < LENGTH(32)
 4. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (4 subgoals):
 1. \<And>sz. unat max_ipc_words \<le> 2 ^ (msg_align_bits - 2)
 2. \<And>sz. 2 \<le> msg_align_bits
 3. \<And>sz. msg_align_bits < LENGTH(32)
 4. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (3 subgoals):
 1. \<And>sz. 2 \<le> msg_align_bits
 2. \<And>sz. msg_align_bits < LENGTH(32)
 3. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. \<And>sz. msg_align_bits < LENGTH(32)
 2. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal (1 subgoal):
 1. \<And>sz. msg_align_bits \<le> pageBitsForSize sz proof (prove)
goal:
No subgoals! proof (state)
this:
a + word_of_nat y * 4 && ~~ mask (pageBitsForSize ?sz) = a && ~~ mask (pageBitsForSize ?sz)

goal (1 subgoal):
 1. in_user_frame (a + word_of_nat y * 4) s = in_user_frame a s proof (prove)
using this:
a + word_of_nat y * 4 && ~~ mask (pageBitsForSize ?sz) = a && ~~ mask (pageBitsForSize ?sz)

goal (1 subgoal):
 1. in_user_frame (a + word_of_nat y * 4) s = in_user_frame a s proof (state)
this:
in_user_frame (a + word_of_nat y * 4) s = in_user_frame a s

goal:
No subgoals!
theory TcbAcc_R

lemma doMachineOp_bind:
 "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> doMachineOp (a >>= b) = (doMachineOp a >>= (\<lambda>rv. doMachineOp (b rv)))" by (blast intro: submonad_bind submonad_doMachineOp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail a; \<And>x. empty_fail (b x)\<rbrakk> \<Longrightarrow> doMachineOp (a >>= b) = do rv <- doMachineOp a;
doMachineOp (b rv)
od
theory TcbAcc_R

lemma valid_ipc_buffer_ptr'_def2:
  "valid_ipc_buffer_ptr' = (\<lambda>p s. (is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s))" apply (rule ext, rule ext) apply (simp add: valid_ipc_buffer_ptr'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ipc_buffer_ptr' = (\<lambda>p s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s) proof (prove)
goal (1 subgoal):
 1. \<And>p s. valid_ipc_buffer_ptr' p s = (is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma storeWordUser_valid_ipc_buffer_ptr' [wp]:
  "\<lbrace>valid_ipc_buffer_ptr' p\<rbrace> storeWordUser p' w \<lbrace>\<lambda>_. valid_ipc_buffer_ptr' p\<rbrace>" unfolding valid_ipc_buffer_ptr'_def2 by (wp hoare_vcg_all_lift storeWordUser_typ_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ipc_buffer_ptr' p\<rbrace> storeWordUser p' w \<lbrace>\<lambda>_. valid_ipc_buffer_ptr' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s\<rbrace> storeWordUser p' w \<lbrace>\<lambda>_ s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s\<rbrace>
theory TcbAcc_R

lemma no_0_obj_kheap:
  assumes no0: "no_0_obj' s'"
  and     psr: "pspace_relation (kheap s) (ksPSpace s')"
  shows   "kheap s 0 = None" proof (rule ccontr) assume "kheap s 0 \<noteq> None" hence "0 \<in> dom (kheap s)" .. hence "0 \<in> pspace_dom (kheap s)" by (rule set_mp [OF pspace_dom_dom]) moreover from no0 have "0 \<notin> dom (ksPSpace s')" unfolding no_0_obj'_def by clarsimp ultimately show False using psr by (clarsimp simp: pspace_relation_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s 0 = None proof (state)
goal (1 subgoal):
 1. kheap s 0 \<noteq> None \<Longrightarrow> False proof (state)
this:
kheap s 0 \<noteq> None

goal (1 subgoal):
 1. kheap s 0 \<noteq> None \<Longrightarrow> False proof (prove)
using this:
kheap s 0 \<noteq> None

goal (1 subgoal):
 1. 0 \<in> dom (kheap s) proof (state)
this:
0 \<in> dom (kheap s)

goal (1 subgoal):
 1. kheap s 0 \<noteq> None \<Longrightarrow> False proof (prove)
using this:
0 \<in> dom (kheap s)

goal (1 subgoal):
 1. 0 \<in> pspace_dom (kheap s) proof (state)
this:
0 \<in> pspace_dom (kheap s)

goal (1 subgoal):
 1. kheap s 0 \<noteq> None \<Longrightarrow> False proof (state)
this:
0 \<in> pspace_dom (kheap s)

goal (1 subgoal):
 1. kheap s 0 \<noteq> None \<Longrightarrow> False proof (chain)
picking this:
no_0_obj' s' proof (prove)
using this:
no_0_obj' s'

goal (1 subgoal):
 1. 0 \<notin> dom (ksPSpace s') proof (prove)
using this:
ksPSpace s' 0 = None

goal (1 subgoal):
 1. 0 \<notin> dom (ksPSpace s') proof (state)
this:
0 \<notin> dom (ksPSpace s')

goal (1 subgoal):
 1. kheap s 0 \<noteq> None \<Longrightarrow> False proof (chain)
picking this:
0 \<in> pspace_dom (kheap s)
0 \<notin> dom (ksPSpace s') proof (prove)
using this:
0 \<in> pspace_dom (kheap s)
0 \<notin> dom (ksPSpace s')

goal (1 subgoal):
 1. False proof (prove)
using this:
0 \<in> pspace_dom (kheap s)
0 \<notin> dom (ksPSpace s')
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!
theory TcbAcc_R

lemma lookupIPCBuffer_corres:
  "corres (=) (tcb_at t and invs)
               (tcb_at' t and invs')
               (lookup_ipc_buffer w t) (lookupIPCBuffer w t)" using lookupIPCBuffer_corres' by (rule corres_guard_imp, auto simp: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t and invs) (tcb_at' t and invs') (lookup_ipc_buffer w t) (lookupIPCBuffer w t) proof (prove)
using this:
corres (=) (tcb_at ?t and valid_objs and pspace_aligned) (tcb_at' ?t and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') (lookup_ipc_buffer ?w ?t) (lookupIPCBuffer ?w ?t)

goal (1 subgoal):
 1. corres (=) (tcb_at t and invs) (tcb_at' t and invs') (lookup_ipc_buffer w t) (lookupIPCBuffer w t)
theory TcbAcc_R

lemma setThreadState_st_tcb':
  "\<lbrace>\<top>\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' (\<lambda>s. s = st) t\<rbrace>" apply (simp add: setThreadState_def) apply (wp threadSet_pred_tcb_at_state | simp add: if_apply_def2)+ done

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

lemma setThreadState_st_tcb:
  "\<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" apply (cases "P st") apply simp apply (rule hoare_post_imp [OF _ setThreadState_st_tcb']) apply (erule pred_tcb'_weakenE, simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. P st \<Longrightarrow> \<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 2. \<not> P st \<Longrightarrow> \<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. P st \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 2. \<not> P st \<Longrightarrow> \<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>P st; st_tcb_at' (\<lambda>s. s = st) t s\<rbrakk> \<Longrightarrow> st_tcb_at' P t s
 2. \<not> P st \<Longrightarrow> \<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> P st \<Longrightarrow> \<lbrace>\<lambda>s. P st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_bound_tcb':
  "\<lbrace>\<top>\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' (\<lambda>s. s = ntfn) t\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_pred_tcb_at_state | simp add: if_apply_def2)+ done

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

lemma setBoundNotification_bound_tcb:
  "\<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace>" apply (cases "P ntfn") apply simp apply (rule hoare_post_imp [OF _ setBoundNotification_bound_tcb']) apply (erule pred_tcb'_weakenE, simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. P ntfn \<Longrightarrow> \<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace>
 2. \<not> P ntfn \<Longrightarrow> \<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. P ntfn \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace>
 2. \<not> P ntfn \<Longrightarrow> \<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>P ntfn; bound_tcb_at' (\<lambda>s. s = ntfn) t s\<rbrakk> \<Longrightarrow> bound_tcb_at' P t s
 2. \<not> P ntfn \<Longrightarrow> \<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> P ntfn \<Longrightarrow> \<lbrace>\<lambda>s. P ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. bound_tcb_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma ct_in_state'_decomp:
  assumes x: "\<lbrace>\<lambda>s. t = (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>rv s. t = (ksCurThread s)\<rbrace>"
  assumes y: "\<lbrace>Pre\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at' Prop t\<rbrace>"
  shows      "\<lbrace>\<lambda>s. Pre s \<and> t = (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>rv. ct_in_state' Prop\<rbrace>" apply (rule hoare_post_imp [where Q="\<lambda>rv s. t = ksCurThread s \<and> st_tcb_at' Prop t s"]) apply (clarsimp simp add: ct_in_state'_def) apply (rule hoare_vcg_precond_imp) apply (wp x y) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Pre s \<and> t = ksCurThread s\<rbrace> f \<lbrace>\<lambda>rv. ct_in_state' Prop\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. t = ksCurThread s \<and> st_tcb_at' Prop t s \<Longrightarrow> ct_in_state' Prop s
 2. \<lbrace>\<lambda>s. Pre s \<and> t = ksCurThread s\<rbrace> f \<lbrace>\<lambda>rv s. t = ksCurThread s \<and> st_tcb_at' Prop t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Pre s \<and> t = ksCurThread s\<rbrace> f \<lbrace>\<lambda>rv s. t = ksCurThread s \<and> st_tcb_at' Prop t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> f \<lbrace>\<lambda>rv s. t = ksCurThread s \<and> st_tcb_at' Prop t s\<rbrace>
 2. \<And>s. Pre s \<and> t = ksCurThread s \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. Pre s \<and> t = ksCurThread s \<Longrightarrow> t = ksCurThread s \<and> Pre s proof (prove)
goal:
No subgoals!