theory ArchNoninterference

lemma sameFor_scheduler_affects_equiv[Noninterference_assms]:
  "\<lbrakk> (s,s') \<in> same_for aag PSched; (s,s') \<in> same_for aag (Partition l);
     invs (internal_state_if s); invs (internal_state_if s') \<rbrakk>
     \<Longrightarrow> scheduler_equiv aag (internal_state_if s) (internal_state_if s') \<and>
         scheduler_affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s')" apply (rule conjI) apply (blast intro: sameFor_scheduler_equiv) apply (clarsimp simp: scheduler_affects_equiv_def arch_scheduler_affects_equiv_def
                        sameFor_def silc_dom_equiv_def reads_scheduler_def
                        sameFor_scheduler_def globals_equiv_to_exclusive_state_equiv) 
  (* simplifying using sameFor_subject_def in assumptions causes simp to loop *)
   apply (simp (no_asm_use) add: sameFor_subject_def disjoint_iff_not_equal Bex_def) apply (blast intro: globals_equiv_to_scheduler_globals_frame_equiv
                      globals_equiv_to_exclusive_state_equiv globals_equiv_to_cur_thread_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> same_for aag PSched; (s, s') \<in> same_for aag (Partition l); invs (internal_state_if s); invs (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_equiv aag (internal_state_if s) (internal_state_if s') \<and> scheduler_affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> same_for aag PSched; (s, s') \<in> same_for aag (Partition l); invs (internal_state_if s); invs (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_equiv aag (internal_state_if s) (internal_state_if s')
 2. \<lbrakk>(s, s') \<in> same_for aag PSched; (s, s') \<in> same_for aag (Partition l); invs (internal_state_if s); invs (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> same_for aag PSched; (s, s') \<in> same_for aag (Partition l); invs (internal_state_if s); invs (internal_state_if s')\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag (OrdinaryLabel l) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<lbrakk>(((a, b), ba), (aa, bb), bc) \<in> sameFor_subject (pasPolicy aag) (pasObjectAbs aag) (pasIRQAbs aag) (pasASIDAbs aag) (pasDomainAbs aag) l; invs b; invs bb; s = ((a, b), ba); s' = ((aa, bb), bc); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); scheduler_modes ba = scheduler_modes bc; interrupted_modes ba = interrupted_modes bc\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) b bb \<and> ((pasDomainAbs aag (cur_domain b) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) = {} \<longrightarrow> pasDomainAbs aag (cur_domain bb) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_thread b = cur_thread bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> scheduler_globals_frame_equiv b bb \<and> (cur_thread b \<noteq> idle_thread bb \<longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state bb))) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<lbrakk>(((a, b), ba), (aa, bb), bc) \<in> sameFor_subject (pasPolicy aag) (pasObjectAbs aag) (pasIRQAbs aag) (pasASIDAbs aag) (pasDomainAbs aag) l; invs b; invs bb; s = ((a, b), ba); s' = ((aa, bb), bc); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); scheduler_modes ba = scheduler_modes bc; interrupted_modes ba = interrupted_modes bc\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) b bb \<and> ((pasDomainAbs aag (cur_domain b) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) = {} \<longrightarrow> pasDomainAbs aag (cur_domain bb) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_thread b = cur_thread bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> scheduler_globals_frame_equiv b bb \<and> (cur_thread b \<noteq> idle_thread bb \<longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state bb))) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. \<exists>xa. xa \<in> pasDomainAbs aag x \<and> xa \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) b bb \<and> ((\<exists>x. x \<in> pasDomainAbs aag (cur_domain b) \<and> x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) \<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> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap b bb) \<and> ((\<exists>x. x \<in> pasDomainAbs aag (cur_domain bb) \<and> x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) \<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> a = aa) \<and> ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap b bb); invs b; invs bb; s = ((a, b), ba); s' = ((aa, bb), bc); domain_fields_equiv b bb; idle_thread b = idle_thread bb; globals_equiv_scheduler b bb; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap b bb; equiv_irq_state (machine_state b) (machine_state bb); scheduler_modes ba = scheduler_modes bc; interrupted_modes ba = interrupted_modes bc\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. \<exists>xa. xa \<in> pasDomainAbs aag x \<and> xa \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) b bb \<and> (((\<forall>x\<in>pasDomainAbs aag (cur_domain b). \<forall>y\<in>subjectReads (pasPolicy aag) (OrdinaryLabel l). x \<noteq> y) \<longrightarrow> (\<exists>x. x \<in> pasDomainAbs aag (cur_domain bb) \<and> x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l))) \<longrightarrow> cur_thread b = cur_thread bb \<and> scheduler_action b = scheduler_action bb \<and> work_units_completed b = work_units_completed bb \<and> scheduler_globals_frame_equiv b bb \<and> (cur_thread b \<noteq> idle_thread bb \<longrightarrow> exclusive_state (machine_state b) = exclusive_state (machine_state bb))) proof (prove)
goal:
No subgoals!