theory Finalise_AC

lemma rec_del_preserves_cte_zombie_null:
  assumes P_Null: "P (NullCap)"
  assumes P_Zombie: "\<And>word x y. P (Zombie word x y)"
  shows
    "s \<turnstile> \<lbrace>\<lambda>s. ((slot_rdcall call \<noteq> p \<or> exposed_rdcall call) \<longrightarrow> cte_wp_at P p s) \<and>
              (case call of ReduceZombieCall remove slot _ \<Rightarrow> cte_wp_at ((=) remove) slot s
                                                       | _ \<Rightarrow> True)\<rbrace>
         rec_del call
         \<lbrace>\<lambda>_ s :: det_ext state. (slot_rdcall call \<noteq> p \<or> exposed_rdcall call) \<longrightarrow> cte_wp_at P p s\<rbrace>,
         \<lbrace>\<lambda>_. \<top>\<rbrace>" proof (induct rule: rec_del.induct, simp_all only: rec_del_fails) case (1 slot exposed s) show ?case apply (insert P_Null) apply (subst rec_del.simps) apply (simp only: split_def) apply (wp hoare_weak_lift_imp | simp)+ apply (wp empty_slot_cte_wp_at)[1] apply (rule spec_strengthen_postE) apply (rule hoare_pre_spec_validE) apply (rule "1.hyps") apply simp apply clarsimp done next case (2 slot exposed s) show ?case apply (insert P_Null) apply (subst rec_del.simps) apply (simp only: split_def without_preemption_def
                      rec_del_call.simps) apply (wp hoare_weak_lift_imp) apply (wp set_cap_cte_wp_at')[1] apply (wp "2.hyps"[simplified without_preemption_def rec_del_call.simps]) apply ((wp preemption_point_inv | simp)+)[1] apply simp apply (rule "2.hyps"[simplified exposed_rdcall.simps slot_rdcall.simps
                                        simp_thms disj_not1], simp_all)[1] apply (simp add: cte_wp_at_caps_of_state) apply wp+ apply (rule_tac Q = "\<lambda>rv' s. (slot \<noteq> p \<or> exposed \<longrightarrow> cte_wp_at P p s) \<and> P (fst rv')
                             \<and> cte_at slot s" in hoare_post_imp) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (wp hoare_weak_lift_imp set_cap_cte_wp_at' finalise_cap_cte_wp_at_nullinv
                finalise_cap_fst_ret get_cap_wp
             | simp add: is_final_cap_def)+ apply (clarsimp simp add: P_Zombie is_cap_simps cte_wp_at_caps_of_state)+ done next case 3 show ?case apply (simp add: cte_wp_at_caps_of_state) apply wp+ apply clarsimp apply (simp add: P_Zombie is_cap_simps) done next case (4 ptr bits n slot s) show ?case apply (subst rec_del.simps) apply wp apply (simp add: cte_wp_at_caps_of_state) apply wp+ apply simp apply (wp get_cap_wp)[1] apply (rule spec_strengthen_postE) apply (rule spec_valid_conj_liftE1) apply (rule rec_del_delete_cases) apply (rule "4.hyps", assumption+) apply simp apply (clarsimp simp: cte_wp_at_caps_of_state) apply (auto simp: is_cap_simps P_Zombie P_Null)[1] apply wp+ apply (clarsimp simp: cte_wp_at_caps_of_state P_Zombie is_cap_simps) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall call \<noteq> p \<or> exposed_rdcall call \<longrightarrow> cte_wp_at P p s) \<and> (case call of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del call \<lbrace>\<lambda>_ s. slot_rdcall call \<noteq> p \<or> exposed_rdcall call \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<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>\<lambda>s. (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<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>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<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>\<lambda>s. (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<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>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> doE p <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> fst p) $ empty_slot slot (snd p);
returnOk undefined
odE \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((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) s); exposed \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 rv\<rbrace> empty_slot slot (snd rv) \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>
 2. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. True \<and> True \<and> (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> (if exposed \<or> fst rv then ?Q35 rv else cte_wp_at P p) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. True \<and> True \<and> (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> (if exposed \<or> fst rv then \<lambda>a. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p a) else cte_wp_at P p) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q'47\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s r. \<lbrakk>P NullCap; ?Q'47 s r\<rbrakk> \<Longrightarrow> True \<and> True \<and> (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> (if exposed \<or> fst s then \<lambda>a. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p a) else cte_wp_at P p) r) proof (prove)
goal (3 subgoals):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>?P'50\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q'47\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>P NullCap; (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> ?P'50 s
 3. \<And>s r. \<lbrakk>P NullCap; ?Q'47 s r\<rbrakk> \<Longrightarrow> True \<and> True \<and> (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> (if exposed \<or> fst s then \<lambda>a. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p a) else cte_wp_at P p) r) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P NullCap; (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)
 2. \<And>s r. \<lbrakk>P NullCap; slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p r\<rbrakk> \<Longrightarrow> True \<and> True \<and> (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> (if exposed \<or> fst s then \<lambda>a. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p a) else cte_wp_at P p) r) proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>P NullCap; slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p r\<rbrakk> \<Longrightarrow> True \<and> True \<and> (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> (if exposed \<or> fst s then \<lambda>a. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p a) else cte_wp_at P p) r) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall slot exposed) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<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>\<lambda>s. (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<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>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<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>\<lambda>s. (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<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>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<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>\<lambda>s. (slot_rdcall (ReduceZombieCall (fst ?rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst ?rvb) slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (fst ?rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (fst ?rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst ?rvb) slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<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>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv st rva sta rvb stb rvc stc. \<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>\<lambda>s. (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (fst rvb) slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv st rva sta rvb stb rvc stc rvd std rve ste. \<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>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> doE cap <- without_preemption $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
(remainder, cleanup_info) <- without_preemption $ 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 without_preemption $ set_cap remainder slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> doE cap <- liftE $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- liftE $ is_final_cap cap;
p <- liftE $ finalise_cap cap is_final;
if cap_removeable (fst p) slot then returnOk (True, snd p) else if cap_cyclic_zombie (fst p) slot \<and> \<not> exposed then doE liftE $ set_cap (fst p) slot;
returnOk (False, NullCap)
odE else doE liftE $ set_cap (fst p) slot;
rec_del (ReduceZombieCall (fst p) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P'68 rv s'' rva s''a rvb\<rbrace> set_cap (fst rvb) slot \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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'40 rv s'' rva s''a rvb\<rbrace> doE liftE $ set_cap (fst rvb) slot;
rec_del (ReduceZombieCall (fst rvb) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> ?P'68 rv s'' rva s''a rvb s)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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'40 rv s'' rva s''a rvb\<rbrace> doE liftE $ set_cap (fst rvb) slot;
rec_del (ReduceZombieCall (fst rvb) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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>?B75 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>rve s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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>?B73 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B75 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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'40 rv s'' rva s''a rvb\<rbrace> liftE $ set_cap (fst rvb) slot \<lbrace>?B73 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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>?B73 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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'40 rv s'' rva s''a rvb\<rbrace> liftE $ set_cap (fst rvb) slot \<lbrace>?B73 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c. \<lbrakk>P NullCap; (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>?B73 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. (slot = p \<longrightarrow> exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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'40 rv s'' rva s''a rvb\<rbrace> liftE $ set_cap (fst rvb) slot \<lbrace>?B73 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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''); (Inr rvb, s''b) \<in> fst ((liftE $ 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'40 rv s'' rva s''a rvb\<rbrace> liftE $ set_cap (fst rvb) slot \<lbrace>\<lambda>a b. ((slot = p \<longrightarrow> exposed) \<longrightarrow> cte_wp_at P p b) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot b | _ \<Rightarrow> True)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>P NullCap; (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\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'40 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>\<lambda>a b. ((slot = p \<longrightarrow> exposed) \<longrightarrow> (\<exists>cap. caps_of_state b p = Some cap \<and> P cap)) \<and> caps_of_state b slot = Some (fst rvb)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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>?B18 rv s'' rva\<rbrace> liftE $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'40 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>?B18 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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> \<lbrace>?P'127 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> True \<and> ((slot = p \<longrightarrow> exposed) \<longrightarrow> (\<exists>cap. ((caps_of_state s)(slot \<mapsto> fst rvb)) p = Some cap \<and> P cap)) \<and> ((caps_of_state s)(slot \<mapsto> fst rvb)) slot = Some (fst rvb)))\<rbrace>
 2. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'127 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb s. \<lbrakk>P NullCap; (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''); (slot \<noteq> p \<or> exposed \<longrightarrow> cte_wp_at P p s) \<and> P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> (if p = slot then P (fst rvb) \<and> cte_wp_at (\<lambda>_. True) slot s else cte_wp_at P p s))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> True \<and> ((slot = p \<longrightarrow> exposed) \<longrightarrow> (\<exists>cap. ((caps_of_state s)(slot \<mapsto> fst rvb)) p = Some cap \<and> P cap)) \<and> ((caps_of_state s)(slot \<mapsto> fst rvb)) slot = Some (fst rvb)))
 2. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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> \<lbrace>?P'127 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rv' s. (slot \<noteq> p \<or> exposed \<longrightarrow> cte_wp_at P p s) \<and> P (fst rv') \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrace>
 3. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'127 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>P NullCap; (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> \<lbrace>?P'127 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rv' s. (slot \<noteq> p \<or> exposed \<longrightarrow> cte_wp_at P p s) \<and> P (fst rv') \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrace>
 2. \<And>rv s''. \<lbrakk>P NullCap; (Inr rv, s'') \<in> fst ((liftE $ get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'6 rv\<rbrace> liftE $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'127 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. P NullCap \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> True\<rbrace> liftE $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'6 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P NullCap; (slot = p \<longrightarrow> exposed) \<longrightarrow> cte_wp_at P p s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<forall>a b c. P (Zombie a b c)) \<and> cte_wp_at (\<lambda>a. True) slot s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. slot_rdcall (FinaliseSlotCall slot exposed) \<noteq> p \<or> exposed_rdcall (FinaliseSlotCall slot exposed) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>\<lambda>s. (slot_ \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)) \<and> caps_of_state s slot_ = Some (Zombie ptr_ bits_ (Suc n_))\<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>_ s. slot_ \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (slot_ \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)) \<and> caps_of_state s slot_ = Some (Zombie ptr_ bits_ (Suc n_)) \<Longrightarrow> (ptr_, replicate (zombie_cte_bits bits_) False) \<noteq> slot_ \<longrightarrow> True \<and> True \<and> (slot_ \<noteq> p \<longrightarrow> (\<exists>cap. (caps_of_state s \<circ> id((ptr_, replicate (zombie_cte_bits bits_) False) := slot_, slot_ := (ptr_, replicate (zombie_cte_bits bits_) False))) p = Some cap \<and> P cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>caps_of_state s slot_ = Some (Zombie ptr_ bits_ (Suc n_)); p = (ptr_, replicate (zombie_cte_bits bits_) False); (ptr_, replicate (zombie_cte_bits bits_) False) \<noteq> slot_; caps_of_state s (ptr_, replicate (zombie_cte_bits bits_) False) = Some cap; P cap\<rbrakk> \<Longrightarrow> P (Zombie ptr_ bits_ (Suc n_)) proof (prove)
goal:
No subgoals! proof (state)
this:
s_ \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall ?rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall ?rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall ?rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall ?rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall ?rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> st \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_ s. slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> doE end_slot <- returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n);
rec_del (CTEDeleteCall end_slot False);
new_cap <- without_preemption $ get_cap slot;
if new_cap = Zombie ptr bits (Suc n) then without_preemption $ 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> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ get_cap slot) s''a); rvb = Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption (set_cap (Zombie ptr bits n) slot) \<lbrace>\<lambda>rv s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ get_cap slot) s''a); rvb \<noteq> Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'16 rv s'' rva s''a rvb\<rbrace> assertE (rvb = NullCap \<or> is_zombie rvb \<and> first_cslot_of rvb = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot) \<lbrace>\<lambda>rvc s. True \<and> (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B1 rv s'' rva\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rvb s. (rvb = Zombie ptr bits (Suc n) \<longrightarrow> True \<and> True \<and> ?P'25 rv s'' rva s''a rvb s) \<and> (rvb \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> ?P'16 rv s'' rva s''a rvb s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?B1 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst ((doE (success, cleanup_info) <- rec_del (FinaliseSlotCall rv False);
y <- liftE (when success (empty_slot rv cleanup_info));
returnOk undefined
odE) s''); (Zombie ptr bits (Suc n), s''b) \<in> fst (get_cap slot s''a); rvb = Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 rv s'' rva s''a (Zombie ptr bits (Suc n))\<rbrace> liftE (set_cap (Zombie ptr bits n) slot) \<lbrace>\<lambda>rv s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ get_cap slot) s''a); rvb \<noteq> Zombie ptr bits (Suc n)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'16 rv s'' rva s''a rvb\<rbrace> assertE (rvb = NullCap \<or> is_zombie rvb \<and> first_cslot_of rvb = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot) \<lbrace>\<lambda>rvc s. True \<and> (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B1 rv s'' rva\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rvb s. (rvb = Zombie ptr bits (Suc n) \<longrightarrow> True \<and> True \<and> ?P'25 rv s'' rva s''a rvb s) \<and> (rvb \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> ?P'16 rv s'' rva s''a rvb s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?B1 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 rv s'' rva\<rbrace> without_preemption (get_cap slot) \<lbrace>\<lambda>rvb s. (rvb = Zombie ptr bits (Suc n) \<longrightarrow> True \<and> True \<and> (\<exists>cap. ((caps_of_state s)(slot \<mapsto> Zombie ptr bits n)) p = Some cap \<and> P cap)) \<and> (rvb \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> rvb = NullCap \<or> is_zombie rvb \<and> first_cslot_of rvb = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot \<longrightarrow> True \<and> (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s))\<rbrace>, -
 2. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. True \<and> ?P'49 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (Inr rva, s''a) \<in> fst ((doE (success, cleanup_info) <- rec_del (FinaliseSlotCall rv False);
y <- liftE (when success (empty_slot rv cleanup_info));
returnOk undefined
odE) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 rv s'' rva\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rvb s. (p = slot \<longrightarrow> (rvb = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (rvb \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (rvb = NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (is_zombie rvb \<and> first_cslot_of rvb = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot s))) \<and> (p \<noteq> slot \<longrightarrow> (rvb = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)) \<and> (rvb \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (rvb = NullCap \<longrightarrow> cte_wp_at P p s) \<and> (is_zombie rvb \<and> first_cslot_of rvb = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p s)))\<rbrace>, -
 2. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. True \<and> ?P'49 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P slot s) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot s))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P p s) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p s))))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?Q'74 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' s r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); ?Q'74 rv s'' s r\<rbrakk> \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P slot r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot r))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P p r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p r))))
 3. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> \<lbrace>?P78 rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?Q77 rv s''\<rbrace>, -
 2. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'79 rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?Q'77 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' s r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); ?Q77 rv s'' s r \<and> ?Q'77 rv s'' s r\<rbrakk> \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P slot r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot r))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P p r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p r))))
 4. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. ?P78 rv s \<and> ?P'79 rv s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'79 rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?Q'77 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' s r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> False \<and> is_zombie c \<and> rv \<in> fst_cte_ptrs c) rv r \<and> ?Q'77 rv s'' s r\<rbrakk> \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P slot r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot r))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P p r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p r))))
 3. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. True \<and> ?P'79 rv s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s'' s r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> False \<and> is_zombie c \<and> rv \<in> fst_cte_ptrs c) rv r \<and> (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p r)\<rbrakk> \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P slot r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot r))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P p r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p r))))
 2. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. True \<and> (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s'' r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); cte_wp_at (\<lambda>c. c = NullCap \<or> is_zombie c \<and> rv \<in> fst_cte_ptrs c) rv r \<and> (rv \<noteq> p \<longrightarrow> cte_wp_at P p r)\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P slot r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P slot r))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> cte_wp_at P p r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at P p r)))
 2. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. True \<and> (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b s'' r cap capa. \<lbrakk>(Inr (a, b), s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s); (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap); caps_of_state r (a, b) = Some capa; capa = NullCap \<or> is_zombie capa \<and> (a, b) \<in> fst_cte_ptrs capa; caps_of_state r slot = Some cap\<rbrakk> \<Longrightarrow> (p = slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> P (Zombie ptr bits n)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> P NullCap) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> P cap))) \<and> (p \<noteq> slot \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap)) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> (\<exists>cap. caps_of_state r p = Some cap \<and> P cap))))
 2. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. True \<and> (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) \<lbrace>\<lambda>rv s. True \<and> (slot_rdcall (CTEDeleteCall rv False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall rv False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True) \<Longrightarrow> (slot_rdcall (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<noteq> p \<or> exposed_rdcall (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<longrightarrow> cte_wp_at P p s) \<and> (case CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall remove slot x \<Rightarrow> cte_wp_at ((=) remove) slot s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_ s. slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<noteq> p \<or> exposed_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<longrightarrow> cte_wp_at P p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal:
No subgoals!