kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference

lemma do_user_op_A_if_confidentiality':
  "\<lbrakk> (XX, YY) \<in> uwr PSched; XX = s; YY = t; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u; invs_if s;
     invs_if t; invs_if s'; invs_if t'; (part s, u) \<in> policyFlows (pasPolicy initial_aag);
     part s \<noteq> PSched; u \<noteq> PSched; sys_mode_of s = InUserMode; sys_mode_of t = InUserMode;
     ((fst s),None,s_aux) \<in> check_active_irq_A_if; ((fst t),None,t_aux) \<in> check_active_irq_A_if;
     (s_aux,xx,fst s') \<in> do_user_op_A_if utf; (t_aux,yy,fst t') \<in> do_user_op_A_if utf;
     snd s' = (case xx of None \<Rightarrow> InUserMode | Some xxx \<Rightarrow> KernelEntry xxx);
     snd t' = (case yy of None \<Rightarrow> InUserMode | Some yyy \<Rightarrow> KernelEntry yyy) \<rbrakk>
     \<Longrightarrow> xx = yy \<and> (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" by (rule do_user_op_A_if_confidentiality, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 XX PSched YY; XX = s; YY = t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; sys_mode_of s = InUserMode; sys_mode_of t = InUserMode; (fst s, None, s_aux) \<in> check_active_irq_A_if; (fst t, None, t_aux) \<in> check_active_irq_A_if; (s_aux, xx, fst s') \<in> do_user_op_A_if utf; (t_aux, yy, fst t') \<in> do_user_op_A_if utf; snd s' = (case xx of None \<Rightarrow> InUserMode | Some xxx \<Rightarrow> KernelEntry xxx); snd t' = (case yy of None \<Rightarrow> InUserMode | Some yyy \<Rightarrow> KernelEntry yyy)\<rbrakk> \<Longrightarrow> xx = yy \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
theory Noninterference

lemma kernel_schedule_if_confidentiality':
  "\<lbrakk> (XX, YY) \<in> uwr PSched; XX = s; YY = t; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u; invs_if s;
     invs_if t; invs_if s'; invs_if t'; (part s, u) \<in> policyFlows (pasPolicy initial_aag);
     part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s);
     ((fst s),(),(fst s')) \<in> kernel_schedule_if;
     ((fst t),(),(fst t')) \<in> kernel_schedule_if; snd s' = snd t' \<rbrakk>
     \<Longrightarrow> (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" by (blast dest: kernel_schedule_if_confidentiality)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 XX PSched YY; XX = s; YY = t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s); (fst s, (), fst s') \<in> kernel_schedule_if; (fst t, (), fst t') \<in> kernel_schedule_if; snd s' = snd t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
theory Noninterference

lemma thread_set_tcb_context_update_runnable_globals_equiv:
  "\<lbrace>globals_equiv st and st_tcb_at runnable t and invs\<rbrace>
   thread_set (tcb_arch_update (arch_tcb_context_set uc)) t
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (rule hoare_pre) apply (rule thread_set_context_globals_equiv) apply clarsimp apply (frule invs_valid_idle) apply (fastforce simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and st_tcb_at runnable t and invs\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set uc)) t \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set uc)) t \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (globals_equiv st and st_tcb_at runnable t and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and st_tcb_at runnable t and invs) s \<Longrightarrow> ((\<lambda>s. t = idle_thread s \<longrightarrow> uc = idle_context s) and invs and globals_equiv st) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>globals_equiv st s; st_tcb_at runnable (idle_thread s) s; invs s; t = idle_thread s\<rbrakk> \<Longrightarrow> uc = idle_context s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>globals_equiv st s; st_tcb_at runnable (idle_thread s) s; invs s; t = idle_thread s; valid_idle s\<rbrakk> \<Longrightarrow> uc = idle_context s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma thread_set_tcb_context_update_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_g aag (l :: 'a subject_label) (st_tcb_at runnable t and invs)
                          (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule thread_set_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp thread_set_tcb_context_update_runnable_globals_equiv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (st_tcb_at runnable t and invs) (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t)
 2. \<And>s. (st_tcb_at runnable t and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t)
 2. doesnt_touch_globals ?Q3 (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t)
 3. \<And>s. (st_tcb_at runnable t and invs) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t)
 2. \<And>s. (st_tcb_at runnable t and invs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set uc)) t \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (st_tcb_at runnable t and invs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> (globals_equiv st and st_tcb_at runnable t and invs) s
 2. \<And>s. (st_tcb_at runnable t and invs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q3) s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma thread_set_tcb_context_update_silc_inv:
  "thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>silc_inv aag st\<rbrace>" apply (rule thread_set_silc_inv) apply (simp add: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcb_arch_update (arch_tcb_context_set f) tcb) = getF tcb proof (prove)
goal:
No subgoals!
theory Noninterference

lemma kernel_call_A_if_confidentiality':
  "\<lbrakk> (XX, YY) \<in> uwr PSched; XX = s; YY = t; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u;
     invs_if s; invs_if t; invs_if s'; invs_if t';
     (part s, u) \<in> policyFlows (pasPolicy initial_aag); part s \<noteq> PSched; u \<noteq> PSched;
     ((fst s),x,(fst s')) \<in> kernel_call_A_if e; ((fst t),y,(fst t')) \<in> kernel_call_A_if e;
     e \<noteq> Interrupt; sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e;
     snd s' = (case x of True \<Rightarrow> KernelPreempted | _ \<Rightarrow> KernelSchedule False);
     snd t' = (case y of True \<Rightarrow> KernelPreempted | _ \<Rightarrow> KernelSchedule False) \<rbrakk>
     \<Longrightarrow> x = y \<and> (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" by (blast dest: kernel_call_A_if_confidentiality)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 XX PSched YY; XX = s; YY = t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; (fst s, x, fst s') \<in> kernel_call_A_if e; (fst t, y, fst t') \<in> kernel_call_A_if e; e \<noteq> Interrupt; sys_mode_of s = KernelEntry e; sys_mode_of t = KernelEntry e; snd s' = (case x of True \<Rightarrow> KernelPreempted | False \<Rightarrow> KernelSchedule False); snd t' = (case y of True \<Rightarrow> KernelPreempted | False \<Rightarrow> KernelSchedule False)\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
theory Noninterference

lemma thread_get_tcb_context_reads_respects_g:
  "reads_respects_g aag l
     (\<lambda>s. t = idle_thread s \<or> is_subject aag t) (thread_get (arch_tcb_context_get o tcb_arch) t)" apply (simp add: thread_get_def gets_the_def equiv_valid_def2) apply (rule_tac W="\<lambda> rv rv'. arch_tcb_context_get (tcb_arch rv) = arch_tcb_context_get (tcb_arch rv')"
              and Q="\<top>\<top>" in equiv_valid_rv_bind) apply (rule thread_get_tcb_context_reads_respects_g_helper) apply (rule return_ev2, simp) apply (rule hoare_post_taut) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. t = idle_thread s \<or> is_subject aag t) (thread_get (arch_tcb_context_get \<circ> tcb_arch) t) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (=) (\<lambda>s. t = idle_thread s \<or> is_subject aag t) (do tcb <- gets (get_tcb t) >>= assert_opt;
return (arch_tcb_context_get (tcb_arch tcb))
od) proof (prove)
goal (3 subgoals):
 1. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>rv rv'. arch_tcb_context_get (tcb_arch rv) = arch_tcb_context_get (tcb_arch rv')) (\<lambda>s. t = idle_thread s \<or> is_subject aag t) (gets (get_tcb t) >>= assert_opt)
 2. \<And>rv rv'. arch_tcb_context_get (tcb_arch rv) = arch_tcb_context_get (tcb_arch rv') \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (return (arch_tcb_context_get (tcb_arch rv))) (return (arch_tcb_context_get (tcb_arch rv')))
 3. \<lbrace>\<lambda>s. t = idle_thread s \<or> is_subject aag t\<rbrace> gets (get_tcb t) >>= assert_opt \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. arch_tcb_context_get (tcb_arch rv) = arch_tcb_context_get (tcb_arch rv') \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (return (arch_tcb_context_get (tcb_arch rv))) (return (arch_tcb_context_get (tcb_arch rv')))
 2. \<lbrace>\<lambda>s. t = idle_thread s \<or> is_subject aag t\<rbrace> gets (get_tcb t) >>= assert_opt \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t = idle_thread s \<or> is_subject aag t\<rbrace> gets (get_tcb t) >>= assert_opt \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory Noninterference

lemma kernel_exit_if_reads_respects_g_2:
  "equiv_valid_2 (reads_equiv_g aag) (affects_equiv aag l) (affects_equiv aag l) (=)
                 (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))
                 (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))
                 (kernel_exit_if tc) (kernel_exit_if tc')" apply (simp add: kernel_exit_if_def) apply (fold equiv_valid_def2) apply (wp thread_get_tcb_context_reads_respects_g) apply (fastforce dest: requiv_g_cur_thread_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv_g aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) (kernel_exit_if tc) (kernel_exit_if tc') proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (=) (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) (gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) (gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)) proof (prove)
goal (1 subgoal):
 1. \<And>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s) \<Longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> (cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma kernel_exit_if_reads_respects_f_g_2:
  "equiv_valid_2 (reads_equiv_f_g aag) (affects_equiv aag l) (affects_equiv aag l) (=)
     (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)))
     (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)))
     (kernel_exit_if tc) (kernel_exit_if tc')" apply (rule equiv_valid_2_guard_imp) apply (rule reads_respects_f_g_2'[where Q="\<top>" and Q'="\<top>", OF kernel_exit_if_reads_respects_g_2]) apply (wp | simp | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv_f_g aag) (affects_equiv aag l) (affects_equiv aag l) (=) (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))) (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))) (kernel_exit_if tc) (kernel_exit_if tc') proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 (reads_equiv_f_g aag) (affects_equiv aag l) (affects_equiv aag l) (=) ?Q ?Q' (kernel_exit_if tc) (kernel_exit_if tc')
 2. \<And>s. (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))) s \<Longrightarrow> ?Q s
 3. \<And>s. (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))) s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>silc_inv aag ?st4 and (\<lambda>_. True)\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>_. silc_inv aag ?st4\<rbrace>
 2. \<lbrace>silc_inv aag ?st4 and (\<lambda>_. True)\<rbrace> kernel_exit_if tc' \<lbrace>\<lambda>_. silc_inv aag ?st4\<rbrace>
 3. \<And>s. (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))) s \<Longrightarrow> (silc_inv aag ?st4 and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) and (\<lambda>_. True)) s
 4. \<And>s. (silc_inv aag st and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s))) s \<Longrightarrow> (silc_inv aag ?st4 and (\<lambda>s. cur_thread s = idle_thread s \<or> is_subject aag (cur_thread s)) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma use_ev2:
  "\<lbrakk> equiv_valid_2 I A B R P P' f f'; (rv,s') \<in> fst (f s);
     (rv',t') \<in> fst (f' t); P s; P' t; I s t; A s t \<rbrakk>
     \<Longrightarrow> R rv rv' \<and> I s' t' \<and> B s' t'" by (fastforce simp: equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid_2 I A B R P P' f f'; (rv, s') \<in> fst (f s); (rv', t') \<in> fst (f' t); P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R rv rv' \<and> I s' t' \<and> B s' t'
theory Noninterference

lemma reads_equiv_f_g_reads_equiv_g:
  "reads_equiv_f_g aag s t \<Longrightarrow> reads_equiv_g aag s t" by (fastforce simp: reads_equiv_f_g_def reads_equiv_g_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_f_g aag s t \<Longrightarrow> reads_equiv_g aag s t
theory Noninterference

lemma partitionIntegrity_part_unchanged:
  "\<lbrakk>partitionIntegrity aag (internal_state_if s) (internal_state_if s'); part s \<noteq> PSched;
    part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' = part s" apply (simp add: part_def split: if_splits
             add: partition_def partitionIntegrity_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag (internal_state_if s) (internal_state_if s'); part s \<noteq> PSched; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' = part s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma big_step_R_rtranclp:
  "system.reachable (big_step_ADT_A_if utf) s0 s
       \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s" apply (simp add: reachable_def execution_def) apply (clarsimp simp: big_step_ADT_A_if_def Fin_big_step_adt Fin_ADT_if steps_eq_Run) apply (rule Run_big_steps_tranclp) apply (simp add: big_step_ADT_A_if_def big_step_adt_def Init_ADT_if) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s proof (prove)
goal (1 subgoal):
 1. \<exists>js. s \<in> Fin (big_step_ADT_A_if utf) ` steps (data_type.Step (big_step_ADT_A_if utf)) (Init (big_step_ADT_A_if utf) s0) js \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s proof (prove)
goal (1 subgoal):
 1. \<And>js a b ba. \<lbrakk>((a, b), ba) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s0; (((a, b), ba), s) \<in> Run (data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap)) js\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s proof (prove)
goal (1 subgoal):
 1. \<And>js a b ba. \<lbrakk>((a, b), ba) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s0; (((a, b), ba), s) \<in> Run (data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap)) js\<rbrakk> \<Longrightarrow> (s0, s) \<in> Run (big_steps (?C11 js a b ba) big_step_R (?exmap11 js a b ba)) (?js11 js a b ba) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma sub_big_steps_strict_prefix:
  "(s', as @ bs) \<in> sub_big_steps A R s \<Longrightarrow>
   \<exists>t. (t, as) \<in> sub_big_steps A R s" apply (induct bs arbitrary: s s' rule: rev_induct) apply fastforce apply (subst (asm) append_assoc[symmetric]) apply (drule sub_big_steps_App) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s', as @ bs) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. (s', as @ []) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s
 2. \<And>x xs s s'. \<lbrakk>\<And>s s'. (s', as @ xs) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s; (s', as @ xs @ [x]) \<in> sub_big_steps A R s\<rbrakk> \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s'. \<lbrakk>\<And>s s'. (s', as @ xs) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s; (s', as @ xs @ [x]) \<in> sub_big_steps A R s\<rbrakk> \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s'. \<lbrakk>\<And>s s'. (s', as @ xs) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s; (s', (as @ xs) @ [x]) \<in> sub_big_steps A R s\<rbrakk> \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s'. \<lbrakk>\<And>s s'. (s', as @ xs) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s; \<exists>s'a. (s'a, as @ xs) \<in> sub_big_steps A R s \<and> (s'a, s') \<in> data_type.Step A x \<and> \<not> R s s'\<rbrakk> \<Longrightarrow> \<exists>t. (t, as) \<in> sub_big_steps A R s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma uwr_part_sys_mode_of_eq':
  "\<lbrakk>(s,t) \<in> uwr (part x); part s = part x; part t = part x; part x \<noteq> PSched\<rbrakk>
    \<Longrightarrow> sys_mode_of s = sys_mode_of t" apply (fastforce intro: uwr_part_sys_mode_of_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s (part x) t; part s = part x; part t = part x; part x \<noteq> PSched\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal:
No subgoals!
theory Noninterference

lemma app_Cons:
  "xs @ (a # b) = (xs @ [a]) @ b" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs @ a # b = (xs @ [a]) @ b
theory Noninterference

lemma sys_mode_of_eq_big_step_R_contradiction:
  "\<lbrakk> sys_mode_of s = sys_mode_of t; sys_mode_of s' = sys_mode_of t';
     big_step_R s s'; \<not> big_step_R t t' \<rbrakk>
     \<Longrightarrow> False" apply (simp add: big_step_R_def) apply (case_tac s, case_tac t, simp_all) apply (case_tac s', case_tac t', simp_all) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = sys_mode_of t; sys_mode_of s' = sys_mode_of t'; big_step_R s s'; \<not> big_step_R t t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = sys_mode_of t; sys_mode_of s' = sys_mode_of t'; snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit; (snd t = KernelExit \<longrightarrow> \<not> interrupted_modes (snd t')) \<and> (interrupted_modes (snd t) \<longrightarrow> snd t' \<noteq> KernelExit)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>sys_mode_of (a, b) = sys_mode_of (aa, ba); sys_mode_of s' = sys_mode_of t'; b = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes b \<and> snd s' = KernelExit; (ba = KernelExit \<longrightarrow> \<not> interrupted_modes (snd t')) \<and> (interrupted_modes ba \<longrightarrow> snd t' \<noteq> KernelExit); s = (a, b); t = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>sys_mode_of (a, b) = sys_mode_of (aa, ba); sys_mode_of (ab, bb) = sys_mode_of (ac, bc); b = KernelExit \<and> interrupted_modes bb \<or> interrupted_modes b \<and> bb = KernelExit; (ba = KernelExit \<longrightarrow> \<not> interrupted_modes bc) \<and> (interrupted_modes ba \<longrightarrow> bc \<noteq> KernelExit); s = (a, b); t = (aa, ba); s' = (ab, bb); t' = (ac, bc)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Noninterference

lemma unit_list_as_replicate:
  "(as::unit list) = replicate (length as) ()" apply (induct as, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. as = replicate (length as) () proof (prove)
goal:
No subgoals!
theory Noninterference

lemma kernel_exit_A_if_confidentiality':
  "\<lbrakk>(XX, YY) \<in> uwr PSched; XX = s; YY = t; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u;
    invs_if s;     invs_if t;   invs_if s'; invs_if t';
    (part s, u) \<in> policyFlows (pasPolicy initial_aag);
    part s \<noteq> PSched; u \<noteq> PSched;
    ((fst s),x,(fst s')) \<in> kernel_exit_A_if;
    ((fst t),y,(fst t')) \<in> kernel_exit_A_if;
    sys_mode_of s = KernelExit; sys_mode_of t = KernelExit;
    snd s' = f x; snd t' = f y\<rbrakk> \<Longrightarrow>
   x = y \<and>
   (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s)" apply (blast dest: kernel_exit_A_if_confidentiality) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 XX PSched YY; XX = s; YY = t; uwr2 s (part s) t; uwr2 s u t; invs_if s; invs_if t; invs_if s'; invs_if t'; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; (fst s, x, fst s') \<in> kernel_exit_A_if; (fst t, y, fst t') \<in> kernel_exit_A_if; sys_mode_of s = KernelExit; sys_mode_of t = KernelExit; snd s' = f x; snd t' = f y\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' proof (prove)
goal:
No subgoals!