theory Fastpath_Equiv

lemma receiveIPC_simple_rewrite:
  "monadic_rewrite True False
     ((\<lambda>_. isEndpointCap ep_cap \<and> \<not> isSendEP ep) and (ko_at' ep (capEPPtr ep_cap) and
      (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> isActive) ntfnptr s)))
     (receiveIPC thread ep_cap True)
     (do
       setThreadState (BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
       setEndpoint (capEPPtr ep_cap) (RecvEP (case ep of RecvEP q \<Rightarrow> (q @ [thread]) | _ \<Rightarrow> [thread]))
      od)" supply empty_fail_getEndpoint[wp] apply (rule monadic_rewrite_gen_asm) apply (simp add: receiveIPC_def) apply (monadic_rewrite_symb_exec_l_known ep) apply monadic_rewrite_symb_exec_l+ apply (monadic_rewrite_l monadic_rewrite_if_l_False) apply (rule monadic_rewrite_is_refl) apply (cases ep; simp add: isSendEP_def) apply (wpsimp wp: getNotification_wp gbn_wp' getEndpoint_wp
                    simp: getBoundNotification_def)+ apply (clarsimp simp: obj_at'_def projectKOs pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False ((\<lambda>_. isEndpointCap ep_cap \<and> \<not> isSendEP ep) and (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s))) (receiveIPC thread ep_cap True) (do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False ((\<lambda>_. isEndpointCap ep_cap \<and> \<not> isSendEP ep) and (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s))) (receiveIPC thread ep_cap True) (do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od) proof (prove)
goal (1 subgoal):
 1. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> monadic_rewrite True False (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) (receiveIPC thread ep_cap True) (do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od) proof (prove)
goal (1 subgoal):
 1. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> monadic_rewrite True False (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) (do ep <- getEndpoint (capEPPtr ep_cap);
ntfnPtr <- getBoundNotification thread;
ntfn <- case ntfnPtr of None \<Rightarrow> return (NTFN Structures_H.ntfn.IdleNtfn None) | Some x2 \<Rightarrow> getNotification x2;
if (\<exists>y. ntfnPtr = Some y) \<and> EndpointDecls_H.isActive ntfn then completeSignal (the ntfnPtr) thread else case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap)) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread (capEPCanGrant ep_cap) | (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) (do y <- setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od) proof (prove)
goal (3 subgoals):
 1. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> monadic_rewrite True False ?Q21 (do ntfnPtr <- getBoundNotification thread;
ntfn <- case ntfnPtr of None \<Rightarrow> return (NTFN Structures_H.ntfn.IdleNtfn None) | Some x2 \<Rightarrow> getNotification x2;
if (\<exists>y. ntfnPtr = Some y) \<and> EndpointDecls_H.isActive ntfn then completeSignal (the ntfnPtr) thread else case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap)) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread (capEPCanGrant ep_cap) | (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) (do y <- setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od)
 2. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?P21\<rbrace> getEndpoint (capEPPtr ep_cap) \<lbrace>\<lambda>rv' _. rv' = ep\<rbrace>
 3. \<And>s. \<lbrakk>isEndpointCap ep_cap \<and> \<not> isSendEP ep; (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) s\<rbrakk> \<Longrightarrow> (?P21 and ?Q21) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr ntfn. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> monadic_rewrite True False (?Q67 ntfnPtr ntfn) (if (\<exists>y. ntfnPtr = Some y) \<and> EndpointDecls_H.isActive ntfn then completeSignal (the ntfnPtr) thread else case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap)) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread (capEPCanGrant ep_cap) | (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) (do y <- setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od)
 2. \<And>ntfnPtr. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q46 ntfnPtr\<rbrace> case ntfnPtr of None \<Rightarrow> return (NTFN Structures_H.ntfn.IdleNtfn None) | Some x2 \<Rightarrow> getNotification x2 \<lbrace>?Q67 ntfnPtr\<rbrace>
 3. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> empty_fail (getBoundNotification thread)
 4. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q21\<rbrace> getBoundNotification thread \<lbrace>?Q46\<rbrace>
 5. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?P21\<rbrace> getEndpoint (capEPPtr ep_cap) \<lbrace>\<lambda>rv' _. rv' = ep\<rbrace>
 6. \<And>s. \<lbrakk>isEndpointCap ep_cap \<and> \<not> isSendEP ep; (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) s\<rbrakk> \<Longrightarrow> (?P21 and ?Q21) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr ntfn. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> monadic_rewrite True False (?Q120 ntfnPtr ntfn) (case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap)) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread (capEPCanGrant ep_cap) | (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) (do y <- setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od)
 2. \<And>ntfnPtr. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q46 ntfnPtr\<rbrace> case ntfnPtr of None \<Rightarrow> return (NTFN Structures_H.ntfn.IdleNtfn None) | Some x2 \<Rightarrow> getNotification x2 \<lbrace>\<lambda>ntfn. (\<lambda>_. \<not> ((\<exists>y. ntfnPtr = Some y) \<and> EndpointDecls_H.isActive ntfn)) and (\<lambda>_. True) and ?Q120 ntfnPtr ntfn\<rbrace>
 3. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> empty_fail (getBoundNotification thread)
 4. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q21\<rbrace> getBoundNotification thread \<lbrace>?Q46\<rbrace>
 5. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?P21\<rbrace> getEndpoint (capEPPtr ep_cap) \<lbrace>\<lambda>rv' _. rv' = ep\<rbrace>
 6. \<And>s. \<lbrakk>isEndpointCap ep_cap \<and> \<not> isSendEP ep; (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) s\<rbrakk> \<Longrightarrow> (?P21 and ?Q21) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr ntfn. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> (case ep of Structures_H.endpoint.RecvEP queue \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ Structures_H.endpoint.RecvEP $ queue @ [thread]
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.endpoint.IdleEP \<Rightarrow> case True of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap) $ 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 (capEPPtr ep_cap)) badge canGrant thread;
call <- return (blockingIPCIsCall senderState);
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap sender thread (capEPCanGrant ep_cap) | (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) = do y <- setThreadState (Structures_H.thread_state.BlockedOnReceive (capEPPtr ep_cap) (capEPCanGrant ep_cap)) thread;
setEndpoint (capEPPtr ep_cap) (Structures_H.endpoint.RecvEP (case ep of Structures_H.endpoint.RecvEP q \<Rightarrow> q @ [thread] | _ \<Rightarrow> [thread]))
od
 2. \<And>ntfnPtr. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q46 ntfnPtr\<rbrace> case ntfnPtr of None \<Rightarrow> return (NTFN Structures_H.ntfn.IdleNtfn None) | Some x2 \<Rightarrow> getNotification x2 \<lbrace>\<lambda>ntfn. (\<lambda>_. \<not> ((\<exists>y. ntfnPtr = Some y) \<and> EndpointDecls_H.isActive ntfn)) and (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> empty_fail (getBoundNotification thread)
 4. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q21\<rbrace> getBoundNotification thread \<lbrace>?Q46\<rbrace>
 5. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?P21\<rbrace> getEndpoint (capEPPtr ep_cap) \<lbrace>\<lambda>rv' _. rv' = ep\<rbrace>
 6. \<And>s. \<lbrakk>isEndpointCap ep_cap \<and> \<not> isSendEP ep; (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) s\<rbrakk> \<Longrightarrow> (?P21 and ?Q21) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q46 ntfnPtr\<rbrace> case ntfnPtr of None \<Rightarrow> return (NTFN Structures_H.ntfn.IdleNtfn None) | Some x2 \<Rightarrow> getNotification x2 \<lbrace>\<lambda>ntfn. (\<lambda>_. \<not> ((\<exists>y. ntfnPtr = Some y) \<and> EndpointDecls_H.isActive ntfn)) and (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 2. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> empty_fail (getBoundNotification thread)
 3. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?Q21\<rbrace> getBoundNotification thread \<lbrace>?Q46\<rbrace>
 4. isEndpointCap ep_cap \<and> \<not> isSendEP ep \<Longrightarrow> \<lbrace>?P21\<rbrace> getEndpoint (capEPPtr ep_cap) \<lbrace>\<lambda>rv' _. rv' = ep\<rbrace>
 5. \<And>s. \<lbrakk>isEndpointCap ep_cap \<and> \<not> isSendEP ep; (ko_at' ep (capEPPtr ep_cap) and (\<lambda>s. \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s)) s\<rbrakk> \<Longrightarrow> (?P21 and ?Q21) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>isEndpointCap ep_cap; \<not> isSendEP ep; ko_at' ep (capEPPtr ep_cap) s; \<forall>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<longrightarrow> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s\<rbrakk> \<Longrightarrow> (\<forall>epa. ko_at' epa (capEPPtr ep_cap) s \<longrightarrow> epa = ep) \<and> (\<forall>ntfn. bound_tcb_at' ((=) ntfn) thread s \<longrightarrow> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> \<not> EndpointDecls_H.isActive ntfn))) proof (prove)
goal:
No subgoals!