theory Orphanage

lemma cancelIPC_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<rbrace>
   cancelIPC t
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding cancelIPC_def Let_def apply (rule hoare_pre) apply (wp setThreadState_not_active_no_orphans hoare_drop_imps weak_if_wp
             threadSet_valid_queues' threadSet_valid_objs' threadSet_no_orphans | wpc
          | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def
                           inQ_def valid_tcb'_def tcb_cte_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do epptr <- return (blockingObject state);
ep <- getEndpoint epptr;
haskell_assert (Not $ case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) [];
queue' <- return (delete t $ epQueue ep);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. queue') ep;
setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do threadSet (tcbFault_update (\<lambda>_. Nothing)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) $ getCTE slot;
when (callerCap \<noteq> nullPointer) $ do 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 epptr <- return (blockingObject state);
ep <- getEndpoint epptr;
haskell_assert (Not $ case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) [];
queue' <- return (delete t $ epQueue ep);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. queue') ep;
setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do epptr <- return (blockingObject state);
ep <- getEndpoint epptr;
haskell_assert (Not $ case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) [];
queue' <- return (delete t $ epQueue ep);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. queue') ep;
setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do threadSet (tcbFault_update (\<lambda>_. Nothing)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) $ getCTE slot;
when (callerCap \<noteq> nullPointer) $ do 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 epptr <- return (blockingObject state);
ep <- getEndpoint epptr;
haskell_assert (Not $ case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) [];
queue' <- return (delete t $ epQueue ep);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. queue') ep;
setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!