theory ArchFinalCaps

lemma perform_page_invocation_silc_inv:
  "\<lbrace>silc_inv aag st and valid_page_inv blah and K (authorised_page_inv aag blah)\<rbrace>
   perform_page_invocation blah
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding perform_page_invocation_def apply (rule hoare_pre) apply (wp mapM_wp[OF _ subset_refl] set_cap_silc_inv
            mapM_x_wp[OF _ subset_refl]
            perform_page_table_invocation_silc_inv_get_cap_helper'[where st=st]
            hoare_vcg_all_lift hoare_vcg_if_lift hoare_weak_lift_imp
         | wpc
         | simp only: swp_def o_def fun_app_def K_def
         | wp (once) hoare_drop_imps)+ apply (clarsimp simp: valid_page_inv_def authorised_page_inv_def
                  split: page_invocation.splits) apply (intro allI impI conjI) apply (drule_tac slot="(aa,bb)" in overlapping_slots_have_labelled_overlapping_caps[rotated]) apply (fastforce) apply (fastforce elim: is_arch_update_overlaps[rotated] cte_wp_at_weakenE) apply fastforce apply (fastforce simp: silc_inv_def) apply (drule_tac slot="(aa,bb)" in overlapping_slots_have_labelled_overlapping_caps[rotated]) apply (fastforce) apply (fastforce elim: is_arch_update_overlaps[rotated] cte_wp_at_weakenE) apply fastforce apply (fastforce simp: silc_inv_def) apply (fastforce dest: is_arch_eq_pg_is_pt_or_pg_cap simp: silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_page_inv blah and K (authorised_page_inv aag blah)\<rbrace> perform_page_invocation blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_page_inv blah and K (authorised_page_inv aag blah)\<rbrace> case blah of PageMap asid cap ct_slot entries \<Rightarrow> do set_cap cap ct_slot;
case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od;
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case blah of PageMap asid cap ct_slot entries \<Rightarrow> do set_cap cap ct_slot;
case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od;
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and valid_page_inv blah and K (authorised_page_inv aag blah)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and valid_page_inv blah and (\<lambda>y. authorised_page_inv aag blah)) s \<Longrightarrow> (\<forall>x xa xb xc. blah = PageMap x xa xb xc \<longrightarrow> (\<forall>x. xc = Inl x \<longrightarrow> (\<forall>xc xd. x = (xc, xd) \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag xa (pasObjectAbs aag (fst xb)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps xa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and (\<lambda>y. pasObjectAbs aag (fst xb) \<noteq> SilcLabel)) s \<and> ((\<lambda>s. \<not> cap_points_to_label aag xa (pasObjectAbs aag (fst xb)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps xa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and (\<lambda>y. pasObjectAbs aag (fst xb) \<noteq> SilcLabel)) s)) \<and> (\<forall>x. xc = Inr x \<longrightarrow> (\<forall>xc xd. x = (xc, xd) \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag xa (pasObjectAbs aag (fst xb)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps xa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and (\<lambda>y. pasObjectAbs aag (fst xb) \<noteq> SilcLabel)) s \<and> ((\<lambda>s. \<not> cap_points_to_label aag xa (pasObjectAbs aag (fst xb)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps xa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and (\<lambda>y. pasObjectAbs aag (fst xb) \<noteq> SilcLabel)) s))) \<and> (\<forall>x xa. blah = PageUnmap x xa \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> True) \<and> (x = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>xb xc xd xe xf. x = PageCap xb xc xd xe xf \<longrightarrow> (xf = None \<longrightarrow> silc_inv aag st s \<and> cte_wp_at (is_pt_cap or is_pg_cap) xa s \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst xa) \<noteq> SilcLabel) \<and> (\<forall>x. xf = Some x \<longrightarrow> (\<forall>xb xc. x = (xb, xc) \<longrightarrow> silc_inv aag st s \<and> cte_wp_at (is_pt_cap or is_pg_cap) xa s \<and> silc_inv aag st s \<and> pasObjectAbs aag (fst xa) \<noteq> SilcLabel))) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb xc xd xe. blah = PageFlush x xa xb xc xd xe \<longrightarrow> (if xa < xb then \<lambda>s. silc_inv aag st s \<and> silc_inv aag st s else silc_inv aag st) s) \<and> (\<forall>x. blah = PageGetAddr x \<longrightarrow> silc_inv aag st s) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14\<rbrakk> \<Longrightarrow> ((\<exists>a b. x14 = Inl (a, b)) \<longrightarrow> (\<not> cap_points_to_label aag x12 (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. x14 = Inr (a, b)) \<longrightarrow> (\<not> cap_points_to_label aag x12 (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasSubject aag \<noteq> SilcLabel)
 2. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (5 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 5. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (7 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (?cap464 s x11 x12 x14 aa ab ba pd bb) (pasObjectAbs aag (fst (aa, bb)))
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps (?cap464 s x11 x12 x14 aa ab ba pd bb) s
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap464 s x11 x12 x14 aa ab ba pd bb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 5. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 6. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 7. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (6 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps x12 s
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps x12 s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 4. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 5. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 6. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (5 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps x12 s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 5. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (4 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inl (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 4. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (3 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (5 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (?cap503 s x11 x12 x14 aa ab ba pd bb) (pasObjectAbs aag (fst (aa, bb)))
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps (?cap503 s x11 x12 x14 aa ab ba pd bb) s
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap503 s x11 x12 x14 aa ab ba pd bb) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 5. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (4 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag)\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps x12 s
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps x12 s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 4. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (3 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b); \<not> cap_points_to_label aag x12 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps x12 s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x12 s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x14 aa ab ba pd bb. \<lbrakk>blah = PageMap x11 x12 (aa, bb) x14; silc_inv aag st s; cte_wp_at (is_arch_update x12) (aa, bb) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (aa, bb) s \<or> cte_wp_at (\<lambda>c. same_refs x14 c s) (aa, bb) s; cte_wp_at is_pg_cap (aa, bb) s; same_refs x14 x12 s; valid_slots x14 s; s \<turnstile> x12; is_pg_cap x12; empty_refs x14; x11 \<le> mask local.asid_bits; x11 \<noteq> 0; cte_wp_at (parent_for_refs x14) (ab, ba) s; vspace_at_asid x11 pd s; pas_cap_cur_auth aag x12; is_subject aag aa; authorised_slots aag x14; \<exists>a b. x14 = Inr (a, b)\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 2. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba x xa xb xc xd. \<lbrakk>blah = PageUnmap (PageCap x xa xb xc xd) (aa, ba); silc_inv aag st s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x xa xb xc xd)); is_subject aag aa; case xd of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_unmap xc x2; cte_wp_at ((=) (ArchObjectCap (PageCap x xa xb xc xd))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageCap x xa xb xc xd)\<rbrakk> \<Longrightarrow> (xd = None \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) \<and> ((\<exists>a b. xd = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) (aa, ba) s \<and> pasSubject aag \<noteq> SilcLabel) proof (prove)
goal:
No subgoals!