theory FinalCaps

lemma cap_insert_silc_inv':
  "\<lbrace>silc_inv aag st and K (is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and>
                           cap_points_to_label aag cap (pasSubject aag))\<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 allI impI conjI) apply clarsimp apply (fastforce dest: silc_invD simp: intra_label_cap_def) apply (clarsimp simp: silc_inv_def) apply (fastforce dest!: silc_inv_all_children 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 (is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag))\<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 K (is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag))\<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> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag) \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<longrightarrow> (\<not> cap_points_to_label aag capa (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasSubject aag \<noteq> 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. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; \<not> cap_points_to_label aag capa (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest 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 (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 (pasSubject aag); silc_inv aag st s; is_subject aag (fst dest); is_subject aag (fst src); cap_points_to_label aag cap (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest 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 (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest 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. \<lbrakk>silc_inv aag st s \<and> is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> cap_points_to_label aag cap (pasSubject aag); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest 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:
No subgoals!