theory Orphanage

lemma sendFaultIPC_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<rbrace>
   sendFaultIPC tptr fault
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding sendFaultIPC_def apply (rule hoare_pre) apply (wp threadSet_valid_queues' threadSet_no_orphans threadSet_valid_objs'
             threadSet_sch_act | wpc | clarsimp)+ apply (rule_tac Q'="\<lambda>handlerCap s. no_orphans s \<and> valid_queues' s
                                         \<and> valid_objs' s
                                         \<and> sch_act_wf (ksSchedulerAction s) s"
             in hoare_post_imp_R) apply (wp | clarsimp simp: 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 \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> sendFaultIPC tptr fault \<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 \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> doE handlerCPtr <- withoutFailure $ threadGet tcbFaultHandler tptr;
handlerCap <- capFaultOnFailure handlerCPtr False $ lookupCap tptr handlerCPtr;
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just fault)) tptr;
sendIPC True True (capEPBadge handlerCap) canGrant True tptr (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE handlerCPtr <- withoutFailure $ threadGet tcbFaultHandler tptr;
handlerCap <- capFaultOnFailure handlerCPtr False $ lookupCap tptr handlerCPtr;
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just fault)) tptr;
sendIPC True True (capEPBadge handlerCap) canGrant True tptr (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>handlerCPtr. \<lbrace>?P'360 handlerCPtr\<rbrace> lookupCap tptr handlerCPtr \<lbrace>\<lambda>handlerCap s. ((\<exists>x. handlerCap = capability.ThreadCap x) \<longrightarrow> no_orphans s) \<and> (handlerCap = capability.NullCap \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc. handlerCap = capability.NotificationCap x xa xb xc) \<longrightarrow> no_orphans s) \<and> ((\<exists>x. handlerCap = capability.IRQHandlerCap x) \<longrightarrow> no_orphans s) \<and> (\<forall>x xa xb xc xd xe. handlerCap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xb \<longrightarrow> (xd \<longrightarrow> no_orphans s \<and> (\<forall>ko qdom prio. ko_at' ko tptr s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. Some fault) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (xe \<longrightarrow> no_orphans s \<and> (\<forall>ko qdom prio. ko_at' ko tptr s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. Some fault) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> xd \<and> \<not> xe \<longrightarrow> no_orphans s)) \<and> (\<not> xb \<longrightarrow> no_orphans s)) \<and> (handlerCap = capability.DomainCap \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb. handlerCap = capability.Zombie x xa xb) \<longrightarrow> no_orphans s) \<and> ((\<exists>x. handlerCap = capability.ArchObjectCap x) \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb. handlerCap = capability.ReplyCap x xa xb) \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc. handlerCap = capability.UntypedCap x xa xb xc) \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc. handlerCap = capability.CNodeCap x xa xb xc) \<longrightarrow> no_orphans s) \<and> (handlerCap = capability.IRQControlCap \<longrightarrow> no_orphans s)\<rbrace>, -
 2. \<lbrace>?Q\<rbrace> withoutFailure $ threadGet tcbFaultHandler tptr \<lbrace>\<lambda>handlerCPtr s. (no_orphans s \<and> True) \<and> ?P'360 handlerCPtr s\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>handlerCPtr. \<lbrace>?P'360 handlerCPtr\<rbrace> lookupCap tptr handlerCPtr \<lbrace>\<lambda>handlerCap s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>, -
 2. \<And>handlerCPtr rv s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ((\<exists>x. rv = capability.ThreadCap x) \<longrightarrow> no_orphans s) \<and> (rv = capability.NullCap \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc. rv = capability.NotificationCap x xa xb xc) \<longrightarrow> no_orphans s) \<and> ((\<exists>x. rv = capability.IRQHandlerCap x) \<longrightarrow> no_orphans s) \<and> (\<forall>x xa xb xc xd xe. rv = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xb \<longrightarrow> (xd \<longrightarrow> no_orphans s \<and> (\<forall>ko qdom prio. ko_at' ko tptr s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. Some fault) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (xe \<longrightarrow> no_orphans s \<and> (\<forall>ko qdom prio. ko_at' ko tptr s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. Some fault) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> xd \<and> \<not> xe \<longrightarrow> no_orphans s)) \<and> (\<not> xb \<longrightarrow> no_orphans s)) \<and> (rv = capability.DomainCap \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb. rv = capability.Zombie x xa xb) \<longrightarrow> no_orphans s) \<and> ((\<exists>x. rv = capability.ArchObjectCap x) \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc. rv = capability.UntypedCap x xa xb xc) \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc. rv = capability.CNodeCap x xa xb xc) \<longrightarrow> no_orphans s) \<and> (rv = capability.IRQControlCap \<longrightarrow> no_orphans s)
 3. \<lbrace>?Q\<rbrace> withoutFailure $ threadGet tcbFaultHandler tptr \<lbrace>\<lambda>handlerCPtr s. (no_orphans s \<and> True) \<and> ?P'360 handlerCPtr s\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!