theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_st_tcb_at:
  assumes x[simp]: "\<And>st. simple' st \<longrightarrow> P st" shows
  "\<lbrace>st_tcb_at' P t\<rbrace>
     cancelIPC t'
   \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def
             cong: if_cong Structures_H.thread_state.case_cong) apply (rule hoare_seq_ext [OF _ gts_sp']) apply (case_tac x, simp_all add: isTS_defs list_case_If) apply (wp sts_st_tcb_at'_cases delete_one_st_tcb_at
                   threadSet_pred_tcb_no_state
                   cancelSignal_st_tcb_at hoare_drop_imps
                | clarsimp simp: o_def if_fun_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> cancelIPC t' \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> getThreadState t' >>= Structures_H.thread_state.case_thread_state (\<lambda>x xa. do ep <- getEndpoint x;
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 x ep';
setThreadState Structures_H.thread_state.Inactive t'
od) (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) (cancelSignal t') (return ()) (return ()) (return ()) (\<lambda>x xa xb xc xd. do ep <- getEndpoint x;
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 x ep';
setThreadState Structures_H.thread_state.Inactive t'
od) (return ()) \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>st_tcb_at' (\<lambda>st. st = x) t' and st_tcb_at' P t\<rbrace> case x of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint x;
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 x 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' x | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint x;
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 x ep';
setThreadState Structures_H.thread_state.Inactive t'
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x x11 x12. x = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnReceive x11 x12) t' and st_tcb_at' P t\<rbrace> do ep <- getEndpoint x11;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- if remove1 t' (epQueue ep) = [] then return Structures_H.endpoint.IdleEP else return $ epQueue_update (\<lambda>_. remove1 t' (epQueue ep)) ep;
y <- setEndpoint x11 ep';
setThreadState Structures_H.thread_state.Inactive t'
od \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 2. \<lbrace>st_tcb_at' awaiting_reply' t' and st_tcb_at' P t\<rbrace> 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 \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 3. \<And>x x3. x = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnNotification x3) t' and st_tcb_at' P t\<rbrace> cancelSignal t' x3 \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t' and st_tcb_at' P t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 5. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t' and st_tcb_at' P t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 6. \<lbrace>st_tcb_at' idle' t' and st_tcb_at' P t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 7. \<And>x x71 x72 x73 x74 x75. x = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75) t' and st_tcb_at' P t\<rbrace> do ep <- getEndpoint x71;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- if remove1 t' (epQueue ep) = [] then return Structures_H.endpoint.IdleEP else return $ epQueue_update (\<lambda>_. remove1 t' (epQueue ep)) ep;
y <- setEndpoint x71 ep';
setThreadState Structures_H.thread_state.Inactive t'
od \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>
 8. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t' and st_tcb_at' P t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal:
No subgoals!