theory CNodeInv_AI

lemma rec_del_abort_cases:
  "\<And>args (s::'state_ext state).
  case args of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<top>\<rbrace>
     rec_del (FinaliseSlotCall sl ex)
   \<lbrace>\<lambda>rv s. (fst rv) \<or> (\<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>
      | _ \<Rightarrow> True" subgoal for args s proof (induct rule: rec_del_induct) case (2 slot exposed) note wp = "2.hyps"[simplified rec_del_call.simps] show ?case apply (subst rec_del_simps_ext) apply (simp only: rec_del_call.simps split_def) apply wp apply (simp add: cte_wp_at_caps_of_state) apply (wp wp)+ apply (wp irq_state_independent_AI | simp)+ apply (rule hoare_strengthen_post) apply (rule finalise_cap_cases[where slot=slot]) apply clarsimp apply (fastforce simp: fst_cte_ptrs_def) apply (simp add: is_final_cap_def | wp get_cap_wp)+ done qed (simp_all add: rec_del_fails) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>args s. case args of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True proof (prove)
goal (1 subgoal):
 1. case args of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True proof (state)
goal (28 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (CTEDeleteCall slot exposed, s); case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case CTEDeleteCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 2. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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> case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> stc \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True; \<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> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> ste \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 3. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 4. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> case CTEDeleteCall rv False of FinaliseSlotCall sl ex \<Rightarrow> st \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 5. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> case ReduceZombieCall NullCap slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 6. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (UntypedCap v va vb vc) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (EndpointCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (NotificationCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (ReplyCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 10. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (CNodeCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
A total of 28 subgoals... proof (state)
this:
rec_del_dom (FinaliseSlotCall slot exposed, s_)
\<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> case ReduceZombieCall (fst ?rvb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> ?stc \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
\<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> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> ?ste \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True

goal (28 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (CTEDeleteCall slot exposed, s); case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case CTEDeleteCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 2. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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> case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> stc \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True; \<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> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> ste \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 3. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 4. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> case CTEDeleteCall rv False of FinaliseSlotCall sl ex \<Rightarrow> st \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 5. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> case ReduceZombieCall NullCap slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 6. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (UntypedCap v va vb vc) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (EndpointCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (NotificationCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (ReplyCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 10. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (CNodeCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
A total of 28 subgoals... proof (state)
this:
rec_del_dom (FinaliseSlotCall slot exposed, s_)
\<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> True
\<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>_. True\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (28 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (CTEDeleteCall slot exposed, s); case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case CTEDeleteCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 2. \<And>slot exposed s. \<lbrakk>rec_del_dom (FinaliseSlotCall slot exposed, s); \<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> case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> stc \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True; \<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> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> ste \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 3. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 4. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> case CTEDeleteCall rv False of FinaliseSlotCall sl ex \<Rightarrow> st \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 5. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> case ReduceZombieCall NullCap slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 6. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (UntypedCap v va vb vc) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (EndpointCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (NotificationCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (ReplyCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 10. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (CNodeCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
A total of 28 subgoals... proof (prove)
goal (1 subgoal):
 1. case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True proof (prove)
goal (1 subgoal):
 1. case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s_ \<turnstile> \<lbrace>\<lambda>_. 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> ex 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 ex);
preemption_point;
rec_del (FinaliseSlotCall sl ex)
odE
odE
odE \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> doE cap <- without_preemption $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
p <- without_preemption $ finalise_cap cap is_final;
if cap_removeable (fst p) slot then returnOk (True, snd p) else if cap_cyclic_zombie (fst p) slot \<and> \<not> exposed then doE without_preemption $ set_cap (fst p) slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap (fst p) slot;
rec_del (ReduceZombieCall (fst p) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv s. fst rv \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot 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 ((without_preemption $ get_cap slot) 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) slot; cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 rv s'' rva s''a rvb\<rbrace> without_preemption (set_cap (fst rvb) slot) \<lbrace>\<lambda>rv s. fst (False, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) 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) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'29 rv s'' rva s''a rvb\<rbrace> doE without_preemption $ set_cap (fst rvb) slot;
rec_del (ReduceZombieCall (fst rvb) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>rv s. fst rv \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (fst (True, snd rvb) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> ?P'46 rv s'' rva s''a rvb s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'29 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 slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv 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 (liftE (get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); (Inr rvb, s''b) \<in> fst (liftE (finalise_cap rv rva) s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 rv s'' rva s''a rvb\<rbrace> liftE (set_cap (fst rvb) slot) \<lbrace>\<lambda>rv s. \<exists>cap. caps_of_state s slot = Some cap \<and> is_zombie cap \<and> slot \<in> fst_cte_ptrs cap\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) 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) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'29 rv s'' rva s''a rvb\<rbrace> doE without_preemption $ set_cap (fst rvb) slot;
rec_del (ReduceZombieCall (fst rvb) slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>rv s. fst rv \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B12 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (fst (True, snd rvb) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> ?P'46 rv s'' rva s''a rvb s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'29 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 slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst ((without_preemption $ is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 rv s'' rva\<rbrace> without_preemption (finalise_cap rv rva) \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> True \<and> (fst (True, snd rvb) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> True \<and> True \<and> (\<exists>cap. ((caps_of_state s)(slot \<mapsto> fst rvb)) slot = Some cap \<and> is_zombie cap \<and> slot \<in> fst_cte_ptrs cap)) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> True \<and> True \<and> True \<and> True))\<rbrace>, -
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'111 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. \<not> cap_removeable (fst rvb) slot \<longrightarrow> cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> is_zombie (fst rvb) \<and> slot \<in> fst_cte_ptrs (fst rvb)\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'111 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q121 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); ?Q121 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> \<not> cap_removeable (fst rvb) slot \<longrightarrow> cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> is_zombie (fst rvb) \<and> slot \<in> fst_cte_ptrs (fst rvb)
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> ?P'111 rv s'' rva s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a rvb s. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); 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 s) \<or> is_zombie (fst rvb) \<and> is_final_cap' rv s \<and> is_final_cap' (fst rvb) s \<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> \<not> cap_removeable (fst rvb) slot \<longrightarrow> cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> is_zombie (fst rvb) \<and> slot \<in> fst_cte_ptrs (fst rvb)
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s'' rva s''a s p zb n. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap (p, replicate (zombie_cte_bits zb) False)) s_); rv \<noteq> NullCap; (Inr rva, s''a) \<in> fst (liftE (is_final_cap rv) s''); \<not> exposed; slot = (p, replicate (zombie_cte_bits zb) False); is_zombie (Zombie p zb n); 0 < n; n \<noteq> Suc 0; is_final_cap' rv s; is_final_cap' (Zombie p zb n) s; appropriate_cte_cap (Zombie p zb n) = appropriate_cte_cap rv; cte_refs (Zombie p zb n) = cte_refs rv; gen_obj_refs (Zombie p zb n) = gen_obj_refs rv; (case zb of None \<Rightarrow> 1 << obj_bits (TCB undefined) | Some n \<Rightarrow> 1 << cte_level_bits + n) = obj_size rv; fst_cte_ptrs (Zombie p zb n) = fst_cte_ptrs rv; vs_cap_ref rv = None\<rbrakk> \<Longrightarrow> (p, replicate (zombie_cte_bits zb) False) \<in> fst_cte_ptrs rv
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'5 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. True \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True \<and> (fst (True, NullCap) \<or> \<not> exposed \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> slot \<in> fst_cte_ptrs c) slot s)) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'5 rv s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s_ \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True

goal (27 subgoals):
 1. \<And>slot exposed s. \<lbrakk>rec_del_dom (CTEDeleteCall slot exposed, s); case FinaliseSlotCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case CTEDeleteCall slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 2. \<And>ptr bits n slot s. rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False, s) \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 3. \<And>ptr bits n slot s. \<lbrakk>rec_del_dom (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True, s); \<And>rv st. (Inr rv, st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> case CTEDeleteCall rv False of FinaliseSlotCall sl ex \<Rightarrow> st \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 4. \<And>slot exposed s. rec_del_dom (ReduceZombieCall NullCap slot exposed, s) \<Longrightarrow> case ReduceZombieCall NullCap slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 5. \<And>v va vb vc slot exposed s. rec_del_dom (ReduceZombieCall (UntypedCap v va vb vc) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (UntypedCap v va vb vc) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 6. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (EndpointCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (EndpointCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 7. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (NotificationCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (NotificationCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 8. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (ReplyCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (ReplyCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 9. \<And>v va vb slot exposed s. rec_del_dom (ReduceZombieCall (CNodeCap v va vb) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (CNodeCap v va vb) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
 10. \<And>v slot exposed s. rec_del_dom (ReduceZombieCall (ThreadCap v) slot exposed, s) \<Longrightarrow> case ReduceZombieCall (ThreadCap v) slot exposed of FinaliseSlotCall sl ex \<Rightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True
A total of 27 subgoals... proof (prove)
goal:
No subgoals!