theory ArchNoninterference

lemma partitionIntegrity_subjectAffects_aobj[Noninterference_assms]:
  assumes par_inte: "partitionIntegrity aag s s'"
  and "kheap s x = Some (ArchObj ao)"
      "kheap s x \<noteq> kheap s' x"
      "silc_inv aag st s"
      "pas_refined aag s"
      "pas_wellformed_noninterference aag"
  notes inte_obj = par_inte[THEN partitionIntegrity_integrity, THEN integrity_subjects_obj,
                            THEN spec[where x=x], simplified integrity_obj_def, simplified]
  shows "subject_can_affect_label_directly aag (pasObjectAbs aag x)" proof (cases "pasObjectAbs aag x = pasSubject aag") case True then show ?thesis by (simp add: subjectAffects.intros(1)) next case False obtain ao' where ao': "kheap s' x = Some (ArchObj ao')" using assms False inte_obj_arch[OF inte_obj] by (auto elim: integrity_obj_atomic.cases) have arch_tro:
    "arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
                               {pasSubject aag} (pasObjectAbs aag x) ao ao'" using assms False ao' inte_obj_arch[OF inte_obj] by (auto elim: integrity_obj_atomic.cases) show ?thesis using assms ao' arch_tro by (fastforce dest: partitionIntegrity_subjectAffects_aobj') qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (2 subgoals):
 1. is_subject aag x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
is_subject aag x

goal (2 subgoals):
 1. is_subject aag x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (chain)
picking this:
is_subject aag x proof (prove)
using this:
is_subject aag x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (1 subgoal):
 1. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (1 subgoal):
 1. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
pasObjectAbs aag x \<noteq> pasSubject aag

goal (1 subgoal):
 1. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. (\<And>ao'. kheap s' x = Some (ArchObj ao') \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
partitionIntegrity aag s s'
kheap s x = Some (ArchObj ao)
kheap s x \<noteq> kheap s' x
silc_inv aag st s
pas_refined aag s
pas_wellformed_noninterference aag
pasObjectAbs aag x \<noteq> pasSubject aag
\<lbrakk>kheap s x = Some (ArchObj ?ao); kheap s x \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) (kheap s' x)

goal (1 subgoal):
 1. (\<And>ao'. kheap s' x = Some (ArchObj ao') \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
kheap s' x = Some (ArchObj ao')

goal (1 subgoal):
 1. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao' proof (prove)
using this:
partitionIntegrity aag s s'
kheap s x = Some (ArchObj ao)
kheap s x \<noteq> kheap s' x
silc_inv aag st s
pas_refined aag s
pas_wellformed_noninterference aag
pasObjectAbs aag x \<noteq> pasSubject aag
kheap s' x = Some (ArchObj ao')
\<lbrakk>kheap s x = Some (ArchObj ?ao); kheap s x \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) (kheap s' x)

goal (1 subgoal):
 1. arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao' proof (state)
this:
arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'

goal (1 subgoal):
 1. pasObjectAbs aag x \<noteq> pasSubject aag \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
partitionIntegrity aag s s'
kheap s x = Some (ArchObj ao)
kheap s x \<noteq> kheap s' x
silc_inv aag st s
pas_refined aag s
pas_wellformed_noninterference aag
kheap s' x = Some (ArchObj ao')
arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal:
No subgoals!