theory DomainSepInv

lemma rec_del_domain_sep_inv':
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
         rec_del.simps[simp del]
  shows
  "s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace>
       rec_del call
       \<lbrace>\<lambda>rv s. (case call of (FinaliseSlotCall x y) \<Rightarrow> (y \<or> fst rv) \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap
                                                | _ \<Rightarrow> True) \<and>
               domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>,
       \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" proof (induct s arbitrary: rule: rec_del.induct, simp_all only: rec_del_fails hoare_fail_any) case (1 slot exposed s) show ?case apply (simp add: split_def rec_del.simps) apply (wpsimp wp: empty_slot_domain_sep_inv
                      drop_spec_validE[OF returnOk_wp]
                      drop_spec_validE[OF liftE_wp]) apply (rule spec_strengthen_postE[OF "1.hyps"]) apply fastforce done next case (2 slot exposed s) show ?case apply (simp add: rec_del.simps split del: if_split) apply (rule hoare_pre_spec_validE) apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv
            | simp add: split_def split del: if_split)+ apply (rule spec_strengthen_postE) apply (rule "2.hyps", fastforce+) apply (rule drop_spec_validE, (wp preemption_point_inv| simp)+)[1] apply simp apply (rule spec_strengthen_postE) apply (rule "2.hyps", fastforce+) apply (wp  finalise_cap_domain_sep_inv_cap get_cap_wp
                   finalise_cap_returns_NullCap
                   drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv
               |simp split del: if_split
               |wp (once) hoare_drop_imps)+ apply (blast dest: cte_wp_at_domain_sep_inv_cap) done next case (3 ptr bits n slot s) show ?case apply (simp add: rec_del.simps) apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp]) apply (rule hoare_pre_spec_validE) apply (wp drop_spec_validE[OF assertE_wp]) apply (fastforce) done next case (4 ptr bits n slot s) show ?case apply (simp add: rec_del.simps) apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv
              drop_spec_validE[OF assertE_wp] get_cap_wp | simp)+ apply (rule spec_strengthen_postE[OF "4.hyps"]) apply (simp add: returnOk_def return_def) apply (clarsimp simp: domain_sep_inv_cap_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del call \<lbrace>\<lambda>rv s. (case call of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> doE p <- rec_del (FinaliseSlotCall slot exposed);
y <- liftE (when (exposed \<or> fst p) (empty_slot slot (snd p)));
returnOk undefined
odE \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then \<lambda>b. domain_sep_inv irqs st b \<and> (\<not> irqs \<longrightarrow> snd a = NullCap) else domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s r. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst s \<longrightarrow> \<not> irqs \<longrightarrow> snd s = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st r \<Longrightarrow> (if exposed \<or> fst s then \<lambda>a. domain_sep_inv irqs st a \<and> (\<not> irqs \<longrightarrow> snd s = NullCap) else domain_sep_inv irqs st) r proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); ?rv \<noteq> NullCap; (Inr ?rva, ?sta) \<in> fst ((without_preemption $ is_final_cap ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((without_preemption $ finalise_cap ?rv ?rva) ?sta); \<not> cap_removeable (fst ?rvb) slot; \<not> (cap_cyclic_zombie (fst ?rvb) slot \<and> \<not> exposed); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) slot) ?stb)\<rbrakk> \<Longrightarrow> ?stc \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (fst ?rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); ?rv \<noteq> NullCap; (Inr ?rva, ?sta) \<in> fst ((without_preemption $ is_final_cap ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((without_preemption $ finalise_cap ?rv ?rva) ?sta); \<not> cap_removeable (fst ?rvb) slot; \<not> (cap_cyclic_zombie (fst ?rvb) slot \<and> \<not> exposed); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) slot) ?stb); (Inr ?rvd, ?std) \<in> fst (rec_del (ReduceZombieCall (fst ?rvb) slot exposed) ?stc); (Inr ?rve, ?ste) \<in> fst (preemption_point ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, stc) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) stb); (Inr rvd, std) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) stc); (Inr rve, ste) \<in> fst (preemption_point std)\<rbrakk> \<Longrightarrow> ste \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> doE cap <- liftE (get_cap slot);
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- liftE (is_final_cap cap);
(remainder, cleanup_info) <- liftE (finalise_cap cap is_final);
if cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> exposed then doE y <- liftE (set_cap remainder slot);
returnOk (False, NullCap)
odE else doE y <- liftE (set_cap remainder slot);
y <- rec_del (ReduceZombieCall remainder slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap) \<and> (fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'8\<rbrace> doE cap <- liftE (get_cap slot);
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- liftE (is_final_cap cap);
(remainder, cleanup_info) <- liftE (finalise_cap cap is_final);
if cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> exposed then doE y <- liftE (set_cap remainder slot);
returnOk (False, NullCap)
odE else doE y <- liftE (set_cap remainder slot);
y <- rec_del (ReduceZombieCall remainder slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap) \<and> (fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c); (Inr (), s''e) \<in> fst (preemption_point s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B56 rv s'' rva s''a rvb s''b () s''c rvd s''d ()\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap) \<and> (fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B55 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>?B56 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B54 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B55 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B54 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 8. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c); (Inr (), s''e) \<in> fst (preemption_point s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B56 rv s'' rva s''a rvb s''b () s''c rvd s''d ()\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q'58 rv s'' rva s''a rvb s''b s''c rvd s''d s''e\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e s r. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c); (Inr (), s''e) \<in> fst (preemption_point s''d); ?Q'58 rv s'' rva s''a rvb s''b s''c rvd s''d s''e s r\<rbrakk> \<Longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd s = NullCap) \<and> (fst s \<longrightarrow> \<not> irqs \<longrightarrow> snd s = NullCap) \<and> domain_sep_inv irqs st r
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B55 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>?B56 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B54 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B55 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B54 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 8. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 9. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B55 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>a. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B54 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B55 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B54 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst (liftE (set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B54 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. domain_sep_inv irqs st s \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B54 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B54 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B54 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B54 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?Q'125 rv s'' rva s''a rvb s''b s''c\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b s''c s r. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); ?Q'125 rv s'' rva s''a rvb s''b s''c s r\<rbrakk> \<Longrightarrow> domain_sep_inv irqs st r
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>?B54 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'35 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>\<lambda>a. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> liftE (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (fst (False, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (False, NullCap) = NullCap) \<and> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (fst rvb))) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'35 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'17 rv\<rbrace> liftE (is_final_cap rv) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. s \<turnstile> \<lbrace>?P'8\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> \<not> irqs \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv irqs st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'17 rv s)\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. domain_sep_inv irqs st s \<Longrightarrow> ?P'8 s proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> doE y <- assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (ptr, replicate (zombie_cte_bits bits) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'9\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. domain_sep_inv irqs st s \<Longrightarrow> ?P'9 s proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st s \<Longrightarrow> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv irqs st s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>rv s. (case CTEDeleteCall ?rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rva \<longrightarrow> \<not> irqs \<longrightarrow> snd rva = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> doE y <- rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False);
new_cap <- liftE (get_cap slot);
y <- if new_cap = Zombie ptr bits (Suc n) then liftE (set_cap (Zombie ptr bits n) slot) else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>rv s. \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> domain_sep_inv irqs st s \<and> domain_sep_inv_cap irqs (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st s) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv irqs st s))\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. (Inr (ptr, nat_to_cref (zombie_cte_bits bits) n), s) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s)
 2. \<And>s r. (case CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst s \<longrightarrow> \<not> irqs \<longrightarrow> snd s = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st r \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> domain_sep_inv irqs st r \<and> domain_sep_inv_cap irqs (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv irqs st r)) proof (prove)
goal (1 subgoal):
 1. \<And>s r. (case CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst s \<longrightarrow> \<not> irqs \<longrightarrow> snd s = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st r \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> domain_sep_inv irqs st r \<and> domain_sep_inv_cap irqs (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv irqs st r)) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> \<not> irqs \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>

goal:
No subgoals!