theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_st_tcb_at':
  "\<lbrace>st_tcb_at' P t' and K (t \<noteq> t')\<rbrace>
     cancelIPC t
   \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def locateSlot_conv
                   capHasProperty_def isCap_simps) apply (wp sts_pred_tcb_neq' hoare_drop_imps delete_one_reply_st_tcb_at
       | wpc | clarsimp)+ apply (wp getCTE_wp | clarsimp)+ apply (wp hoare_vcg_ex_lift threadSet_cte_wp_at' hoare_vcg_imp_lift
                   cancelSignal_pred_tcb_at' sts_pred_tcb_neq' getEndpoint_wp gts_wp'
                   threadSet_pred_tcb_no_state
              | wpc | clarsimp)+ apply (auto simp: cte_wp_at_ctes_of isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t' and K (t \<noteq> 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' and (\<lambda>y. t \<noteq> 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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. delete 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;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE (t + 2 ^ cte_level_bits * tcbReplySlot));
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (cte_wp_at' (\<lambda>c. (\<exists>v0 v1 v2. cteCap c = capability.ReplyCap v0 v1 v2) \<and> \<not> capReplyMaster (cteCap c)) callerCap) [];
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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. delete t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<lbrace>?B91 Structures_H.thread_state.BlockedOnReply ()\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>(\<lambda>callerCap. if callerCap \<noteq> nullPointer then \<lambda>s. cte_wp_at' (\<lambda>c. (\<exists>v0 v1 v2. cteCap c = capability.ReplyCap v0 v1 v2) \<and> \<not> capReplyMaster (cteCap c)) callerCap s \<longrightarrow> st_tcb_at' P t' s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) callerCap s) else st_tcb_at' P t') \<circ> (mdbNext \<circ> cteMDBNode)\<rbrace>
 2. \<And>state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R26 state\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B91 state\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 5. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 6. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. delete t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 8. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> st_tcb_at' P t' s \<and> t' \<noteq> t) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R23 state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R14 state s)\<rbrace>
 10. \<And>s. (st_tcb_at' P t' and (\<lambda>y. t \<noteq> t')) s \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<lbrace>?R26 Structures_H.thread_state.BlockedOnReply\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>x xa. cte_wp_at' (\<lambda>_. True) (t + 2 ^ cte_level_bits * tcbReplySlot) xa \<longrightarrow> (\<exists>cte. (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) xa \<and> (cte_wp_at' (\<lambda>c. (\<exists>v0 v1 v2. cteCap c = capability.ReplyCap v0 v1 v2) \<and> \<not> capReplyMaster (cteCap c)) (mdbNext (cteMDBNode cte)) xa \<longrightarrow> st_tcb_at' P t' xa \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) (mdbNext (cteMDBNode cte)) xa))) \<and> (mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) xa \<and> st_tcb_at' P t' xa))\<rbrace>
 2. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R25 state x3\<rbrace> cancelSignal t (waitingOnNotification state) \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 3. \<And>state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 4. \<And>state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R22 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 5. \<And>state. idle' state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 6. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R20 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 delete t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. delete t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 7. \<And>state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R14 state\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>
 8. \<lbrace>?Q2\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> (st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> st_tcb_at' P t' s \<and> t' \<noteq> t) \<and> (awaiting_reply' state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R23 state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R22 state s) \<and> (idle' state \<longrightarrow> ?R21 state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R20 state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R14 state s)\<rbrace>
 9. \<And>s. (st_tcb_at' P t' and (\<lambda>y. t \<noteq> t')) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at' P t' s; t \<noteq> t'; st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t s; cte_wp_at' (\<lambda>a. True) (t + 2 ^ cte_level_bits * tcbReplySlot) s\<rbrakk> \<Longrightarrow> \<exists>x. (mdbNext (cteMDBNode x) \<noteq> nullPointer \<longrightarrow> cte_wp_at' ((=) x) (t + 2 ^ cte_level_bits * tcbReplySlot) s) \<and> (cte_wp_at' (\<lambda>a. (\<exists>v0 v1 v2. cteCap a = capability.ReplyCap v0 v1 v2) \<and> \<not> capReplyMaster (cteCap a)) (mdbNext (cteMDBNode x)) s \<longrightarrow> mdbNext (cteMDBNode x) = nullPointer \<or> (\<exists>xa xb. cte_wp_at' (\<lambda>a. cteCap a = capability.ReplyCap xa False xb) (mdbNext (cteMDBNode x)) s)) \<and> (mdbNext (cteMDBNode x) = nullPointer \<longrightarrow> cte_wp_at' ((=) x) (t + 2 ^ cte_level_bits * tcbReplySlot) s) proof (prove)
goal:
No subgoals!