theory ADT_IF

lemma rec_del_irq_state_inv':
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del] rec_del.simps[simp del]
  shows
    "s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace>
         rec_del call
         \<lbrace>\<lambda>a s. (case call of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap
                            | _ \<Rightarrow> True) \<and>
                domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" proof (induct s arbitrary: rule: rec_del.induct, simp_all only: rec_del_fails hoare_fail_any) case (1 slot exposed s) show ?case apply (simp add: split_def rec_del.simps) apply (wp drop_spec_validE[OF returnOk_wp]
              drop_spec_validE[OF liftE_wp] empty_slot_domain_sep_inv) apply (wp irq_state_inv_triv' empty_slot_irq_masks) apply (rule spec_strengthen_postE[OF "1.hyps", simplified]) apply fastforce done next case (2 slot exposed s) show ?case apply (rule hoare_spec_gen_asm) apply (simp add: rec_del.simps split del: if_split) apply (rule hoare_pre_spec_validE) apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv
            | simp add: split_def split del: if_split)+ apply (wp irq_state_inv_triv)[1] apply (wp | simp split del: if_split)+ apply (rule spec_strengthen_postE) apply (rule "2.hyps"[simplified], fastforce+) apply (rule drop_spec_validE,
                 (wp preemption_point_irq_state_inv[where irq=irq] | simp)+)[1] apply (rule spec_strengthen_postE) apply (rule "2.hyps"[simplified], fastforce+) apply (wp  finalise_cap_domain_sep_inv_cap get_cap_wp
                     finalise_cap_returns_NullCap[where irqs=False, simplified]
                     drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv
                  | simp add: without_preemption_def split del: if_split
                  | wp (once) hoare_drop_imps
                  | wp irq_state_inv_triv)+ apply (blast dest: cte_wp_at_domain_sep_inv_cap) done next case (3 ptr bits n slot s) show ?case apply (simp add: rec_del.simps) apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] irq_state_inv_triv) apply (rule hoare_pre_spec_validE) apply (wp drop_spec_validE[OF assertE_wp]) apply (fastforce) done next case (4 ptr bits n slot s) show ?case apply (simp add: rec_del.simps) apply (wpsimp wp: irq_state_inv_triv set_cap_domain_sep_inv drop_spec_validE[OF liftE_wp]
                      drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp] get_cap_wp) apply (rule spec_strengthen_postE[OF "4.hyps", simplified]) apply (simp add: returnOk_def return_def) apply (clarsimp simp: domain_sep_inv_cap_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del call \<lbrace>\<lambda>a s. (case call of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>a s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv stb rva staa rvb stba rvc stc. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>; \<And>rv stb rva staa rvb stba rvc stc rvd std rve ste. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>a s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv stb rva staa rvb stba rvc stc. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>; \<And>rv stb rva staa rvb stba rvc stc rvd std rve ste. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>a s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace> doE p <- rec_del (FinaliseSlotCall slot exposed);
y <- liftE (when (exposed \<or> fst p) (empty_slot slot (snd p)));
returnOk undefined
odE \<lbrace>\<lambda>a s. domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (rec_del (FinaliseSlotCall slot exposed) s); exposed \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?P'12 rv\<rbrace> empty_slot slot (snd rv) \<lbrace>\<lambda>rv. irq_state_inv st\<rbrace>
 2. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then \<lambda>b. (domain_sep_inv False sta b \<and> (\<not> False \<longrightarrow> snd a = NullCap)) \<and> ?P'12 a b else (\<lambda>a. domain_sep_inv False sta a \<and> irq_state_inv st a)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then \<lambda>b. (domain_sep_inv False sta b \<and> (\<not> False \<longrightarrow> snd a = NullCap)) \<and> (irq_state_inv st and K (snd a = NullCap)) b else (\<lambda>a. domain_sep_inv False sta a \<and> irq_state_inv st a)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s r. (exposed \<longrightarrow> snd s = NullCap) \<and> (fst s \<longrightarrow> snd s = NullCap) \<and> domain_sep_inv False sta r \<and> irq_state_inv st r \<Longrightarrow> (if exposed \<or> fst s then \<lambda>a. (domain_sep_inv False sta a \<and> (\<not> False \<longrightarrow> snd s = NullCap)) \<and> (irq_state_inv st and K (snd s = NullCap)) a else (\<lambda>a. domain_sep_inv False sta a \<and> irq_state_inv st a)) r proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>a s. (case CTEDeleteCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv stb rva staa rvb stba rvc stc. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>; \<And>rv stb rva staa rvb stba rvc stc rvd std rve ste. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv stb rva staa rvb stba rvc stc. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>; \<And>rv stb rva staa rvb stba rvc stc rvd std rve ste. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); ?rv \<noteq> NullCap; (Inr ?rva, ?sta) \<in> fst ((without_preemption $ is_final_cap ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((without_preemption $ finalise_cap ?rv ?rva) ?sta); \<not> cap_removeable (fst ?rvb) slot; \<not> (cap_cyclic_zombie (fst ?rvb) slot \<and> \<not> exposed); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) slot) ?stb)\<rbrakk> \<Longrightarrow> ?stc \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>a s. (case ReduceZombieCall (fst ?rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); ?rv \<noteq> NullCap; (Inr ?rva, ?sta) \<in> fst ((without_preemption $ is_final_cap ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst ((without_preemption $ finalise_cap ?rv ?rva) ?sta); \<not> cap_removeable (fst ?rvb) slot; \<not> (cap_cyclic_zombie (fst ?rvb) slot \<and> \<not> exposed); (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ set_cap (fst ?rvb) slot) ?stb); (Inr ?rvd, ?std) \<in> fst (rec_del (ReduceZombieCall (fst ?rvb) slot exposed) ?stc); (Inr ?rve, ?ste) \<in> fst (preemption_point ?std)\<rbrakk> \<Longrightarrow> ?ste \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv stb rva staa rvb stba rvc stc. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a s. (case ReduceZombieCall (fst rvb) slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>; \<And>rv stb rva staa rvb stba rvc stc rvd std rve ste. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) stb); (Inr rvb, stba) \<in> fst ((without_preemption $ finalise_cap rv rva) staa); \<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) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a\<rbrace> doE cap <- liftE (get_cap slot);
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
(remainder, cleanup_info) <- without_preemption $ finalise_cap cap is_final;
if cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> exposed then doE without_preemption $ set_cap remainder slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>a s. (exposed \<longrightarrow> snd a = NullCap) \<and> (fst a \<longrightarrow> snd a = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> doE cap <- liftE (get_cap slot);
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
(remainder, cleanup_info) <- without_preemption $ finalise_cap cap is_final;
if cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> exposed then doE without_preemption $ set_cap remainder slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>a s. (exposed \<longrightarrow> snd a = NullCap) \<and> (fst a \<longrightarrow> snd a = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P'41 rv s'' rva s''a rvb\<rbrace> set_cap (fst rvb) slot \<lbrace>\<lambda>rv. irq_state_inv st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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>a s. (exposed \<longrightarrow> snd a = NullCap) \<and> (fst a \<longrightarrow> snd a = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> ?P'41 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>_. irq_state_next st\<rbrace>
 4. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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>a s. (exposed \<longrightarrow> snd a = NullCap) \<and> (fst a \<longrightarrow> snd a = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 3. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c); (Inr (), s''e) \<in> fst (preemption_point s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B61 rv s'' rva s''a rvb s''b () s''c rvd s''d ()\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (exposed \<longrightarrow> snd a = NullCap) \<and> (fst a \<longrightarrow> snd a = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B59 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>?B61 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B57 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B59 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B57 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 6. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 8. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c); (Inr (), s''e) \<in> fst (preemption_point s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B61 rv s'' rva s''a rvb s''b () s''c rvd s''d ()\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q'64 rv s'' rva s''a rvb s''b s''c rvd s''d s''e\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d s''e s r. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed; ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c); (Inr (), s''e) \<in> fst (preemption_point s''d); ?Q'64 rv s'' rva s''a rvb s''b s''c rvd s''d s''e s r\<rbrakk> \<Longrightarrow> (exposed \<longrightarrow> snd s = NullCap) \<and> (fst s \<longrightarrow> snd s = NullCap) \<and> domain_sep_inv False sta r \<and> irq_state_inv st r
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B59 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>?B61 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B57 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B59 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B57 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 7. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 8. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 9. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); (Inr rvd, s''d) \<in> fst (rec_del (ReduceZombieCall (fst rvb) slot exposed) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B59 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>a b. irq_state_inv st b \<and> domain_sep_inv False sta b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B57 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B59 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B57 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 5. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B57 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rvd s. (irq_state_inv st and K (irq_is_recurring (?irq112 rv s'' rva s''a rvb s''b rvc s''c rvd) st)) s \<and> (irq_state_inv st and K (irq_is_recurring irq st)) s \<and> domain_sep_inv False sta s \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B57 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 4. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B57 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?Q'131 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); ?Q'131 rv s'' rva s''a rvb s''b rvc s''c s r\<rbrakk> \<Longrightarrow> (irq_state_inv st and K (irq_is_recurring (?irq112 rv s'' rva s''a rvb s''b rvc s''c s) st)) r \<and> (irq_state_inv st and K (irq_is_recurring irq st)) r \<and> domain_sep_inv False sta r \<and> irq_is_recurring irq st
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B57 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 5. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b)\<rbrakk> \<Longrightarrow> ((), s''c) \<in> fst (set_cap (fst rvb) slot s''b)
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c s r. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed); (Inr rvc, s''c) \<in> fst ((without_preemption $ set_cap (fst rvb) slot) s''b); domain_sep_inv False sta r \<and> irq_state_inv st r\<rbrakk> \<Longrightarrow> (irq_state_inv st and K (irq_is_recurring (?irq112 rv s'' rva s''a rvb s''b rvc s''c s) st)) r \<and> (irq_state_inv st and K (irq_is_recurring irq st)) r \<and> domain_sep_inv False sta r \<and> irq_is_recurring irq st
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (rvb, s''b) \<in> fst (finalise_cap rv rva s''a); \<not> cap_removeable (fst rvb) slot; \<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> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>rvc a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (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>?B14 rv s'' rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> (exposed \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> (fst (True, snd rvb) \<longrightarrow> snd (True, snd rvb) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (domain_sep_inv False sta and K (domain_sep_inv_cap False (fst rvb))) s \<and> irq_state_inv st 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>_. irq_state_next st\<rbrace>
 6. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'11 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B14 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> (exposed \<longrightarrow> snd (True, NullCap) = NullCap) \<and> (fst (True, NullCap) \<longrightarrow> snd (True, NullCap) = NullCap) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'11 rv s)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 8. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> domain_sep_inv_cap False cap proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a s. (case FinaliseSlotCall slot exposed of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<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>a s. domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv s. domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'19\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv s. domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. irq_state_inv st s \<and> domain_sep_inv False sta s \<and> irq_is_recurring irq st \<Longrightarrow> ?P'19 s proof (prove)
goal (1 subgoal):
 1. irq_state_inv st s \<and> domain_sep_inv False sta s \<and> irq_is_recurring irq st \<Longrightarrow> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv False sta s \<and> irq_state_inv st s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
this:
(Inr ?rv, ?st) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> ?st \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall ?rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv stb. (Inr rv, stb) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> stb \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>a s. (case CTEDeleteCall rv False of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace> doE y <- rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False);
new_cap <- liftE (get_cap slot);
y <- if new_cap = Zombie ptr bits (Suc n) then without_preemption $ set_cap (Zombie ptr bits n) slot else assertE (new_cap = NullCap \<or> is_zombie new_cap \<and> first_cslot_of new_cap = slot \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot);
returnOk undefined
odE \<lbrace>\<lambda>a s. domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. irq_state_inv st a \<and> domain_sep_inv False sta a \<and> irq_is_recurring irq st\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>rv s. \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> domain_sep_inv False sta s \<and> domain_sep_inv_cap False (Zombie ptr bits n) \<and> irq_state_inv st s) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv False sta s \<and> irq_state_inv st s) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv False sta s \<and> irq_state_inv st s))\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. (Inr (ptr, nat_to_cref (zombie_cte_bits bits) n), s) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s)
 2. \<And>s r. domain_sep_inv False sta r \<and> irq_state_inv st r \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> domain_sep_inv False sta r \<and> domain_sep_inv_cap False (Zombie ptr bits n) \<and> irq_state_inv st r) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv False sta r \<and> irq_state_inv st r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv False sta r \<and> irq_state_inv st r)) proof (prove)
goal (1 subgoal):
 1. \<And>s r. domain_sep_inv False sta r \<and> irq_state_inv st r \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> domain_sep_inv False sta r \<and> domain_sep_inv_cap False (Zombie ptr bits n) \<and> irq_state_inv st r) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv False sta r \<and> irq_state_inv st r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> domain_sep_inv False sta r \<and> irq_state_inv st r)) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>a s. (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of FinaliseSlotCall x y \<Rightarrow> y \<or> fst a \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal:
No subgoals!