theory Orphanage

lemma handleReply_no_orphans [wp]:
  "\<lbrace>no_orphans and invs'\<rbrace> handleReply \<lbrace>\<lambda>_. no_orphans\<rbrace>" unfolding handleReply_def apply (rule hoare_pre) apply (wp hoare_drop_imps | wpc | clarsimp)+ apply (wp hoare_vcg_all_lift) apply (rule_tac Q="\<lambda>rv s. no_orphans s \<and> invs' s \<and> tcb_at' thread s \<and>
                                valid_cap' rv s" in hoare_post_imp) apply (wp hoare_drop_imps | clarsimp simp: valid_cap'_def
              | clarsimp simp: invs'_def cur_tcb'_def valid_state'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans and invs'\<rbrace> handleReply \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans and invs'\<rbrace> do thread <- getCurThread;
callerSlot <- getThreadCallerSlot thread;
callerCap <- getSlotCap callerSlot;
case callerCap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap caller True canGrant \<Rightarrow> haskell_fail [] | capability.ReplyCap caller False canGrant \<Rightarrow> do haskell_assert (caller \<noteq> thread) [];
doReplyTransfer thread caller callerSlot canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do thread <- getCurThread;
callerSlot <- getThreadCallerSlot thread;
callerCap <- getSlotCap callerSlot;
case callerCap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap caller True canGrant \<Rightarrow> haskell_fail [] | capability.ReplyCap caller False canGrant \<Rightarrow> do haskell_assert (caller \<noteq> thread) [];
doReplyTransfer thread caller callerSlot canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>_. no_orphans\<rbrace>
 2. \<And>s. (no_orphans and invs') s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread callerSlot. \<lbrace>?P'147 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>rv s. (\<forall>x xa. (\<exists>xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> (xa \<longrightarrow> no_orphans s) \<and> (\<not> xa \<longrightarrow> no_orphans s \<and> invs' s \<and> tcb_at' thread s \<and> tcb_at' x 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)\<rbrace>
 2. \<And>thread. \<lbrace>?B4 thread\<rbrace> getThreadCallerSlot thread \<lbrace>\<lambda>callerSlot s. no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> ?P'147 thread callerSlot s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 4. \<And>s. (no_orphans and invs') s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread callerSlot x xa. \<lbrace>?P154 thread callerSlot x xa\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>rv s. (\<exists>xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> (xa \<longrightarrow> no_orphans s) \<and> (\<not> xa \<longrightarrow> no_orphans s \<and> invs' s \<and> tcb_at' thread s \<and> tcb_at' x s)\<rbrace>
 2. \<And>thread callerSlot. \<lbrace>?P'152 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>rv s. ((\<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)\<rbrace>
 3. \<And>thread. \<lbrace>?B4 thread\<rbrace> getThreadCallerSlot thread \<lbrace>\<lambda>callerSlot s. no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> (\<forall>x xa. ?P154 thread callerSlot x xa s) \<and> ?P'152 thread callerSlot s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 5. \<And>s. (no_orphans and invs') s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>thread callerSlot x xa rv s. no_orphans s \<and> invs' s \<and> tcb_at' thread s \<and> valid_cap' rv s \<Longrightarrow> (\<exists>xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> (xa \<longrightarrow> no_orphans s) \<and> (\<not> xa \<longrightarrow> no_orphans s \<and> invs' s \<and> tcb_at' thread s \<and> tcb_at' x s)
 2. \<And>thread callerSlot x xa. \<lbrace>?P154 thread callerSlot x xa\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>rv s. no_orphans s \<and> invs' s \<and> tcb_at' thread s \<and> valid_cap' rv s\<rbrace>
 3. \<And>thread callerSlot. \<lbrace>?P'152 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>rv s. ((\<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)\<rbrace>
 4. \<And>thread. \<lbrace>?B4 thread\<rbrace> getThreadCallerSlot thread \<lbrace>\<lambda>callerSlot s. no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> no_orphans s \<and> (\<forall>x xa. ?P154 thread callerSlot x xa s) \<and> ?P'152 thread callerSlot s\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 6. \<And>s. (no_orphans and invs') s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!