theory Finalise_IF

lemma empty_slot_reads_respects:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "reads_respects aag l (K (aag_can_read aag (fst slot))) (empty_slot slot free_irq)" unfolding empty_slot_def post_cap_deletion_def fun_app_def apply (simp add: bind_assoc[symmetric] cong: if_cong) apply (fold update_cdt_def) apply (simp add: bind_assoc empty_slot_ext_def cong: if_cong) apply (rule gen_asm_ev) apply (wp deleted_irq_handler_reads_respects set_cap_reads_respects set_original_reads_respects
            update_cdt_list_reads_respects update_cdt_reads_respects get_cap_wp get_cap_rev
         | wpsimp
         | frule aag_can_read_self, fastforce simp: equiv_for_def split: option.splits)+ by (fastforce simp: reads_equiv_def2 equiv_for_def
                elim: states_equiv_forE_cdt
                dest: aag_can_read_self
               split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst slot))) (empty_slot slot free_irq) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst slot))) (do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return (cdt slot);
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
set_cap NullCap slot;
case free_irq of IRQHandlerCap irq \<Rightarrow> deleted_irq_handler irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return ()
od
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read aag (fst slot)) (do cap <- get_cap slot;
if cap = NullCap then return () else do y <- do y <- do y <- do slot_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None))
od;
empty_slot_ext slot slot_p
od;
set_original slot False
od;
set_cap NullCap slot
od;
case free_irq of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | ArchObjectCap x \<Rightarrow> arch_post_cap_deletion x | _ \<Rightarrow> return ()
od
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read aag (fst slot)) (do cap <- get_cap slot;
if cap = NullCap then return () else do y <- do y <- do y <- do slot_p <- gets (\<lambda>s. cdt s slot);
y <- update_cdt (\<lambda>cdt. (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
empty_slot_ext slot slot_p
od;
set_original slot False
od;
set_cap NullCap slot
od;
case free_irq of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | ArchObjectCap x \<Rightarrow> arch_post_cap_deletion x | _ \<Rightarrow> return ()
od
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read aag (fst slot)) (do cap <- get_cap slot;
if cap = NullCap then return () else do x <- gets (\<lambda>s. cdt s slot);
xa <- update_cdt (\<lambda>cdt. (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
x <- update_cdt_list (\<lambda>list. case x of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> if p = slot then list(slot := list_remove (list slot) slot) else list(p := list_replace_list (list p) slot (list slot), slot := []));
x <- set_original slot False;
y <- set_cap NullCap slot;
case free_irq of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | ArchObjectCap x \<Rightarrow> arch_post_cap_deletion x | _ \<Rightarrow> return ()
od
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag (fst slot) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do cap <- get_cap slot;
if cap = NullCap then return () else do x <- gets (\<lambda>s. cdt s slot);
xa <- update_cdt (\<lambda>cdt. (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
x <- update_cdt_list (\<lambda>list. case x of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> if p = slot then list(slot := list_remove (list slot) slot) else list(p := list_replace_list (list p) slot (list slot), slot := []));
x <- set_original slot False;
y <- set_cap NullCap slot;
case free_irq of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | ArchObjectCap x \<Rightarrow> arch_post_cap_deletion x | _ \<Rightarrow> return ()
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>aag_can_read aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cdt s slot = cdt t slot) \<and> (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)) rv rv') \<and> (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. case cdt s slot of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> if p = slot then list(slot := list_remove (list slot) slot) else list(p := list_replace_list (list p) slot (list slot), slot := [])) rv rv')