theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_tcb_at_runnable':
  "\<lbrace>st_tcb_at' runnable' t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") apply (clarsimp simp: cancelIPC_def Let_def) apply (case_tac "t'=t") apply (rule_tac B="\<lambda>st. st_tcb_at' runnable' t and K (runnable' st)"
            in hoare_seq_ext) apply(case_tac x; simp) apply (wpsimp wp: sts_pred_tcb_neq')+ apply (rule_tac Q="\<lambda>rv. ?PRE" in hoare_post_imp, fastforce) apply (wp cteDeleteOne_tcb_at_runnable'
                    threadSet_pred_tcb_no_state
                    cancelSignal_tcb_at_runnable'
                    sts_pred_tcb_neq' hoare_drop_imps
                  | wpc | simp add: o_def if_fun_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' t'\<rbrace> cancelIPC t \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' 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>_. st_tcb_at' runnable' t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t' = t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' 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>_. st_tcb_at' runnable' t'\<rbrace>
 2. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' 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>_. st_tcb_at' runnable' t'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. t' = t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' t and K (runnable' x)\<rbrace> case x of Structures_H.thread_state.BlockedOnReceive xa xaa \<Rightarrow> do ep <- getEndpoint (blockingObject 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 (blockingObject 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 <- 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 xa \<Rightarrow> cancelSignal t (waitingOnNotification x) | Structures_H.thread_state.BlockedOnSend xa xaa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject 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 (blockingObject x) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 2. t' = t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' t'\<rbrace> getThreadState t \<lbrace>\<lambda>st. st_tcb_at' runnable' t and K (runnable' st)\<rbrace>
 3. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' 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>_. st_tcb_at' runnable' t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t' = t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' t'\<rbrace> getThreadState t \<lbrace>\<lambda>st. st_tcb_at' runnable' t and K (runnable' st)\<rbrace>
 2. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at' runnable' 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>_. st_tcb_at' runnable' t'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x11 x12. t' \<noteq> t \<Longrightarrow> \<lbrace>?R62 (Structures_H.thread_state.BlockedOnReceive x11 x12) x11 x12\<rbrace> getEndpoint x11 \<lbrace>\<lambda>ep s. \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (epQueue ep) = [] \<longrightarrow> st_tcb_at' runnable' t' s) \<and> ((\<exists>x xa. remove1 t (epQueue ep) = x # xa) \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 2. \<And>state. \<lbrakk>t' \<noteq> t; awaiting_reply' state\<rbrakk> \<Longrightarrow> \<lbrace>?R59 state\<rbrace> 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 \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 3. \<And>state x3. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> \<lbrace>?R58 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 4. \<And>state. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R56 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 5. \<And>state. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> \<lbrace>?R55 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 6. \<And>state. \<lbrakk>t' \<noteq> t; idle' state\<rbrakk> \<Longrightarrow> \<lbrace>?R54 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> \<lbrace>?R53 state x71 x72 x73 x74 x75\<rbrace> 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 \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 8. \<And>state. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> \<lbrace>?R47 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 9. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q35\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R62 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R59 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R58 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R56 state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R55 state s) \<and> (idle' state \<longrightarrow> ?R54 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R53 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R47 state s)\<rbrace>
 10. \<And>s. \<lbrakk>t' \<noteq> t; st_tcb_at' runnable' t' s\<rbrakk> \<Longrightarrow> ?Q35 s proof (prove)
goal (10 subgoals):
 1. \<And>x11 x12. t' \<noteq> t \<Longrightarrow> \<lbrace>?R62 (Structures_H.thread_state.BlockedOnReceive x11 x12) x11 x12\<rbrace> getEndpoint x11 \<lbrace>\<lambda>rv. st_tcb_at' runnable' t'\<rbrace>
 2. \<And>state. \<lbrakk>t' \<noteq> t; awaiting_reply' state\<rbrakk> \<Longrightarrow> \<lbrace>?R59 state\<rbrace> 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 \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 3. \<And>state x3. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> \<lbrace>?R58 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 4. \<And>state. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R56 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 5. \<And>state. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> \<lbrace>?R55 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 6. \<And>state. \<lbrakk>t' \<noteq> t; idle' state\<rbrakk> \<Longrightarrow> \<lbrace>?R54 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> \<lbrace>?R53 state x71 x72 x73 x74 x75\<rbrace> 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 \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 8. \<And>state. \<lbrakk>t' \<noteq> t; state = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> \<lbrace>?R47 state\<rbrace> return () \<lbrace>\<lambda>_. st_tcb_at' runnable' t'\<rbrace>
 9. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q35\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R62 state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R59 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R58 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R56 state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R55 state s) \<and> (idle' state \<longrightarrow> ?R54 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R53 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R47 state s)\<rbrace>
 10. \<And>s. \<lbrakk>t' \<noteq> t; st_tcb_at' runnable' t' s\<rbrakk> \<Longrightarrow> ?Q35 s proof (prove)
goal:
No subgoals!