theory Noninterference

lemma uwr_reads_equiv_f_g_affects_equiv:
  "\<lbrakk> (s, t) \<in> uwr PSched; (s, t) \<in> uwr (part s); (s, t) \<in> uwr (Partition l); invs_if s; invs_if t;
     (part s, Partition l) \<in> policyFlows (pasPolicy initial_aag); part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> reads_equiv_f_g (current_aag (internal_state_if s))
                         (internal_state_if s) (internal_state_if t) \<and>
         affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel l)
                       (internal_state_if s) (internal_state_if t)" apply (rule sameFor_reads_f_g_affects_equiv) apply (simp add: current_aag_def) apply (simp add: invs_if_def Invs_def) apply blast apply (clarsimp simp: uwr_def part_def current_aag_def partition_def split: if_splits) apply (simp add: part_def split: if_splits add: partition_def current_aag_def flow_then_affect) apply (clarsimp simp: uwr_def part_def current_aag_def partition_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> reads_equiv_f_g (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) \<and> affects_equiv (current_aag (internal_state_if s)) (OrdinaryLabel l) (internal_state_if s) (internal_state_if t) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> pas_cur_domain (current_aag (internal_state_if s)) (internal_state_if s)
 2. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s)) ?st (internal_state_if s)
 3. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))
 4. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy (current_aag (internal_state_if s))) (label_of (pasSubject (current_aag (internal_state_if s))))
 5. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition l) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s)) ?st (internal_state_if s)
 2. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))
 3. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy (current_aag (internal_state_if s))) (label_of (pasSubject (current_aag (internal_state_if s))))
 4. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition l) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if s) \<and> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) \<and> domain_sep_inv False s0_internal (internal_state_if s) \<and> pas_refined_if s \<and> guarded_pas_domain_if s \<and> idle_equiv s0_internal (internal_state_if s) \<and> valid_domain_list (internal_state_if s) \<and> valid_vspace_objs_if (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s) \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if s)) \<and> (domain_time (internal_state_if s) = 0 \<longrightarrow> scheduler_action (internal_state_if s) = choose_new_thread) \<and> (snd s \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if s) \<longrightarrow> user_context_of s = idle_context (internal_state_if s)) \<and> (case snd s of InUserMode \<Rightarrow> ct_running (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if s) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if s)) \<and> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if s) \<or> ct_idle (internal_state_if s)) \<and> scheduler_action (internal_state_if s) = resume_cur_thread | _ \<Rightarrow> True); invs (internal_state_if t) \<and> valid_list (internal_state_if t) \<and> valid_sched (internal_state_if t) \<and> only_timer_irq_inv timer_irq s0_internal (internal_state_if t) \<and> silc_inv (current_aag (internal_state_if t)) s0_internal (internal_state_if t) \<and> domain_sep_inv False s0_internal (internal_state_if t) \<and> pas_refined_if t \<and> guarded_pas_domain_if t \<and> idle_equiv s0_internal (internal_state_if t) \<and> valid_domain_list (internal_state_if t) \<and> valid_vspace_objs_if (internal_state_if t) \<and> det_inv (sys_mode_of t) (cur_thread_context_of t) (internal_state_if t) \<and> (snd t \<noteq> KernelSchedule True \<longrightarrow> 0 < domain_time (internal_state_if t)) \<and> (domain_time (internal_state_if t) = 0 \<longrightarrow> scheduler_action (internal_state_if t) = choose_new_thread) \<and> (snd t \<noteq> KernelExit \<longrightarrow> ct_idle (internal_state_if t) \<longrightarrow> user_context_of t = idle_context (internal_state_if t)) \<and> (case snd t of InUserMode \<Rightarrow> ct_running (internal_state_if t) \<and> scheduler_action (internal_state_if t) = resume_cur_thread | InIdleMode \<Rightarrow> ct_idle (internal_state_if t) \<and> scheduler_action (internal_state_if t) = resume_cur_thread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running (internal_state_if t)) \<and> (ct_running (internal_state_if t) \<or> ct_idle (internal_state_if t)) \<and> scheduler_action (internal_state_if t) = resume_cur_thread | KernelExit \<Rightarrow> (ct_running (internal_state_if t) \<or> ct_idle (internal_state_if t)) \<and> scheduler_action (internal_state_if t) = resume_cur_thread | _ \<Rightarrow> True); policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s)) ?st (internal_state_if s)
 2. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))
 3. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy (current_aag (internal_state_if s))) (label_of (pasSubject (current_aag (internal_state_if s))))
 4. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition l) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition (label_of (pasSubject (current_aag (internal_state_if s)))))
 2. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy (current_aag (internal_state_if s))) (label_of (pasSubject (current_aag (internal_state_if s))))
 3. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition l) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy (current_aag (internal_state_if s))) (label_of (pasSubject (current_aag (internal_state_if s))))
 2. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition l) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s (Partition l) t; invs_if s; invs_if t; policy2 (part s) (Partition l); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (s, t) \<in> same_for (current_aag (internal_state_if s)) (Partition l) proof (prove)
goal:
No subgoals!