theory FinalCaps

lemma rec_del_silc_inv':
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
        drop_spec_ev[wp_split del] rec_del.simps[simp del]
  shows
  "s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call call
                        and emptyable (slot_rdcall call) and pas_refined aag
                        and K (case call of
                                 CTEDeleteCall slot _ \<Rightarrow> is_subject aag (fst slot) |
                                 FinaliseSlotCall slot _ \<Rightarrow> is_subject aag (fst slot) |
                                 ReduceZombieCall cap slot _ \<Rightarrow> is_subject aag (fst slot) \<and>
                                                                is_subject aag (obj_ref_of cap))\<rbrace>
       rec_del call
       \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" proof (induct s 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 (rule hoare_pre_spec_validE) apply (wp empty_slot_silc_inv drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp]
            | simp)+ apply (rule_tac Q'="\<lambda>_ s. silc_inv aag st s \<and> is_subject aag (fst slot)"
                 and E="\<lambda>_. silc_inv aag st"
                  in spec_strengthen_postE) apply (rule spec_valid_conj_liftE2) apply wp apply (rule "1.hyps"[simplified]) apply (simp | fastforce simp: silc_inv_def)+ done next case (2 slot exposed s) show ?case 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_silc_inv "2.hyps"
            | simp add: split_def split del: if_split)+ apply (rule drop_spec_validE, (wp preemption_point_inv'| simp)+)[1] apply simp apply (rule spec_valid_conj_liftE2) apply (wp rec_del_ReduceZombie_emptyable preemption_point_inv' rec_del_invs
                    valid_validE_R[OF rec_del_respects(2)[simplified]] "2.hyps"
                    drop_spec_validE[OF liftE_wp] set_cap_silc_inv
                    set_cap_pas_refined replace_cap_invs  final_cap_same_objrefs set_cap_cte_cap_wp_to
                    set_cap_cte_wp_at hoare_weak_lift_imp hoare_vcg_ball_lift
                 | simp add: finalise_cap_not_reply_master_unlifted split del: if_split)+ 
       (* where the action is *)
        apply (simp cong: conj_cong add: conj_comms) apply (rule hoare_strengthen_post) apply (rule_tac Q="\<lambda> fin s. pas_refined aag s \<and>
                                    replaceable s slot (fst fin) rv \<and>
                                    cte_wp_at ((=) rv) slot s \<and>
                                    ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and>
                                    (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s) \<and>
                                    einvs s \<and>
                                    silc_inv aag st s \<and>
                                    pasSubject aag \<noteq> SilcLabel \<and>
                                    emptyable slot s \<and> s \<turnstile> (fst fin) \<and>
                                    simple_sched_action s \<and>
                                    pas_cap_cur_auth aag (fst fin) \<and>
                                    is_subject aag (fst slot) \<and>
                                    (is_zombie (fst fin) \<or> fst fin = NullCap) \<and>
                                    (is_zombie (fst fin) \<longrightarrow> is_subject aag (obj_ref_of (fst fin))) \<and>
                                    (\<not> cap_points_to_label aag (fst fin) (pasObjectAbs aag (fst slot))
                                     \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst fin) s
                                               \<and> pasObjectAbs aag (fst slot) = SilcLabel))"
                     in hoare_vcg_conj_lift[OF _ finalise_cap_cases[where slot=slot]]) prefer 2 subgoal for cap s'' isfinal s' fin s0 apply (clarsimp simp: cte_wp_at_caps_of_state simp del:split_paired_Ex split_paired_All) apply (elim disjE; clarsimp simp: cte_wp_at_caps_of_state) apply (clarsimp simp: is_cap_simps gen_obj_refs_eq replaceable_zombie_not_transferable
                                cap_auth_conferred_def clas_no_asid aag_cap_auth_def
                                pas_refined_all_auth_is_owns cli_no_irqs
                      simp del: split_paired_Ex split_paired_All
                         dest!: appropriate_Zombie[symmetric, THEN trans, symmetric]) apply (fastforce dest: sym[where s="{_}"]) done apply (wp finalise_cap_pas_refined finalise_cap_silc_inv finalise_cap_auth' finalise_cap_ret'
                 finalise_cap_ret_is_subject' finalise_cap_ret_is_silc[where st=st]
                 finalise_cap_invs[where slot=slot]
                 finalise_cap_replaceable[where sl=slot]
                 finalise_cap_makes_halted[where slot=slot]
                 finalise_cap_auth' hoare_weak_lift_imp) apply (wp drop_spec_validE[OF liftE_wp] get_cap_auth_wp[where aag=aag]
             | simp add: is_final_cap_def)+ apply (clarsimp simp: conj_comms caps_of_state_cteD) apply (frule (1) caps_of_state_valid) apply (frule if_unsafe_then_capD [OF caps_of_state_cteD]; clarsimp) apply (rule conjI, clarsimp simp: silc_inv_def) apply (case_tac cap;
           simp add: is_zombie_def aag_cap_auth_CNode aag_cap_auth_Thread aag_cap_auth_Zombie;
           fastforce dest:caps_of_state_valid silc_inv_not_subject) 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]
              cap_swap_for_delete_silc_inv) apply (simp add: pred_conj_def) apply (rule hoare_pre_spec_validE) apply (rule spec_valid_conj_liftE2) apply (wp | simp)+ apply (wp drop_spec_validE[OF assertE_wp]) apply (fastforce simp: silc_inv_def) done next case (4 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] set_cap_silc_inv
              drop_spec_validE[OF assertE_wp] get_cap_wp | simp)+ apply (rule_tac Q'="\<lambda> _. silc_inv aag st and
                    K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)" in spec_strengthen_postE) prefer 2 apply (clarsimp) apply (drule silc_invD) apply assumption apply (simp add: intra_label_cap_def) apply (rule exI) apply (rule conjI) apply assumption apply (fastforce simp: cap_points_to_label_def) apply (clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (simp add: pred_conj_def) apply (rule hoare_pre_spec_validE) apply (wp spec_valid_conj_liftE2 "4.hyps") apply (simp add: in_monad) apply (fastforce simp: silc_inv_def cte_wp_at_caps_of_state zombie_ptr_emptyable) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call call and emptyable (slot_rdcall call) and pas_refined aag and K (case call of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del call \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and pas_refined aag and K (case CTEDeleteCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and pas_refined aag and K (case ReduceZombieCall (fst rvb) slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
this:
s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (4 subgoals):
 1. \<And>slot exposed s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and pas_refined aag and K (case CTEDeleteCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and pas_refined aag and K (case ReduceZombieCall (fst rvb) slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and pas_refined aag and K (case CTEDeleteCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot)\<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>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<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>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>a. if exposed \<or> fst a then silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) else silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_ s. silc_inv aag st s \<and> is_subject aag (fst slot)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s r. silc_inv aag st r \<and> is_subject aag (fst slot) \<Longrightarrow> (if exposed \<or> fst s then silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) else silc_inv aag st) r
 3. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P20\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv s. is_subject aag (fst slot)\<rbrace>, -
 2. s \<turnstile> \<lbrace>?P'20\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>s r. silc_inv aag st r \<and> is_subject aag (fst slot) \<Longrightarrow> (if exposed \<or> fst s then silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) else silc_inv aag st) r
 4. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P20 s \<and> ?P'20 s proof (prove)
goal (3 subgoals):
 1. s \<turnstile> \<lbrace>?P'20\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s r. silc_inv aag st r \<and> is_subject aag (fst slot) \<Longrightarrow> (if exposed \<or> fst s then silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) else silc_inv aag st) r
 3. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> is_subject aag (fst slot) \<and> ?P'20 s proof (prove)
goal (2 subgoals):
 1. \<And>s r. silc_inv aag st r \<and> is_subject aag (fst slot) \<Longrightarrow> (if exposed \<or> fst s then silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) else silc_inv aag st) r
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> is_subject aag (fst slot) \<and> silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and pas_refined aag and K (case CTEDeleteCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and pas_refined aag and K (case ReduceZombieCall (fst rvb) slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and pas_refined aag and K (case ReduceZombieCall (fst rvb) slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (fst ?rvb) slot exposed) and emptyable (slot_rdcall (ReduceZombieCall (fst ?rvb) slot exposed)) and pas_refined aag and K (case ReduceZombieCall (fst ?rvb) slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (fst ?rvb) slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (3 subgoals):
 1. \<And>slot exposed s. \<lbrakk>\<And>rv sta rva staa rvb stb rvc stc. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) stb)\<rbrakk> \<Longrightarrow> stc \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (fst rvb) slot exposed) and emptyable (slot_rdcall (ReduceZombieCall (fst rvb) slot exposed)) and pas_refined aag and K (case ReduceZombieCall (fst rvb) slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; \<And>rv sta rva staa rvb stb rvc stc rvd std rve ste. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); rv \<noteq> NullCap; (Inr rva, staa) \<in> fst ((without_preemption $ is_final_cap rv) sta); (Inr rvb, stb) \<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) 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot)\<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>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<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>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c rvd s''d. \<lbrakk>(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)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B52 rv s'' rva s''a rvb s''b () s''c rvd\<rbrace> preemption_point \<lbrace>\<lambda>rve a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(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>?B50 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>?B52 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(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'27 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B50 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<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 ((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> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'27 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(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>?B50 rv s'' rva s''a rvb s''b rvc\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a b. silc_inv aag st b \<and> silc_inv aag st b \<and> invs b \<and> valid_list b \<and> valid_sched b \<and> simple_sched_action b \<and> emptyable slot b \<and> pas_refined aag b \<and> is_subject aag (fst slot)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(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'27 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B50 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<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 ((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> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'27 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c. \<lbrakk>(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)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B50 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>a b. silc_inv aag st b \<and> invs b \<and> valid_list b \<and> valid_sched b \<and> simple_sched_action b \<and> emptyable slot b \<and> pas_refined aag b \<and> is_subject aag (fst slot)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(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'27 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>?B50 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<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 ((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> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'27 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b s''c. \<lbrakk>(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)\<rbrakk> \<Longrightarrow> \<lbrace>?P116 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv s. invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot)\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b s''c. \<lbrakk>(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)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'115 rv s'' rva s''a rvb s''b ()\<rbrace> rec_del (ReduceZombieCall (fst rvb) slot exposed) \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(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'27 rv s'' rva s''a rvb\<rbrace> without_preemption $ set_cap (fst rvb) slot \<lbrace>\<lambda>a b. ?P116 rv s'' rva s''a rvb s''b a b \<and> ?P'115 rv s'' rva s''a rvb s''b a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<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 ((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> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s) \<and> (\<not> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed) \<longrightarrow> ?P'27 rv s'' rva s''a rvb s))\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B12 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag (fst slot)) (fst rvb) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> is_subject aag (fst slot) \<and> (\<forall>x\<in>obj_refs_ac (fst rvb). is_subject aag x) \<and> is_subject aag (fst slot) \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag (fst slot)) (fst rvb) \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst rvb))))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B12 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (cap_cyclic_zombie (fst rvb) slot \<and> \<not> exposed \<longrightarrow> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag (fst slot)) (fst rvb) \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> (\<not> exposed \<longrightarrow> cte_wp_at (\<lambda>cap'. slot \<in> cte_refs cap' (interrupt_irq_node s) \<and> cap_irqs cap' = {} \<longrightarrow> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s) \<and> cap_irqs (fst rvb) = {}) slot s \<and> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s) \<and> is_subject aag (fst slot) \<and> (\<forall>x\<in>obj_refs_ac (fst rvb). is_subject aag x) \<and> is_subject aag (fst slot) \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> invs s \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> fst rvb \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> s \<turnstile> fst rvb \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> is_final_cap' (fst rvb) s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> is_zombie (fst rvb) \<and> emptyable slot s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag (fst slot)) (fst rvb) \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst rvb))))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B12 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. (cap_removeable (fst rvb) slot \<longrightarrow> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst rvb) slot \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s)))) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> invs s \<and> pas_refined aag s \<and> emptyable slot s \<and> is_zombie (fst rvb) \<and> simple_sched_action s \<and> silc_inv aag st s \<and> s \<turnstile> fst rvb \<and> is_final_cap' (fst rvb) s \<and> fst rvb \<noteq> NullCap \<and> pasSubject aag \<noteq> SilcLabel \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pas_cap_cur_auth aag (fst rvb) \<and> valid_list s \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst rvb)) \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> (\<forall>x\<in>obj_refs_ac (fst rvb). is_subject aag x) \<and> valid_sched s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> (\<not> cap_points_to_label aag (fst rvb) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s))) \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s \<and> cte_wp_at (\<lambda>cap'. cap_irqs cap' = {} \<and> slot \<in> cte_refs cap' (interrupt_irq_node s) \<longrightarrow> cap_irqs (fst rvb) = {} \<and> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s)) slot s)))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?B12 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>?Q465 rv s'' rva s''a\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); ?Q465 rv s'' rva s''a rvb s\<rbrakk> \<Longrightarrow> (cap_removeable (fst rvb) slot \<longrightarrow> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst rvb) slot \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s)))) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> invs s \<and> pas_refined aag s \<and> emptyable slot s \<and> is_zombie (fst rvb) \<and> simple_sched_action s \<and> silc_inv aag st s \<and> s \<turnstile> fst rvb \<and> is_final_cap' (fst rvb) s \<and> fst rvb \<noteq> NullCap \<and> pasSubject aag \<noteq> SilcLabel \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pas_cap_cur_auth aag (fst rvb) \<and> valid_list s \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst rvb)) \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> (\<forall>x\<in>obj_refs_ac (fst rvb). is_subject aag x) \<and> valid_sched s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> (\<not> cap_points_to_label aag (fst rvb) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s))) \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s \<and> cte_wp_at (\<lambda>cap'. cap_irqs cap' = {} \<and> slot \<in> cte_refs cap' (interrupt_irq_node s) \<longrightarrow> cap_irqs (fst rvb) = {} \<and> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s)) slot s)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>?B12 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P470 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>fin s. pas_refined aag s \<and> replaceable s slot (fst fin) rv \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s) \<and> einvs s \<and> silc_inv aag st s \<and> pasSubject aag \<noteq> SilcLabel \<and> emptyable slot s \<and> s \<turnstile> fst fin \<and> simple_sched_action s \<and> pas_cap_cur_auth aag (fst fin) \<and> is_subject aag (fst slot) \<and> (is_zombie (fst fin) \<or> fst fin = NullCap) \<and> (is_zombie (fst fin) \<longrightarrow> is_subject aag (obj_ref_of (fst fin))) \<and> (\<not> cap_points_to_label aag (fst fin) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst fin) s \<and> pasObjectAbs aag (fst slot) = SilcLabel))\<rbrace>
 2. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (pas_refined aag s \<and> replaceable s slot (fst rvb) rv \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (\<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s) \<and> einvs s \<and> silc_inv aag st s \<and> pasSubject aag \<noteq> SilcLabel \<and> emptyable slot s \<and> s \<turnstile> fst rvb \<and> simple_sched_action s \<and> pas_cap_cur_auth aag (fst rvb) \<and> is_subject aag (fst slot) \<and> (is_zombie (fst rvb) \<or> fst rvb = NullCap) \<and> (is_zombie (fst rvb) \<longrightarrow> is_subject aag (obj_ref_of (fst rvb))) \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst slot) = SilcLabel))) \<and> (fst rvb = NullCap \<and> snd rvb = (if rva then cap_cleanup_opt rv else NullCap) \<and> (snd rvb \<noteq> NullCap \<longrightarrow> is_final_cap' rv 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> (cap_removeable (fst rvb) slot \<longrightarrow> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst rvb) slot \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s)))) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> invs s \<and> pas_refined aag s \<and> emptyable slot s \<and> is_zombie (fst rvb) \<and> simple_sched_action s \<and> silc_inv aag st s \<and> s \<turnstile> fst rvb \<and> is_final_cap' (fst rvb) s \<and> fst rvb \<noteq> NullCap \<and> pasSubject aag \<noteq> SilcLabel \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pas_cap_cur_auth aag (fst rvb) \<and> valid_list s \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst rvb)) \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> (\<forall>x\<in>obj_refs_ac (fst rvb). is_subject aag x) \<and> valid_sched s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> (\<not> cap_points_to_label aag (fst rvb) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s))) \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s \<and> cte_wp_at (\<lambda>cap'. cap_irqs cap' = {} \<and> slot \<in> cte_refs cap' (interrupt_irq_node s) \<longrightarrow> cap_irqs (fst rvb) = {} \<and> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s)) slot s)))
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P470 rv s'' rva s \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s'' rva s''a rvb s. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s''); (pas_refined aag s \<and> replaceable s slot (fst rvb) rv \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (\<forall>t\<in>obj_refs (fst rvb). halted_if_tcb t s) \<and> einvs s \<and> silc_inv aag st s \<and> pasSubject aag \<noteq> SilcLabel \<and> emptyable slot s \<and> s \<turnstile> fst rvb \<and> simple_sched_action s \<and> pas_cap_cur_auth aag (fst rvb) \<and> is_subject aag (fst slot) \<and> (is_zombie (fst rvb) \<or> fst rvb = NullCap) \<and> (is_zombie (fst rvb) \<longrightarrow> is_subject aag (obj_ref_of (fst rvb))) \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst rvb) s \<and> pasObjectAbs aag (fst slot) = SilcLabel))) \<and> (fst rvb = NullCap \<and> snd rvb = (if rva then cap_cleanup_opt rv else NullCap) \<and> (snd rvb \<noteq> NullCap \<longrightarrow> is_final_cap' rv 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> (cap_removeable (fst rvb) slot \<longrightarrow> silc_inv aag st s) \<and> (\<not> cap_removeable (fst rvb) slot \<longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst rvb) slot \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s)))) \<and> ((cap_cyclic_zombie (fst rvb) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> invs s \<and> pas_refined aag s \<and> emptyable slot s \<and> is_zombie (fst rvb) \<and> simple_sched_action s \<and> silc_inv aag st s \<and> s \<turnstile> fst rvb \<and> is_final_cap' (fst rvb) s \<and> fst rvb \<noteq> NullCap \<and> pasSubject aag \<noteq> SilcLabel \<and> cte_wp_at (\<lambda>_. True) slot s \<and> pas_cap_cur_auth aag (fst rvb) \<and> valid_list s \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst rvb)) slot s \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst rvb)) \<and> cte_wp_at (replaceable s slot (fst rvb)) slot s \<and> (\<forall>x\<in>obj_refs (fst rvb). halted_if_tcb x s) \<and> (\<forall>x\<in>obj_refs_ac (fst rvb). is_subject aag x) \<and> valid_sched s \<and> cte_wp_at (\<lambda>c. obj_refs (fst rvb) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst rvb) \<inter> cap_irqs c \<noteq> {}) slot s \<and> (\<not> cap_points_to_label aag (fst rvb) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst rvb) s))) \<and> (is_transferable_in slot s \<and> \<not> Option.is_none (cdt s slot) \<longrightarrow> is_transferable_cap (fst rvb) \<or> (pasObjectAbs aag (fst (the (cdt s slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s \<and> cte_wp_at (\<lambda>cap'. cap_irqs cap' = {} \<and> slot \<in> cte_refs cap' (interrupt_irq_node s) \<longrightarrow> cap_irqs (fst rvb) = {} \<and> slot \<in> cte_refs (fst rvb) (interrupt_irq_node s)) slot s)))
 2. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P470 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>fin s. pas_refined aag s \<and> replaceable s slot (fst fin) rv \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s) \<and> einvs s \<and> silc_inv aag st s \<and> pasSubject aag \<noteq> SilcLabel \<and> emptyable slot s \<and> s \<turnstile> fst fin \<and> simple_sched_action s \<and> pas_cap_cur_auth aag (fst fin) \<and> is_subject aag (fst slot) \<and> (is_zombie (fst fin) \<or> fst fin = NullCap) \<and> (is_zombie (fst fin) \<longrightarrow> is_subject aag (obj_ref_of (fst fin))) \<and> (\<not> cap_points_to_label aag (fst fin) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst fin) s \<and> pasObjectAbs aag (fst slot) = SilcLabel))\<rbrace>
 3. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P470 rv s'' rva s \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cap, s'') \<in> fst (get_cap slot s); cap \<noteq> NullCap; (isfinal, s') \<in> fst (is_final_cap cap s''); (pas_refined aag s0 \<and> replaceable s0 slot (fst fin) cap \<and> cte_wp_at ((=) cap) slot s0 \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s0 \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s0) \<and> einvs s0 \<and> silc_inv aag st s0 \<and> pasSubject aag \<noteq> SilcLabel \<and> emptyable slot s0 \<and> s0 \<turnstile> fst fin \<and> simple_sched_action s0 \<and> pas_cap_cur_auth aag (fst fin) \<and> is_subject aag (fst slot) \<and> (is_zombie (fst fin) \<or> fst fin = NullCap) \<and> (is_zombie (fst fin) \<longrightarrow> is_subject aag (obj_ref_of (fst fin))) \<and> (\<not> cap_points_to_label aag (fst fin) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst fin) s0 \<and> pasObjectAbs aag (fst slot) = SilcLabel))) \<and> (fst fin = NullCap \<and> snd fin = (if isfinal then cap_cleanup_opt cap else NullCap) \<and> (snd fin \<noteq> NullCap \<longrightarrow> is_final_cap' cap s0) \<or> is_zombie (fst fin) \<and> is_final_cap' cap s0 \<and> is_final_cap' (fst fin) s0 \<and> snd fin = NullCap \<and> appropriate_cte_cap (fst fin) = appropriate_cte_cap cap \<and> cte_refs (fst fin) = cte_refs cap \<and> gen_obj_refs (fst fin) = gen_obj_refs cap \<and> obj_size (fst fin) = obj_size cap \<and> fst_cte_ptrs (fst fin) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None)\<rbrakk> \<Longrightarrow> (cap_removeable (fst fin) slot \<longrightarrow> silc_inv aag st s0) \<and> (\<not> cap_removeable (fst fin) slot \<longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst fin) slot \<longrightarrow> silc_inv aag st s0 \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (\<not> cap_points_to_label aag (fst fin) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0)))) \<and> ((cap_cyclic_zombie (fst fin) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s0 \<and> valid_vspace_objs s0 \<and> pspace_aligned s0 \<and> invs s0 \<and> pas_refined aag s0 \<and> emptyable slot s0 \<and> is_zombie (fst fin) \<and> simple_sched_action s0 \<and> silc_inv aag st s0 \<and> s0 \<turnstile> fst fin \<and> is_final_cap' (fst fin) s0 \<and> fst fin \<noteq> NullCap \<and> pasSubject aag \<noteq> SilcLabel \<and> cte_wp_at (\<lambda>_. True) slot s0 \<and> pas_cap_cur_auth aag (fst fin) \<and> valid_list s0 \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst fin)) slot s0 \<and> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of (fst fin)) \<and> cte_wp_at (replaceable s0 slot (fst fin)) slot s0 \<and> (\<forall>x\<in>obj_refs (fst fin). halted_if_tcb x s0) \<and> (\<forall>x\<in>obj_refs_ac (fst fin). is_subject aag x) \<and> valid_sched s0 \<and> cte_wp_at (\<lambda>c. obj_refs (fst fin) \<inter> obj_refs c = {} \<longrightarrow> cap_irqs (fst fin) \<inter> cap_irqs c \<noteq> {}) slot s0 \<and> (\<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0))) \<and> (is_transferable_in slot s0 \<and> \<not> Option.is_none (cdt s0 slot) \<longrightarrow> is_transferable_cap (fst fin) \<or> (pasObjectAbs aag (fst (the (cdt s0 slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s0 \<and> cte_wp_at (\<lambda>cap'. cap_irqs cap' = {} \<and> slot \<in> cte_refs cap' (interrupt_irq_node s0) \<longrightarrow> cap_irqs (fst fin) = {} \<and> slot \<in> cte_refs (fst fin) (interrupt_irq_node s0)) slot s0))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cap, s'') \<in> fst (get_cap slot s); cap \<noteq> NullCap; (isfinal, s') \<in> fst (is_final_cap cap s''); pas_refined aag s0; replaceable s0 slot (fst fin) cap; caps_of_state s0 slot = Some cap; ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s0; \<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s0; invs s0; valid_list s0; valid_sched s0; silc_inv aag st s0; pasSubject aag \<noteq> SilcLabel; emptyable slot s0; s0 \<turnstile> fst fin; simple_sched_action s0; pas_cap_cur_auth aag (fst fin); is_subject aag (fst slot); is_zombie (fst fin) \<or> fst fin = NullCap; is_zombie (fst fin) \<longrightarrow> is_subject aag (obj_ref_of (fst fin)); \<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst fin) s0 \<and> pasObjectAbs aag (fst slot) = SilcLabel); fst fin = NullCap \<and> snd fin = (if isfinal then cap_cleanup_opt cap else NullCap) \<and> (snd fin \<noteq> NullCap \<longrightarrow> is_final_cap' cap s0) \<or> is_zombie (fst fin) \<and> is_final_cap' cap s0 \<and> is_final_cap' (fst fin) s0 \<and> snd fin = NullCap \<and> appropriate_cte_cap (fst fin) = appropriate_cte_cap cap \<and> cte_refs (fst fin) = cte_refs cap \<and> gen_obj_refs (fst fin) = gen_obj_refs cap \<and> obj_size (fst fin) = obj_size cap \<and> fst_cte_ptrs (fst fin) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None; \<not> cap_removeable (fst fin) slot\<rbrakk> \<Longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst fin) slot \<longrightarrow> \<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0))) \<and> ((cap_cyclic_zombie (fst fin) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s0 \<and> valid_vspace_objs s0 \<and> pspace_aligned s0 \<and> is_zombie (fst fin) \<and> is_final_cap' (fst fin) s0 \<and> fst fin \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap (fst fin)) slot s0 \<and> is_subject aag (obj_ref_of (fst fin)) \<and> (\<forall>x\<in>obj_refs_ac (fst fin). is_subject aag x) \<and> (obj_refs (fst fin) \<inter> obj_refs cap = {} \<longrightarrow> cap_irqs (fst fin) \<inter> cap_irqs cap \<noteq> {}) \<and> (\<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0))) \<and> (is_transferable_cap cap \<and> \<not> Option.is_none (cdt s0 slot) \<longrightarrow> is_transferable_cap (fst fin) \<or> (pasObjectAbs aag (fst (the (cdt s0 slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s0 \<and> (cap_irqs cap = {} \<and> slot \<in> cte_refs cap (interrupt_irq_node s0) \<longrightarrow> cap_irqs (fst fin) = {} \<and> slot \<in> cte_refs (fst fin) (interrupt_irq_node s0)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cap, s'') \<in> fst (get_cap slot s); cap \<noteq> NullCap; (isfinal, s') \<in> fst (is_final_cap cap s''); pas_refined aag s0; replaceable s0 slot (fst fin) cap; caps_of_state s0 slot = Some cap; ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s0; \<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s0; invs s0; valid_list s0; valid_sched s0; silc_inv aag st s0; pasSubject aag \<noteq> SilcLabel; emptyable slot s0; s0 \<turnstile> fst fin; simple_sched_action s0; pas_cap_cur_auth aag (fst fin); is_subject aag (fst slot); is_subject aag (obj_ref_of (fst fin)); \<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0) \<and> pasObjectAbs aag a = SilcLabel); \<not> cap_removeable (fst fin) slot; is_zombie (fst fin); is_final_cap' cap s0; is_final_cap' (fst fin) s0; snd fin = NullCap; appropriate_cte_cap (fst fin) = appropriate_cte_cap cap; cte_refs (fst fin) = cte_refs cap; gen_obj_refs (fst fin) = gen_obj_refs cap; obj_size (fst fin) = obj_size cap; fst_cte_ptrs (fst fin) = fst_cte_ptrs cap; vs_cap_ref cap = None\<rbrakk> \<Longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (fst fin) slot \<longrightarrow> \<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0))) \<and> ((cap_cyclic_zombie (fst fin) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s0 \<and> valid_vspace_objs s0 \<and> pspace_aligned s0 \<and> fst fin \<noteq> NullCap \<and> (\<forall>x\<in>obj_refs_ac (fst fin). is_subject aag x) \<and> (obj_refs (fst fin) \<inter> obj_refs cap = {} \<longrightarrow> cap_irqs (fst fin) \<inter> cap_irqs cap \<noteq> {}) \<and> (\<not> cap_points_to_label aag (fst fin) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (fst fin) s0))) \<and> (is_transferable_cap cap \<and> \<not> Option.is_none (cdt s0 slot) \<longrightarrow> is_transferable_cap (fst fin) \<or> (pasObjectAbs aag (fst (the (cdt s0 slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>a. cap_irqs a = {}) slot s0 \<and> (cap_irqs cap = {} \<and> slot \<in> cte_refs cap (interrupt_irq_node s0) \<longrightarrow> cap_irqs (fst fin) = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>r b n. \<lbrakk>(cap, s'') \<in> fst (get_cap slot s); cap \<noteq> NullCap; (isfinal, s') \<in> fst (is_final_cap cap s''); pas_refined aag s0; replaceable s0 slot (Zombie r b n) cap; caps_of_state s0 slot = Some cap; ex_cte_cap_wp_to (\<lambda>cap. cap_irqs cap = {}) slot s0; \<forall>t\<in>obj_refs cap. halted_if_tcb t s0; invs s0; valid_list s0; valid_sched s0; silc_inv aag st s0; pasSubject aag \<noteq> SilcLabel; emptyable slot s0; s0 \<turnstile> Zombie r b n; simple_sched_action s0; is_subject aag (fst slot); is_subject aag r; \<not> cap_points_to_label aag (Zombie r b n) (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps (Zombie r b n) s0) \<and> pasObjectAbs aag a = SilcLabel); is_final_cap' cap s0; is_final_cap' (Zombie r b n) s0; snd fin = NullCap; cte_refs (Zombie r b n) = cte_refs cap; (case b of None \<Rightarrow> 0x200 | Some n \<Rightarrow> 2 ^ (cte_level_bits + n)) = obj_size cap; fst_cte_ptrs (Zombie r b n) = fst_cte_ptrs cap; vs_cap_ref cap = None; fst fin = Zombie r b n; (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag; {r} = obj_refs cap; {} = cap_irqs cap; {} = arch_gen_refs cap; appropriate_cte_cap cap = (\<lambda>cap. cap_irqs cap = {}); 0 < n; n = Suc 0 \<longrightarrow> (r, replicate (zombie_cte_bits b) False) \<noteq> slot\<rbrakk> \<Longrightarrow> (\<not> exposed \<and> cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> \<not> cap_points_to_label aag (Zombie r b n) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps (Zombie r b n) s0))) \<and> ((cap_cyclic_zombie (Zombie r b n) slot \<longrightarrow> exposed) \<longrightarrow> valid_arch_state s0 \<and> valid_vspace_objs s0 \<and> pspace_aligned s0 \<and> (\<forall>x\<in>obj_refs cap. is_subject aag x) \<and> obj_refs cap \<noteq> {} \<and> (\<not> cap_points_to_label aag (Zombie r b n) (pasSubject aag) \<longrightarrow> (\<exists>a. pasObjectAbs aag a = SilcLabel \<and> (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps (Zombie r b n) s0)))) proof (prove)
goal:
No subgoals! proof (prove)
goal (4 subgoals):
 1. \<And>rv s'' rva s''a. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); rv \<noteq> NullCap; (rva, s''a) \<in> fst (is_final_cap rv s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P470 rv s'' rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>fin s. pas_refined aag s \<and> replaceable s slot (fst fin) rv \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s) \<and> einvs s \<and> silc_inv aag st s \<and> pasSubject aag \<noteq> SilcLabel \<and> emptyable slot s \<and> s \<turnstile> fst fin \<and> simple_sched_action s \<and> pas_cap_cur_auth aag (fst fin) \<and> is_subject aag (fst slot) \<and> (is_zombie (fst fin) \<or> fst fin = NullCap) \<and> (is_zombie (fst fin) \<longrightarrow> is_subject aag (obj_ref_of (fst fin))) \<and> (\<not> cap_points_to_label aag (fst fin) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>slot. slot \<in> slots_holding_overlapping_caps (fst fin) s \<and> pasObjectAbs aag (fst slot) = SilcLabel))\<rbrace>
 2. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P470 rv s'' rva s \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. \<lbrakk>(Inr rv, s'') \<in> fst (liftE (get_cap slot) s); rv \<noteq> NullCap\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?P'9 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ((pas_refined aag and invs and valid_cap rv and K (pas_cap_cur_auth aag rv)) s \<and> (s \<turnstile> rv \<and> rva = is_final_cap' rv s \<and> valid_mdb s \<and> cte_wp_at ((=) rv) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs rv \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap rv \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s)) \<and> cte_wp_at ((=) rv) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s \<and> (invs and valid_cap rv and (\<lambda>s. rva = is_final_cap' rv s) and cte_wp_at ((=) rv) slot) s \<and> (invs and cte_wp_at ((=) rv) slot) s \<and> valid_list s \<and> (valid_sched and simple_sched_action) s \<and> (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag rv)) s \<and> pasSubject aag \<noteq> SilcLabel \<and> (emptyable slot and invs) s \<and> s \<turnstile> rv \<and> simple_sched_action s \<and> (pas_refined aag and K (pas_cap_cur_auth aag rv)) s \<and> is_subject aag (fst slot) \<and> True \<and> K (is_cnode_cap rv \<or> is_thread_cap rv \<or> is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv)) s \<and> (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at ((=) rv) slot and pas_refined aag and K (pas_cap_cur_auth aag rv)) s) \<and> (rva \<longrightarrow> is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. s \<turnstile> \<lbrace>?P'\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> silc_inv aag st s) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'9 rv s)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> \<forall>cap. caps_of_state s slot = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> s \<turnstile> cap \<and> valid_mdb s \<and> cte_wp_at ((=) cap) slot s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_arch_caps s) \<and> cte_wp_at ((=) cap) slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) slot s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> pasSubject aag \<noteq> SilcLabel \<and> s \<turnstile> cap \<and> (is_cnode_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_thread_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> cte_wp_at ((=) cap) slot s \<and> (is_final_cap' cap s \<longrightarrow> cte_wp_at ((=) cap) slot s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; pas_refined aag s; emptyable slot s; simple_sched_action s; silc_inv aag st s; valid_list s; is_subject aag (fst slot); valid_sched s; pas_cap_cur_auth aag cap; caps_of_state s slot = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> s \<turnstile> cap \<and> pasSubject aag \<noteq> SilcLabel \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s \<and> (is_cnode_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_thread_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> valid_arch_caps s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; pas_refined aag s; emptyable slot s; simple_sched_action s; silc_inv aag st s; valid_list s; is_subject aag (fst slot); valid_sched s; pas_cap_cur_auth aag cap; caps_of_state s slot = Some cap; cap \<noteq> NullCap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> s \<turnstile> cap \<and> pasSubject aag \<noteq> SilcLabel \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s \<and> (is_cnode_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_thread_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> valid_arch_caps s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; pas_refined aag s; emptyable slot s; simple_sched_action s; silc_inv aag st s; valid_list s; is_subject aag (fst slot); valid_sched s; pas_cap_cur_auth aag cap; caps_of_state s slot = Some cap; cap \<noteq> NullCap; s \<turnstile> cap; ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s\<rbrakk> \<Longrightarrow> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> pasSubject aag \<noteq> SilcLabel \<and> (is_cnode_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_thread_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> valid_arch_caps s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; pas_refined aag s; emptyable slot s; simple_sched_action s; silc_inv aag st s; valid_list s; is_subject aag (fst slot); valid_sched s; pas_cap_cur_auth aag cap; caps_of_state s slot = Some cap; cap \<noteq> NullCap; s \<turnstile> cap; ex_cte_cap_wp_to (appropriate_cte_cap cap) slot s\<rbrakk> \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> pasSubject aag \<noteq> SilcLabel \<and> (is_cnode_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_thread_cap cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap)) \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s) \<and> (is_arch_cap cap \<longrightarrow> valid_arch_caps s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> pspace_aligned s) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot exposed) and emptyable (slot_rdcall (FinaliseSlotCall slot exposed)) and pas_refined aag and K (case FinaliseSlotCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
this:


goal (2 subgoals):
 1. \<And>ptr bits n slot s. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<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>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv. silc_inv aag st and K (pasObjectAbs aag (fst (ptr, replicate (zombie_cte_bits bits) False)) = pasObjectAbs aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv x. silc_inv aag st x \<and> pasObjectAbs aag ptr = pasObjectAbs aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'11\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv x. silc_inv aag st x \<and> pasObjectAbs aag ptr = pasObjectAbs aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> ?P'11 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P14\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv s. pasObjectAbs aag ptr = pasObjectAbs aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>, -
 2. s \<turnstile> \<lbrace>?P'14\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> ?P14 s \<and> ?P'14 s proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'14\<rbrace> assertE ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot) \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> pasObjectAbs aag ptr = pasObjectAbs aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> ?P'14 s proof (prove)
goal (1 subgoal):
 1. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> pasObjectAbs aag ptr = pasObjectAbs aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> ((ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> silc_inv aag st s) proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag 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>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall ?rv False) and emptyable (slot_rdcall (CTEDeleteCall ?rv False)) and pas_refined aag and K (case CTEDeleteCall ?rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall ?rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (1 subgoal):
 1. \<And>ptr bits n slot s. (\<And>rv sta. (Inr rv, sta) \<in> fst (returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n) s) \<Longrightarrow> sta \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall rv False) and emptyable (slot_rdcall (CTEDeleteCall rv False)) and pas_refined aag and K (case CTEDeleteCall rv False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (CTEDeleteCall rv False) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<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>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<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> (\<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> silc_inv aag st s))\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s r. (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) r \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st r \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> silc_inv aag st r)) proof (prove)
goal (2 subgoals):
 1. \<And>s r. (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) r \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot r \<longrightarrow> (cap = Zombie ptr bits (Suc n) \<longrightarrow> (\<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_inv aag st r \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (cap \<noteq> Zombie ptr bits (Suc n) \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st r) \<and> (is_zombie cap \<and> first_cslot_of cap = slot \<and> (ptr, replicate (zombie_cte_bits bits) False) \<noteq> slot \<longrightarrow> silc_inv aag st r))
 2. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>silc_inv aag st r; pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 2. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap35 r)) (?slot35 r) r
 2. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot35 r) r
 3. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap35 r) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 4. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot r
 2. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (Zombie ptr bits (Suc n)) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 3. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) slot r \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
 2. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (Zombie ptr bits (Suc n)) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 3. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap39 r)) slot r \<and> \<not> cap_points_to_label aag (?cap39 r) (pasObjectAbs aag (fst slot))
 2. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (Zombie ptr bits (Suc n)) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 3. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap39 r)) slot r
 2. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (?cap39 r) (pasObjectAbs aag (fst slot))
 3. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (Zombie ptr bits (Suc n)) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 4. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (Zombie ptr bits (Suc n)) (pasObjectAbs aag (fst slot))
 2. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (Zombie ptr bits (Suc n)) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 3. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot r; \<not> cap_points_to_label aag (Zombie ptr bits n) (pasObjectAbs aag (fst slot)); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (Zombie ptr bits (Suc n)) r \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (Zombie ptr bits n) r) \<and> pasObjectAbs aag a = SilcLabel
 2. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_. silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>a. silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot a \<and> is_final_cap' (Zombie ptr bits (Suc n)) a \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot a \<and> pas_refined aag a \<and> is_subject aag (fst slot) \<and> is_subject aag ptr\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_ x. silc_inv aag st x \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'47\<rbrace> rec_del (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) \<lbrace>\<lambda>_ x. silc_inv aag st x \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> ?P'47 s 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. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) and emptyable (slot_rdcall (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False)) and pas_refined aag and K (case CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))) s proof (prove)
goal (1 subgoal):
 1. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cte_wp_at ((=) (Zombie ptr bits (Suc n))) slot s \<and> is_final_cap' (Zombie ptr bits (Suc n)) s \<and> is_zombie (Zombie ptr bits (Suc n)) \<and> emptyable slot s \<and> pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr \<Longrightarrow> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> (silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False) and emptyable (slot_rdcall (CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False)) and pas_refined aag and K (case CTEDeleteCall (ptr, nat_to_cref (zombie_cte_bits bits) n) False of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))) s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) and emptyable (slot_rdcall (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True)) and pas_refined aag and K (case ReduceZombieCall (Zombie ptr bits (Suc n)) slot True of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))\<rbrace> rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal:
No subgoals!