theory Finalise_IF

lemma rec_del_CTEDeleteCall_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_f aag l
     (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action
                      and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot
                      and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s))
     (rec_del (CTEDeleteCall slot exposed))" apply (cases "is_subject aag (fst slot)") apply (rule equiv_valid_guard_imp) apply (wp rec_del_reads_respects_f) apply fastforce apply (subst rec_del.simps[abs_def]) apply (wp when_ev reads_respects_f[OF empty_slot_reads_respects] empty_slot_silc_inv
            rec_del_Finalise_transferable_read_respects_f hoare_vcg_all_lift_R hoare_drop_impE_R
            rec_del_Finalise_transferableE_R
         | wpc | simp)+ apply clarsimp apply (frule(3) cca_can_read[OF invs_mdb invs_valid_objs]) apply (frule(2) cdt_change_allowed_not_silc[rotated 2], force, force) apply (frule(1) cca_to_transferable_or_subject[rotated 2], force, force) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (rec_del (CTEDeleteCall slot exposed)) proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (rec_del (CTEDeleteCall slot exposed))
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (rec_del (CTEDeleteCall slot exposed)) proof (prove)
goal (3 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> reads_respects_f aag l ?Q1 (rec_del (CTEDeleteCall slot exposed))
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (rec_del (CTEDeleteCall slot exposed)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) s\<rbrakk> \<Longrightarrow> (silc_inv aag ?st5 and only_timer_irq_inv ?irq5 ?st'5 and einvs and simple_sched_action and pas_refined aag and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall slot exposed) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (CTEDeleteCall slot exposed)) s) and K (case CTEDeleteCall slot exposed of CTEDeleteCall slot exposed \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot exposed \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot exposed \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))) s
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (rec_del (CTEDeleteCall slot exposed)) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (rec_del (CTEDeleteCall slot exposed)) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and cdt_change_allowed' aag slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)) (doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> emptyable slot s \<and> cdt_change_allowed' aag slot s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)\<rbrakk> \<Longrightarrow> silc_inv aag ?st86 s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s \<and> (\<forall>x xa. silc_inv aag (?st97 x xa) s) \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; emptyable slot s; cdt_change_allowed' aag slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s\<rbrakk> \<Longrightarrow> silc_inv aag ?st86 s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s \<and> (\<forall>x xa. silc_inv aag (?st97 x xa) s) \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; emptyable slot s; cdt_change_allowed' aag slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; aag_can_read aag (fst slot)\<rbrakk> \<Longrightarrow> silc_inv aag ?st86 s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s \<and> (\<forall>x xa. silc_inv aag (?st97 x xa) s) \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; emptyable slot s; cdt_change_allowed' aag slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> silc_inv aag ?st86 s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s \<and> (\<forall>x xa. silc_inv aag (?st97 x xa) s) \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; emptyable slot s; cdt_change_allowed' aag slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_subject aag (fst slot) \<or> is_transferable_in slot s\<rbrakk> \<Longrightarrow> silc_inv aag ?st86 s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s \<and> (\<forall>x xa. silc_inv aag (?st97 x xa) s) \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<and> is_transferable_in slot s proof (prove)
goal:
No subgoals!