theory Finalise_R

lemma cancelIPC_bound_tcb_at'[wp]:
  "\<lbrace>bound_tcb_at' P tptr\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>" apply (simp add: cancelIPC_def Let_def) apply (rule hoare_seq_ext[OF _ gts_sp']) apply (case_tac "state", simp_all) defer 2 apply (rule hoare_pre) apply ((wp sts_bound_tcb_at' getEndpoint_wp | wpc | simp)+)[8] apply (simp add: getThreadReplySlot_def locateSlot_conv liftM_def) apply (rule hoare_pre) apply (wp capDeleteOne_bound_tcb_at' getCTE_ctes_of) apply (rule_tac Q="\<lambda>_. bound_tcb_at' P tptr" in hoare_post_imp) apply (clarsimp simp: capHasProperty_def cte_wp_at_ctes_of) apply (wp threadSet_pred_tcb_no_state | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' P tptr\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' P tptr\<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>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at' (\<lambda>st. st = state) t and bound_tcb_at' P tptr\<rbrace> 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 () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnReceive x11 x12) t and bound_tcb_at' P tptr\<rbrace> do ep <- getEndpoint x11;
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 x11 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 2. \<lbrace>st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr\<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>rv. bound_tcb_at' P tptr\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnNotification x3) t and bound_tcb_at' P tptr\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 5. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 6. \<lbrace>st_tcb_at' idle' t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = 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 bound_tcb_at' P tptr\<rbrace> do ep <- getEndpoint x71;
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 x71 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 8. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnReceive x11 x12) t and bound_tcb_at' P tptr\<rbrace> do ep <- getEndpoint x11;
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 x11 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 2. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnNotification x3) t and bound_tcb_at' P tptr\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 3. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 5. \<lbrace>st_tcb_at' idle' t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 6. \<And>state x71 x72 x73 x74 x75. state = 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 bound_tcb_at' P tptr\<rbrace> do ep <- getEndpoint x71;
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 x71 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 7. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 8. \<lbrace>st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr\<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>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?Q7 state x11 x12\<rbrace> do ep <- getEndpoint x11;
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 x11 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 2. \<And>state x11 x12 s. \<lbrakk>state = Structures_H.thread_state.BlockedOnReceive x11 x12; (st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnReceive x11 x12) t and bound_tcb_at' P tptr) s\<rbrakk> \<Longrightarrow> ?Q7 state x11 x12 s
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnNotification x3) t and bound_tcb_at' P tptr\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 5. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 6. \<lbrace>st_tcb_at' idle' t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = 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 bound_tcb_at' P tptr\<rbrace> do ep <- getEndpoint x71;
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 x71 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 8. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and bound_tcb_at' P tptr\<rbrace> return () \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 9. \<lbrace>st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr\<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>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr\<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>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
x <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q97\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
x <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (mdbNext (cteMDBNode x) \<noteq> nullPointer) (do y <- stateAssert (capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne (mdbNext (cteMDBNode x))
od)
od \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>
 2. \<And>s. (st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr) s \<Longrightarrow> ?Q97 s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B101 y\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>x. if mdbNext (cteMDBNode x) \<noteq> nullPointer then \<lambda>s. capHasProperty (mdbNext (cteMDBNode x)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> (bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) (mdbNext (cteMDBNode x))) s else bound_tcb_at' P tptr\<rbrace>
 2. \<lbrace>?Q97\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B101\<rbrace>
 3. \<And>s. (st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr) s \<Longrightarrow> ?Q97 s proof (prove)
goal (4 subgoals):
 1. \<And>y rv s. bound_tcb_at' P tptr s \<Longrightarrow> (if mdbNext (cteMDBNode rv) \<noteq> nullPointer then \<lambda>s. capHasProperty (mdbNext (cteMDBNode rv)) (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap) s \<longrightarrow> (bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) (mdbNext (cteMDBNode rv))) s else bound_tcb_at' P tptr) s
 2. \<And>y. \<lbrace>?B101 y\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>_. bound_tcb_at' P tptr\<rbrace>
 3. \<lbrace>?Q97\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B101\<rbrace>
 4. \<And>s. (st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr) s \<Longrightarrow> ?Q97 s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B101 y\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>_. bound_tcb_at' P tptr\<rbrace>
 2. \<lbrace>?Q97\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B101\<rbrace>
 3. \<And>s. (st_tcb_at' awaiting_reply' t and bound_tcb_at' P tptr) s \<Longrightarrow> ?Q97 s proof (prove)
goal:
No subgoals!