theory FinalCaps

lemma retype_region_silc_inv:
  "\<lbrace>silc_inv aag st and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and>
                           (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace>
   retype_region ptr num_objects o_bits type dev
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp only: retype_region_def retype_addrs_def
                   foldr_upd_app_if fun_app_def K_bind_def) apply (wp modify_wp dxo_wp_weak | simp)+ apply (simp add: trans_state_update[symmetric] del: trans_state_update) apply wp+ apply (clarsimp simp: not_less) apply (clarsimp simp add: silc_inv_def) apply (intro conjI impI allI) apply (fastforce simp: obj_at_def silc_inv_def
                     dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
                     simp: image_def p_assoc_help power_sub) defer apply (fastforce simp: silc_dom_equiv_def equiv_for_def silc_inv_def
                    dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
                    simp: image_def p_assoc_help power_sub) apply (case_tac "a \<in> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) `
                         {0..<num_objects}") apply clarsimp apply (subgoal_tac "cap = NullCap") apply (clarsimp simp: intra_label_cap_def cap_points_to_label_def) apply (drule (1) cte_wp_at_eqD2) apply fastforce apply (erule cte_wp_atE) subgoal by (fastforce simp: default_object_def empty_cnode_def
                         split: apiobject_type.splits if_splits) subgoal by (clarsimp simp: default_object_def default_tcb_def tcb_cap_cases_def
                       split: apiobject_type.splits if_splits) apply (subgoal_tac "cte_wp_at ((=) cap) (a,b) s \<and> \<not> intra_label_cap aag (a,b) s") apply (drule_tac x=a in spec, drule_tac x=b in spec, drule_tac x=cap in spec, simp) apply (elim exE conjE, rename_tac la lb) apply (rule_tac x=la in exI, simp, rule_tac x=lb in exI) apply (simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (subgoal_tac "la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) `
                          {0..<num_objects}") apply (erule_tac t="(la,lb)" in cte_wp_atE) apply (rule cte_wp_at_cteI) apply fastforce apply assumption apply assumption apply assumption apply (rule cte_wp_at_tcbI) apply fastforce apply assumption apply assumption subgoal by (fastforce simp: silc_inv_def
                         dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
                         simp: image_def p_assoc_help power_sub) apply (rule conjI) subgoal by (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) apply (clarsimp simp: intra_label_cap_def cap_points_to_label_def) apply (drule (1) cte_wp_at_eqD2) apply (rule_tac x=capa in exI) apply clarsimp by (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x))\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> do obj_size <- return (2 ^ obj_bits_api type o_bits);
ptrs <- return (map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<num_objects]);
y <- when (type \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return (\<lambda>x. if x \<in> set ptrs then Some (default_object type dev o_bits) else kh x);
y <- do_extended_op (retype_region_ext ptrs type);
modify (kheap_update (K kh'))
od);
return ptrs
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>kh' s f. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); type \<noteq> Untyped\<rbrakk> \<Longrightarrow> silc_inv aag st (trans_state f s\<lparr>kheap := kh'\<rparr>) = silc_inv aag st (s\<lparr>kheap := kh'\<rparr>)
 2. \<And>obj_size ptrs kh. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); type \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?B8 obj_size ptrs kh\<rbrace> return (\<lambda>x. if x \<in> set ptrs then Some (default_object type dev o_bits) else kh x) \<lbrace>\<lambda>kh' s. silc_inv aag st (kheap_update (K kh') s)\<rbrace>
 3. \<And>obj_size ptrs. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); type \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 obj_size ptrs\<rbrace> gets kheap \<lbrace>?B8 obj_size ptrs\<rbrace>
 4. \<And>obj_size. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>?B3 obj_size\<rbrace> return (map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<num_objects]) \<lbrace>\<lambda>ptrs. if type \<noteq> Untyped then ?Q7 obj_size ptrs else silc_inv aag st\<rbrace>
 5. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>?Q2\<rbrace> return (2 ^ obj_bits_api type o_bits) \<lbrace>?B3\<rbrace>
 6. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); silc_inv aag st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>obj_size ptrs kh. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); type \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?B8 obj_size ptrs kh\<rbrace> return (\<lambda>x. if x \<in> set ptrs then Some (default_object type dev o_bits) else kh x) \<lbrace>\<lambda>kh' s. silc_inv aag st (kheap_update (K kh') s)\<rbrace>
 2. \<And>obj_size ptrs. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); type \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 obj_size ptrs\<rbrace> gets kheap \<lbrace>?B8 obj_size ptrs\<rbrace>
 3. \<And>obj_size. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>?B3 obj_size\<rbrace> return (map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<num_objects]) \<lbrace>\<lambda>ptrs. if type \<noteq> Untyped then ?Q7 obj_size ptrs else silc_inv aag st\<rbrace>
 4. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>?Q2\<rbrace> return (2 ^ obj_bits_api type o_bits) \<lbrace>?B3\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); silc_inv aag st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); silc_inv aag st s\<rbrakk> \<Longrightarrow> (if type \<noteq> Untyped then \<lambda>s. silc_inv aag st (kheap_update (K (\<lambda>a. if a \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<num_objects]) then Some (default_object type dev o_bits) else kheap s a)) s) else silc_inv aag st) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s; range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped\<rbrakk> \<Longrightarrow> silc_inv aag st (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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)\<rbrakk> \<Longrightarrow> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>))) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel)) \<and> silc_dom_equiv aag st (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>sz. cap_table_at sz x (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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)\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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)\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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)\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<in> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s b cap p. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; cte_wp_at ((=) cap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s b cap p. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; cte_wp_at ((=) cap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b cap p. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; cte_wp_at ((=) cap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> cap = NullCap
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s b p capa. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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. (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); p < num_objects; cte_wp_at ((=) NullCap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) capa) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); (\<exists>x\<in>obj_refs capa. pasObjectAbs aag x \<noteq> pasObjectAbs aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits))) \<or> (\<exists>x\<in>cap_irqs capa. pasIRQAbs aag x \<noteq> pasObjectAbs aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b cap p. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; cte_wp_at ((=) cap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> cap = NullCap
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s b p capa. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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. (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); p < num_objects; cte_wp_at ((=) capa) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); (\<exists>x\<in>obj_refs capa. pasObjectAbs aag x \<noteq> pasObjectAbs aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits))) \<or> (\<exists>x\<in>cap_irqs capa. pasIRQAbs aag x \<noteq> pasObjectAbs aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits))); capa = NullCap\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps NullCap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b cap p. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; cte_wp_at ((=) cap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> cap = NullCap
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s b cap p. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; cte_wp_at ((=) cap) (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> cap = NullCap
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s b cap p sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) (fst (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b)) = Some cte; cap = cte\<rbrakk> \<Longrightarrow> cap = NullCap
 2. \<And>s b cap p tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) (fst (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b)) = Some (TCB tcb); tcb_cap_cases (snd (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b)) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> cap = NullCap
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p_ < num_objects; \<not> intra_label_cap aag (ptr_add ptr (p_ * 2 ^ obj_bits_api type o_bits), b_) (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>); kheap (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>) (fst (ptr_add ptr (p_ * 2 ^ obj_bits_api type o_bits), b_)) = Some (CNode sza_ fun_); well_formed_cnode_n sza_ fun_; fun_ (snd (ptr_add ptr (p_ * 2 ^ obj_bits_api type o_bits), b_)) = Some cte_; cap_ = cte_\<rbrakk> \<Longrightarrow> cap_ = NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s b cap p tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p < num_objects; \<not> intra_label_cap aag (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) (fst (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b)) = Some (TCB tcb); tcb_cap_cases (snd (ptr_add ptr (p * 2 ^ obj_bits_api type o_bits), b)) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> cap = NullCap
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); p_ < num_objects; \<not> intra_label_cap aag (ptr_add ptr (p_ * 2 ^ obj_bits_api type o_bits), b_) (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>); kheap (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>) (fst (ptr_add ptr (p_ * 2 ^ obj_bits_api type o_bits), b_)) = Some (TCB tcb_); tcb_cap_cases (snd (ptr_add ptr (p_ * 2 ^ obj_bits_api type o_bits), b_)) = Some (getF_, setF_, restr_); cap_ = getF_ tcb_\<rbrakk> \<Longrightarrow> cap_ = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s; \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; (la, lb) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> (la, lb) \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 3. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 4. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (7 subgoals):
 1. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) (fst (la, lb)) = Some (CNode (?sz201 s a b cap la lb sza fun cte) (?fun201 s a b cap la lb sza fun cte))
 2. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> well_formed_cnode_n (?sz201 s a b cap la lb sza fun cte) (?fun201 s a b cap la lb sza fun cte)
 3. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> ?fun201 s a b cap la lb sza fun cte (snd (la, lb)) = Some (?cte201 s a b cap la lb sza fun cte)
 4. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs (?cte201 s a b cap la lb sza fun cte) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (?cte201 s a b cap la lb sza fun cte) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (?cte201 s a b cap la lb sza fun cte) \<noteq> {}
 5. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 6. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 7. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (6 subgoals):
 1. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> well_formed_cnode_n sza fun
 2. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> fun (snd (la, lb)) = Some (?cte201 s a b cap la lb sza fun cte)
 3. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs (?cte201 s a b cap la lb sza fun cte) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (?cte201 s a b cap la lb sza fun cte) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (?cte201 s a b cap la lb sza fun cte) \<noteq> {}
 4. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 5. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 6. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (5 subgoals):
 1. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> fun (snd (la, lb)) = Some (?cte201 s a b cap la lb sza fun cte)
 2. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs (?cte201 s a b cap la lb sza fun cte) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (?cte201 s a b cap la lb sza fun cte) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (?cte201 s a b cap la lb sza fun cte) \<noteq> {}
 3. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 4. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 5. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap la lb sza fun cte. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd (la, lb)) = Some cte; cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs cte = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cte = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cte \<noteq> {}
 2. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 3. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 4. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>)
 2. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (5 subgoals):
 1. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) (fst (la, lb)) = Some (TCB (?tcb230 s a b cap la lb tcb getF setF restr))
 2. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (la, lb)) = Some (?getF230 s a b cap la lb tcb getF setF restr, ?setF230 s a b cap la lb tcb getF setF restr)
 3. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs (?getF230 s a b cap la lb tcb getF setF restr (?tcb230 s a b cap la lb tcb getF setF restr)) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (?getF230 s a b cap la lb tcb getF setF restr (?tcb230 s a b cap la lb tcb getF setF restr)) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (?getF230 s a b cap la lb tcb getF setF restr (?tcb230 s a b cap la lb tcb getF setF restr)) \<noteq> {}
 4. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 5. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (la, lb)) = Some (?getF230 s a b cap la lb tcb getF setF restr, ?setF230 s a b cap la lb tcb getF setF restr)
 2. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs (?getF230 s a b cap la lb tcb getF setF restr tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (?getF230 s a b cap la lb tcb getF setF restr tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (?getF230 s a b cap la lb tcb getF setF restr tcb) \<noteq> {}
 3. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 4. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap la lb tcb getF setF restr. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; kheap s (fst (la, lb)) = Some (TCB tcb); tcb_cap_cases (snd (la, lb)) = Some (getF, setF, restr); cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs (getF tcb) = {} \<longrightarrow> obj_refs cap \<inter> obj_refs (getF tcb) = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs (getF tcb) \<noteq> {}
 2. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 3. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap la lb. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) cap) (a, b) s; \<not> intra_label_cap aag (a, b) s; pasObjectAbs aag la = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (la, lb) s\<rbrakk> \<Longrightarrow> la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); a_ \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap_) (a_, b_) (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>); \<not> intra_label_cap aag (a_, b_) (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>); cte_wp_at ((=) cap_) (a_, b_) s_; \<not> intra_label_cap aag (a_, b_) s_; pasObjectAbs aag la_ = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap_ \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap_ \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap_ \<inter> arch_gen_refs c \<noteq> {}) (la_, lb_) s_\<rbrakk> \<Longrightarrow> la_ \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, b) s
 2. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap_) (a_, b_) (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>) \<and> \<not> intra_label_cap aag (a_, b_) (s_\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s_ a\<rparr>); a_ \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap_) (a_, b_) s_ proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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); cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) \<and> \<not> intra_label_cap aag (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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. (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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); cte_wp_at ((=) capa) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); (\<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>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)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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. (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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) capa) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); (\<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>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)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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. (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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) capa) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); (\<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> cte_wp_at ((=) capa) (a, b) s \<and> ((\<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped; 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. (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); a \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects}; cte_wp_at ((=) cap) (a, b) (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>); (\<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> cte_wp_at ((=) cap) (a, b) s