kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_R

lemma sts_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (simp add: setThreadState_def) apply (wp threadSet_valid_inQ_queues [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<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. valid_inQ_queues\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. valid_inQ_queues s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then valid_inQ_queues else valid_inQ_queues) s
 2. \<And>s. valid_inQ_queues s \<Longrightarrow> (valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbState_update (\<lambda>_. st) tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbState_update (\<lambda>_. st) tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma updateObject_ep_inv:
  "\<lbrace>P\<rbrace> updateObject (obj::endpoint) ko p q n \<lbrace>\<lambda>rv. P\<rbrace>" by simp (rule updateObject_default_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> updateObject obj ko p q n \<lbrace>\<lambda>rv. P\<rbrace>
theory IpcCancel_R

lemma sbn_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_valid_inQ_queues [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_inQ_queues s \<Longrightarrow> (valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbBoundNotification_update (\<lambda>_. ntfn) tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbBoundNotification_update (\<lambda>_. ntfn) tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setEndpoint_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (unfold setEndpoint_def) apply (rule setObject_ep_pre) apply (simp add: valid_inQ_queues_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift setObject_queues_unchanged[OF updateObject_ep_inv]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> setEndpoint ptr ep \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> setObject ptr ep \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues and ep_at' ptr\<rbrace> setObject ptr ep \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))) and ep_at' ptr\<rbrace> setObject ptr ep \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))) and ep_at' ptr) s \<Longrightarrow> \<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). obj_at' (inQ x xa) xb s) \<and> distinct (ksReadyQueues s (x, xa)) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma set_ntfn_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (unfold setNotification_def) apply (rule setObject_ntfn_pre) apply (simp add: valid_inQ_queues_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift) apply (clarsimp simp: updateObject_default_def in_monad) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues and ntfn_at' ptr\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))) and ntfn_at' ptr\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d p P q n obj. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, p)))\<rbrace> updateObject ntfn obj ptr q n \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>d p. \<lbrace>?P'5 d p\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>s. ((\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))) and ntfn_at' ptr) s \<Longrightarrow> \<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). obj_at' (inQ x xa) xb s) \<and> ?P'5 x xa s proof (prove)
goal (3 subgoals):
 1. \<And>d p P q n obj. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, p)))\<rbrace> do y <- assert (ptr = q);
_ <- projectKO obj;
y <- alignCheck ptr (objBits ntfn);
y <- magnitudeCheck ptr n (objBits ntfn);
return (KONotification ntfn)
od \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>d p. \<lbrace>?P'5 d p\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>s. ((\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))) and ntfn_at' ptr) s \<Longrightarrow> \<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). obj_at' (inQ x xa) xb s) \<and> ?P'5 x xa s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> cancelIPC t \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def) apply (wp hoare_drop_imps delete_one_inQ_queues threadSet_valid_inQ_queues | wpc | simp add:if_apply_def2 Fun.comp_def)+ apply (clarsimp simp: valid_inQ_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> cancelIPC t \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_inQ_queues s \<Longrightarrow> \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbFault_update (\<lambda>_. None) tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbFault_update (\<lambda>_. None) tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma valid_queues_inQ_queues:
  "Invariants_H.valid_queues s \<Longrightarrow> valid_inQ_queues s" by (force simp: Invariants_H.valid_queues_def valid_inQ_queues_def obj_at'_def
                  valid_queues_no_bitmap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Invariants_H.valid_queues s \<Longrightarrow> valid_inQ_queues s
theory IpcCancel_R

lemma (in delete_one) prepareThreadDelete_corres:
  "corres dc (tcb_at t) (tcb_at' t)
        (prepare_thread_delete t) (ArchRetypeDecls_H.ARM_H.prepareThreadDelete t)" by (simp add: ArchVSpace_A.ARM_A.prepare_thread_delete_def ArchRetype_H.ARM_H.prepareThreadDelete_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (prepare_thread_delete t) (Arch.prepareThreadDelete t)
theory IpcCancel_R

lemma no_refs_simple_strg':
  "st_tcb_at' simple' t s' \<and> P {} \<longrightarrow> st_tcb_at' (\<lambda>st. P (tcb_st_refs_of' st)) t s'" by (fastforce elim!: pred_tcb'_weakenE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' simple' t s' \<and> P {} \<longrightarrow> st_tcb_at' (\<lambda>st. P (tcb_st_refs_of' st)) t s'
theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_it[wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace>
   cancelIPC t
   \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def) apply (wp hoare_drop_imps delete_one_it | wpc | simp add:if_apply_def2 Fun.comp_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma asUser_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace> asUser s t \<lbrace>\<lambda>_. sch_act_simple\<rbrace>" unfolding sch_act_simple_def apply (rule asUser_nosch) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> asUser s t \<lbrace>\<lambda>_. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrace> asUser s t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc_pre) suspend_tcb'[wp]:
  "\<lbrace>tcb_at' t'\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" apply (simp add: suspend_def unless_def) apply wp apply (wpsimp simp: updateRestartPC_def) apply (wp hoare_drop_imps |clarsimp|rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?Q7 y state\<rbrace> updateRestartPC t \<lbrace>\<lambda>ya. tcb_at' t'\<rbrace>
 2. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R7 y state\<rbrace> return () \<lbrace>\<lambda>ya. tcb_at' t'\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> ?Q7 y state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R7 y state s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. tcb_at' t' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R7 y state\<rbrace> return () \<lbrace>\<lambda>ya. tcb_at' t'\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> tcb_at' t' s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R7 y state s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 4. \<And>s. tcb_at' t' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc_pre) suspend_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace>
  ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (simp add: suspend_def when_def updateRestartPC_def) apply (wp cancelIPC_sch_act_simple | simp add: unless_def
       | rule sch_act_simple_lift)+ apply (simp add: updateRestartPC_def) apply (rule asUser_nosch) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> updateRestartPC t \<lbrace>\<lambda>ya s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R16 y state\<rbrace> return () \<lbrace>\<lambda>ya. sch_act_simple\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R16 y state s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. sch_act_simple s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) \<lbrace>\<lambda>ya s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R16 y state\<rbrace> return () \<lbrace>\<lambda>ya. sch_act_simple\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R16 y state s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. sch_act_simple s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R16 y state\<rbrace> return () \<lbrace>\<lambda>ya. sch_act_simple\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R16 y state s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 4. \<And>s. sch_act_simple s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc) suspend_objs':
  "\<lbrace>invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace>
   suspend t \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (rule_tac Q="\<lambda>_. invs'" in hoare_strengthen_post) apply (wp suspend_invs') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>rv s. invs' s \<Longrightarrow> valid_objs' s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. invs' s \<Longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc_pre) suspend_st_tcb_at':
  assumes x[simp]: "\<And>st. simple' st \<longrightarrow> P st" shows
  "\<lbrace>st_tcb_at' P t\<rbrace>
     suspend thread
   \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" unfolding suspend_def updateRestartPC_def apply (wp sts_st_tcb_at'_cases threadSet_pred_tcb_no_state
            cancelIPC_st_tcb_at hoare_drop_imps asUser_pred_tcb_at' x
         | simp)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> ThreadDecls_H.suspend thread \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> do cancelIPC thread;
state <- getThreadState thread;
if state = Structures_H.thread_state.Running then asUser thread (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) else return ();
setThreadState Structures_H.thread_state.Inactive thread;
tcbSchedDequeue thread
od \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' P t s \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma tcbSchedDequeue_nonq[wp]:
  "\<lbrace>Invariants_H.valid_queues and tcb_at' t and K (t = t')\<rbrace>
    tcbSchedDequeue t \<lbrace>\<lambda>_ s. \<forall>d p. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: tcbSchedDequeue_def) apply (wp threadGet_wp|simp)+ apply (fastforce simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def obj_at'_def projectKOs inQ_def) done

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