theory IpcCancel_R

lemma (in delete_one) cancel_ipc_corres:
  "corres dc (einvs and tcb_at t) (invs' and tcb_at' t)
      (cancel_ipc t) (cancelIPC t)" apply (simp add: cancel_ipc_def cancelIPC_def Let_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getThreadState_corres]) apply (rule_tac P="einvs and st_tcb_at ((=) state) t" and
                      P'="invs' and st_tcb_at' ((=) statea) t" in corres_inst) apply (case_tac state, simp_all add: isTS_defs list_case_If)[1] apply (rule corres_guard_imp) apply (rule blocked_cancelIPC_corres) apply fastforce apply fastforce apply simp apply simp apply (clarsimp simp add: isTS_defs list_case_If) apply (rule corres_guard_imp) apply (rule blocked_cancelIPC_corres) apply fastforce apply fastforce apply simp apply simp apply (rule corres_guard_imp) apply (rule cancelIPC_ReplyCap_corres) apply (clarsimp elim!: st_tcb_weakenE) apply (clarsimp elim!: pred_tcb'_weakenE) apply (rule corres_guard_imp [OF cancelSignal_corres], simp+) apply (wp gts_sp[where P="\<top>",simplified])+ apply (rule hoare_strengthen_post) apply (rule gts_sp'[where P="\<top>"]) apply (clarsimp elim!: pred_tcb'_weakenE) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (cancel_ipc t) (cancelIPC t) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do state <- get_thread_state t;
case state of Structures_A.thread_state.BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnReply \<Rightarrow> reply_cancel_ipc t | Structures_A.thread_state.BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od) (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) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q2 ?Q'2 (do state <- get_thread_state t;
case state of Structures_A.thread_state.BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnReply \<Rightarrow> reply_cancel_ipc t | Structures_A.thread_state.BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od) (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)
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> ?Q2 s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R6 state) (?R'6 statea) (case state of Structures_A.thread_state.BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnReply \<Rightarrow> reply_cancel_ipc t | Structures_A.thread_state.BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()) (case statea of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject statea);
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 statea) 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 statea) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject statea);
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 statea) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ())
 2. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>?R'6\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) state) t) (invs' and st_tcb_at' ((=) statea) t) (case state of Structures_A.thread_state.BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | Structures_A.thread_state.BlockedOnReply \<Rightarrow> reply_cancel_ipc t | Structures_A.thread_state.BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()) (case statea of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject statea);
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 statea) 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 statea) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject statea);
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 statea) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ())
 2. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>state statea x41 x42. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnReceive x41 x42) t) (do ep <- getEndpoint x41;
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 x41 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 3. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 4. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 5. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 7. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 8. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>state statea x41 x42. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> corres dc (?Q15 state statea x41 x42) (?Q'15 state statea x41 x42) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnReceive x41 x42) t) (do ep <- getEndpoint x41;
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 x41 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s\<rbrakk> \<Longrightarrow> ?Q15 state statea x41 x42 s
 3. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42))) t) s\<rbrakk> \<Longrightarrow> ?Q'15 state statea x41 x42 s
 4. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 5. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 6. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 7. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 9. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (11 subgoals):
 1. \<And>state statea x41 x42. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> Structures_A.thread_state.BlockedOnReceive x41 x42 = Structures_A.thread_state.BlockedOnReceive x41 (?p'19 state statea x41 x42) \<or> Structures_A.thread_state.BlockedOnReceive x41 x42 = Structures_A.thread_state.BlockedOnSend x41 (?p19 state statea x41 x42)
 2. \<And>state statea x41 x42. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> thread_state_relation (Structures_A.thread_state.BlockedOnReceive x41 x42) (?st'19 state statea x41 x42)
 3. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s\<rbrakk> \<Longrightarrow> (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s
 4. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42))) t) s\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' ((=) (?st'19 state statea x41 x42)) t) s
 5. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 6. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 7. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 8. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state statea x41 x42. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> thread_state_relation (Structures_A.thread_state.BlockedOnReceive x41 x42) (?st'19 state statea x41 x42)
 2. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s\<rbrakk> \<Longrightarrow> (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s
 3. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42))) t) s\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' ((=) (?st'19 state statea x41 x42)) t) s
 4. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 5. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 6. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 7. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 9. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s\<rbrakk> \<Longrightarrow> (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnReceive x41 x42)) t) s
 2. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42))) t) s\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' ((=) statea) t) s
 3. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 4. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 5. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 6. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 8. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 9. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>state statea x41 x42 s. \<lbrakk>statea = Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42); state = Structures_A.thread_state.BlockedOnReceive x41 x42; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x41 (receiver_can_grant x42))) t) s\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' ((=) statea) t) s
 2. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 3. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 4. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 5. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 7. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 8. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>state statea x51 x52. \<lbrakk>statea = Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52); state = Structures_A.thread_state.BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 2. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 3. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 4. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>x51 x52. corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 2. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 3. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 4. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>x51 x52. corres dc (?Q41 x51 x52) (?Q'41 x51 x52) (blocked_cancel_ipc (Structures_A.thread_state.BlockedOnSend x51 x52) t) (do ep <- getEndpoint x51;
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 x51 ep';
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>x51 x52 s. (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s \<Longrightarrow> ?Q41 x51 x52 s
 3. \<And>x51 x52 s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s \<Longrightarrow> ?Q'41 x51 x52 s
 4. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 5. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 6. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 8. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 9. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>x51 x52. Structures_A.thread_state.BlockedOnSend x51 x52 = Structures_A.thread_state.BlockedOnReceive x51 (?p'45 x51 x52) \<or> Structures_A.thread_state.BlockedOnSend x51 x52 = Structures_A.thread_state.BlockedOnSend x51 (?p45 x51 x52)
 2. \<And>x51 x52. thread_state_relation (Structures_A.thread_state.BlockedOnSend x51 x52) (?st'45 x51 x52)
 3. \<And>x51 x52 s. (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s \<Longrightarrow> (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s
 4. \<And>x51 x52 s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s \<Longrightarrow> (invs' and st_tcb_at' ((=) (?st'45 x51 x52)) t) s
 5. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 6. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 7. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 9. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>x51 x52. thread_state_relation (Structures_A.thread_state.BlockedOnSend x51 x52) (?st'45 x51 x52)
 2. \<And>x51 x52 s. (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s \<Longrightarrow> (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s
 3. \<And>x51 x52 s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s \<Longrightarrow> (invs' and st_tcb_at' ((=) (?st'45 x51 x52)) t) s
 4. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 5. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 6. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 8. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 9. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>x51 x52 s. (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s \<Longrightarrow> (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnSend x51 x52)) t) s
 2. \<And>x51 x52 s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s \<Longrightarrow> (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s
 3. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 4. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 5. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 7. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 8. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>x51 x52 s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s \<Longrightarrow> (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x51 (sender_badge x52) (sender_can_grant x52) (sender_can_grant_reply x52) (sender_is_call x52))) t) s
 2. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 3. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 4. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. corres dc (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) (reply_cancel_ipc t) (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)
 2. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 3. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. corres dc ?Q59 ?Q'59 (reply_cancel_ipc t) (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)
 2. \<And>s. (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) s \<Longrightarrow> ?Q59 s
 3. \<And>s. (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) s \<Longrightarrow> ?Q'59 s
 4. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 5. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 7. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 8. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>s. (einvs and st_tcb_at ((=) Structures_A.thread_state.BlockedOnReply) t) s \<Longrightarrow> (einvs and st_tcb_at awaiting_reply t) s
 2. \<And>s. (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) s \<Longrightarrow> (invs' and st_tcb_at' awaiting_reply' t) s
 3. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 4. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>s. (invs' and st_tcb_at' ((=) Structures_H.thread_state.BlockedOnReply) t) s \<Longrightarrow> (invs' and st_tcb_at' awaiting_reply' t) s
 2. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 3. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>state statea x7. \<lbrakk>statea = Structures_H.thread_state.BlockedOnNotification x7; state = Structures_A.thread_state.BlockedOnNotification x7\<rbrakk> \<Longrightarrow> corres dc (einvs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification x7)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification x7)) t) (cancel_signal t x7) (cancelSignal t x7)
 2. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and st_tcb_at ((=) state) t\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> getThreadState t \<lbrace>\<lambda>statea. invs' and st_tcb_at' ((=) statea) t\<rbrace>
 3. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q6) s
 4. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'90\<rbrace> getThreadState t \<lbrace>\<lambda>rv. st_tcb_at' ((=) rv) t\<rbrace>
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and (\<lambda>s. einvs s \<and> True)) s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. invs' s \<and> ?P'90 s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'90\<rbrace> getThreadState t \<lbrace>?Q93\<rbrace>
 2. \<And>rv s. ?Q93 rv s \<Longrightarrow> st_tcb_at' ((=) rv) t s
 3. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and (\<lambda>s. einvs s \<and> True)) s
 4. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. invs' s \<and> ?P'90 s)) s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>_. True)) s \<Longrightarrow> st_tcb_at' ((=) rv) t s
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and (\<lambda>s. einvs s \<and> True)) s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. invs' s \<and> True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and (\<lambda>s. einvs s \<and> True)) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. invs' s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. invs' s \<and> True)) s proof (prove)
goal:
No subgoals!