theory Noninterference

lemma sameFor_current_partition_sys_mode_of_eq:
  "\<lbrakk> (s, t) \<in> sameFor_subject (pasPolicy initial_aag) (pasObjectAbs initial_aag)
                              (pasIRQAbs initial_aag) (pasASIDAbs initial_aag)
                              (pasDomainAbs initial_aag) a;
     label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = a;
     OrdinaryLabel a \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if s)) \<rbrakk>
     \<Longrightarrow> sys_mode_of s = sys_mode_of t" apply (simp add: sameFor_subject_def2) apply clarify apply (erule impE) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> sameFor_subject (pasPolicy initial_aag) (pasObjectAbs initial_aag) (pasIRQAbs initial_aag) (pasASIDAbs initial_aag) (pasDomainAbs initial_aag) a; label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = a; OrdinaryLabel a \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if s))\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>aa b ba. s = ((aa, b), ba) \<and> (\<exists>ab bb bc. t = ((ab, bb), bc) \<and> (\<forall>d\<in>subjectReads (pasPolicy initial_aag) (OrdinaryLabel a). states_equiv_for (\<lambda>x. pasObjectAbs initial_aag x = d) (\<lambda>x. pasIRQAbs initial_aag x = d) (\<lambda>x. pasASIDAbs initial_aag x = d) (\<lambda>x. d \<in> pasDomainAbs initial_aag x) b bb) \<and> ((pasDomainAbs initial_aag (cur_domain b) \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) = {} \<longrightarrow> pasDomainAbs initial_aag (cur_domain bb) \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> aa = ab) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb)); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = a; OrdinaryLabel a \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if s))\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba aaa bb bc. \<lbrakk>OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc)))))) \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if ((aa, b), ba))); a = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))); s = ((aa, b), ba); t = ((aaa, bb), bc); \<forall>d\<in>subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))). states_equiv_for (\<lambda>x. pasObjectAbs initial_aag x = d) (\<lambda>x. pasIRQAbs initial_aag x = d) (\<lambda>x. pasASIDAbs initial_aag x = d) (\<lambda>x. d \<in> pasDomainAbs initial_aag x) b bb; (pasDomainAbs initial_aag (cur_domain b) \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))) = {} \<longrightarrow> pasDomainAbs initial_aag (cur_domain bb) \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))) \<noteq> {}) \<longrightarrow> cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> aa = aaa) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb\<rbrakk> \<Longrightarrow> sys_mode_of ((aa, b), ba) = sys_mode_of ((aaa, bb), bc) proof (prove)
goal (2 subgoals):
 1. \<And>aa b ba aaa bb bc. \<lbrakk>OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc)))))) \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if ((aa, b), ba))); a = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))); s = ((aa, b), ba); t = ((aaa, bb), bc); \<forall>d\<in>subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))). states_equiv_for (\<lambda>x. pasObjectAbs initial_aag x = d) (\<lambda>x. pasIRQAbs initial_aag x = d) (\<lambda>x. pasASIDAbs initial_aag x = d) (\<lambda>x. d \<in> pasDomainAbs initial_aag x) b bb\<rbrakk> \<Longrightarrow> pasDomainAbs initial_aag (cur_domain b) \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))) = {} \<longrightarrow> pasDomainAbs initial_aag (cur_domain bb) \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))) \<noteq> {}
 2. \<And>aa b ba aaa bb bc. \<lbrakk>OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc)))))) \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if ((aa, b), ba))); a = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))); s = ((aa, b), ba); t = ((aaa, bb), bc); \<forall>d\<in>subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))). states_equiv_for (\<lambda>x. pasObjectAbs initial_aag x = d) (\<lambda>x. pasIRQAbs initial_aag x = d) (\<lambda>x. pasASIDAbs initial_aag x = d) (\<lambda>x. d \<in> pasDomainAbs initial_aag x) b bb; cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> aa = aaa) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb\<rbrakk> \<Longrightarrow> sys_mode_of ((aa, b), ba) = sys_mode_of ((aaa, bb), bc) proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba aaa bb bc. \<lbrakk>OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc)))))) \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if ((aa, b), ba))); a = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))); s = ((aa, b), ba); t = ((aaa, bb), bc); \<forall>d\<in>subjectReads (pasPolicy initial_aag) (OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if ((aaa, bb), bc))))))). states_equiv_for (\<lambda>x. pasObjectAbs initial_aag x = d) (\<lambda>x. pasIRQAbs initial_aag x = d) (\<lambda>x. pasASIDAbs initial_aag x = d) (\<lambda>x. d \<in> pasDomainAbs initial_aag x) b bb; cur_domain b = cur_domain bb \<and> globals_equiv b bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> equiv_irq_state (machine_state b) (machine_state bb) \<and> (user_modes ba \<longrightarrow> aa = aaa) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb\<rbrakk> \<Longrightarrow> sys_mode_of ((aa, b), ba) = sys_mode_of ((aaa, bb), bc) proof (prove)
goal:
No subgoals!