theory FinalCaps

lemma empty_slot_silc_inv:
  "\<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>
   empty_slot slot free_irq
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding empty_slot_def post_cap_deletion_def apply (wp set_cap_silc_inv hoare_vcg_all_lift hoare_vcg_ex_lift
            slots_holding_overlapping_caps_lift get_cap_wp
            set_cdt_silc_inv dxo_wp_weak hoare_drop_imps
         | wpc | simp del: empty_slot_extended.dxo_eq)+ apply (clarsimp simp: cap_points_to_label_def) apply (drule silc_inv_all_children) apply (fastforce simp: all_children_def simp del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace> empty_slot slot free_irq \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace> 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 \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) \<and> (\<not> cap_points_to_label aag NullCap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) ((\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)) proof (prove)
goal:
No subgoals!