theory Orphanage

lemma finaliseSlot_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_to' slot s) \<rbrace>
    finaliseSlot slot e
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding finaliseSlot_def apply (rule validE_valid, rule hoare_pre,
    rule hoare_post_impErr, rule use_spec) apply (rule finaliseSlot_invs'[where p=slot and slot=slot and Pr=no_orphans]) apply (simp_all add: no_orphans_finalise_prop_stuff) apply (wp | simp)+ apply (auto dest: cte_wp_at_valid_objs_valid_cap') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot' slot e \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?Q2\<rbrace> finaliseSlot' slot e \<lbrace>?Q5\<rbrace>, \<lbrace>?E5\<rbrace>
 2. \<And>rv s. ?Q5 rv s \<Longrightarrow> no_orphans s
 3. \<And>e s. ?E5 e s \<Longrightarrow> no_orphans s
 4. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>s cap final sl. \<lbrace>no_cte_prop no_orphans and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap final False \<lbrace>\<lambda>rv. no_cte_prop no_orphans\<rbrace>
 2. \<And>s. finalise_prop_stuff no_orphans
 3. \<And>rv s. no_cte_prop no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (e \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P17 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P17 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<Longrightarrow> no_orphans s
 4. \<And>e s. no_cte_prop no_orphans s \<and> invs' s \<and> sch_act_simple s \<Longrightarrow> no_orphans s
 5. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> no_cte_prop no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (e \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (e \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P17 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P17 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) proof (prove)
goal (2 subgoals):
 1. \<And>cap final sl. \<lbrace>no_orphans and invs' and sch_act_simple and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap final False \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> e \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal (2 subgoals):
 1. \<And>cap sl s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s \<Longrightarrow> valid_cap' cap s
 2. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<Longrightarrow> e \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal:
No subgoals!