kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference

lemma schedule_reads_affects_equiv_sameFor_PSched':
  "\<lbrakk> scheduler_equiv aag (internal_state_if s) (internal_state_if s');
     scheduler_modes (sys_mode_of s) = scheduler_modes (sys_mode_of s');
     interrupted_modes (sys_mode_of s) = interrupted_modes (sys_mode_of s') \<rbrakk>
     \<Longrightarrow> (s,s') \<in> same_for aag PSched" apply (case_tac s) apply (case_tac a) apply (case_tac s') apply (case_tac ab) apply clarsimp apply (rule schedule_reads_affects_equiv_sameFor_PSched; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag (internal_state_if s) (internal_state_if s'); scheduler_modes (sys_mode_of s) = scheduler_modes (sys_mode_of s'); interrupted_modes (sys_mode_of s) = interrupted_modes (sys_mode_of s')\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for aag PSched proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>scheduler_equiv aag (internal_state_if s) (internal_state_if s'); scheduler_modes (sys_mode_of s) = scheduler_modes (sys_mode_of s'); interrupted_modes (sys_mode_of s) = interrupted_modes (sys_mode_of s'); s = (a, b)\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for aag PSched proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>scheduler_equiv aag (internal_state_if s) (internal_state_if s'); scheduler_modes (sys_mode_of s) = scheduler_modes (sys_mode_of s'); interrupted_modes (sys_mode_of s) = interrupted_modes (sys_mode_of s'); s = (a, b); a = (aa, ba)\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for aag PSched proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>scheduler_equiv aag (internal_state_if s) (internal_state_if s'); scheduler_modes (sys_mode_of s) = scheduler_modes (sys_mode_of s'); interrupted_modes (sys_mode_of s) = interrupted_modes (sys_mode_of s'); s = (a, b); a = (aa, ba); s' = (ab, bb)\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for aag PSched proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>scheduler_equiv aag (internal_state_if s) (internal_state_if s'); scheduler_modes (sys_mode_of s) = scheduler_modes (sys_mode_of s'); interrupted_modes (sys_mode_of s) = interrupted_modes (sys_mode_of s'); s = (a, b); a = (aa, ba); s' = (ab, bb); ab = (ac, bc)\<rbrakk> \<Longrightarrow> (s, s') \<in> same_for aag PSched proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa bba ac bc. \<lbrakk>scheduler_equiv aag baa bc; scheduler_modes ba = scheduler_modes bba; interrupted_modes ba = interrupted_modes bba; s = ((aa, baa), ba); s' = ((ac, bc), bba)\<rbrakk> \<Longrightarrow> (((aa, baa), ba), (ac, bc), bba) \<in> same_for aag PSched proof (prove)
goal:
No subgoals!
theory Noninterference

lemma observable_if_cases:
  "P (s::observable_if) \<Longrightarrow> P (((user_context_of s),(internal_state_if s)),sys_mode_of s)" by (case_tac s, case_tac "fst s", simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> P ((user_context_of s, internal_state_if s), sys_mode_of s)
theory Noninterference

lemma schedule_reads_affects_equiv_sameFor:
  "\<lbrakk> scheduler_equiv aag s s'; scheduler_affects_equiv aag (OrdinaryLabel l) s s';
     user_modes mode \<longrightarrow> uc = uc' \<rbrakk>
     \<Longrightarrow> (((uc,s),mode),((uc',s'),mode)) \<in> same_for aag (Partition l)" by (auto simp: scheduler_equiv_def scheduler_affects_equiv_def sameFor_def sameFor_subject_def
                 silc_dom_equiv_def reads_scheduler_def domain_fields_equiv_def
                 disjoint_iff_not_equal Bex_def
          intro: globals_equiv_from_scheduler)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_affects_equiv aag (OrdinaryLabel l) s s'; user_modes mode \<longrightarrow> uc = uc'\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc', s'), mode) \<in> same_for aag (Partition l)
theory Noninterference

lemma globals_equiv_to_scheduler_globals_frame_equiv:
  "\<lbrakk> globals_equiv s t; invs s; invs t \<rbrakk>
     \<Longrightarrow> scheduler_globals_frame_equiv s t" by (simp add: globals_equiv_def scheduler_globals_frame_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_equiv s t; invs s; invs t\<rbrakk> \<Longrightarrow> scheduler_globals_frame_equiv s t
theory Noninterference

lemma globals_equiv_to_cur_thread_eq:
  "globals_equiv s t \<Longrightarrow> cur_thread s = cur_thread t" by (simp add: globals_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s t \<Longrightarrow> cur_thread s = cur_thread t
theory Noninterference

lemma no_subject_affects_PSched:
  "PSched \<notin> partsSubjectAffects g l" by (auto simp: partsSubjectAffects_def elim: subjectAffects.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PSched \<notin> partsSubjectAffects g l
theory Noninterference

lemma no_partition_flows_to_PSched:
  "(Partition l, PSched) \<notin> policyFlows g" apply (rule notI) apply (erule policyFlows.cases) apply (simp_all add: no_subject_affects_PSched) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Partition l, PSched) \<notin> policyFlows g proof (prove)
goal (1 subgoal):
 1. (Partition l, PSched) \<in> policyFlows g \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>d la. \<lbrakk>Partition l = Partition la; PSched = d; d \<in> partsSubjectAffects g la\<rbrakk> \<Longrightarrow> False
 2. \<And>d. \<lbrakk>Partition l = PSched; PSched = d\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Noninterference

lemma partsSubjectAffects_bounds_those_subject_not_allowed_to_affect:
  "(Partition l,d) \<notin> policyFlows g \<Longrightarrow> d \<notin> partsSubjectAffects g l" apply (clarify) apply (drule policy_affects) apply (blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Partition l, d) \<notin> policyFlows g \<Longrightarrow> d \<notin> partsSubjectAffects g l proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Partition l, d) \<notin> policyFlows g; d \<in> partsSubjectAffects g l\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Partition l, d) \<notin> policyFlows g; (Partition l, d) \<in> policyFlows g\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Noninterference

lemma PSched_flows_to_all:
  "(PSched,d) \<in> policyFlows g" by (rule policyFlows.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (PSched, d) \<in> policyFlows g
theory Noninterference

lemma policyFlows_refl:
  "refl (policyFlows g)" apply (rule refl_onI) apply simp apply (case_tac x) apply simp apply (rule policy_affects) apply (simp add: partsSubjectAffects_def image_def) apply (simp add: label_can_affect_partition_def) apply (blast intro: affects_lrefl) apply (blast intro: PSched_flows_to_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refl (policyFlows g) proof (prove)
goal (2 subgoals):
 1. policyFlows g \<subseteq> UNIV \<times> UNIV
 2. \<And>x. x \<in> UNIV \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (2 subgoals):
 1. \<And>x x1. \<lbrakk>x \<in> UNIV; x = Partition x1\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g
 2. \<And>x. \<lbrakk>x \<in> UNIV; x = PSched\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (2 subgoals):
 1. \<And>x x1. x = Partition x1 \<Longrightarrow> (Partition x1, Partition x1) \<in> policyFlows g
 2. \<And>x. \<lbrakk>x \<in> UNIV; x = PSched\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (2 subgoals):
 1. \<And>x x1. x = Partition x1 \<Longrightarrow> Partition x1 \<in> partsSubjectAffects g x1
 2. \<And>x. \<lbrakk>x \<in> UNIV; x = PSched\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (2 subgoals):
 1. \<And>x x1. x = Partition x1 \<Longrightarrow> label_can_affect_partition g (OrdinaryLabel x1) (OrdinaryLabel x1)
 2. \<And>x. \<lbrakk>x \<in> UNIV; x = PSched\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (2 subgoals):
 1. \<And>x x1. x = Partition x1 \<Longrightarrow> \<exists>d. d \<in> subjectAffects g (OrdinaryLabel x1) \<and> d \<in> subjectReads g (OrdinaryLabel x1)
 2. \<And>x. \<lbrakk>x \<in> UNIV; x = PSched\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> UNIV; x = PSched\<rbrakk> \<Longrightarrow> (x, x) \<in> policyFlows g proof (prove)
goal:
No subgoals!
theory Noninterference

lemma thread_set_tcb_context_update_ct_active[wp]:
  "thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>s. P (ct_active s)\<rbrace>" apply (simp add: thread_set_def ct_in_state_def | wp set_object_wp)+ apply (clarsimp simp: st_tcb_at_def obj_at_def get_tcb_def
                 split: option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ct_active s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set f)) t \<lbrace>\<lambda>_ s. P (ct_active s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (st_tcb_at active (cur_thread s) s) \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> P (st_tcb_at active (cur_thread s) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set f) (the (get_tcb t s))))\<rparr>)) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma prop_of_two_valid:
  assumes f: "\<And>P. m \<lbrace>\<lambda>s. P (f s)\<rbrace>"
  assumes g: "\<And>P. m \<lbrace>\<lambda>s. P (g s)\<rbrace>"
  shows "m \<lbrace>\<lambda>s. P (f s) (g s)\<rbrace>" by (rule hoare_pre, wps f g, wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (f s) (g s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) (g s)\<rbrace>
theory Noninterference

lemma thread_set_tcb_context_update_wp:
  "\<lbrace>\<lambda>s. P (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update f (the (get_tcb t s))))\<rparr>)\<rbrace>
   thread_set (tcb_arch_update f) t
   \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update f (the (get_tcb t s))))\<rparr>)\<rbrace> thread_set (tcb_arch_update f) t \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update f (the (get_tcb t s))))\<rparr>)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb_arch_update f tcb))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update f (the (get_tcb t s))))\<rparr>) \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> P (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma check_active_irq_if_integrity:
  "check_active_irq_if tc \<lbrace>integrity aag X st\<rbrace>" by (wpsimp wp: check_active_irq_if_wp simp: integrity_subjects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Noninterference

lemma ct_running_not_idle:
  "\<lbrakk> ct_running s; valid_idle s \<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s" by (clarsimp simp add: ct_in_state_def pred_tcb_at_def obj_at_def valid_idle_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_running s; valid_idle s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
theory Noninterference

lemma kernel_entry_if_globals_equiv_scheduler:
  "\<lbrace>globals_equiv_scheduler st and valid_arch_state and invs
                               and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)
                               and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" apply (wp globals_equiv_scheduler_inv' kernel_entry_if_globals_equiv) apply (clarsimp) apply assumption apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>st s. (?P1 and globals_equiv st) s \<Longrightarrow> (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s
 2. \<And>s. (globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> (?P1 and globals_equiv_scheduler st) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>?P1 s; globals_equiv st s\<rbrakk> \<Longrightarrow> invs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> (ct_idle s \<longrightarrow> tc = idle_context s)
 2. \<And>s. (globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> (?P1 and globals_equiv_scheduler st) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> (ct_idle s \<longrightarrow> tc = idle_context s)) and globals_equiv_scheduler st) s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma domain_fields_equiv_lift:
  assumes a: "\<And>P. \<lbrace>domain_fields P and Q\<rbrace> f \<lbrace>\<lambda>_. domain_fields P\<rbrace>"
  assumes b: "\<And>P. \<lbrace>(\<lambda>s. P (cur_domain s)) and R\<rbrace> f \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>"
  shows "\<lbrace>domain_fields_equiv st and Q and R\<rbrace> f \<lbrace>\<lambda>_. domain_fields_equiv st\<rbrace>" apply (clarsimp simp: valid_def domain_fields_equiv_def) apply (erule use_valid, wp a b) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_fields_equiv st and Q and R\<rbrace> f \<lbrace>\<lambda>_. domain_fields_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; Q s; R s\<rbrakk> \<Longrightarrow> cur_domain s = cur_domain b \<and> domain_time s = domain_time b \<and> domain_index s = domain_index b \<and> domain_list s = domain_list b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; Q s; R s\<rbrakk> \<Longrightarrow> ((\<lambda>sa. cur_domain s = cur_domain sa) and R) s \<and> ((\<lambda>sa. domain_time s = domain_time sa \<and> domain_index s = domain_index sa \<and> domain_list s = domain_list sa) and Q) s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma do_machine_op_globals_equiv_scheduler:
   "(\<And>s sa. \<lbrakk> P sa; globals_equiv_scheduler s sa \<rbrakk>
              \<Longrightarrow> \<forall>x \<in> fst (f (machine_state sa)).
                    globals_equiv_scheduler s (sa\<lparr>machine_state := snd x\<rparr>))
    \<Longrightarrow> \<lbrace>globals_equiv_scheduler s and P\<rbrace>
        do_machine_op f
        \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace>" unfolding do_machine_op_def by (wp | simp add: split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s sa. \<lbrakk>P sa; globals_equiv_scheduler s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv_scheduler s (sa\<lparr>machine_state := snd x\<rparr>)) \<Longrightarrow> \<lbrace>globals_equiv_scheduler s and P\<rbrace> do_machine_op f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s sa. \<lbrakk>P sa; globals_equiv_scheduler s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv_scheduler s (sa\<lparr>machine_state := snd x\<rparr>)) \<Longrightarrow> \<lbrace>globals_equiv_scheduler s and P\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace>
theory Noninterference

lemma dmo_device_memory_update_globals_equiv_scheduler:
  "\<lbrace>globals_equiv_scheduler st and (\<lambda>s. device_region s = S)\<rbrace>
   do_machine_op
     (device_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` S))
   \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" apply (rule do_machine_op_globals_equiv_scheduler) apply clarsimp apply (simp add: device_memory_update_def simpler_modify_def) apply (clarsimp simp: globals_equiv_scheduler_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and (\<lambda>s. dom (device_state (machine_state s)) = S)\<rbrace> do_machine_op (device_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` S)) \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>dom (device_state (machine_state sa)) = S; globals_equiv_scheduler s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (device_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` S) (machine_state sa)). globals_equiv_scheduler s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; S = dom (device_state (machine_state sa)); ((), b) \<in> fst (device_memory_update ((ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom (device_state (machine_state sa))) (machine_state sa))\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s sa b. \<lbrakk>globals_equiv_scheduler s sa; S = dom (device_state (machine_state sa)); b = machine_state sa\<lparr>device_state := device_state (machine_state sa) ++ (ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom (device_state (machine_state sa))\<rparr>\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := machine_state sa\<lparr>device_state := device_state (machine_state sa) ++ (ba |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom (device_state (machine_state sa))\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma pas_refined_pasMayActivate_update[simp]:
  "pas_refined (aag\<lparr>pasMayActivate := x, pasMayEditReadyQueues := x\<rparr>) s =
   pas_refined (aag :: 'a subject_label PAS) s" apply (simp add: pas_refined_def irq_map_wellformed_aux_def tcb_domain_map_wellformed_aux_def) apply (simp add: state_asids_to_policy_pasMayActivate_update[simplified]
                  state_irqs_to_policy_pasMayActivate_update
                  state_asids_to_policy_pasMayEditReadyQueues_update[simplified]
                  state_irqs_to_policy_pasMayEditReadyQueues_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined (aag\<lparr>pasMayActivate := x, pasMayEditReadyQueues := x\<rparr>) s = pas_refined aag s proof (prove)
goal (1 subgoal):
 1. (pas_wellformed aag \<and> (\<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq) \<and> (\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d) \<and> state_objs_in_policy aag s \<and> state_asids_to_policy (aag\<lparr>pasMayActivate := x, pasMayEditReadyQueues := x\<rparr>) s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy (aag\<lparr>pasMayActivate := x, pasMayEditReadyQueues := x\<rparr>) s \<subseteq> pasPolicy aag) = (pas_wellformed aag \<and> (\<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq) \<and> (\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d) \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma activate_thread_globals_equiv_scheduler:
  "\<lbrace>globals_equiv_scheduler st and valid_arch_state and valid_idle\<rbrace>
   activate_thread
   \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" by (wp globals_equiv_scheduler_inv' activate_thread_globals_equiv | force | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and valid_arch_state and valid_idle\<rbrace> activate_thread \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>
theory Noninterference

lemma partitionIntegrity_integrity:
  "partitionIntegrity aag s s'
   \<Longrightarrow> integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
                 (scheduler_affects_globals_frame s) s s'" by (clarsimp simp: partitionIntegrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partitionIntegrity aag s s' \<Longrightarrow> integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'
theory Noninterference

lemma receive_blocked_on_eq:
  "\<lbrakk> receive_blocked_on ep ts; receive_blocked_on ep' ts \<rbrakk>
     \<Longrightarrow> ep = ep'" by (case_tac ts; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked_on ep ts; receive_blocked_on ep' ts\<rbrakk> \<Longrightarrow> ep = ep'
theory Noninterference

lemma receive_blocked_on_eq':
  "\<lbrakk> receive_blocked_on ep ts; blocked_on ep' ts \<rbrakk>
     \<Longrightarrow> ep = ep'" by (case_tac ts; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked_on ep ts; blocked_on ep' ts\<rbrakk> \<Longrightarrow> ep = ep'
theory Noninterference

lemma receive_blocked_on_contradiction:
  "\<lbrakk> receive_blocked_on ep ts; send_blocked_on ep' ts \<rbrakk>
     \<Longrightarrow> False" by (case_tac ts; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked_on ep ts; send_blocked_on ep' ts\<rbrakk> \<Longrightarrow> False