theory FinalCaps

lemma cap_swap_silc_inv:
  "\<lbrace>silc_inv aag st and cte_wp_at (weak_derived cap) slot and
        cte_wp_at (weak_derived cap') slot' and
        K(pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and>
         pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace>
      cap_swap cap slot cap' slot'
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) unfolding cap_swap_def apply (rule hoare_pre) apply (wp set_cap_silc_inv hoare_vcg_ex_lift hoare_weak_lift_imp
            set_cap_slots_holding_overlapping_caps_other[where aag=aag] set_cdt_silc_inv
        | simp  split del: if_split)+ apply (rule conjI) apply (rule impI, elim conjE) apply (drule weak_derived_overlaps) apply (erule nonempty_refs) apply (drule overlapping_slots_have_labelled_overlapping_caps) apply assumption apply simp apply fastforce apply (rule conjI) apply (rule impI, elim conjE) apply (drule weak_derived_overlaps, erule nonempty_refs) apply (drule overlapping_slots_have_labelled_overlapping_caps) apply assumption apply simp apply fastforce apply (elim conjE) apply (drule silc_inv_all_children) apply simp apply (intro impI conjI) by (fastforce simp: all_children_def simp del: split_paired_All
     | simp add: all_children_def del: split_paired_All)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and cte_wp_at (weak_derived cap) slot and cte_wp_at (weak_derived cap') slot' and K (pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace> cap_swap cap slot cap' slot' \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel \<Longrightarrow> \<lbrace>silc_inv aag st and cte_wp_at (weak_derived cap) slot and cte_wp_at (weak_derived cap') slot'\<rbrace> cap_swap cap slot cap' slot' \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel \<Longrightarrow> \<lbrace>silc_inv aag st and cte_wp_at (weak_derived cap) slot and cte_wp_at (weak_derived cap') slot'\<rbrace> do set_cap cap' slot;
set_cap cap slot';
slot1_p <- gets (\<lambda>s. cdt s slot);
slot2_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some slot then Some slot' else if cdt n = Some slot' then Some slot else cdt n);
set_cdt (cdt'(slot := cdt' slot', slot' := cdt' slot));
do_extended_op (cap_swap_ext slot slot' slot1_p slot2_p);
is_original <- gets is_original_cap;
set_original slot (is_original slot');
set_original slot' (is_original slot)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel \<Longrightarrow> \<lbrace>?Q2\<rbrace> do set_cap cap' slot;
set_cap cap slot';
slot1_p <- gets (\<lambda>s. cdt s slot);
slot2_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some slot then Some slot' else if cdt n = Some slot' then Some slot else cdt n);
set_cdt (cdt'(slot := cdt' slot', slot' := cdt' slot));
do_extended_op (cap_swap_ext slot slot' slot1_p slot2_p);
is_original <- gets is_original_cap;
set_original slot (is_original slot');
set_original slot' (is_original slot)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; (silc_inv aag st and cte_wp_at (weak_derived cap) slot and cte_wp_at (weak_derived cap') slot') s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}
 2. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s; slot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s; slot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> silc_inv aag (?st107 s) s
 2. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
 3. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
 2. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap') slot' s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; slot' \<in> slots_holding_overlapping_caps cap' s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s\<rbrakk> \<Longrightarrow> silc_inv aag (?st132 s) s
 2. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot'))
 3. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot'))
 2. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot')); pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap' s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s \<and> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; silc_inv aag st s; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then if cdt s slot = Some slot then Some slot' else if cdt s slot = Some slot' then Some slot else cdt s slot else if a = slot then if cdt s slot' = Some slot then Some slot' else if cdt s slot' = Some slot' then Some slot else cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> (cdt s slot' = Some slot' \<longrightarrow> (slot' = slot \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then Some slot else cdt s a)) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then cdt s slot else cdt s a))) \<and> (slot' \<noteq> slot \<longrightarrow> (cdt s slot = Some slot' \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else if a = slot then Some slot else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)) \<and> (cdt s slot \<noteq> Some slot' \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot' else if a = slot then Some slot else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else if a = slot then Some slot else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a))))) \<and> (cdt s slot' \<noteq> Some slot' \<longrightarrow> (cdt s slot' = Some slot \<longrightarrow> (cdt s slot = Some slot' \<longrightarrow> (slot' = slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then Some slot else cdt s a)) \<and> (slot' \<noteq> slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else if a = slot then Some slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a))) \<and> (cdt s slot \<noteq> Some slot' \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot' else if a = slot then Some slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else if a = slot then Some slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)))) \<and> (cdt s slot' \<noteq> Some slot \<longrightarrow> (cdt s slot = Some slot' \<longrightarrow> (slot' = slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then Some slot else cdt s a)) \<and> (slot' \<noteq> slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else if a = slot then cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a))) \<and> (cdt s slot \<noteq> Some slot' \<longrightarrow> (cdt s slot = Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot' else if a = slot then cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)) \<and> (cdt s slot \<noteq> Some slot \<longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else if a = slot then cdt s slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a))))) proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' = Some slot'; slot' = slot; cdt s slot = Some slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then Some slot else cdt s a)
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' = Some slot'; slot' = slot; cdt s slot \<noteq> Some slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then cdt s slot else cdt s a)
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' = Some slot'; slot' \<noteq> slot; cdt s slot = Some slot'\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else if a = slot then Some slot else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)
 4. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' = Some slot'; slot' \<noteq> slot; cdt s slot \<noteq> Some slot'; cdt s slot = Some slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot' else if a = slot then Some slot else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)
 5. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' = Some slot'; slot' \<noteq> slot; cdt s slot \<noteq> Some slot'; cdt s slot \<noteq> Some slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else if a = slot then Some slot else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)
 6. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' \<noteq> Some slot'; cdt s slot' = Some slot; cdt s slot = Some slot'; slot' = slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then Some slot else cdt s a)
 7. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' \<noteq> Some slot'; cdt s slot' = Some slot; cdt s slot = Some slot'; slot' \<noteq> slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else if a = slot then Some slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)
 8. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' \<noteq> Some slot'; cdt s slot' = Some slot; cdt s slot \<noteq> Some slot'; cdt s slot = Some slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot' else if a = slot then Some slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)
 9. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' \<noteq> Some slot'; cdt s slot' = Some slot; cdt s slot \<noteq> Some slot'; cdt s slot \<noteq> Some slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else if a = slot then Some slot' else if cdt s a = Some slot then Some slot' else if cdt s a = Some slot' then Some slot else cdt s a)
 10. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at (weak_derived cap) slot s; cte_wp_at (weak_derived cap') slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); cdt s slot' \<noteq> Some slot'; cdt s slot' \<noteq> Some slot; cdt s slot = Some slot'; slot' = slot\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot then Some slot else cdt s a)
A total of 13 subgoals...