theory ArchFinalCaps

lemma perform_asid_control_invocation_silc_inv:
  notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
  shows
  "\<lbrace>silc_inv aag st and valid_aci blah and invs and K (authorised_asid_control_inv aag blah)\<rbrace>
   perform_asid_control_invocation blah
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) unfolding perform_asid_control_invocation_def apply (rule hoare_pre) apply (wp modify_wp cap_insert_silc_inv' retype_region_silc_inv[where sz=pageBits]
            set_cap_silc_inv get_cap_slots_holding_overlapping_caps[where st=st]
            delete_objects_silc_inv hoare_weak_lift_imp
         | wpc | simp )+ apply (clarsimp simp: authorised_asid_control_inv_def silc_inv_def valid_aci_def ptr_range_def page_bits_def) apply (rule conjI) apply (clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def asid_bits_def pageBits_def) apply (rule of_nat_inverse) apply simp apply (drule is_aligned_neg_mask_eq'[THEN iffD1, THEN sym]) apply (erule_tac t=x in ssubst) apply (simp add: mask_AND_NOT_mask) apply simp apply (simp add: p_assoc_help) apply (clarsimp simp: cap_points_to_label_def) apply (erule bspec) apply (fastforce intro: is_aligned_no_wrap' simp: blah) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_aci blah and invs and K (authorised_asid_control_inv aag blah)\<rbrace> perform_asid_control_invocation blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_asid_control_inv aag blah \<Longrightarrow> \<lbrace>silc_inv aag st and valid_aci blah and invs\<rbrace> perform_asid_control_invocation blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_asid_control_inv aag blah \<Longrightarrow> \<lbrace>silc_inv aag st and valid_aci blah and invs\<rbrace> case blah of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag blah \<Longrightarrow> \<lbrace>?Q2\<rbrace> case blah of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag blah; (silc_inv aag st and valid_aci blah and invs) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>authorised_asid_control_inv aag blah; silc_inv aag st s \<and> valid_aci blah s \<and> invs s\<rbrakk> \<Longrightarrow> \<forall>x a b aa ba xa. blah = MakePool x (a, b) (aa, ba) xa \<longrightarrow> xa && mask local.asid_low_bits = 0 \<longrightarrow> (\<forall>p\<in>ptr_range x page_bits. is_subject aag p) \<and> pasObjectAbs aag aa \<noteq> SilcLabel \<and> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>up_aligned_area x pageBits. is_subject aag x) \<and> is_subject aag a \<and> is_subject aag aa \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> range_cover x pageBits (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0)
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> unat (x && mask 12 >> 12) = 0
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (3 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> word_of_nat 0 = x && mask 12 >> 12
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> 0 < 2 ^ LENGTH(32)
 3. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (3 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> x && mask 12 >> 12 = 0
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> 0 < 2 ^ LENGTH(32)
 3. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (3 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None; x = x && ~~ mask 12\<rbrakk> \<Longrightarrow> x && mask 12 >> 12 = 0
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> 0 < 2 ^ LENGTH(32)
 3. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (3 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (x && ~~ mask 12) && mask 12 >> 12 = 0
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> 0 < 2 ^ LENGTH(32)
 3. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x 12; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..0xFFF + x}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x 12 idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 0x20000; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> 0 < 2 ^ LENGTH(32)
 2. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + 2 ^ pageBits - 1}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> (\<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x) \<and> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> cap_points_to_label aag (ArchObjectCap (ASIDPoolCap x xa)) (pasSubject aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; \<forall>x\<in>{x..x + (2 ^ pageBits - 1)}. is_subject aag x; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<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); invs s; blah = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; is_aligned x pageBits; cap_table_at (length b) a s; \<forall>asid. is_subject_asid aag asid; ex_cte_cap_wp_to is_cnode_cap (a, b) s; is_subject aag aa; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False x pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned xa local.asid_low_bits; xa < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of xa) = None\<rbrakk> \<Longrightarrow> x \<in> {x..x + (2 ^ pageBits - 1)} proof (prove)
goal:
No subgoals!