kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_ksCurDomain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>" apply (simp add: cancelIPC_def Let_def) apply (wp hoare_vcg_conj_lift delete_one_ksCurDomain
     | wpc
     | rule hoare_drop_imps
     | simp add: getThreadReplySlot_def o_def if_fun_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain 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 <- getThreadReplySlot t;
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 (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_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 IpcCancel_R

lemma setBoundNotification_not_ntfn:
  "(\<And>tcb ntfn. P (tcb\<lparr>tcbBoundNotification := ntfn\<rparr>) \<longleftrightarrow> P tcb)
     \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp hoare_vcg_conj_lift
     | wpc
     | rule hoare_drop_imps
     | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb ntfn. P (tcbBoundNotification_update (\<lambda>_. ntfn) tcb) = P tcb) \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb ntfn. P (tcbBoundNotification_update (\<lambda>_. ntfn) tcb) = P tcb) \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setThreadState_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace>" apply (simp add: tcb_in_cur_domain'_def) apply (rule hoare_pre) apply wps apply (wp setThreadState_not_st | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. ksCurDomain prev_s = tcbDomain tcb) t'\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?P3 s s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma cancelSignal_tcb_obj_at':
  "(\<And>tcb st qd. P (tcb\<lparr>tcbState := st, tcbQueued := qd\<rparr>) \<longleftrightarrow> P tcb)
     \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> cancelSignal t word \<lbrace>\<lambda>_. obj_at' P t'\<rbrace>" apply (simp add: cancelSignal_def setNotification_def) apply (wp setThreadState_not_st getNotification_wp | wpc | simp)+ 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> cancelSignal t word \<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 ntfn <- getNotification word;
y <- assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn);
y <- setObject word (ntfnObj_update (\<lambda>_. ntfn') ntfn);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_tcbDomain_obj_at':
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (simp add: cancelIPC_def Let_def) apply (wp hoare_vcg_conj_lift
          setThreadState_not_st delete_one_tcbDomain_obj_at' cancelSignal_tcb_obj_at'
     | wpc
     | rule hoare_drop_imps
     | simp add: getThreadReplySlot_def o_def if_fun_split)+ done

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

lemma (in delete_one_conc_pre) cancelIPC_tcb_in_cur_domain':
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace>" apply (simp add: tcb_in_cur_domain'_def) apply (rule hoare_pre) apply wps apply (wp cancelIPC_tcbDomain_obj_at' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. ksCurDomain prev_s = tcbDomain tcb) t'\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?P3 s s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_sch_act_not:
  "\<lbrace>sch_act_not t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_. sch_act_not t'\<rbrace>" apply (simp add: cancelIPC_def Let_def) apply (wp hoare_vcg_conj_lift
            delete_one_sch_act_not
       | wpc
       | simp add: getThreadReplySlot_def o_def if_apply_def2
              split del: if_split
       | rule hoare_drop_imps)+ done

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

lemma (in delete_one_conc_pre) cancelIPC_weak_sch_act_wf:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
      cancelIPC t
   \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (rule weak_sch_act_wf_lift_linear) apply (wp cancelIPC_sch_act_not cancelIPC_tcb_in_cur_domain' cancelIPC_tcb_at_runnable')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> cancelIPC t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ta. \<lbrace>sch_act_not ta\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. sch_act_not ta\<rbrace>
 2. \<And>ta. \<lbrace>st_tcb_at' runnable' ta\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. st_tcb_at' runnable' ta\<rbrace>
 3. \<And>ta. \<lbrace>tcb_in_cur_domain' ta\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. tcb_in_cur_domain' ta\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma sbn_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" by (simp add: setBoundNotification_def, wp threadSet_nosch)

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

lemma sbn_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   setBoundNotification ntfn t
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp weak_sch_act_wf_lift sbn_st_tcb')

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

lemma setObject_ntfn_sa_unchanged[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
    setObject ptr (ntfn::Structures_H.notification)
   \<lbrace>\<lambda>rv s.  P (ksSchedulerAction s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp | simp add: updateObject_default_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 (fromPPtr ptr) ps));
obj' <- updateObject_default ntfn (snd p) (fromPPtr ptr) (fst p) (snd (lookupAround2 (fromPPtr ptr) ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setObject_oa_unchanged[wp]:
  "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb::tcb. P tcb) t s\<rbrace>
    setObject ptr (ntfn::Structures_H.notification)
   \<lbrace>\<lambda>rv s.  obj_at' P t s\<rbrace>" apply (rule obj_at_setObject2) apply (clarsimp simp add: updateObject_type
                            updateObject_default_def
                            in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setObject ptr ntfn \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setNotification_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
    setNotification ntfnptr ntfn
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (wp hoare_vcg_all_lift hoare_convert_imp hoare_vcg_conj_lift
         | simp add: setNotification_def weak_sch_act_wf_def st_tcb_at'_def tcb_in_cur_domain'_def)+ apply (rule hoare_pre) apply (wps setObject_ntfn_cur_domain) apply (wp setObject_ntfn_obj_at'_tcb | simp add: o_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> setNotification ntfnptr ntfn \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrace>?P'7 t\<rbrace> setObject ntfnptr ntfn \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace>
 2. \<And>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s \<Longrightarrow> \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> obj_at' (runnable' \<circ> tcbState) x s \<and> ?P'7 x s proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>?Q9 t\<rbrace> setObject ntfnptr ntfn \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace>
 2. \<And>t s. ?P'7 t s \<Longrightarrow> ?Q9 t s
 3. \<And>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s \<Longrightarrow> \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> obj_at' (runnable' \<circ> tcbState) x s \<and> ?P'7 x s proof (prove)
goal (3 subgoals):
 1. \<And>t prev_s. \<lbrace>?P12 t prev_s\<rbrace> setObject ntfnptr ntfn \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. ksCurDomain prev_s = tcbDomain tcb) t\<rbrace>
 2. \<And>t s. ?P'7 t s \<Longrightarrow> ?P12 t s s
 3. \<And>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s \<Longrightarrow> \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> obj_at' (runnable' \<circ> tcbState) x s \<and> ?P'7 x s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma setQueue_valid_inQ_queues:
  "\<lbrace>valid_inQ_queues
      and (\<lambda>s. \<forall>t \<in> set ts. obj_at' (inQ d p) t s)
      and K (distinct ts)\<rbrace>
  setQueue d p ts
  \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" apply (simp add: setQueue_def valid_inQ_queues_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues and (\<lambda>s. \<forall>t\<in>set ts. obj_at' (inQ d p) t s) and K (distinct ts)\<rbrace> setQueue d p ts \<lbrace>\<lambda>_. 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 (\<lambda>s. \<forall>t\<in>set ts. obj_at' (inQ d p) t s) and (\<lambda>y. distinct ts)\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := ts)\<rparr>) \<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))\<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 (\<lambda>s. \<forall>t\<in>set ts. obj_at' (inQ d p) t s) and (\<lambda>y. distinct ts)) s \<Longrightarrow> \<forall>da pa. (\<forall>t\<in>set (ksReadyQueues (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := ts)\<rparr>) (da, pa)). obj_at' (inQ da pa) t (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := ts)\<rparr>)) \<and> distinct (ksReadyQueues (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := ts)\<rparr>) (da, pa)) proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma rescheduleRequired_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" apply (simp add: rescheduleRequired_def) apply wpsimp done

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