theory ArchNoninterference

lemma partitionIntegrity_subjectAffects_asid[Noninterference_assms]:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; valid_objs s;
     valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag;
     silc_inv aag st s'; invs s'; \<not> equiv_asids (\<lambda>x. pasASIDAbs aag x = a) s s' \<rbrakk>
     \<Longrightarrow> a \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (clarsimp simp: equiv_asids_def equiv_asid_def asid_pool_at_kheap) apply (case_tac "arm_asid_table (arch_state s) (asid_high_bits_of asid) =
                   arm_asid_table (arch_state s') (asid_high_bits_of asid)") apply (clarsimp simp: valid_arch_state_def valid_asid_table_def) apply (drule_tac x=pool_ptr in bspec) apply blast apply (drule_tac x=pool_ptr in bspec) apply blast apply (clarsimp simp: asid_pool_at_kheap) apply (rule affects_asidpool_map) apply (rule pas_refined_asid_mem) apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_obj) apply (drule_tac x="pool_ptr" in spec)+ apply (drule tro_tro_alt, erule integrity_obj_alt.cases;simp ) apply (drule_tac t="pasSubject aag" in sym) apply simp apply (rule sata_asidpool) apply assumption apply assumption apply (simp add: arch_integrity_obj_alt.simps asid_pool_integrity_def) apply (drule_tac x="ucast asid" in spec)+ apply clarsimp apply (drule owns_mapping_owns_asidpool) apply ((simp | blast intro: pas_refined_Control[THEN sym]
                     | fastforce intro: pas_wellformed_pasSubject_update[simplified])+)[4] apply (drule_tac t="pasSubject aag" in sym)+ apply simp apply (rule sata_asidpool) apply assumption apply assumption apply assumption apply clarsimp apply (drule partitionIntegrity_integrity) apply (clarsimp simp: integrity_def) apply (drule_tac x=asid in spec)+ apply (clarsimp simp: integrity_asids_def) apply (fastforce intro: affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; \<not> equiv_asids (\<lambda>x. pasASIDAbs aag x = a) s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag a proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; \<forall>p\<in>ran (asid_table s'). typ_at (AArch AASIDPool) p s'; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s'))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; \<forall>p\<in>ran (asid_table s'). typ_at (AArch AASIDPool) p s'; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s'))\<rbrakk> \<Longrightarrow> pool_ptr \<in> ran (asid_table s)
 2. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; \<forall>p\<in>ran (asid_table s'). typ_at (AArch AASIDPool) p s'; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); typ_at (AArch AASIDPool) pool_ptr s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; \<forall>p\<in>ran (asid_table s'). typ_at (AArch AASIDPool) p s'; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); typ_at (AArch AASIDPool) pool_ptr s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); typ_at (AArch AASIDPool) pool_ptr s\<rbrakk> \<Longrightarrow> pool_ptr \<in> ran (asid_table s')
 2. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); typ_at (AArch AASIDPool) pool_ptr s; typ_at (AArch AASIDPool) pool_ptr s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid pool_ptr. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); typ_at (AArch AASIDPool) pool_ptr s; typ_at (AArch AASIDPool) pool_ptr s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid)
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> pasPolicy aag
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag (?s172 asid pool_ptr asid_pool asid_poola)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag (?s172 asid pool_ptr asid_pool asid_poola)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); integrity_obj_state (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} s s'\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag (?s172 asid pool_ptr asid_pool asid_poola)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); object_integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) pool_ptr) (kheap s pool_ptr) (kheap s' pool_ptr)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy aag (?s172 asid pool_ptr asid_pool asid_poola)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (4 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); tro_tag LRefl; is_subject aag pool_ptr\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 2. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag pool_ptr) (ASIDPool asid_pool) (ASIDPool asid_poola)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 3. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 4. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (4 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); tro_tag LRefl; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 2. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag pool_ptr) (ASIDPool asid_pool) (ASIDPool asid_poola)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 3. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 4. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (4 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); tro_tag LRefl; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> (pasObjectAbs aag pool_ptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 2. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag pool_ptr) (ASIDPool asid_pool) (ASIDPool asid_poola)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 3. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 4. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (5 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); tro_tag LRefl; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> asid_table (?s172 asid pool_ptr asid_pool asid_poola) (asid_high_bits_of asid) = Some pool_ptr
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); tro_tag LRefl; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 3. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag pool_ptr) (ASIDPool asid_pool) (ASIDPool asid_poola)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state (?s172 asid pool_ptr asid_pool asid_poola)) (asid_table (?s172 asid pool_ptr asid_pool asid_poola)) (state_vrefs (?s172 asid pool_ptr asid_pool asid_poola))
 4. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag (?s172 asid pool_ptr asid_pool asid_poola)
 5. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (4 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); tro_tag LRefl; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 2. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag pool_ptr) (ASIDPool asid_pool) (ASIDPool asid_poola)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 3. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag pool_ptr) (ASIDPool asid_pool) (ASIDPool asid_poola)\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); \<forall>x. asid_poola x \<noteq> asid_pool x \<longrightarrow> asid_poola x = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (asid_pool x))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola ao ao'. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); ao = ASIDPool asid_pool; ao' = ASIDPool asid_poola; tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_poola (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<longrightarrow> asid_poola (UCAST(32 \<rightarrow> 10) asid) = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (asid_pool (UCAST(32 \<rightarrow> 10) asid)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (7 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> asid_pool (?r242 asid pool_ptr asid_pool asid_poola y) = Some (?p'242 asid pool_ptr asid_pool asid_poola y)
 2. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined (?aag242 asid pool_ptr asid_pool asid_poola y) s
 3. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject (?aag242 asid pool_ptr asid_pool asid_poola y) (?p'242 asid pool_ptr asid_pool asid_poola y)
 4. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_wellformed (?aag242 asid pool_ptr asid_pool asid_poola y\<lparr>pasSubject := pasObjectAbs (?aag242 asid pool_ptr asid_pool asid_poola y) pool_ptr\<rparr>)
 5. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag; is_subject (?aag242 asid pool_ptr asid_pool asid_poola y) pool_ptr\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 6. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 7. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag; is_subject aag pool_ptr\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasObjectAbs aag pool_ptr, Control, pasObjectAbs aag y) \<in> pasPolicy aag; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> (pasObjectAbs aag pool_ptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (4 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasObjectAbs aag pool_ptr, Control, pasObjectAbs aag y) \<in> pasPolicy aag; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of asid) = Some pool_ptr
 2. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasObjectAbs aag pool_ptr, Control, pasObjectAbs aag y) \<in> pasPolicy aag; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 3. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (3 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola y. \<lbrakk>pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); tro_tag RArch; kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola)); asid_pool (UCAST(32 \<rightarrow> 10) asid) = Some y; asid_poola (UCAST(32 \<rightarrow> 10) asid) = None; (pasObjectAbs aag pool_ptr, Control, pasObjectAbs aag y) \<in> pasPolicy aag; pasSubject aag = pasObjectAbs aag pool_ptr\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 2. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (2 subgoals):
 1. \<And>asid pool_ptr asid_pool asid_poola. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) = Some pool_ptr; asid_table s' (asid_high_bits_of asid) = Some pool_ptr; asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_poola (UCAST(32 \<rightarrow> 10) asid); inj_on (asid_table s) (dom (asid_table s)); inj_on (asid_table s') (dom (asid_table s')); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s')) s'; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_global_pts s'; is_inv (arm_hwasid_table (arch_state s')) (map_option fst \<circ> arm_asid_map (arch_state s')); kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)); kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_poola))\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<longrightarrow> (\<exists>pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr \<and> ((\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<forall>asid_pool. kheap s' pool_ptr \<noteq> Some (ArchObj (ASIDPool asid_pool))) \<or> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> (\<exists>asid_pool'. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<and> asid_pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> asid_pool' (UCAST(32 \<rightarrow> 10) asid))))); a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid); integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid); \<forall>x. integrity_obj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) (kheap s' x); \<forall>x. integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>a b. integrity_cdt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt s) (tcb_states_of_state s) (a, b) (cdt s (a, b), is_original_cap s (a, b)) (cdt s' (a, b), is_original_cap s' (a, b)); \<forall>a b. integrity_cdt_list (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt s) (tcb_states_of_state s) (a, b) (cdt_list s (a, b)) (cdt_list s' (a, b)); \<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>x. integrity_mem (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) {} (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>a. asid_table s (asid_high_bits_of a) = asid_table s' (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasASIDAbs aag asid; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid); \<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); integrity_obj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag asid) (kheap s asid) (kheap s' asid); integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag asid) (ekheap s asid) (ekheap s' asid); \<forall>b. integrity_cdt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt s) (tcb_states_of_state s) (asid, b) (cdt s (asid, b), is_original_cap s (asid, b)) (cdt s' (asid, b), is_original_cap s' (asid, b)); \<forall>b. integrity_cdt_list (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt s) (tcb_states_of_state s) (asid, b) (cdt_list s (asid, b)) (cdt_list s' (asid, b)); integrity_mem (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} asid (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) {} (underlying_memory (machine_state s) asid) (underlying_memory (machine_state s') asid); integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} asid (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) asid) (device_state (machine_state s') asid); asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasASIDAbs aag asid) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>pas_refined aag s; valid_objs s; valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag; silc_inv aag st s'; invs s'; asid \<noteq> 0; a = pasSubject aag; asid_table s (asid_high_bits_of asid) \<noteq> asid_table s' (asid_high_bits_of asid); \<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>d p. integrity_ready_queues (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); integrity_obj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag asid) (kheap s asid) (kheap s' asid); integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag asid) (ekheap s asid) (ekheap s' asid); \<forall>b. integrity_cdt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt s) (tcb_states_of_state s) (asid, b) (cdt s (asid, b), is_original_cap s (asid, b)) (cdt s' (asid, b), is_original_cap s' (asid, b)); \<forall>b. integrity_cdt_list (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt s) (tcb_states_of_state s) (asid, b) (cdt_list s (asid, b)) (cdt_list s' (asid, b)); integrity_mem (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} asid (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) {} (underlying_memory (machine_state s) asid) (underlying_memory (machine_state s') asid); integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} asid (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) asid) (device_state (machine_state s') asid); \<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> is_subject_asid aag asid'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasSubject aag) proof (prove)
goal:
No subgoals!