kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference

lemma try_some_magic:
  "(\<forall>x. y = Some x \<longrightarrow> P x) = ((\<exists>x. y = Some x) \<longrightarrow> P (the y))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. y = Some x \<longrightarrow> P x) = ((\<exists>x. y = Some x) \<longrightarrow> P (the y))
theory Noninterference

lemma thread_set_as_user2:
  "thread_set (tcb_arch_update (arch_tcb_context_set uc)) t = as_user t (modify (\<lambda>_. uc))" proof - have P: "\<And>f. det (modify f)" by (simp add: modify_def) thus ?thesis apply (simp add: as_user_def P thread_set_def) apply (clarsimp simp: select_f_def simpler_modify_def bind_def
                          image_def fun_cong[OF arch_tcb_update_aux2]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_set (tcb_arch_update (arch_tcb_context_set uc)) t = as_user t (modify (\<lambda>_. uc)) proof (state)
goal (1 subgoal):
 1. thread_set (tcb_arch_update (arch_tcb_context_set uc)) t = as_user t (modify (\<lambda>_. uc)) proof (prove)
goal (1 subgoal):
 1. \<And>f. det (modify f) proof (state)
this:
det (modify ?f)

goal (1 subgoal):
 1. thread_set (tcb_arch_update (arch_tcb_context_set uc)) t = as_user t (modify (\<lambda>_. uc)) proof (prove)
using this:
det (modify ?f)

goal (1 subgoal):
 1. thread_set (tcb_arch_update (arch_tcb_context_set uc)) t = as_user t (modify (\<lambda>_. uc)) proof (prove)
goal (1 subgoal):
 1. do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb_arch_update (arch_tcb_context_set uc) tcb))
od = do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (modify (\<lambda>_. uc) (arch_tcb_context_get (tcb_arch tcb)));
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od proof (prove)
goal:
No subgoals! proof (state)
this:
thread_set (tcb_arch_update (arch_tcb_context_set uc)) t = as_user t (modify (\<lambda>_. uc))

goal:
No subgoals!
theory Noninterference

lemma handle_preemption_agnostic_tc:
  "\<forall>P Q uc uc'. \<lbrace>P\<rbrace> handle_preemption_if uc \<lbrace>\<lambda>_. Q\<rbrace> \<longrightarrow> \<lbrace>P\<rbrace> handle_preemption_if uc' \<lbrace>\<lambda>_. Q\<rbrace>" apply (clarsimp simp add: handle_preemption_if_def bind_assoc[symmetric]) apply (erule bind_return_ign) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>P Q uc uc'. \<lbrace>P\<rbrace> handle_preemption_if uc \<lbrace>\<lambda>_. Q\<rbrace> \<longrightarrow> \<lbrace>P\<rbrace> handle_preemption_if uc' \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P Q uc uc'. \<lbrace>P\<rbrace> do y <- do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od;
return uc
od \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od;
return uc'
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Noninterference

lemma handle_preemption_reads_respects_scheduler:
  assumes domains_distinct[wp]: "pas_domains_distinct (aag :: 'a subject_label PAS)"
  shows
    "reads_respects_scheduler aag l (einvs and pas_refined aag and guarded_pas_domain aag
                                           and domain_sep_inv False st and silc_inv aag st'
                                           and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s))
                              (handle_preemption_if uc)" apply (simp add: handle_preemption_if_def) apply (wp when_ev handle_interrupt_reads_respects_scheduler
            dmo_getActiveIRQ_return_axiom[simplified try_some_magic]
            dmo_getActive_IRQ_reads_respect_scheduler
         | simp add: imp_conjR| wp (once) hoare_drop_imps)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)) (handle_preemption_if uc) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)) (do irq <- do_machine_op (getActiveIRQ True);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return uc
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> pas_refined aag s \<and> guarded_pas_domain aag s \<and> domain_sep_inv False st s \<and> silc_inv aag st' s \<and> irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> irq_masks_of_state ?st6 = irq_masks_of_state s \<and> domain_sep_inv False ?st42 s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma internal_state_s0: "internal_state_if s0 = s0_internal" by (simp add: s0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. internal_state_if s0 = s0_internal
theory Noninterference

lemma cur_domain_reads:
  "(s,s') \<in> uwr u
   \<Longrightarrow> reads_scheduler_cur_domain initial_aag (label_for_partition u) (internal_state_if s)
   \<Longrightarrow> (user_modes (sys_mode_of s) \<longrightarrow> user_context_of s = user_context_of s') \<and>
       sys_mode_of s = sys_mode_of s'" by (cases u) (auto simp: reads_scheduler_def uwr_def sameFor_def sameFor_subject_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s u s'; reads_scheduler_cur_domain initial_aag (label_for_partition u) (internal_state_if s)\<rbrakk> \<Longrightarrow> (user_modes (sys_mode_of s) \<longrightarrow> user_context_of s = user_context_of s') \<and> sys_mode_of s = sys_mode_of s'
theory Noninterference

lemma equiv_valid_2E:
  assumes ev: "equiv_valid_2 I A B R P P' f g"
  assumes f: "(a,s') \<in> fst (f s)"
  assumes g: "(b,t') \<in> fst (g t)"
  assumes I: "I s t \<and> A s t"
  assumes P: "P s"
  assumes P': "P' t"
  assumes Q: "I s' t' \<Longrightarrow> B s' t' \<Longrightarrow> R a b \<Longrightarrow> S"
  shows S apply (insert ev) apply (clarsimp simp: equiv_valid_2_def) apply (drule_tac x=s in spec) apply (drule_tac x=t in spec) apply (simp add: I P P') apply (drule bspec[OF _ f],simp) apply (drule bspec[OF _ g],simp) apply (rule Q,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' f g \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. \<forall>s t. P s \<and> P' t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t') \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. \<forall>t. P s \<and> P' t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t') \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. P s \<and> P' t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t') \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. \<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (g t). R rva rvb \<and> I s' t' \<and> B s' t' \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> R a rvb \<and> I s' t' \<and> B s' t' \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. R a b \<and> I s' t' \<and> B s' t' \<Longrightarrow> S proof (prove)
goal:
No subgoals!
theory Noninterference

lemma schedule_if_context:
  "\<lbrace>\<top>\<rbrace> schedule_if tc \<lbrace>\<lambda>r s. r = tc\<rbrace>" apply (simp add: schedule_if_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> schedule_if tc \<lbrace>\<lambda>r s. r = tc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do y <- schedule;
y <- activate_thread;
return tc
od \<lbrace>\<lambda>r s. r = tc\<rbrace> proof (prove)
goal:
No subgoals!
theory Noninterference

lemma schedule_step:
  assumes schedule:
    "\<And>r. \<lbrakk> (r,internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s));
            sys_mode_of s' = KernelExit; r = user_context_of s; r = user_context_of s' \<rbrakk>
            \<Longrightarrow> P"
  shows
    "\<lbrakk> (sys_mode_of s) = KernelSchedule True; (s,s') \<in> data_type.Step (ADT_A_if utf) () \<rbrakk>
       \<Longrightarrow> P" apply (insert schedule) apply atomize apply (case_tac s, clarsimp) apply (rename_tac uc i_s) apply (simp_all add: system.Step_def execution_def steps_def ADT_A_if_def
                       global_automaton_if_def kernel_schedule_if_def
         | safe | clarsimp)+ apply (frule use_valid[OF _ schedule_if_context], simp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = KernelSchedule True; (s, s') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = KernelSchedule True; (s, s') \<in> Step (ADT_A_if utf) (); \<And>r. \<lbrakk>(r, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)); sys_mode_of s' = KernelExit; r = user_context_of s; r = user_context_of s'\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mode_of s = KernelSchedule True; (s, s') \<in> Step (ADT_A_if utf) (); \<forall>r. (r, internal_state_if s') \<in> fst (schedule_if (user_context_of s) (internal_state_if s)) \<longrightarrow> sys_mode_of s' = KernelExit \<longrightarrow> r = user_context_of s \<longrightarrow> r = user_context_of s' \<longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(((a, b), KernelSchedule True), s') \<in> Step (ADT_A_if utf) (); (a, internal_state_if s') \<in> fst (schedule_if a b) \<longrightarrow> sys_mode_of s' = KernelExit \<longrightarrow> a = user_context_of s' \<longrightarrow> P; s = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>uc i_s. \<lbrakk>(((uc, i_s), KernelSchedule True), s') \<in> Step (ADT_A_if utf) (); (uc, internal_state_if s') \<in> fst (schedule_if uc i_s) \<longrightarrow> sys_mode_of s' = KernelExit \<longrightarrow> uc = user_context_of s' \<longrightarrow> P; s = ((uc, i_s), KernelSchedule True)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>uc i_s a b. \<lbrakk>s = ((uc, i_s), KernelSchedule True); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit); (uc, b) \<notin> fst (schedule_if uc i_s)\<rbrakk> \<Longrightarrow> P
 2. \<And>uc i_s a b. \<lbrakk>s = ((uc, i_s), KernelSchedule True); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit); uc \<noteq> a\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Noninterference

lemma schedule_if_reads_respects_scheduler:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l
           (einvs and pas_refined aag and silc_inv aag st and guarded_pas_domain aag and tick_done)
           (schedule_if uc)" apply (simp add: schedule_if_def) apply (wp schedule_reads_respects_scheduler schedule_guarded_pas_domain) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (einvs and pas_refined aag and silc_inv aag st and guarded_pas_domain aag and tick_done) (schedule_if uc) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (einvs and pas_refined aag and silc_inv aag st and guarded_pas_domain aag and tick_done) (do y <- schedule;
y <- activate_thread;
return uc
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. (einvs and pas_refined aag and silc_inv aag st and guarded_pas_domain aag and tick_done) s \<Longrightarrow> (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done) s \<and> invs s \<and> silc_inv aag ?st13 s \<and> (guarded_pas_domain aag and einvs and pas_refined aag) s \<and> True proof (prove)
goal:
No subgoals!
theory Noninterference

lemma schedule_if_agnostic_tc:
  "\<forall>P Q uc uc'. \<lbrace>P\<rbrace> schedule_if uc \<lbrace>\<lambda>_. Q\<rbrace> \<longrightarrow> \<lbrace>P\<rbrace> schedule_if uc' \<lbrace>\<lambda>_. Q\<rbrace>" apply (clarsimp simp add: schedule_if_def bind_assoc[symmetric]) apply (erule bind_return_ign) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>P Q uc uc'. \<lbrace>P\<rbrace> schedule_if uc \<lbrace>\<lambda>_. Q\<rbrace> \<longrightarrow> \<lbrace>P\<rbrace> schedule_if uc' \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P Q uc uc'. \<lbrace>P\<rbrace> do y <- do y <- schedule;
activate_thread
od;
return uc
od \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- do y <- schedule;
activate_thread
od;
return uc'
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Noninterference

lemma PSched_reachable_interrupted:
  "\<lbrakk> part s = PSched; system.reachable (big_step_ADT_A_if utf) s0 s \<rbrakk>
     \<Longrightarrow> interrupted_modes (sys_mode_of s)" apply (drule big_step_R_rtranclp) apply (drule tranclp_s0) apply (clarsimp simp add: part_def sys_mode_of_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>part s = PSched; reachable s\<rbrakk> \<Longrightarrow> interrupted_modes (sys_mode_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>part s = PSched; big_step_R\<^sup>*\<^sup>* s0 s\<rbrakk> \<Longrightarrow> interrupted_modes (sys_mode_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>part s = PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> interrupted_modes (sys_mode_of s) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma reachable_nonsched_exit:
  "\<lbrakk> system.reachable (big_step_ADT_A_if utf) s0 s; part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> (snd s) = KernelExit" apply (drule big_step_R_rtranclp) apply (drule tranclp_s0) apply (clarsimp simp add: part_def split: if_split_asm) apply (case_tac s) apply simp apply (simp add: sys_mode_of_def) apply (case_tac b; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> snd s = KernelExit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>part s \<noteq> PSched; big_step_R\<^sup>*\<^sup>* s0 s\<rbrakk> \<Longrightarrow> snd s = KernelExit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> snd s = KernelExit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); interrupted_modes (snd s)\<rbrakk> \<Longrightarrow> snd s = KernelExit proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); interrupted_modes (snd s); s = (a, b)\<rbrakk> \<Longrightarrow> snd s = KernelExit proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<not> scheduler_modes (sys_mode_of (a, b)); interrupted_modes b; s = (a, b)\<rbrakk> \<Longrightarrow> b = KernelExit proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<not> scheduler_modes b; interrupted_modes b; s = (a, b)\<rbrakk> \<Longrightarrow> b = KernelExit proof (prove)
goal:
No subgoals!
theory Noninterference

lemma silc_dom_equiv_current_aag:
  "silc_dom_equiv (current_aag s) st s' = silc_dom_equiv initial_aag st s'" by (simp add: silc_dom_equiv_def pasObjectAbs_current_aag)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv (current_aag s) st s' = silc_dom_equiv initial_aag st s'
theory Noninterference

lemma big_Step2:
  "(s,s') \<in> system.Step (big_step_ADT_A_if utf) u \<Longrightarrow>
   (s,s') \<in> Simulation.Step (big_step_ADT_A_if utf) u" apply (simp add: system.Step_def execution_def big_step_ADT_A_if_def
                   big_step_adt_def ADT_A_if_def steps_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> system.Step (big_step_ADT_A_if utf) u \<Longrightarrow> (s, s') \<in> Step (big_step_ADT_A_if utf) u proof (prove)
goal (1 subgoal):
 1. s' \<in> big_steps \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> Collect step_restrict, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, y). step_restrict y}\<rparr> big_step_R big_step_evmap () `` ({s} \<inter> full_invs_if \<inter> Collect step_restrict) \<Longrightarrow> (s, s') \<in> big_steps \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> Collect step_restrict, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, y). step_restrict y}\<rparr> big_step_R big_step_evmap () proof (prove)
goal:
No subgoals!
theory Noninterference

lemma confidentiality_part:
  "\<lbrakk> (s, t) \<in> uwr PSched; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u;
     system.reachable (big_step_ADT_A_if utf) s0 s; system.reachable (big_step_ADT_A_if utf) s0 t;
     (s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) ();
     (t, t') \<in> Simulation.Step (big_step_ADT_A_if utf) ();
     (part s, u) \<in> policyFlows (pasPolicy initial_aag); u = PSched \<longrightarrow> part s = PSched \<rbrakk>
     \<Longrightarrow> (s', t') \<in> uwr u" apply (frule schedIncludesCurrentDom) apply (case_tac "part s = PSched") apply (fastforce intro: confidentiality_part_sched_transition) apply (fastforce intro: confidentiality_part_not_PSched[rule_format]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); policy2 (part s) u; u = PSched \<longrightarrow> part s = PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); policy2 (part s) u; u = PSched \<longrightarrow> part s = PSched; part s = part t\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); policy2 (part s) u; u = PSched \<longrightarrow> part s = PSched; part s = part t; part s = PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t'
 2. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); policy2 (part s) u; u = PSched \<longrightarrow> part s = PSched; part s = part t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; reachable s; reachable t; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) (); policy2 (part s) u; u = PSched \<longrightarrow> part s = PSched; part s = part t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' proof (prove)
goal:
No subgoals!
theory Noninterference

lemma nonleakage:
  "ni.Nonleakage_gen" apply (rule Nonleakage_gen[OF confidentiality_u]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Nonleakage_gen proof (prove)
goal:
No subgoals!
theory Noninterference

lemma xnonleakage:
  "ni.xNonleakage_gen" apply (rule xNonleakage_gen[OF confidentiality_u]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xNonleakage_gen proof (prove)
goal:
No subgoals!
theory ArchNoninterference

lemma globals_equiv_to_exclusive_state_equiv:
  "globals_equiv s t \<Longrightarrow> cur_thread s \<noteq> idle_thread t \<Longrightarrow> exclusive_state_equiv s t" by (simp add: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_equiv s t; cur_thread s \<noteq> idle_thread t\<rbrakk> \<Longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state t)
theory ArchNoninterference

lemma globals_equiv_scheduler_exclusive_state_update[simp]:
  "globals_equiv_scheduler st (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) =
   globals_equiv_scheduler st s" by (simp add: globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv_scheduler st (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = globals_equiv_scheduler st s
theory ArchNoninterference

lemma silc_dom_equiv_exclusive_state_update[simp]:
  "silc_dom_equiv aag st (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) =
   silc_dom_equiv aag st s" by (simp add: silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag st (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = silc_dom_equiv aag st s
theory ArchNoninterference

lemma arch_activate_idle_thread_reads_respects_g[Noninterference_assms, wp]:
  "reads_respects_g aag l \<top> (arch_activate_idle_thread t)" unfolding arch_activate_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (arch_activate_idle_thread t) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (return ())
theory ArchNoninterference

lemma arch_globals_equiv_strengthener_thread_independent[Noninterference_assms]:
  "arch_globals_equiv_strengthener (machine_state s) (machine_state s')
   \<Longrightarrow> \<forall>ct ct' it it'. arch_globals_equiv ct it (kheap s) (kheap s')
                         (arch_state s) (arch_state s') (machine_state s) (machine_state s') =
                       arch_globals_equiv ct' it' (kheap s) (kheap s')
                         (arch_state s) (arch_state s') (machine_state s) (machine_state s')" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv_strengthener (machine_state s) (machine_state s') \<Longrightarrow> \<forall>ct ct' it it'. arch_globals_equiv ct it (kheap s) (kheap s') (arch_state s) (arch_state s') (machine_state s) (machine_state s') = arch_globals_equiv ct' it' (kheap s) (kheap s') (arch_state s) (arch_state s') (machine_state s) (machine_state s')