theory FinalCaps

lemma cap_insert_silc_inv''':
  "\<lbrace>silc_inv aag st and (\<lambda> s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest))
                              \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                                           pasObjectAbs aag (fst lslot) = SilcLabel))
                    and K (pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and>
                           pasObjectAbs aag (fst dest) \<noteq> SilcLabel)\<rbrace>
   cap_insert cap src dest
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cap_insert_def apply (wp set_cap_silc_inv hoare_vcg_ex_lift
            set_untyped_cap_as_full_slots_holding_overlapping_caps_other[where aag=aag]
            get_cap_wp update_cdt_silc_inv set_cap_caps_of_state2
            set_untyped_cap_as_full_cdt_is_original_cap hoare_weak_lift_imp
         | simp split del: if_split)+ apply (intro impI conjI allI) apply clarsimp apply (fastforce simp: silc_inv_def) apply clarsimp apply (drule_tac cap=capa in silc_invD) apply assumption apply (fastforce simp: intra_label_cap_def) apply fastforce apply (elim conjE) apply (drule silc_inv_all_children) apply (simp add: all_children_def del: split_paired_All) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel)\<rbrace> do src_cap <- get_cap src;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap dest;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap cap src;
set_cap cap dest;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src) cap dest_original;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
update_cdt (\<lambda>cdt. cdt(dest := if src_parent then Some src else cdt src));
do_extended_op (cap_insert_ext src_parent src dest src_p dest_p);
set_original dest dest_original
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> capb = NullCap \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst src) \<and> pasObjectAbs aag a = SilcLabel)) \<and> (capb = NullCap \<longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a))) proof (prove)
goal (3 subgoals):
 1. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)); capaa = NullCap\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst src) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)); silc_inv aag st s; pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel; pasObjectAbs aag a = SilcLabel; (a, b) \<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 src) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); silc_inv aag st s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (4 subgoals):
 1. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> cte_wp_at ((=) capa) (?slot159 s capa) s
 2. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot159 s capa) s
 3. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag src s
 2. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst src)); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa. \<lbrakk>silc_inv aag st s \<and> (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel; cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap; silc_inv aag st s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) capaa) dest s; capaa = NullCap; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel; 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 = dest then if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa. \<lbrakk>cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; capaa = NullCap; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) \<noteq> SilcLabel; pasObjectAbs aag (fst dest) \<noteq> SilcLabel; \<forall>c p. cdt s c = Some p \<longrightarrow> pasObjectAbs aag (fst p) = SilcLabel \<longrightarrow> pasObjectAbs aag (fst c) = SilcLabel\<rbrakk> \<Longrightarrow> \<not> should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) \<longrightarrow> (\<forall>p. cdt s src = Some p \<longrightarrow> pasObjectAbs aag (fst p) \<noteq> SilcLabel) proof (prove)
goal:
No subgoals!