theory Orphanage

lemma performInvocation_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_invocation' i s \<and> ct_active' s \<and> sch_act_simple s \<rbrace>
   performInvocation block call i
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (simp add: performInvocation_def
              cong: invocation.case_cong) apply (rule hoare_pre) apply (wp | wpc | clarsimp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_invocation' i s \<and> ct_active' s \<and> sch_act_simple s\<rbrace> global.performInvocation block call i \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_invocation' i s \<and> ct_active' s \<and> sch_act_simple s\<rbrace> case i of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC block call badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case i of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC block call badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> valid_invocation' i s \<and> ct_active' s \<and> sch_act_simple s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; valid_invocation' i s; ct_active' s; sch_act_simple s\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x s) \<and> ((\<exists>x xa xb xc. i = Invocations_H.invocation.InvokeEndpoint x xa xb xc) \<longrightarrow> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ((\<exists>x xa. i = Invocations_H.invocation.InvokeNotification x xa) \<longrightarrow> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>x. (\<exists>xa xb. i = Invocations_H.invocation.InvokeReply x xa xb) \<longrightarrow> tcb_at' (ksCurThread s) s \<and> tcb_at' x s) \<and> ((\<exists>x xa. i = Invocations_H.invocation.InvokeDomain x xa) \<longrightarrow> Invariants_H.valid_queues s \<and> valid_queues' s \<and> cur_tcb' s) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> tcb_inv_wf' x s) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x s) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x s) proof (prove)
goal:
No subgoals!