theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_simple[wp]:
  "\<lbrace>\<top>\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def
             cong: Structures_H.thread_state.case_cong list.case_cong) apply (rule hoare_seq_ext [OF _ gts_sp']) apply (rule hoare_pre) apply (wpc
           | wp sts_st_tcb_at'_cases hoare_vcg_conj_lift
                hoare_vcg_const_imp_lift delete_one_st_tcb_at
                threadSet_pred_tcb_no_state
                hoare_strengthen_post [OF cancelSignal_simple]
           | simp add: o_def if_fun_split
           | rule hoare_drop_imps
           | clarsimp elim!: pred_tcb'_weakenE)+ apply (auto simp: pred_tcb_at'
             elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) 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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od) (return ()) \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>st_tcb_at' (\<lambda>st. st = x) t and (\<lambda>_. True)\<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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) 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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?Q14 x\<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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) 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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 2. \<And>x s. (st_tcb_at' (\<lambda>st. st = x) t and (\<lambda>_. True)) s \<Longrightarrow> ?Q14 x s proof (prove)
goal (1 subgoal):
 1. \<And>x s. st_tcb_at' (\<lambda>st. st = x) t s \<Longrightarrow> ((\<exists>xa xb. x = Structures_H.thread_state.BlockedOnReceive xa xb) \<longrightarrow> tcb_at' t s) \<and> (awaiting_reply' x \<longrightarrow> st_tcb_at' simple' t s) \<and> (x = Structures_H.thread_state.Running \<longrightarrow> st_tcb_at' simple' t s) \<and> (x = Structures_H.thread_state.Inactive \<longrightarrow> st_tcb_at' simple' t s) \<and> (idle' x \<longrightarrow> st_tcb_at' simple' t s) \<and> ((\<exists>xa xb xc xd xe. x = Structures_H.thread_state.BlockedOnSend xa xb xc xd xe) \<longrightarrow> tcb_at' t s) \<and> (x = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' simple' t s) proof (prove)
goal:
No subgoals!