theory ArchFinalCaps

lemma perform_page_table_invocation_silc_inv:
  "\<lbrace>silc_inv aag st and valid_pti blah and K (authorised_page_table_inv aag blah)\<rbrace>
   perform_page_table_invocation blah
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding perform_page_table_invocation_def apply (rule hoare_pre) apply (wp set_cap_silc_inv mapM_x_wp[OF _ subset_refl]
            perform_page_table_invocation_silc_inv_get_cap_helper'[where st=st]
         | wpc | simp only: o_def fun_app_def K_def swp_def)+ apply (clarsimp simp: valid_pti_def authorised_page_table_inv_def
                 split: page_table_invocation.splits) apply (rule conjI) apply (clarsimp) defer apply (fastforce simp: silc_inv_def) apply (fastforce dest: is_arch_eq_pt_is_pt_or_pg_cap simp: silc_inv_def) apply (drule_tac slot="(aa,ba)" in overlapping_slots_have_labelled_overlapping_caps[rotated]) apply (fastforce) apply (fastforce elim: is_arch_update_overlaps[rotated] cte_wp_at_weakenE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_pti blah and K (authorised_page_table_inv aag blah)\<rbrace> perform_page_table_invocation blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_pti blah and K (authorised_page_table_inv aag blah)\<rbrace> case blah of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case blah of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and valid_pti blah and K (authorised_page_table_inv aag blah)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and valid_pti blah and (\<lambda>y. authorised_page_table_inv aag blah)) s \<Longrightarrow> (\<forall>x xa xb xc. blah = PageTableMap x xa xb xc \<longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag x (pasObjectAbs aag (fst xa)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps x s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and (\<lambda>y. pasObjectAbs aag (fst xa) \<noteq> SilcLabel)) s) \<and> (\<forall>x xa. blah = PageTableUnmap x xa \<longrightarrow> (x = NullCap \<longrightarrow> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> True) \<and> (x = DomainCap \<longrightarrow> True) \<and> (x = IRQControlCap \<longrightarrow> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> True) \<and> (\<forall>xb. x = ArchObjectCap xb \<longrightarrow> (\<forall>x xa. xb = ASIDPoolCap x xa \<longrightarrow> True) \<and> (xb = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>x xa xc xd xe. xb = PageCap x xa xc xd xe \<longrightarrow> True) \<and> (\<forall>x xc. xb = PageTableCap x xc \<longrightarrow> (xc = 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. xc = 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>x xa. xb = PageDirectoryCap x xa \<longrightarrow> True))) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag x11 (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasSubject aag \<noteq> SilcLabel
 2. \<And>s aa ba xa xb. \<lbrakk>blah = PageTableUnmap (ArchObjectCap (PageTableCap xa xb)) (aa, ba); silc_inv aag st s; cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageTableCap xa xb); is_final_cap' (ArchObjectCap (PageTableCap xa xb)) s; is_pt_cap (ArchObjectCap (PageTableCap xa xb)); is_subject aag aa; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap xa xb)); \<forall>asid. (\<exists>vspace_ref. xb = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [xa , xa + 4 .e. xa + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (xb = 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. xb = 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 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag x11 (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s aa ba xa xb. \<lbrakk>blah = PageTableUnmap (ArchObjectCap (PageTableCap xa xb)) (aa, ba); silc_inv aag st s; cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageTableCap xa xb); is_final_cap' (ArchObjectCap (PageTableCap xa xb)) s; is_pt_cap (ArchObjectCap (PageTableCap xa xb)); is_subject aag aa; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap xa xb)); \<forall>asid. (\<exists>vspace_ref. xb = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [xa , xa + 4 .e. xa + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (xb = 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. xb = 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 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 3. \<And>s aa ba xa xb. \<lbrakk>blah = PageTableUnmap (ArchObjectCap (PageTableCap xa xb)) (aa, ba); silc_inv aag st s; cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageTableCap xa xb); is_final_cap' (ArchObjectCap (PageTableCap xa xb)) s; is_pt_cap (ArchObjectCap (PageTableCap xa xb)); is_subject aag aa; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap xa xb)); \<forall>asid. (\<exists>vspace_ref. xb = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [xa , xa + 4 .e. xa + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (xb = 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. xb = 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 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
 2. \<And>s aa ba xa xb. \<lbrakk>blah = PageTableUnmap (ArchObjectCap (PageTableCap xa xb)) (aa, ba); silc_inv aag st s; cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageTableCap xa xb); is_final_cap' (ArchObjectCap (PageTableCap xa xb)) s; is_pt_cap (ArchObjectCap (PageTableCap xa xb)); is_subject aag aa; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap xa xb)); \<forall>asid. (\<exists>vspace_ref. xb = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [xa , xa + 4 .e. xa + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (xb = 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. xb = 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)
 3. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba xa xb. \<lbrakk>blah = PageTableUnmap (ArchObjectCap (PageTableCap xa xb)) (aa, ba); silc_inv aag st s; cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) (aa, ba) s; s \<turnstile> ArchObjectCap (PageTableCap xa xb); is_final_cap' (ArchObjectCap (PageTableCap xa xb)) s; is_pt_cap (ArchObjectCap (PageTableCap xa xb)); is_subject aag aa; pas_cap_cur_auth aag (ArchObjectCap (PageTableCap xa xb)); \<forall>asid. (\<exists>vspace_ref. xb = Some (asid, vspace_ref)) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [xa , xa + 4 .e. xa + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))\<rbrakk> \<Longrightarrow> (xb = 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. xb = 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)
 2. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; silc_inv aag st s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (?cap376 s x11 x13 x14 aa p' ref y ao ba) (pasObjectAbs aag (fst (aa, ba)))
 2. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> slots_holding_overlapping_caps (?cap376 s x11 x13 x14 aa p' ref y ao ba) s
 3. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap376 s x11 x13 x14 aa p' ref y ao ba) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> slots_holding_overlapping_caps x11 s
 2. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps x11 s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x13 x14 aa p' ref y ao ba. \<lbrakk>blah = PageTableMap x11 (aa, ba) x13 x14; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (aa, ba) s; empty_pde_at x14 s; is_pt_cap x11; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); cap_asid x11 = Some y; (ref \<rhd> (x14 && ~~ mask pd_bits)) s; is_subject aag aa; pde_ref x13 = Some p'; is_subject aag (x14 && ~~ mask pd_bits); p' \<in> obj_refs x11; case pde_ref2 x13 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_subject aag (fst x2); pas_cap_cur_auth aag x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; \<not> cap_points_to_label aag x11 (pasSubject aag); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps x11 s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps x11 s) \<and> pasObjectAbs aag a = SilcLabel proof (prove)
goal:
No subgoals!