theory Noninterference

lemma scheduler_step_2_confidentiality:
  notes blob = invs_if_def Invs_def sys_mode_of_def silc_inv_cur pas_refined_cur
               guarded_pas_domain_cur internal_state_s0 tick_done_def
  assumes uwr: "(s,t) \<in> uwr PSched" "(s,t) \<in> uwr u"
  assumes step_s: "(s,s') \<in> data_type.Step (ADT_A_if utf) ()"
  assumes step_t: "(t,t') \<in> data_type.Step (ADT_A_if utf) ()"
  assumes reach_s: "system.reachable (ADT_A_if utf) s0 s"
  assumes reach_t: "system.reachable (ADT_A_if utf) s0 t"
  shows "\<lbrakk> (sys_mode_of s) = KernelSchedule True; (sys_mode_of t) = KernelSchedule True \<rbrakk>
           \<Longrightarrow> (s',t') \<in> uwr u" apply (insert uwr step_s step_t) apply (rule_tac s=s and s'=s' in schedule_step,simp_all) apply (rule_tac s=t and s'=t' in schedule_step,simp_all) apply (cut_tac ADT_A_if_reachable_invs_if[OF reach_s]) apply (cut_tac ADT_A_if_reachable_invs_if[OF reach_t]) apply (rule equiv_valid_2E[where s="internal_state_if s" and t="internal_state_if t",
                             OF schedule_if_reads_respects_scheduler_2
                                  [where aag="initial_aag" and st="s0_internal"
                                     and l="label_for_partition u", OF domains_distinct]],
         assumption,assumption) apply (rule uwr_scheduler_affects_equiv,simp+) apply ((clarsimp simp: blob)+)[2] apply (rule scheduler_affects_equiv_uwr,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (4 subgoals):
 1. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> scheduler_equiv initial_aag (internal_state_if s) (internal_state_if t) \<and> scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s) (internal_state_if t)
 2. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> (einvs and pas_refined initial_aag and silc_inv initial_aag s0_internal and guarded_pas_domain initial_aag and tick_done) (internal_state_if s)
 3. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> (einvs and pas_refined initial_aag and silc_inv initial_aag s0_internal and guarded_pas_domain initial_aag and tick_done) (internal_state_if t)
 4. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t; scheduler_equiv initial_aag (internal_state_if s') (internal_state_if t'); scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s') (internal_state_if t'); user_context_of s = user_context_of s \<and> user_context_of t = user_context_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (3 subgoals):
 1. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> invs (internal_state_if s) \<and> valid_list (internal_state_if s) \<and> valid_sched (internal_state_if s) \<and> pas_refined initial_aag (internal_state_if s) \<and> silc_inv initial_aag s0_internal (internal_state_if s) \<and> guarded_pas_domain initial_aag (internal_state_if s) \<and> tick_done (internal_state_if s)
 2. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t\<rbrakk> \<Longrightarrow> (einvs and pas_refined initial_aag and silc_inv initial_aag s0_internal and guarded_pas_domain initial_aag and tick_done) (internal_state_if t)
 3. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t; scheduler_equiv initial_aag (internal_state_if s') (internal_state_if t'); scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s') (internal_state_if t'); user_context_of s = user_context_of s \<and> user_context_of t = user_context_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>sys_mode_of s = KernelSchedule True; sys_mode_of t = KernelSchedule True; uwr2 s PSched t; uwr2 s u t; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (t, t') \<in> data_type.Step (ADT_A_if utf) (); (user_context_of s, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; user_context_of s' = user_context_of s; r = user_context_of s; (user_context_of t, internal_state_if t') \<in> fst (schedule_if (user_context_of t) (internal_state_if t)); sys_mode_of t' = KernelExit; user_context_of t' = user_context_of t; ra = user_context_of t; invs_if s; invs_if t; scheduler_equiv initial_aag (internal_state_if s') (internal_state_if t'); scheduler_affects_equiv initial_aag (label_for_partition u) (internal_state_if s') (internal_state_if t'); user_context_of s = user_context_of s \<and> user_context_of t = user_context_of t\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal:
No subgoals!