theory Orphanage

lemma receiveIPC_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   receiveIPC thread cap is_blocking
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding receiveIPC_def apply (rule hoare_pre) apply (wp setThreadState_not_active_no_orphans hoare_drop_imps
             hoare_vcg_all_lift sts_st_tcb'
          | wpc
          | clarsimp simp: is_active_thread_state_def isRunning_def isRestart_def
                           doNBRecvFailedTransfer_def invs_valid_queues'
          | strengthen sch_act_wf_weak)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> receiveIPC thread cap is_blocking \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> let cap = cap in if isEndpointCap cap then do epptr <- return (capEPPtr cap);
recvCanGrant <- return (capEPCanGrant cap);
ep <- getEndpoint epptr;
ntfnPtr <- getBoundNotification thread;
ntfn <- maybe (return $ NTFN Structures_H.ntfn.IdleNtfn Nothing) getNotification ntfnPtr;
if isJust ntfnPtr \<and> EndpointDecls_H.isActive ntfn then completeSignal (fromJust ntfnPtr) thread else case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive epptr recvCanGrant) thread;
setEndpoint epptr $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive epptr recvCanGrant) thread;
setEndpoint epptr $ Structures_H.endpoint.RecvEP [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.SendEP [] \<Rightarrow> haskell_fail [] | Structures_H.endpoint.SendEP (sender # queue) \<Rightarrow> do setEndpoint epptr $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP queue;
senderState <- getThreadState sender;
haskell_assert (isSend senderState) [];
badge <- return (blockingIPCBadge senderState);
canGrant <- return (blockingIPCCanGrant senderState);
canGrantReply <- return (blockingIPCCanGrantReply senderState);
doIPCTransfer sender (Just epptr) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread recvCanGrant | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive sender | (False, xa) \<Rightarrow> do setThreadState Structures_H.thread_state.Running sender;
possibleSwitchTo sender
od
od
od else haskell_fail [] \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> let cap = cap in if isEndpointCap cap then do epptr <- return (capEPPtr cap);
recvCanGrant <- return (capEPCanGrant cap);
ep <- getEndpoint epptr;
ntfnPtr <- getBoundNotification thread;
ntfn <- maybe (return $ NTFN Structures_H.ntfn.IdleNtfn Nothing) getNotification ntfnPtr;
if isJust ntfnPtr \<and> EndpointDecls_H.isActive ntfn then completeSignal (fromJust ntfnPtr) thread else case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive epptr recvCanGrant) thread;
setEndpoint epptr $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive epptr recvCanGrant) thread;
setEndpoint epptr $ Structures_H.endpoint.RecvEP [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.SendEP [] \<Rightarrow> haskell_fail [] | Structures_H.endpoint.SendEP (sender # queue) \<Rightarrow> do setEndpoint epptr $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP queue;
senderState <- getThreadState sender;
haskell_assert (isSend senderState) [];
badge <- return (blockingIPCBadge senderState);
canGrant <- return (blockingIPCCanGrant senderState);
canGrantReply <- return (blockingIPCCanGrantReply senderState);
doIPCTransfer sender (Just epptr) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread recvCanGrant | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive sender | (False, xa) \<Rightarrow> do setThreadState Structures_H.thread_state.Running sender;
possibleSwitchTo sender
od
od
od else haskell_fail [] \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!