theory Orphanage

lemma handleRecv_no_orphans [wp]:
notes if_cong[cong] shows
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   handleRecv isBlocking
   \<lbrace> \<lambda>rv . no_orphans \<rbrace>" unfolding handleRecv_def apply (clarsimp simp: whenE_def split del: if_split | wp hoare_drop_imps getNotification_wp | wpc )+  (*takes a while*)
      apply (rule_tac Q'="\<lambda>rv s. no_orphans s \<and> invs' s" in hoare_post_imp_R) apply (wp, fastforce) apply (rule_tac Q="\<lambda>rv s. no_orphans s \<and> invs' s" in hoare_post_imp) apply (wp | clarsimp | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> handleRecv isBlocking \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do thread <- getCurThread;
epCPtr <- asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister;
(capFaultOnFailure epCPtr True $ doE epCap <- lookupCap thread epCPtr;
case epCap of capability.NotificationCap ntfnPtr x xa True \<Rightarrow> doE ntfn <- withoutFailure $ getNotification ntfnPtr;
boundTCB <- returnOk $ ntfnBoundTCB ntfn;
if boundTCB = Just thread \<or> boundTCB = Nothing then withoutFailure $ receiveSignal thread epCap isBlocking else throw $ Fault_H.lookup_failure.MissingCapability 0
odE | capability.NotificationCap ntfnPtr x xa False \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap x xa xb True xc xd \<Rightarrow> withoutFailure $ do deleteCallerCap thread;
receiveIPC thread epCap isBlocking
od | capability.EndpointCap x xa xb False xc xd \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0
odE) `~catchFailure~` handleFault thread;
return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?P'460 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. (\<forall>x xa xb xc. rv = capability.NotificationCap x xa xb xc \<longrightarrow> (xc \<longrightarrow> ((\<exists>ntfn. ko_at' ntfn x s) \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> ((\<exists>ntfn. ko_at' ntfn x s) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (\<not> xc \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> ((\<exists>x. rv = capability.IRQHandlerCap x) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>x xa xb xc. (\<exists>xd xe. rv = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> (xc \<longrightarrow> no_orphans s \<and> invs' s) \<and> (\<not> xc \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (rv = capability.DomainCap \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb. rv = capability.Zombie x xa xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x. rv = capability.ArchObjectCap x) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb xc. rv = capability.UntypedCap x xa xb xc) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb xc. rv = capability.CNodeCap x xa xb xc) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (rv = capability.IRQControlCap \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>, -
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ?P'460 thread epCPtr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?P'460 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. (\<forall>x xa xb xc. rv = capability.NotificationCap x xa xb xc \<longrightarrow> (xc \<longrightarrow> ((\<exists>ntfn. ko_at' ntfn x s) \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> ((\<exists>ntfn. ko_at' ntfn x s) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (\<not> xc \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> ((\<exists>x. rv = capability.IRQHandlerCap x) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>x xa xb xc. (\<exists>xd xe. rv = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> (xc \<longrightarrow> no_orphans s \<and> invs' s) \<and> (\<not> xc \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (rv = capability.DomainCap \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb. rv = capability.Zombie x xa xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x. rv = capability.ArchObjectCap x) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb xc. rv = capability.UntypedCap x xa xb xc) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb xc. rv = capability.CNodeCap x xa xb xc) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (rv = capability.IRQControlCap \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>, -
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ?P'460 thread epCPtr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?P'460 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. no_orphans s \<and> invs' s\<rbrace>, -
 2. \<And>thread epCPtr rv s. no_orphans s \<and> invs' s \<Longrightarrow> (\<forall>x xa xb xc. rv = capability.NotificationCap x xa xb xc \<longrightarrow> (xc \<longrightarrow> ((\<exists>ntfn. ko_at' ntfn x s) \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> ((\<exists>ntfn. ko_at' ntfn x s) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (\<not> xc \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> ((\<exists>x. rv = capability.IRQHandlerCap x) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>x xa xb xc. (\<exists>xd xe. rv = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> (xc \<longrightarrow> no_orphans s \<and> invs' s) \<and> (\<not> xc \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (rv = capability.DomainCap \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb. rv = capability.Zombie x xa xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x. rv = capability.ArchObjectCap x) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb xc. rv = capability.UntypedCap x xa xb xc) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa xb xc. rv = capability.CNodeCap x xa xb xc) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (rv = capability.IRQControlCap \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)
 3. \<And>thread. \<lbrace>?B1 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ?P'460 thread epCPtr s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> no_orphans s \<and> invs' s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 3. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread rv s. no_orphans s \<and> invs' s \<Longrightarrow> no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> no_orphans s \<and> invs' s
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>rv s. no_orphans s \<and> invs' s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!