theory Noninterference

lemma silc_dom_equiv_from_silc_inv_valid':
  assumes "\<And>st. \<lbrace>P and silc_inv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
  shows "\<lbrace>P and silc_inv aag st and silc_dom_equiv aag sta\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>" apply (rule hoare_pre) apply (rule hoare_strengthen_post) apply (rule assms) apply (fastforce simp: silc_inv_def) 
    (* we can't use clarsimp below because it splits pairs unconditionally *)
   apply (simp add: silc_inv_def silc_dom_equiv_def del: split_paired_All) apply (elim conjE) apply (intro allI impI notI) apply (drule(1) equiv_forD)+ apply (frule(1) cte_wp_at_pspace'[THEN iffD1]) apply (drule spec, drule(1) mp, erule notE, erule(1) cte_wp_at_pspace'[THEN iffD2]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and silc_inv aag st and silc_dom_equiv aag sta\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 2. \<And>s. (P and silc_inv aag st and silc_dom_equiv aag sta) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> silc_dom_equiv aag sta s
 3. \<And>s. (P and silc_inv aag st and silc_dom_equiv aag sta) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. silc_inv aag ?st6 s \<Longrightarrow> silc_dom_equiv aag sta s
 2. \<And>s. (P and silc_inv aag st and silc_dom_equiv aag sta) s \<Longrightarrow> (P and silc_inv aag ?st6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and silc_inv aag st and silc_dom_equiv aag sta) s \<Longrightarrow> (P and silc_inv aag sta) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and silc_inv aag st and silc_dom_equiv aag sta) s \<Longrightarrow> (P and silc_inv aag sta) s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<and> SilcLabel \<noteq> pasSubject aag \<and> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s)) \<and> (\<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel) \<and> (\<forall>slot cap. cte_wp_at ((=) cap) slot s \<and> \<not> intra_label_cap aag slot s \<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) (cdt s) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s \<and> (\<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap sta s \<Longrightarrow> \<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot sta proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>slot cap. cte_wp_at ((=) cap) slot s \<and> \<not> intra_label_cap aag slot s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s; \<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap sta s\<rbrakk> \<Longrightarrow> \<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot sta proof (prove)
goal (1 subgoal):
 1. \<And>s slot. \<lbrakk>P s; SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>slot cap. cte_wp_at ((=) cap) slot s \<and> \<not> intra_label_cap aag slot s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s; \<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap sta s; pasObjectAbs aag (fst slot) = SilcLabel; cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot sta\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s slot. \<lbrakk>P s; SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>slot cap. cte_wp_at ((=) cap) slot s \<and> \<not> intra_label_cap aag slot s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); \<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st; pasObjectAbs aag (fst slot) = SilcLabel; cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot sta; kheap st (fst slot) = kheap s (fst slot); kheap sta (fst slot) = kheap s (fst slot)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s slot. \<lbrakk>P s; SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>slot cap. cte_wp_at ((=) cap) slot s \<and> \<not> intra_label_cap aag slot s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); \<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st; pasObjectAbs aag (fst slot) = SilcLabel; cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot sta; kheap st (fst slot) = kheap s (fst slot); kheap sta (fst slot) = kheap s (fst slot); cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!