theory FinalCaps

lemma checked_cap_insert_silc_inv:
  "\<lbrace>silc_inv aag st and K (is_subject aag (fst b) \<and> is_subject aag (fst e))\<rbrace>
   check_cap_at a b (check_cap_at c d (cap_insert a b e))
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (wp cap_insert_silc_inv'' get_cap_wp | simp add: check_cap_at_def)+ apply clarsimp apply (drule_tac cap=cap in silc_invD) apply assumption apply (clarsimp simp: intra_label_cap_def) apply (fastforce dest: same_object_as_cap_points_to_label) apply (fastforce dest: same_object_as_slots_holding_overlapping_caps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag (fst b) \<and> is_subject aag (fst e))\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<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 b) \<and> is_subject aag (fst e) \<Longrightarrow> \<forall>cap. same_object_as a cap \<longrightarrow> cte_wp_at ((=) cap) b s \<longrightarrow> (\<forall>cap. same_object_as c cap \<longrightarrow> cte_wp_at ((=) cap) d s \<longrightarrow> \<not> cap_points_to_label aag a (pasSubject aag) \<longrightarrow> (\<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s) \<and> pasObjectAbs aag aa = SilcLabel)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>silc_inv aag st s; is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s) \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (?slot34 s cap capa) s
 2. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot34 s cap capa) s
 3. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s) \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag b s
 2. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s) \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) b s \<and> \<not> cap_points_to_label aag cap (pasSubject aag)
 2. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s) \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>is_subject aag (fst b); is_subject aag (fst e); same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; \<not> cap_points_to_label aag a (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>b. (aa, b) \<in> slots_holding_overlapping_caps a s) \<and> pasObjectAbs aag aa = SilcLabel proof (prove)
goal:
No subgoals!