theory Orphanage

lemma invokeCNode_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_cnode_inv' cinv s \<and> sch_act_simple s \<rbrace>
   invokeCNode cinv
   \<lbrace> \<lambda>rv. no_orphans \<rbrace>" unfolding invokeCNode_def apply (rule hoare_pre) apply (wp hoare_drop_imps unless_wp | wpc | clarsimp split del: if_split)+ apply (simp add: invs_valid_queues') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_cnode_inv' cinv s \<and> sch_act_simple s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_cnode_inv' cinv s \<and> sch_act_simple s\<rbrace> case cinv of Insert cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteInsert cap srcSlot destSlot | Rotate cap1 cap2 slot1 slot2 slot3 \<Rightarrow> withoutPreemption $ if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od | Revoke destSlot \<Rightarrow> cteRevoke destSlot | Move cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteMove cap srcSlot destSlot | CancelBadgedSends (capability.EndpointCap ptr b xa xaa xb xc) \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | CancelBadgedSends _ \<Rightarrow> haskell_fail [] | SaveCaller destSlot \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od | Delete destSlot \<Rightarrow> cteDelete destSlot True \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case cinv of Insert cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteInsert cap srcSlot destSlot | Rotate cap1 cap2 slot1 slot2 slot3 \<Rightarrow> withoutPreemption $ if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od | Revoke destSlot \<Rightarrow> cteRevoke destSlot | Move cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteMove cap srcSlot destSlot | CancelBadgedSends (capability.EndpointCap ptr b xa xaa xb xc) \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | CancelBadgedSends _ \<Rightarrow> haskell_fail [] | SaveCaller destSlot \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od | Delete destSlot \<Rightarrow> cteDelete destSlot True \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> valid_cnode_inv' cinv s \<and> sch_act_simple s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s xa xb xc xd xe xf. \<lbrakk>no_orphans s; invs' s; sch_act_simple s; cinv = CancelBadgedSends (capability.EndpointCap xa xb xc xd xe xf); valid_cap' (capability.EndpointCap xa xb xc xd xe xf) s; hasCancelSendRights (capability.EndpointCap xa xb xc xd xe xf)\<rbrakk> \<Longrightarrow> (if xb = 0 then no_orphans else (\<lambda>a. no_orphans a \<and> valid_queues' a)) s proof (prove)
goal:
No subgoals!