theory BCorres2_AI

lemma rec_del_s_bcorres[wp]:
notes rec_del.simps[simp del]
shows
"s_bcorres (rec_del c) (rec_del c) s" proof (induct s rule: rec_del.induct, simp_all only: fail_s_bcorres_underlying rec_del_simps_ext(5-)) case (1 slot exposed s) show ?case apply (simp add: rec_del.simps) apply wp apply (simp split: prod.splits  | intro impI conjI allI)+ apply (wp drop_sbcorres_underlying)[1] apply (wp "1") done next case (2 slot exposed s) show ?case apply (simp add: rec_del.simps) apply (wp "2" | wpc | simp split: prod.splits | intro impI conjI allI | (rule ssubst[rotated, where s="fst x" for x], rule "2",simp+) | wp (once) drop_sbcorres_underlying)+ done next case (3 slot exposed s) show ?case apply (simp add: rec_del.simps) apply (wp | wp (once) drop_sbcorres_underlying)+ done next case (4 slot exposed s) show ?case apply (simp add: rec_del.simps) apply (simp add: in_monad | wp "4" | intro impI conjI | wp (once) drop_sbcorres_underlying)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres (rec_del c) (rec_del c) s proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s \<Longrightarrow> s_bcorres (rec_del (CTEDeleteCall slot exposed)) (rec_del (CTEDeleteCall slot exposed)) s
 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> s_bcorres (rec_del (ReduceZombieCall (fst rvb) slot exposed)) (rec_del (ReduceZombieCall (fst rvb) slot exposed)) stc; \<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> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s
 3. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (state)
this:
s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s

goal (4 subgoals):
 1. \<And>slot exposed s. s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s \<Longrightarrow> s_bcorres (rec_del (CTEDeleteCall slot exposed)) (rec_del (CTEDeleteCall slot exposed)) s
 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> s_bcorres (rec_del (ReduceZombieCall (fst rvb) slot exposed)) (rec_del (ReduceZombieCall (fst rvb) slot exposed)) stc; \<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> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s
 3. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (rec_del (CTEDeleteCall slot exposed)) (rec_del (CTEDeleteCall slot exposed)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
y <- liftE (when (exposed \<or> success) (empty_slot slot cleanup_info));
returnOk undefined
odE) (doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
y <- liftE (when (exposed \<or> success) (empty_slot slot cleanup_info));
returnOk undefined
odE) s proof (prove)
goal (2 subgoals):
 1. \<And>r s'. (Inr r, s') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s) \<Longrightarrow> s_bcorres (case r of (success, cleanup_info) \<Rightarrow> doE y <- liftE (when (exposed \<or> success) (empty_slot slot cleanup_info));
returnOk undefined
odE) (case r of (success, cleanup_info) \<Rightarrow> doE y <- liftE (when (exposed \<or> success) (empty_slot slot cleanup_info));
returnOk undefined
odE) s'
 2. s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s proof (prove)
goal (2 subgoals):
 1. \<And>r s' x1 x2. \<lbrakk>(Inr (x1, x2), s') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s); r = (x1, x2)\<rbrakk> \<Longrightarrow> s_bcorres (doE y <- liftE (when (exposed \<or> x1) (empty_slot slot x2));
returnOk undefined
odE) (doE y <- liftE (when (exposed \<or> x1) (empty_slot slot x2));
returnOk undefined
odE) s'
 2. s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s proof (prove)
goal:
No subgoals! proof (state)
this:
s_bcorres (rec_del (CTEDeleteCall slot exposed)) (rec_del (CTEDeleteCall slot exposed)) s

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> s_bcorres (rec_del (ReduceZombieCall (fst rvb) slot exposed)) (rec_del (ReduceZombieCall (fst rvb) slot exposed)) stc; \<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> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s 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> s_bcorres (rec_del (ReduceZombieCall (fst rvb) slot exposed)) (rec_del (ReduceZombieCall (fst rvb) slot exposed)) stc; \<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> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s 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> s_bcorres (rec_del (ReduceZombieCall (fst ?rvb) slot exposed)) (rec_del (ReduceZombieCall (fst ?rvb) slot exposed)) ?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); (Inr ?rvd, ?std) \<in> fst (rec_del (ReduceZombieCall (fst ?rvb) slot exposed) ?stc); (Inr ?rve, ?ste) \<in> fst (preemption_point ?std)\<rbrakk> \<Longrightarrow> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) ?ste

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> s_bcorres (rec_del (ReduceZombieCall (fst rvb) slot exposed)) (rec_del (ReduceZombieCall (fst rvb) slot exposed)) stc; \<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> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (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) (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 proof (prove)
goal:
No subgoals! proof (state)
this:
s_bcorres (rec_del (FinaliseSlotCall slot exposed)) (rec_del (FinaliseSlotCall slot exposed)) s

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) s
 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ False)) (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ False)) s_ proof (prove)
goal (1 subgoal):
 1. s_bcorres (doE y <- assertE ((slot, replicate (zombie_cte_bits exposed) False) \<noteq> slot_);
y <- liftE (cap_swap_for_delete (slot, replicate (zombie_cte_bits exposed) False) slot_);
returnOk undefined
odE) (doE y <- assertE ((slot, replicate (zombie_cte_bits exposed) False) \<noteq> slot_);
y <- liftE (cap_swap_for_delete (slot, replicate (zombie_cte_bits exposed) False) slot_);
returnOk undefined
odE) s_ proof (prove)
goal:
No subgoals! proof (state)
this:
s_bcorres (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ False)) (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ False)) s_

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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s 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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (slot, nat_to_cref (zombie_cte_bits exposed) s) s_) \<Longrightarrow> s_bcorres (rec_del (CTEDeleteCall ?rv False)) (rec_del (CTEDeleteCall ?rv False)) ?st

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> s_bcorres (rec_del (CTEDeleteCall rv False)) (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> s_bcorres (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ True)) (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ True)) s_ proof (prove)
goal (1 subgoal):
 1. s_bcorres (doE y <- rec_del (CTEDeleteCall (slot, nat_to_cref (zombie_cte_bits exposed) s) False);
new_cap <- liftE (get_cap slot_);
y <- if new_cap = Zombie slot exposed (Suc s) then liftE (set_cap (Zombie slot exposed s) slot_) else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot_ \<and> (slot, replicate (zombie_cte_bits exposed) False) \<noteq> slot_);
returnOk undefined
odE) (doE y <- rec_del (CTEDeleteCall (slot, nat_to_cref (zombie_cte_bits exposed) s) False);
new_cap <- liftE (get_cap slot_);
y <- if new_cap = Zombie slot exposed (Suc s) then liftE (set_cap (Zombie slot exposed s) slot_) else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot_ \<and> (slot, replicate (zombie_cte_bits exposed) False) \<noteq> slot_);
returnOk undefined
odE) s_ proof (prove)
goal:
No subgoals! proof (state)
this:
s_bcorres (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ True)) (rec_del (ReduceZombieCall (Zombie slot exposed (Suc s)) slot_ True)) s_

goal:
No subgoals!