theory IpcCancel_R

lemma (in delete_one_conc_pre) cancelIPC_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
   cancelIPC t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def
             cong: Structures_H.thread_state.case_cong list.case_cong) apply (rule hoare_seq_ext [OF _ gts_sp']) apply (rule hoare_pre) apply (wpc
           | wp hoare_vcg_conj_lift delete_one_queues threadSet_valid_queues
                threadSet_valid_objs' sts_valid_queues setEndpoint_ksQ
                hoare_vcg_all_lift threadSet_sch_act threadSet_weak_sch_act_wf
           | simp add: o_def if_apply_def2 inQ_def
           | rule hoare_drop_imps
           | clarsimp simp: valid_tcb'_def tcb_cte_cases_def
                     elim!: pred_tcb'_weakenE)+ apply (fastforce dest: valid_queues_not_runnable'_not_ksQ elim: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> getThreadState t >>= Structures_H.thread_state.case_thread_state (\<lambda>x xa. do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od) (do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od) (cancelSignal t) (return ()) (return ()) (return ()) (\<lambda>x xa xb xc xd. do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od) (return ()) \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>st_tcb_at' (\<lambda>st. st = x) t and (Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))\<rbrace> case x of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t x | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?Q14 x\<rbrace> case x of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t x | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint x;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>
 2. \<And>x s. (st_tcb_at' (\<lambda>st. st = x) t and (Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))) s \<Longrightarrow> ?Q14 x s proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>st_tcb_at' (\<lambda>st. st = x) t s; Invariants_H.valid_queues s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> ((\<exists>xa xb. x = Structures_H.thread_state.BlockedOnReceive xa xb) \<longrightarrow> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (awaiting_reply' x \<longrightarrow> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> runnable' (tcbState tcb) \<and> (tcbPriority tcb = p \<longrightarrow> tcbQueued tcb \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> runnable' (tcbState tcb) \<and> (tcbPriority tcb = p \<longrightarrow> tcbQueued tcb \<longrightarrow> \<not> runnable' (tcbState tcb))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) \<and> ((\<exists>xa. x = Structures_H.thread_state.BlockedOnNotification xa) \<longrightarrow> st_tcb_at' (\<lambda>x. \<not> runnable' x) t s) \<and> ((\<exists>xa xb xc xd xe. x = Structures_H.thread_state.BlockedOnSend xa xb xc xd xe) \<longrightarrow> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) proof (prove)
goal:
No subgoals!