theory FinalCaps

lemma detype_silc_inv:
  "\<lbrace>silc_inv aag st and (K (\<forall>p\<in>S. is_subject aag p))\<rbrace>
   modify (detype S)
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (wp modify_wp) apply (clarsimp simp: silc_inv_def) apply (rule conjI, fastforce) apply (rule conjI) apply (clarsimp simp: slots_holding_overlapping_caps_def intra_label_cap_def
                         cap_points_to_label_def get_cap_cte_wp_at') apply (drule (1) cte_wp_at_eqD2) apply clarsimp apply (drule_tac x=a in spec, drule_tac x=b in spec, drule_tac x=cap in spec) apply simp apply (erule impE) apply fastforce apply (elim exE conjE, rename_tac la lb lcap) apply (rule_tac x=la in exI, simp, rule_tac x=lb in exI, rule_tac x=lcap in exI) apply simp apply fastforce apply (clarsimp simp: silc_dom_equiv_def equiv_for_def detype_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (\<forall>p\<in>S. is_subject aag p)\<rbrace> modify (detype S) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and K (\<forall>p\<in>S. is_subject aag p)) s \<Longrightarrow> silc_inv aag st (detype S s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> x \<notin> S) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> a \<notin> S \<and> \<not> intra_label_cap aag (a, b) (detype S s) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (detype S s)) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_dom_equiv aag st (detype S s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> a \<notin> S \<and> \<not> intra_label_cap aag (a, b) (detype S s) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (detype S s)) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> a \<notin> S \<and> \<not> intra_label_cap aag (a, b) (detype S s) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (detype S s)) \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> ((\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a))) \<longrightarrow> (\<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; cte_wp_at ((=) capa) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs capa. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs capa. pasIRQAbs aag x \<noteq> pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> ((\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a))) \<longrightarrow> (\<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) capa) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs capa. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs capa. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); capa = cap\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> ((\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a))) \<longrightarrow> (\<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); cte_wp_at ((=) cap) (a, b) s \<and> (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> ((\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a))) \<longrightarrow> (\<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> ((\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a))) \<longrightarrow> (\<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> ((\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a))
 2. \<And>s a b cap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb lcap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); pasObjectAbs aag la = SilcLabel; cte_wp_at ((=) lcap) (la, lb) s; cap_irqs cap \<inter> cap_irqs lcap = {} \<longrightarrow> obj_refs cap \<inter> obj_refs lcap = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs lcap \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b cap'. cte_wp_at ((=) cap') (a, b) s \<and> a \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb lcap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); pasObjectAbs aag la = SilcLabel; cte_wp_at ((=) lcap) (la, lb) s; cap_irqs cap \<inter> cap_irqs lcap = {} \<longrightarrow> obj_refs cap \<inter> obj_refs lcap = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs lcap \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) lcap) (la, lb) s \<and> la \<notin> S \<and> (cap_irqs cap \<inter> cap_irqs lcap = {} \<longrightarrow> obj_refs cap \<inter> obj_refs lcap = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs lcap \<noteq> {})
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb lcap. \<lbrakk>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; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p; cte_wp_at ((=) cap) (a, b) s; a \<notin> S; (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasObjectAbs aag a) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasObjectAbs aag a); pasObjectAbs aag la = SilcLabel; cte_wp_at ((=) lcap) (la, lb) s; cap_irqs cap \<inter> cap_irqs lcap = {} \<longrightarrow> obj_refs cap \<inter> obj_refs lcap = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs lcap \<noteq> {}\<rbrakk> \<Longrightarrow> la \<notin> S
 2. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>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>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) 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); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); \<forall>p\<in>S. is_subject aag p\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (detype S s) proof (prove)
goal:
No subgoals!