theory Noninterference

lemma partsSubjectAffects_bounds_subjects_affects:
  assumes domains_distinct: "pas_domains_distinct (aag :: 'a subject_label PAS)"
  shows "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s;
           valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s';
           pas_wellformed_noninterference aag; pas_cur_domain aag s;
           guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s';
           d \<notin> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); d \<noteq> PSched \<rbrakk>
           \<Longrightarrow> (((uc,s),mode),((uc',s'),mode')) \<in> same_for aag d" apply (frule pasSubject_not_SilcLabel) apply (erule contrapos_np) apply (cases d) prefer 2 apply simp apply (clarsimp simp: sameFor_def sameFor_subject_def2 states_equiv_for_def equiv_for_def
                       partsSubjectAffects_def image_def label_can_affect_partition_def) apply (safe del: iffI notI) apply (fastforce dest: partitionIntegrity_subjectAffects_obj) apply ((auto dest: partitionIntegrity_subjectAffects_obj
                                               partitionIntegrity_subjectAffects_eobj
                                               partitionIntegrity_subjectAffects_mem
                                               partitionIntegrity_subjectAffects_device
                                               partitionIntegrity_subjectAffects_cdt
                                               partitionIntegrity_subjectAffects_cdt_list
                                               partitionIntegrity_subjectAffects_is_original_cap
                                               partitionIntegrity_subjectAffects_interrupt_states
                                               partitionIntegrity_subjectAffects_interrupt_irq_node
                                               partitionIntegrity_subjectAffects_asid
                                               partitionIntegrity_subjectAffects_ready_queues
                                                 [folded guarded_is_subject_cur_thread_def,
                                                  OF domains_distinct]
                                               domains_distinct[THEN pas_domains_distinct_inj]
                                    | fastforce simp: partitionIntegrity_def
                                                      silc_dom_equiv_def equiv_for_def)+)[11] apply ((fastforce intro: affects_lrefl
                                   simp: partitionIntegrity_def domain_fields_equiv_def
                                   dest: domains_distinct[THEN pas_domains_distinct_inj])+)[16] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<notin> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); d \<noteq> PSched\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc', s'), mode') \<in> same_for aag d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<notin> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)); d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc', s'), mode') \<in> same_for aag d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel; (((uc, s), mode), (uc', s'), mode') \<notin> same_for aag d\<rbrakk> \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel; (((uc, s), mode), (uc', s'), mode') \<notin> same_for aag d; d = Partition x1\<rbrakk> \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag))
 2. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel; (((uc, s), mode), (uc', s'), mode') \<notin> same_for aag d; d = PSched\<rbrakk> \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel; (((uc, s), mode), (uc', s'), mode') \<notin> same_for aag d; d = PSched\<rbrakk> \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag))
 2. \<And>x1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel; (((uc, s), mode), (uc', s'), mode') \<notin> same_for aag d; d = Partition x1\<rbrakk> \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; einvs s; einvs s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; d \<noteq> PSched; pasSubject aag \<noteq> SilcLabel; (((uc, s), mode), (uc', s'), mode') \<notin> same_for aag d; d = Partition x1\<rbrakk> \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; (\<exists>d\<in>subjectReads (pasPolicy aag) (OrdinaryLabel x1). (\<exists>x. pasObjectAbs aag x = d \<and> kheap s x \<noteq> kheap s' x) \<or> (\<exists>x. pasObjectAbs aag x = d \<and> underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x) \<or> (\<exists>x. pasObjectAbs aag x = d \<and> device_state (machine_state s) x \<noteq> device_state (machine_state s') x) \<or> (\<exists>a. pasObjectAbs aag a = d \<and> (\<exists>b. cdt s (a, b) \<noteq> cdt s' (a, b))) \<or> (\<exists>x. pasObjectAbs aag x = d \<and> ekheap s x \<noteq> ekheap s' x) \<or> (\<exists>a. pasObjectAbs aag a = d \<and> (\<exists>b. cdt_list s (a, b) \<noteq> cdt_list s' (a, b))) \<or> (\<exists>a. pasObjectAbs aag a = d \<and> (\<exists>b. is_original_cap s (a, b) = (\<not> is_original_cap s' (a, b)))) \<or> (\<exists>x. pasIRQAbs aag x = d \<and> interrupt_states s x \<noteq> interrupt_states s' x) \<or> (\<exists>x. pasIRQAbs aag x = d \<and> interrupt_irq_node s x \<noteq> interrupt_irq_node s' x) \<or> (\<exists>x. d \<in> pasDomainAbs aag x \<and> ready_queues s x \<noteq> ready_queues s' x) \<or> \<not> equiv_asids (\<lambda>x. pasASIDAbs aag x = d) s s') \<or> (pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel x1) = {} \<longrightarrow> pasDomainAbs aag (cur_domain s') \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel x1) \<noteq> {}) \<and> (mode = mode' \<longrightarrow> equiv_irq_state (machine_state s) (machine_state s') \<longrightarrow> work_units_completed s = work_units_completed s' \<longrightarrow> scheduler_action s = scheduler_action s' \<longrightarrow> globals_equiv s s' \<longrightarrow> cur_domain s = cur_domain s' \<longrightarrow> user_modes mode' \<and> uc \<noteq> uc' \<or> (\<exists>x. pasObjectAbs aag x = SilcLabel \<and> kheap s x \<noteq> kheap s' x)); d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1) proof (prove)
goal (28 subgoals):
 1. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); kheap s x \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 2. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 3. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); device_state (machine_state s) x \<noteq> device_state (machine_state s') x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 4. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); cdt s (a, b) \<noteq> cdt s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 5. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); ekheap s x \<noteq> ekheap s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 6. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); cdt_list s (a, b) \<noteq> cdt_list s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 7. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); is_original_cap s (a, b); \<not> is_original_cap s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 8. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); \<not> is_original_cap s (a, b); \<not> \<not> is_original_cap s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 9. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); interrupt_states s x \<noteq> interrupt_states s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 10. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); interrupt_irq_node s x \<noteq> interrupt_irq_node s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
A total of 28 subgoals... proof (prove)
goal (27 subgoals):
 1. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 2. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); device_state (machine_state s) x \<noteq> device_state (machine_state s') x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 3. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); cdt s (a, b) \<noteq> cdt s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 4. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); ekheap s x \<noteq> ekheap s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 5. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); cdt_list s (a, b) \<noteq> cdt_list s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 6. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); is_original_cap s (a, b); \<not> is_original_cap s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 7. \<And>x1 da a b. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasObjectAbs aag a \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); \<not> is_original_cap s (a, b); \<not> \<not> is_original_cap s' (a, b)\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 8. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); interrupt_states s x \<noteq> interrupt_states s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 9. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); interrupt_irq_node s x \<noteq> interrupt_irq_node s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
 10. \<And>x1 da x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; da \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); da \<in> pasDomainAbs aag x; ready_queues s x \<noteq> ready_queues s' x\<rbrakk> \<Longrightarrow> \<exists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1)
A total of 27 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); mode \<noteq> mode'\<rbrakk> \<Longrightarrow> x \<in> {}
 2. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); irq_state_of_state s \<noteq> irq_state_of_state s'\<rbrakk> \<Longrightarrow> x \<in> {}
 3. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); work_units_completed s \<noteq> work_units_completed s'\<rbrakk> \<Longrightarrow> x \<in> {}
 4. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); scheduler_action s \<noteq> scheduler_action s'\<rbrakk> \<Longrightarrow> x \<in> {}
 5. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); \<not> globals_equiv s s'\<rbrakk> \<Longrightarrow> x \<in> {}
 6. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); cur_domain s \<noteq> cur_domain s'\<rbrakk> \<Longrightarrow> x \<in> {}
 7. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); user_modes mode'; uc \<noteq> uc'\<rbrakk> \<Longrightarrow> x \<in> {}
 8. \<And>x1 x xa. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); pasObjectAbs aag xa = SilcLabel; kheap s xa \<noteq> kheap s' xa\<rbrakk> \<Longrightarrow> x \<in> {}
 9. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s'); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); mode \<noteq> mode'\<rbrakk> \<Longrightarrow> x \<in> {}
 10. \<And>x1 x. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; pas_refined aag s'; valid_objs s; valid_arch_state s'; silc_inv aag st s; silc_inv aag st' s'; pas_wellformed_noninterference aag; pas_cur_domain aag s; guarded_is_subject_cur_thread aag s; guarded_is_subject_cur_thread aag s'; pasSubject aag \<noteq> SilcLabel; d = Partition x1; invs s; invs s'; valid_list s; valid_sched s; valid_list s'; valid_sched s'; \<nexists>d. subject_can_affect_label_directly aag d \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); x \<in> pasDomainAbs aag (cur_domain s'); x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel x1); irq_state_of_state s \<noteq> irq_state_of_state s'\<rbrakk> \<Longrightarrow> x \<in> {}
A total of 16 subgoals... proof (prove)
goal:
No subgoals!