theory FinalCaps

lemma cap_move_silc_inv:
  "\<lbrace>silc_inv aag st 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_move cap slot slot'
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) unfolding cap_move_def apply (rule hoare_pre) apply (wp set_cap_silc_inv hoare_vcg_ex_lift
            set_cap_slots_holding_overlapping_caps_other[where aag=aag]
            set_cdt_silc_inv hoare_weak_lift_imp
        | simp)+ apply (rule conjI) apply (fastforce simp: cap_points_to_label_def) 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 (elim conjE) 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 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_move cap slot 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\<rbrace> cap_move cap slot 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\<rbrace> do set_cap cap slot';
set_cap NullCap slot;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
parent <- return $ cdt slot;
cdt' <- return $ cdt(slot' := parent, slot := None);
set_cdt (\<lambda>r. if cdt' r = Some slot then Some slot' else cdt' r);
do_extended_op (cap_move_ext slot slot' src_p dest_p);
is_original <- gets is_original_cap;
set_original slot' (is_original slot);
set_original slot False
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 NullCap slot;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s slot');
cdt <- gets cdt;
parent <- return $ cdt slot;
cdt' <- return $ cdt(slot' := parent, slot := None);
set_cdt (\<lambda>r. if cdt' r = Some slot then Some slot' else cdt' r);
do_extended_op (cap_move_ext slot slot' src_p dest_p);
is_original <- gets is_original_cap;
set_original slot' (is_original slot);
set_original slot False
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) 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\<rbrakk> \<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 \<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>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<rbrakk> \<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 \<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\<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>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<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>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<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; 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
 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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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; 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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<rbrakk> \<Longrightarrow> silc_inv aag (?st104 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\<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; \<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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<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; \<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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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; \<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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) 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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>r. if (if r = slot then None else if r = slot' then cdt s slot else cdt s r) = Some slot then Some slot' else if r = slot then None else if r = slot' then cdt s slot else cdt s r) proof (prove)
goal:
No subgoals!