theory EmptyFail_AI

lemma rec_del_spec_empty_fail:
  fixes call and s :: "'state_ext state"
  shows "spec_empty_fail (rec_del call) s" proof (induct rule: rec_del.induct, simp_all only: drop_spec_empty_fail[OF empty_fail_fail] rec_del_fails) case (1 slot exposed s) show ?case apply (subst rec_del.simps) apply (simp only: split_def) apply (rule spec_empty_fail_bindE) apply (simp add: "1.hyps") apply (wp | simp)+ done next case (2 slot exposed s) show ?case apply (subst rec_del.simps) apply (rule spec_empty_fail_bindE') apply ((wp drop_spec_empty_fail | simp)+)[1] apply (simp | intro conjI impI)+ apply (wp drop_spec_empty_fail)[1] apply (rule spec_empty_fail_bindE') apply ((wp drop_spec_empty_fail | simp)+)[1] apply (rule spec_empty_fail_bindE') apply ((wp drop_spec_empty_fail | simp)+)[1] apply (simp add: split_def | intro conjI impI)+ apply ((wp drop_spec_empty_fail | simp)+)[3] apply (rule spec_empty_fail_bindE') apply ((wp drop_spec_empty_fail | simp)+)[1] apply (rule spec_empty_fail_bindE') apply (rule "2.hyps", simp+) apply (rule spec_empty_fail_bindE') apply (wp drop_spec_empty_fail)[1] apply (rule "2.hyps", simp+) done next case 3 show ?case apply (simp | wp drop_spec_empty_fail)+ done next case (4 ptr bits n slot s) show ?case apply (subst rec_del.simps) apply (rule spec_empty_fail_bindE') apply (wp drop_spec_empty_fail)[1] apply (rule spec_empty_fail_bindE) apply (rule "4.hyps", assumption+) apply (wp | simp)+ done qed

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

goal (4 subgoals):
 1. \<And>slot exposed s. spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s \<Longrightarrow> spec_empty_fail (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> spec_empty_fail (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> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s
 3. \<And>ptr bits n slot s. spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (rec_del (CTEDeleteCall slot exposed)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (doE p <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> fst p) $ empty_slot slot (snd p);
returnOk undefined
odE) s proof (prove)
goal (2 subgoals):
 1. spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>x. empty_fail (doE without_preemption $ when (exposed \<or> fst x) $ empty_slot slot (snd x);
returnOk undefined
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail (doE without_preemption $ when (exposed \<or> fst x) $ empty_slot slot (snd x);
returnOk undefined
odE) proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (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> spec_empty_fail (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> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>ptr bits n slot s. spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (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> spec_empty_fail (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> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>ptr bits n slot s. spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (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> spec_empty_fail (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> spec_empty_fail (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> spec_empty_fail (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> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) ste\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s
 2. \<And>ptr bits n slot s. spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (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) s proof (prove)
goal (2 subgoals):
 1. spec_empty_fail (without_preemption $ get_cap slot) s
 2. \<And>x s'. (Inr x, s') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> spec_empty_fail (if x = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap x;
(remainder, cleanup_info) <- without_preemption $ finalise_cap x 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) s' proof (prove)
goal (1 subgoal):
 1. \<And>x s'. (Inr x, s') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> spec_empty_fail (if x = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap x;
(remainder, cleanup_info) <- without_preemption $ finalise_cap x 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) s' proof (prove)
goal (2 subgoals):
 1. \<And>x s'. \<lbrakk>(NullCap, s') \<in> fst (get_cap slot s); x = NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk (True, NullCap)) s'
 2. \<And>x s'. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (doE is_final <- liftE (is_final_cap x);
(remainder, cleanup_info) <- liftE (finalise_cap x 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) s' proof (prove)
goal (1 subgoal):
 1. \<And>x s'. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (doE is_final <- liftE (is_final_cap x);
(remainder, cleanup_info) <- liftE (finalise_cap x 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) s' proof (prove)
goal (2 subgoals):
 1. \<And>x s'. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (liftE (is_final_cap x)) s'
 2. \<And>x s' xa s'a. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (Inr xa, s'a) \<in> fst (liftE (is_final_cap x) s')\<rbrakk> \<Longrightarrow> spec_empty_fail (doE (remainder, cleanup_info) <- liftE (finalise_cap x xa);
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) s'a proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (Inr xa, s'a) \<in> fst (liftE (is_final_cap x) s')\<rbrakk> \<Longrightarrow> spec_empty_fail (doE (remainder, cleanup_info) <- liftE (finalise_cap x xa);
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) s'a proof (prove)
goal (2 subgoals):
 1. \<And>x s' xa s'a. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (Inr xa, s'a) \<in> fst (liftE (is_final_cap x) s')\<rbrakk> \<Longrightarrow> spec_empty_fail (liftE (finalise_cap x xa)) s'a
 2. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (Inr xa, s'a) \<in> fst (liftE (is_final_cap x) s'); (Inr xb, s'b) \<in> fst (liftE (finalise_cap x xa) s'a)\<rbrakk> \<Longrightarrow> spec_empty_fail (case xb of (remainder, cleanup_info) \<Rightarrow> 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) s'b proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (Inr xa, s'a) \<in> fst (liftE (is_final_cap x) s'); (Inr xb, s'b) \<in> fst (liftE (finalise_cap x xa) s'a)\<rbrakk> \<Longrightarrow> spec_empty_fail (case xb of (remainder, cleanup_info) \<Rightarrow> 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) s'b proof (prove)
goal (4 subgoals):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<and> \<not> exposed; cap_removeable (fst xb) slot\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk (True, snd xb)) s'b
 2. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<and> \<not> exposed; \<not> cap_removeable (fst xb) slot\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- liftE (set_cap (fst xb) slot);
returnOk (False, NullCap)
odE) s'b
 3. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; cap_removeable (fst xb) slot\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk (True, snd xb)) s'b
 4. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- liftE (set_cap (fst xb) slot);
y <- rec_del (ReduceZombieCall (fst xb) slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE) s'b proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- liftE (set_cap (fst xb) slot);
y <- rec_del (ReduceZombieCall (fst xb) slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE) s'b proof (prove)
goal (2 subgoals):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot\<rbrakk> \<Longrightarrow> spec_empty_fail (liftE (set_cap (fst xb) slot)) s'b
 2. \<And>x s' xa s'a xb s'b xc s'c. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; (Inr xc, s'c) \<in> fst (liftE (set_cap (fst xb) slot) s'b)\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- rec_del (ReduceZombieCall (fst xb) slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE) s'c proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b xc s'c. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; (Inr xc, s'c) \<in> fst (liftE (set_cap (fst xb) slot) s'b)\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- rec_del (ReduceZombieCall (fst xb) slot exposed);
y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE) s'c proof (prove)
goal (2 subgoals):
 1. \<And>x s' xa s'a xb s'b xc s'c. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; (Inr xc, s'c) \<in> fst (liftE (set_cap (fst xb) slot) s'b)\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (ReduceZombieCall (fst xb) slot exposed)) s'c
 2. \<And>x s' xa s'a xb s'b xc s'c xd s'd. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; (Inr xc, s'c) \<in> fst (liftE (set_cap (fst xb) slot) s'b); (Inr xd, s'd) \<in> fst (rec_del (ReduceZombieCall (fst xb) slot exposed) s'c)\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE) s'd proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b s'c xd s'd. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; ((), s'c) \<in> fst (set_cap (fst xb) slot s'b); (Inr xd, s'd) \<in> fst (rec_del (ReduceZombieCall (fst xb) slot exposed) s'c)\<rbrakk> \<Longrightarrow> spec_empty_fail (doE y <- preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE) s'd proof (prove)
goal (2 subgoals):
 1. \<And>x s' xa s'a xb s'b s'c xd s'd. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; ((), s'c) \<in> fst (set_cap (fst xb) slot s'b); (Inr xd, s'd) \<in> fst (rec_del (ReduceZombieCall (fst xb) slot exposed) s'c)\<rbrakk> \<Longrightarrow> spec_empty_fail preemption_point s'd
 2. \<And>x s' xa s'a xb s'b s'c xd s'd xc s'e. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; ((), s'c) \<in> fst (set_cap (fst xb) slot s'b); (Inr xd, s'd) \<in> fst (rec_del (ReduceZombieCall (fst xb) slot exposed) s'c); (Inr xc, s'e) \<in> fst (preemption_point s'd)\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s'e proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b s'c xd s'd xc s'e. \<lbrakk>(x, s') \<in> fst (get_cap slot s); x \<noteq> NullCap; (xa, s'a) \<in> fst (is_final_cap x s'); (xb, s'b) \<in> fst (finalise_cap x xa s'a); cap_cyclic_zombie (fst xb) slot \<longrightarrow> exposed; \<not> cap_removeable (fst xb) slot; ((), s'c) \<in> fst (set_cap (fst xb) slot s'b); (Inr xd, s'd) \<in> fst (rec_del (ReduceZombieCall (fst xb) slot exposed) s'c); (Inr xc, s'e) \<in> fst (preemption_point s'd)\<rbrakk> \<Longrightarrow> spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s'e proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (rec_del (FinaliseSlotCall slot exposed)) s

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


goal (2 subgoals):
 1. \<And>ptr bits n slot s. spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) slot_ False)) s_ proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr_ bits_ (Suc n_)) 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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> spec_empty_fail (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> spec_empty_fail (rec_del (CTEDeleteCall rv False)) st) \<Longrightarrow> spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (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) s proof (prove)
goal (2 subgoals):
 1. spec_empty_fail (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n)) s
 2. \<And>x s'. (Inr x, s') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> spec_empty_fail (doE rec_del (CTEDeleteCall x 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) s' proof (prove)
goal (1 subgoal):
 1. \<And>x s'. (Inr x, s') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> spec_empty_fail (doE rec_del (CTEDeleteCall x 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) s' proof (prove)
goal (2 subgoals):
 1. \<And>x s'. (Inr x, s') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> spec_empty_fail (rec_del (CTEDeleteCall x False)) s'
 2. \<And>x s' xa. (Inr x, s') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> empty_fail (K_bind (doE 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) xa) proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa. (Inr x, s') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> empty_fail (K_bind (doE 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) xa) proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) s

goal:
No subgoals!