theory Ipc_R

lemma cancelIPC_valid_queues'[wp]:
  "\<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) \<rbrace> cancelIPC t \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def locateSlot_conv liftM_def) apply (rule hoare_seq_ext[OF _ gts_sp']) apply (case_tac state, simp_all) defer 2 apply (rule hoare_pre) apply ((wp getEndpoint_wp getCTE_wp | wpc | simp)+)[8] apply (wp cteDeleteOne_valid_queues') apply (rule_tac Q="\<lambda>_. valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (clarsimp simp: capHasProperty_def cte_wp_at_ctes_of) apply (wp threadSet_valid_queues' threadSet_sch_act| simp)+ apply (clarsimp simp: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<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;
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 | 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. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at' (\<lambda>st. st = state) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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;
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 | 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. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<rbrace>
 2. \<lbrace>st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 5. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 6. \<lbrace>st_tcb_at' idle' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<rbrace>
 8. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 3. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 5. \<lbrace>st_tcb_at' idle' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<rbrace>
 7. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 8. \<lbrace>st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<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. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))) 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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 5. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 6. \<lbrace>st_tcb_at' idle' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<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 (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<rbrace>
 8. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<rbrace> return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 9. \<lbrace>st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))\<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. valid_queues'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B98 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> (valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s else valid_queues'\<rbrace>
 2. \<lbrace>?Q97\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B98\<rbrace>
 3. \<And>s. (st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))) s \<Longrightarrow> ?Q97 s proof (prove)
goal (4 subgoals):
 1. \<And>y rv s. (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) 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> (valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s else valid_queues') s
 2. \<And>y. \<lbrace>?B98 y\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>_. valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<lbrace>?Q97\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B98\<rbrace>
 4. \<And>s. (st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))) s \<Longrightarrow> ?Q97 s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B98 y\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>_. valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<lbrace>?Q97\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>?B98\<rbrace>
 3. \<And>s. (st_tcb_at' awaiting_reply' t and (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s))) s \<Longrightarrow> ?Q97 s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' awaiting_reply' t s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> \<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. None) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)) proof (prove)
goal:
No subgoals!