theory Noninterference

lemma sameFor_reads_equiv_f_g:
  "\<lbrakk> reads_equiv_f_g aag s s'; silc_inv aag st' st'';
     pasSubject aag \<in> pasDomainAbs aag (cur_domain s) \<union> pasDomainAbs aag (cur_domain s') \<rbrakk>
     \<Longrightarrow> (((uc,s),mode),((uc,s'),mode)) \<in> same_for aag (Partition (label_of (pasSubject aag)))" apply (clarsimp simp: reads_equiv_f_g_def reads_equiv_def2 sameFor_def silc_dom_equiv_def) apply (simp add: sameFor_subject_def) apply (frule pasSubject_not_SilcLabel) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f_g aag s s'; silc_inv aag st' st''; pasSubject aag \<in> pasDomainAbs aag (cur_domain s) \<union> pasDomainAbs aag (cur_domain s')\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc, s'), mode) \<in> same_for aag (Partition (label_of (pasSubject aag))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st' st''; pas_cur_domain aag s'; states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); globals_equiv s s'; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc, s'), mode) \<in> sameFor_subject (pasPolicy aag) (pasObjectAbs aag) (pasIRQAbs aag) (pasASIDAbs aag) (pasDomainAbs aag) (label_of (pasSubject aag)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st' st''; pas_cur_domain aag s'; states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); globals_equiv s s'; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag)))) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag)))) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag)))) (\<lambda>x. pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) \<noteq> {}) s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st' st''; pas_cur_domain aag s'; states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); globals_equiv s s'; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'; pasSubject aag \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag)))) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag)))) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag)))) (\<lambda>x. pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) \<noteq> {}) s s' proof (prove)
goal:
No subgoals!