theory ArchCNodeInv_AI

lemma rec_del_rvk_prog [CNodeInv_AI_assms]:
  "st \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)
          \<and> (case args of ReduceZombieCall cap sl ex \<Rightarrow>
               cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s
             | _ \<Rightarrow> True)\<rbrace>
     rec_del args
   \<lbrace>\<lambda>rv s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" proof (induct rule: rec_del.induct,
       simp_all only: rec_del_fails) case (1 slot exposed s) note wp = "1.hyps"[simplified rdcall_simps simp_thms] show ?case apply (subst rec_del.simps) apply (simp only: rdcall_simps simp_thms split_def) apply wp apply (simp(no_asm) del: o_apply) apply (wp empty_slot_rvk_prog)[1] apply (simp del: o_apply) apply (rule wp) done next case (2 sl exp s) note wp = "2.hyps" [simplified rdcall_simps simp_thms] show ?case apply (subst rec_del.simps) apply (simp only: rdcall_simps simp_thms split_def) apply (rule hoare_pre_spec_validE) apply wp apply ((wp | simp)+)[1] apply (wp wp) apply ((wp preemption_point_inv | simp)+)[1] apply (simp(no_asm)) apply (rule wp, assumption+) apply (wp final_cap_same_objrefs
                  set_cap_cte_wp_at_cases
                   | simp)+ apply (rule hoare_strengthen_post) apply (rule_tac Q="\<lambda>fc s. cte_wp_at ((=) rv) sl s
                              \<and> revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)"
                 in hoare_vcg_conj_lift) apply (wp finalise_cap_rvk_prog[folded o_def])[1] apply (rule finalise_cap_cases[where slot=sl]) apply (clarsimp simp: o_def) apply (strengthen rvk_prog_update_strg[unfolded fun_upd_def o_def]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule disjE) apply clarsimp apply (clarsimp simp: is_cap_simps) apply (case_tac "is_zombie rv") apply (clarsimp simp: cap_to_rpo_def is_cap_simps fst_cte_ptrs_def) apply (simp add: is_final_cap'_def) apply (case_tac rv, simp_all add: cap_to_rpo_def is_cap_simps gen_obj_refs_eq)[1] apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all)[1] apply (simp add: is_final_cap_def, wp) apply (simp, wp get_cap_wp) apply (clarsimp simp: o_def) done next case (3 ptr bits n slot s) show ?case apply simp apply (fold o_def) apply (rule hoare_pre_spec_validE) apply (simp del: o_apply | wp (once) cap_swap_fd_rvk_prog)+ apply (clarsimp simp: cte_wp_at_caps_of_state cap_to_rpo_def) done next case (4 ptr zb znum sl s) note wp = "4.hyps"[simplified rdcall_simps] show ?case apply (subst rec_del.simps) apply wp apply (wp | simp)+ apply (wp get_cap_wp)[1] apply (rule spec_strengthen_postE) apply (rule wp, assumption+) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_defs) apply (strengthen rvk_prog_update_strg[unfolded fun_upd_def o_def]) apply (clarsimp simp: cte_wp_at_caps_of_state cap_to_rpo_def) apply (wp | simp add: o_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case args of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del args \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap 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>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<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>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s) \<Longrightarrow> \<lbrace>?P'17 rv\<rbrace> without_preemption (when (exposed \<or> fst rv) $ empty_slot slot (snd rv)) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, -
 2. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. True \<and> True \<and> ?P'17 rv s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (Inr rv, s'') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s) \<Longrightarrow> \<lbrace>?P'17 rv\<rbrace> liftE (when (exposed \<or> fst rv) (empty_slot slot (snd rv))) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, -
 2. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. True \<and> True \<and> ?P'17 rv s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. True \<and> True \<and> (if exposed \<or> fst rv then \<lambda>a. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state a) else (\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s))) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap sl) 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) sl; \<not> (cap_cyclic_zombie (fst ?rvb) sl \<and> \<not> exp); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) sl) ?stb)\<rbrakk> \<Longrightarrow> ?stc \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst ?rvb) sl exp of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) sl exp) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap sl) 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) sl; \<not> (cap_cyclic_zombie (fst ?rvb) sl \<and> \<not> exp); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) sl) ?stb); (Inr ?rvd, ?std) \<in> fst (rec_del (ReduceZombieCall (fst ?rvb) sl exp) ?stc); (Inr ?rve, ?ste) \<in> fst (preemption_point ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall sl exp of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall sl exp) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap sl) 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) sl; \<not> (cap_cyclic_zombie (fst ?rvb) sl \<and> \<not> exp); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) sl) ?stb)\<rbrakk> \<Longrightarrow> ?stc \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> cte_wp_at (\<lambda>c. c = fst ?rvb) sl s \<and> is_final_cap' (fst ?rvb) s\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) sl exp) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap sl) 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) sl; \<not> (cap_cyclic_zombie (fst ?rvb) sl \<and> \<not> exp); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) sl) ?stb); (Inr ?rvd, ?std) \<in> fst (rec_del (ReduceZombieCall (fst ?rvb) sl exp) ?stc); (Inr ?rve, ?ste) \<in> fst (preemption_point ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> rec_del (FinaliseSlotCall sl exp) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (fst rvb) slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall slot exposed of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall sl exp of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall sl exp) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall sl exp of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> doE cap <- without_preemption $ get_cap sl;
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 sl then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder sl \<and> \<not> exp then doE without_preemption $ set_cap remainder sl;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap remainder sl;
rec_del (ReduceZombieCall remainder sl exp);
preemption_point;
rec_del (FinaliseSlotCall sl exp)
odE
odE
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> doE cap <- without_preemption $ get_cap sl;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
p <- without_preemption $ finalise_cap cap is_final;
if cap_removeable (fst p) sl then returnOk (True, snd p) else if cap_cyclic_zombie (fst p) sl \<and> \<not> exp then doE without_preemption $ set_cap (fst p) sl;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap (fst p) sl;
rec_del (ReduceZombieCall (fst p) sl exp);
preemption_point;
rec_del (FinaliseSlotCall sl exp)
odE
odE
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE cap <- without_preemption $ get_cap sl;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
p <- without_preemption $ finalise_cap cap is_final;
if cap_removeable (fst p) sl then returnOk (True, snd p) else if cap_cyclic_zombie (fst p) sl \<and> \<not> exp then doE without_preemption $ set_cap (fst p) sl;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap (fst p) sl;
rec_del (ReduceZombieCall (fst p) sl exp);
preemption_point;
rec_del (FinaliseSlotCall sl exp)
odE
odE
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp\<rbrakk> \<Longrightarrow> \<lbrace>?P'50 rv s'' rva s''a rvb\<rbrace> without_preemption (set_cap (fst rvb) sl) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> doE without_preemption $ set_cap (fst rvb) sl;
rec_del (ReduceZombieCall (fst rvb) sl exp);
preemption_point;
rec_del (FinaliseSlotCall sl exp)
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> True \<and> True \<and> ?P'50 rv s'' rva s''a rvb s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> doE without_preemption $ set_cap (fst rvb) sl;
rec_del (ReduceZombieCall (fst rvb) sl exp);
preemption_point;
rec_del (FinaliseSlotCall sl exp)
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> True \<and> True \<and> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (((caps_of_state s)(sl \<mapsto> fst rvb)) a))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) sl) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) sl exp) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B65 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>rve s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) sl) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B63 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) sl exp) \<lbrace>?B65 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>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) sl \<lbrace>?B63 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> True \<and> True \<and> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (((caps_of_state s)(sl \<mapsto> fst rvb)) a))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) sl) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B63 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) sl exp) \<lbrace>\<lambda>rvd s. True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) sl \<lbrace>?B63 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> True \<and> True \<and> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (((caps_of_state s)(sl \<mapsto> fst rvb)) a))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) sl) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B63 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) sl exp) \<lbrace>\<lambda>rvd s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) sl \<lbrace>?B63 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> True \<and> True \<and> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (((caps_of_state s)(sl \<mapsto> fst rvb)) a))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) sl; \<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) sl \<lbrace>\<lambda>a b. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state b) \<and> cte_wp_at (\<lambda>c. c = fst rvb) sl b \<and> is_final_cap' (fst rvb) b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B16 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> True \<and> True \<and> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (((caps_of_state s)(sl \<mapsto> fst rvb)) a))) \<and> (\<not> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp) \<longrightarrow> ?P'33 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B16 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'123 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a))) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state s a))) \<and> ((cap_cyclic_zombie (fst rvb) sl \<longrightarrow> exp) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state s a)) \<and> cte_wp_at (\<lambda>_. True) sl s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. cap_irqs (fst rvb) \<inter> cap_irqs c = {} \<longrightarrow> obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs (fst rvb) \<inter> arch_gen_refs c \<noteq> {}) sl s))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'123 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'123 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q135 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); ?Q135 rv s'' rva s''a rvb sa\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state sa a))) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a))) \<and> ((cap_cyclic_zombie (fst rvb) sl \<longrightarrow> exp) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a)) \<and> cte_wp_at (\<lambda>_. True) sl sa \<and> is_final_cap' (fst rvb) sa \<and> cte_wp_at (\<lambda>c. cap_irqs (fst rvb) \<inter> cap_irqs c = {} \<longrightarrow> obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs (fst rvb) \<inter> arch_gen_refs c \<noteq> {}) sl sa))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'123 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P140 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>fc s. cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'141 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'138 rv s'' rva s''a\<rbrace>
 3. \<And>rv s'' rva s''a rvb sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (cte_wp_at ((=) rv) sl sa \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state sa)) \<and> ?Q'138 rv s'' rva s''a rvb sa\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state sa a))) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a))) \<and> ((cap_cyclic_zombie (fst rvb) sl \<longrightarrow> exp) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a)) \<and> cte_wp_at (\<lambda>_. True) sl sa \<and> is_final_cap' (fst rvb) sa \<and> cte_wp_at (\<lambda>c. cap_irqs (fst rvb) \<inter> cap_irqs c = {} \<longrightarrow> obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs (fst rvb) \<inter> arch_gen_refs c \<noteq> {}) sl sa))
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P140 rv s'' rva s \<and> ?P'141 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'141 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q'138 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (cte_wp_at ((=) rv) sl sa \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state sa)) \<and> ?Q'138 rv s'' rva s''a rvb sa\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state sa a))) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a))) \<and> ((cap_cyclic_zombie (fst rvb) sl \<longrightarrow> exp) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a)) \<and> cte_wp_at (\<lambda>_. True) sl sa \<and> is_final_cap' (fst rvb) sa \<and> cte_wp_at (\<lambda>c. cap_irqs (fst rvb) \<inter> cap_irqs c = {} \<longrightarrow> obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs (fst rvb) \<inter> arch_gen_refs c \<noteq> {}) sl sa))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> ?P'141 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a rvb sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (cte_wp_at ((=) rv) sl sa \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state sa)) \<and> (fst rvb = NullCap \<and> snd rvb = (if rva then cap_cleanup_opt rv else NullCap) \<and> (snd rvb \<noteq> NullCap \<longrightarrow> is_final_cap' rv sa) \<or> is_zombie (fst rvb) \<and> is_final_cap' rv sa \<and> is_final_cap' (fst rvb) sa \<and> snd rvb = NullCap \<and> appropriate_cte_cap (fst rvb) = appropriate_cte_cap rv \<and> cte_refs (fst rvb) = cte_refs rv \<and> gen_obj_refs (fst rvb) = gen_obj_refs rv \<and> obj_size (fst rvb) = obj_size rv \<and> fst_cte_ptrs (fst rvb) = fst_cte_ptrs rv \<and> vs_cap_ref rv = None)\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state sa a))) \<and> (\<not> cap_removeable (fst rvb) sl \<longrightarrow> (cap_cyclic_zombie (fst rvb) sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a))) \<and> ((cap_cyclic_zombie (fst rvb) sl \<longrightarrow> exp) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (fst rvb) else caps_of_state sa a)) \<and> cte_wp_at (\<lambda>_. True) sl sa \<and> is_final_cap' (fst rvb) sa \<and> cte_wp_at (\<lambda>c. cap_irqs (fst rvb) \<inter> cap_irqs c = {} \<longrightarrow> obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs (fst rvb) \<inter> arch_gen_refs c \<noteq> {}) sl sa))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); cte_wp_at ((=) rv) sl sa; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv sa) \<or> is_zombie a \<and> is_final_cap' rv sa \<and> is_final_cap' a sa \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None; \<not> cap_removeable a sl\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>b. map_option cap_to_rpo (if b = sl then Some a else caps_of_state sa b))) \<and> ((cap_cyclic_zombie a sl \<longrightarrow> exp) \<longrightarrow> revoke_progress_ord m (\<lambda>b. map_option cap_to_rpo (if b = sl then Some a else caps_of_state sa b)) \<and> cte_wp_at (\<lambda>_. True) sl sa \<and> is_final_cap' a sa \<and> cte_wp_at (\<lambda>c. cap_irqs a \<inter> cap_irqs c = {} \<longrightarrow> obj_refs a \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs a \<inter> arch_gen_refs c \<noteq> {}) sl sa)
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); cte_wp_at ((=) rv) sl sa; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv sa) \<or> is_zombie a \<and> is_final_cap' rv sa \<and> is_final_cap' a sa \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None; \<not> cap_removeable a sl\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a sl \<and> \<not> exp \<longrightarrow> revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)) \<and> cte_wp_at (\<lambda>cp. cap_to_rpo cp = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo cp))) sl sa) \<and> ((cap_cyclic_zombie a sl \<longrightarrow> exp) \<longrightarrow> (revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)) \<and> cte_wp_at (\<lambda>cp. cap_to_rpo cp = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo cp))) sl sa) \<and> cte_wp_at (\<lambda>_. True) sl sa \<and> is_final_cap' a sa \<and> cte_wp_at (\<lambda>c. cap_irqs a \<inter> cap_irqs c = {} \<longrightarrow> obj_refs a \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs a \<inter> arch_gen_refs c \<noteq> {}) sl sa)
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv sa) \<or> is_zombie a \<and> is_final_cap' rv sa \<and> is_final_cap' a sa \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None; \<not> cap_removeable a sl\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie a sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> is_final_cap' a sa \<and> (cap_irqs a \<inter> cap_irqs rv = {} \<longrightarrow> obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> arch_gen_refs a \<inter> arch_gen_refs rv \<noteq> {}))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a a b sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); \<not> cap_removeable a sl; a = NullCap \<and> b = (if rva then cap_cleanup_opt rv else NullCap) \<and> (b \<noteq> NullCap \<longrightarrow> is_final_cap' rv sa)\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie a sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> is_final_cap' a sa \<and> (cap_irqs a \<inter> cap_irqs rv = {} \<longrightarrow> obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> arch_gen_refs a \<inter> arch_gen_refs rv \<noteq> {}))
 2. \<And>rv s'' rva s''a a b sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); \<not> cap_removeable a sl; is_zombie a \<and> is_final_cap' rv sa \<and> is_final_cap' a sa \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie a sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> is_final_cap' a sa \<and> (cap_irqs a \<inter> cap_irqs rv = {} \<longrightarrow> obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> arch_gen_refs a \<inter> arch_gen_refs rv \<noteq> {}))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a a b sa. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); \<not> cap_removeable a sl; is_zombie a \<and> is_final_cap' rv sa \<and> is_final_cap' a sa \<and> b = NullCap \<and> appropriate_cte_cap a = appropriate_cte_cap rv \<and> cte_refs a = cte_refs rv \<and> gen_obj_refs a = gen_obj_refs rv \<and> obj_size a = obj_size rv \<and> fst_cte_ptrs a = fst_cte_ptrs rv \<and> vs_cap_ref rv = None\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie a sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie a sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo a \<or> rpo_measure sl (Some (cap_to_rpo a)) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> is_final_cap' a sa \<and> (cap_irqs a \<inter> cap_irqs rv = {} \<longrightarrow> obj_refs a \<inter> obj_refs rv = {} \<longrightarrow> arch_gen_refs a \<inter> arch_gen_refs rv \<noteq> {}))
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a sa r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); is_final_cap' rv sa; is_final_cap' (Zombie r b n) sa; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap rv; cte_refs (Zombie r b n) = cte_refs rv; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> r \<in> obj_refs rv)
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a sa r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); is_final_cap' rv sa; is_final_cap' (Zombie r b n) sa; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap rv; cte_refs (Zombie r b n) = cte_refs rv; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl; is_zombie rv\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> r \<in> obj_refs rv)
 2. \<And>rv s'' rva s''a sa r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); is_final_cap' rv sa; is_final_cap' (Zombie r b n) sa; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap rv; cte_refs (Zombie r b n) = cte_refs rv; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl; \<not> is_zombie rv\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> r \<in> obj_refs rv)
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a sa r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); is_final_cap' rv sa; is_final_cap' (Zombie r b n) sa; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap rv; cte_refs (Zombie r b n) = cte_refs rv; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl; \<not> is_zombie rv\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> r \<in> obj_refs rv)
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a sa r b n. \<lbrakk>(rv, s'') \<in> fst (get_cap sl s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); caps_of_state sa sl = Some rv; revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); \<exists>a b. {cref. \<exists>cap'. fst (get_cap cref sa) = {(cap', sa)} \<and> gen_obj_refs rv \<inter> gen_obj_refs cap' \<noteq> {}} = {(a, b)}; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap rv; cte_refs (Zombie r b n) = cte_refs rv; gen_obj_refs (Zombie r b n) = gen_obj_refs rv; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs rv; vs_cap_ref rv = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl; \<not> is_zombie rv\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<and> \<not> exp \<longrightarrow> cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> ((cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> (cap_to_rpo rv = cap_to_rpo (Zombie r b n) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie r b n))) < rpo_measure sl (Some (cap_to_rpo rv))) \<and> r \<in> obj_refs rv)
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a sa r b n x12. \<lbrakk>(ArchObjectCap x12, s'') \<in> fst (get_cap sl s); (rva, s''a) \<in> fst (is_final_cap (ArchObjectCap x12) s''); caps_of_state sa sl = Some (ArchObjectCap x12); revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); \<exists>a b. {cref. \<exists>cap'. fst (get_cap cref sa) = {(cap', sa)} \<and> gen_obj_refs (ArchObjectCap x12) \<inter> gen_obj_refs cap' \<noteq> {}} = {(a, b)}; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap (ArchObjectCap x12); cte_refs (Zombie r b n) = cte_refs (ArchObjectCap x12); {r} = set_option (aobj_ref x12) \<and> {} = arch_gen_obj_refs x12; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 2 ^ arch_obj_size x12; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs (ArchObjectCap x12); vs_cap_ref (ArchObjectCap x12) = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl; rv = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> aobj_ref x12 = Some r
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a sa r b n arch_cap. \<lbrakk>(ArchObjectCap arch_cap, s'') \<in> fst (get_cap sl s); (rva, s''a) \<in> fst (is_final_cap (ArchObjectCap arch_cap) s''); caps_of_state sa sl = Some (ArchObjectCap arch_cap); revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state sa x)); \<exists>a b. {cref. \<exists>cap'. fst (get_cap cref sa) = {(cap', sa)} \<and> gen_obj_refs (ArchObjectCap arch_cap) \<inter> gen_obj_refs cap' \<noteq> {}} = {(a, b)}; appropriate_cte_cap (Zombie r b n) = appropriate_cte_cap (ArchObjectCap arch_cap); cte_refs (Zombie r b n) = cte_refs (ArchObjectCap arch_cap); {r} = set_option (aobj_ref arch_cap) \<and> {} = arch_gen_obj_refs arch_cap; (case b of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = 2 ^ arch_obj_size arch_cap; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs (ArchObjectCap arch_cap); vs_cap_ref (ArchObjectCap arch_cap) = None; 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> sl; rv = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (cap_cyclic_zombie (Zombie r b n) sl \<longrightarrow> exp) \<longrightarrow> aobj_ref arch_cap = Some r
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap sl) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap sl \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (rv \<noteq> NullCap \<longrightarrow> True \<and> cte_wp_at ((=) rv) sl s \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (is_final_cap' rv s \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) sl s))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) sl s \<longrightarrow> (cap = NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a))) \<and> (cap \<noteq> NullCap \<longrightarrow> cte_wp_at ((=) cap) sl s \<and> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a)) \<and> (is_final_cap' cap s \<longrightarrow> cte_wp_at ((=) cap) sl s))) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case FinaliseSlotCall sl exp of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (FinaliseSlotCall sl exp) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a)) \<and> cte_wp_at (\<lambda>c. c = Zombie ptr bits (Suc n)) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s\<rbrace> doE y <- assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (ptr, replicate (zombie_cte_bits bits) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> cte_wp_at (\<lambda>c. c = Zombie ptr bits (Suc n)) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s\<rbrace> doE y <- assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (ptr, replicate (zombie_cte_bits bits) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE y <- assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (ptr, replicate (zombie_cte_bits bits) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> cte_wp_at (\<lambda>c. c = Zombie ptr bits (Suc n)) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> cte_wp_at (\<lambda>c. c = Zombie ptr bits (Suc n)) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<Longrightarrow> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> cte_wp_at (\<lambda>cp. cap_to_rpo cp = (Some (ptr, replicate (zombie_cte_bits bits) False), 2) \<and> is_final_cap' cp s) slot s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall ?rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> True\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case CTEDeleteCall rv False of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> doE end_slot <- returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum);
rec_del (CTEDeleteCall end_slot False);
new_cap <- without_preemption $ get_cap sl;
if new_cap = Zombie ptr zb (Suc znum) then without_preemption $ set_cap (Zombie ptr zb znum) sl else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = sl \<and> first_cslot_of (Zombie ptr zb (Suc znum)) \<noteq> sl);
returnOk undefined
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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 zb) znum) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ get_cap sl) s''a); rvb = Zombie ptr zb (Suc znum)\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 rv s'' rva s''a rvb\<rbrace> without_preemption (set_cap (Zombie ptr zb znum) sl) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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 zb) znum) s); (Inr rva, s''a) \<in> fst (rec_del (CTEDeleteCall rv False) s''); (Inr rvb, s''b) \<in> fst ((without_preemption $ get_cap sl) s''a); rvb \<noteq> Zombie ptr zb (Suc znum)\<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 = sl \<and> first_cslot_of (Zombie ptr zb (Suc znum)) \<noteq> sl) \<lbrace>\<lambda>rvc s. True \<and> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state 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 zb) znum) 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 sl \<lbrace>\<lambda>rvb s. (rvb = Zombie ptr zb (Suc znum) \<longrightarrow> True \<and> True \<and> ?P'25 rv s'' rva s''a rvb s) \<and> (rvb \<noteq> Zombie ptr zb (Suc znum) \<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 zb) znum) 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. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<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 zb) znum) 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'47 rv s'' rva\<rbrace> get_cap sl \<lbrace>\<lambda>rvb s. (rvb = Zombie ptr zb (Suc znum) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (Zombie ptr zb znum) else caps_of_state s a))) \<and> (rvb \<noteq> Zombie ptr zb (Suc znum) \<longrightarrow> (rvb = NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a))) \<and> (is_zombie rvb \<and> first_cslot_of rvb = sl \<and> (ptr, replicate (zombie_cte_bits zb) False) \<noteq> sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a))))\<rbrace>
 2. \<And>rv s''. (Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>rva s. True \<and> ?P'47 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<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 zb) znum) 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) sl s \<longrightarrow> (cap = Zombie ptr zb (Suc znum) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (Zombie ptr zb znum) else caps_of_state s a))) \<and> (cap \<noteq> Zombie ptr zb (Suc znum) \<longrightarrow> (cap = NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a))) \<and> (is_zombie cap \<and> first_cslot_of cap = sl \<and> (ptr, replicate (zombie_cte_bits zb) False) \<noteq> sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state s a)))))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<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 zb) znum) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>?Q'62 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' sa r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s); ?Q'62 rv s'' sa r\<rbrakk> \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) sl r \<longrightarrow> (cap = Zombie ptr zb (Suc znum) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (Zombie ptr zb znum) else caps_of_state r a))) \<and> (cap \<noteq> Zombie ptr zb (Suc znum) \<longrightarrow> (cap = NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state r a))) \<and> (is_zombie cap \<and> first_cslot_of cap = sl \<and> (ptr, replicate (zombie_cte_bits zb) False) \<noteq> sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state r a)))))
 3. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s'' sa r. \<lbrakk>(Inr rv, s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s); revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state r)\<rbrakk> \<Longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) sl r \<longrightarrow> (cap = Zombie ptr zb (Suc znum) \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (Zombie ptr zb znum) else caps_of_state r a))) \<and> (cap \<noteq> Zombie ptr zb (Suc znum) \<longrightarrow> (cap = NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state r a))) \<and> (is_zombie cap \<and> first_cslot_of cap = sl \<and> (ptr, replicate (zombie_cte_bits zb) False) \<noteq> sl \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state r a)))))
 2. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b s'' r. \<lbrakk>(Inr (a, b), s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s); revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state r a)); caps_of_state r sl = Some (Zombie ptr zb (Suc znum))\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some (Zombie ptr zb znum) else caps_of_state r a))
 2. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b s'' r. \<lbrakk>(Inr (a, b), s'') \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) s); revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state r a)); caps_of_state r sl = Some (Zombie ptr zb (Suc znum))\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state r x)) \<and> cte_wp_at (\<lambda>cp. cap_to_rpo cp = cap_to_rpo (Zombie ptr zb znum) \<or> rpo_measure sl (Some (cap_to_rpo (Zombie ptr zb znum))) < rpo_measure sl (Some (cap_to_rpo cp))) sl r
 2. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> returnOk (ptr, nat_to_cref (zombie_cte_bits zb) znum) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> (case ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr zb (Suc znum)) sl True) \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal:
No subgoals!