kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference

lemma pas_refined_tcb_st_to_auth:
  "\<lbrakk> pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb) \<rbrakk>
     \<Longrightarrow> (pasObjectAbs aag p, auth, pasObjectAbs aag ep) \<in> pasPolicy aag" apply (rule pas_refined_mem) apply (rule_tac s=s in sta_ts) apply (simp add: thread_st_auth_def tcb_states_of_state_def get_tcb_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, auth, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (p, auth, ep) \<in> state_objs_to_policy ?s
 2. \<lbrakk>pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> pas_refined aag ?s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (ep, auth) \<in> thread_st_auth s p
 2. \<lbrakk>pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> pas_refined aag s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; (ep, auth) \<in> tcb_st_to_auth (tcb_state tcb); kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> pas_refined aag s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma pas_wellformed_pasSubject_update_Control:
  "\<lbrakk> pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>);
     (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag p = pasObjectAbs aag p'" by (fastforce simp: policy_wellformed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>); (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag p = pasObjectAbs aag p'
theory Noninterference

lemma pas_wellformed_noninterference_policy_refl:
  "\<lbrakk> pas_wellformed_noninterference aag; pasObjectAbs aag x \<noteq> SilcLabel \<rbrakk>
     \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag x) \<in> pasPolicy aag" unfolding pas_wellformed_noninterference_def by (fastforce intro!:aag_wellformed_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed_noninterference aag; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>l\<in>range (pasObjectAbs aag) \<union> \<Union> (range (pasDomainAbs aag)) - {SilcLabel}. pas_wellformed (aag\<lparr>pasSubject := l\<rparr>)) \<and> (\<forall>d. SilcLabel \<notin> pasDomainAbs aag d) \<and> pas_domains_distinct aag; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag x) \<in> pasPolicy aag
theory Noninterference

lemma pas_wellformed_noninterference_control_to_eq:
  "\<lbrakk> pas_wellformed_noninterference aag;
     (pasObjectAbs aag x, Control, l) \<in> pasPolicy aag; pasObjectAbs aag x \<noteq> SilcLabel \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x = l" unfolding pas_wellformed_noninterference_def by (erule aag_wellformed_Control; fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed_noninterference aag; (pasObjectAbs aag x, Control, l) \<in> pasPolicy aag; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = l proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>l\<in>range (pasObjectAbs aag) \<union> \<Union> (range (pasDomainAbs aag)) - {SilcLabel}. pas_wellformed (aag\<lparr>pasSubject := l\<rparr>)) \<and> (\<forall>d. SilcLabel \<notin> pasDomainAbs aag d) \<and> pas_domains_distinct aag; (pasObjectAbs aag x, Control, l) \<in> pasPolicy aag; pasObjectAbs aag x \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = l
theory Noninterference

lemma fun_noteqD:
  "f \<noteq> g \<Longrightarrow> \<exists>a. f a \<noteq> g a" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<noteq> g \<Longrightarrow> \<exists>a. f a \<noteq> g a
theory Noninterference

lemma integrity_update_reference_state:
  "\<lbrakk> is_subject aag t; integrity aag X st s; st = st'\<lparr>kheap := (kheap st')(t \<mapsto> blah)\<rparr> \<rbrakk>
     \<Longrightarrow> integrity (aag :: 'a subject_label PAS) X st' s" apply (erule integrity_trans[rotated]) apply (clarsimp simp: integrity_def opt_map_def integrity_asids_update_reference_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag t; integrity aag X st s; st = st'\<lparr>kheap := (kheap st')(t \<mapsto> blah)\<rparr>\<rbrakk> \<Longrightarrow> integrity aag X st' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag t; st = st'\<lparr>kheap := (kheap st')(t \<mapsto> blah)\<rparr>\<rbrakk> \<Longrightarrow> integrity aag X st' st proof (prove)
goal:
No subgoals!
theory Noninterference

lemma kheap_ep_tcb_states_of_state_eq:
  "kheap s x = kheap s' x \<Longrightarrow> tcb_states_of_state s x = tcb_states_of_state s' x" unfolding tcb_states_of_state_def get_tcb_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s x = kheap s' x \<Longrightarrow> tcb_states_of_state s x = tcb_states_of_state s' x proof (prove)
goal (1 subgoal):
 1. kheap s x = kheap s' x \<Longrightarrow> map_option tcb_state (case kheap s x of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = map_option tcb_state (case kheap s' x of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None)
theory Noninterference

lemma partitionIntegrity_subjectAffects_cdt:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s;
     valid_mdb s; valid_objs s; cdt s (x,y) \<noteq> cdt s' (x,y) \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_cdt) apply (drule_tac x="(x,y)" in spec) apply (clarsimp simp: integrity_cdt_def) apply (rule affects_delete_derived) apply (frule (3) cdt_change_allowed_delete_derived) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y); integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y); integrity_cdt_state (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y); cdt_integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (cdt s) (tcb_states_of_state s) (x, y) (cdt s (x, y), is_original_cap s (x, y)) (cdt s' (x, y), is_original_cap s' (x, y))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; cdt s (x, y) \<noteq> cdt s' (x, y); cdt_change_allowed' aag (x, y) s; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst (x, y))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag
theory Noninterference

lemma partitionIntegrity_subjectAffects_is_original_cap:
  "\<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_mdb s; valid_objs s;
    is_original_cap s (x,y) \<noteq> is_original_cap s' (x,y)\<rbrakk> \<Longrightarrow>
   pasObjectAbs aag x
     \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_cdt) apply (drule_tac x="(x,y)" in spec) apply (clarsimp simp: integrity_cdt_def) apply (rule affects_delete_derived) apply (frule (3) cdt_change_allowed_delete_derived) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) \<noteq> is_original_cap s' (x, y)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) \<noteq> is_original_cap s' (x, y); integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) \<noteq> is_original_cap s' (x, y); integrity_cdt_state (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) \<noteq> is_original_cap s' (x, y); cdt_integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (cdt s) (tcb_states_of_state s) (x, y) (cdt s (x, y), is_original_cap s (x, y)) (cdt s' (x, y), is_original_cap s' (x, y))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) = (\<not> is_original_cap s' (x, y)); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) = (\<not> is_original_cap s' (x, y)); cdt_change_allowed' aag (x, y) s\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_mdb s; valid_objs s; is_original_cap s (x, y) = (\<not> is_original_cap s' (x, y)); cdt_change_allowed' aag (x, y) s; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst (x, y))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag
theory Noninterference

lemma partitionIntegrity_subjectAffects_interrupt_states:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s;
     valid_objs s; interrupt_states s x \<noteq> interrupt_states s' x \<rbrakk>
     \<Longrightarrow> pasIRQAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_interrupts) apply (drule_tac x=x in spec) apply (clarsimp simp: integrity_interrupts_def) apply (rule affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; interrupt_states s x \<noteq> interrupt_states s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_states s x \<noteq> interrupt_states s' x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_states s x \<noteq> interrupt_states s' x; \<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_states s x \<noteq> interrupt_states s' x; integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_states s x \<noteq> interrupt_states s' x; is_subject_irq aag x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasSubject aag) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma partitionIntegrity_subjectAffects_interrupt_irq_node:
  "\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; valid_objs s;
     interrupt_irq_node s x \<noteq> interrupt_irq_node s' x \<rbrakk>
     \<Longrightarrow> pasIRQAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" apply (drule partitionIntegrity_integrity) apply (drule integrity_subjects_interrupts) apply (drule_tac x=x in spec) apply (clarsimp simp: integrity_interrupts_def) apply (rule affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s s'; pas_refined aag s; valid_objs s; interrupt_irq_node s x \<noteq> interrupt_irq_node s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_irq_node s x \<noteq> interrupt_irq_node s' x; integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} s s'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_irq_node s x \<noteq> interrupt_irq_node s' x; \<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_irq_node s x \<noteq> interrupt_irq_node s' x; integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasIRQAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; interrupt_irq_node s x \<noteq> interrupt_irq_node s' x; is_subject_irq aag x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasSubject aag) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma prefix_helper:
  "\<lbrakk> a @ l = l'; distinct l; distinct l' \<rbrakk> \<Longrightarrow> set a \<inter> set l = {} \<and> set a \<subseteq> set l'" apply (induct l) apply simp+ by (metis append_Cons disjoint_iff_not_equal distinct.simps(2) distinct_append
            distinct_length_2_or_more subset_code(1))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a @ l = l'; distinct l; distinct l'\<rbrakk> \<Longrightarrow> set a \<inter> set l = {} \<and> set a \<subseteq> set l' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a @ [] = l'; distinct []; distinct l'\<rbrakk> \<Longrightarrow> set a \<inter> set [] = {} \<and> set a \<subseteq> set l'
 2. \<And>aa l. \<lbrakk>\<lbrakk>a @ l = l'; distinct l; distinct l'\<rbrakk> \<Longrightarrow> set a \<inter> set l = {} \<and> set a \<subseteq> set l'; a @ aa # l = l'; distinct (aa # l); distinct l'\<rbrakk> \<Longrightarrow> set a \<inter> set (aa # l) = {} \<and> set a \<subseteq> set l' proof (prove)
goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>a @ l = l' \<Longrightarrow> set a \<inter> set l = {} \<and> set a \<subseteq> set l'; a @ aa # l = l'; aa \<notin> set l \<and> distinct l; distinct l'\<rbrakk> \<Longrightarrow> aa \<notin> set a \<and> set a \<inter> set l = {} \<and> set a \<subseteq> set l'
theory Noninterference

lemma valid_queuesE:
  assumes "valid_queues s"
  assumes "t \<in> set (ready_queues s d p)"
  assumes "\<lbrakk> is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s;
             st_tcb_at runnable t s; distinct (ready_queues s d p) \<rbrakk>
             \<Longrightarrow> R "
  shows R using assms by (clarsimp simp: valid_queues_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
valid_queues s
t \<in> set (ready_queues s d p)
\<lbrakk>is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> R

goal (1 subgoal):
 1. R
theory Noninterference

lemma valid_blocked_imp:
  "\<lbrakk> valid_blocked s; tcb_at t s; not_queued t s;
     t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t \<rbrakk>
     \<Longrightarrow> st_tcb_at (\<lambda>s. \<not> runnable s) t s" by (fastforce simp: valid_blocked_def st_tcb_at_def
                      tcb_at_st_tcb_at runnable_eq_active obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_blocked s; tcb_at t s; not_queued t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>s. \<not> runnable s) t s
theory Noninterference

lemma valid_queues_not_in_place:
  "\<lbrakk> valid_queues s; t \<notin> set (ready_queues s d a);
     etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s; is_etcb_at t s\<rbrakk>
     \<Longrightarrow> not_queued t s" by (clarsimp simp: valid_queues_def not_queued_def etcb_at_def is_etcb_at_def
              split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues s; t \<notin> set (ready_queues s d a); etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s; is_etcb_at t s\<rbrakk> \<Longrightarrow> not_queued t s
theory Noninterference

lemma valid_sched_valid_blocked: "valid_sched s \<Longrightarrow> valid_blocked s" by (simp add: valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched s \<Longrightarrow> valid_blocked s
theory Noninterference

lemma subject_can_affect_its_own_partition:
  "d \<notin> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag))
   \<Longrightarrow> d \<noteq> Partition (label_of (pasSubject aag))" apply (erule contrapos_nn) apply (simp add: partsSubjectAffects_def image_def label_can_affect_partition_def) apply (blast intro: affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. d \<notin> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) \<Longrightarrow> d \<noteq> Partition (label_of (pasSubject aag)) proof (prove)
goal (1 subgoal):
 1. d = Partition (label_of (pasSubject aag)) \<Longrightarrow> d \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) proof (prove)
goal (1 subgoal):
 1. d = Partition (label_of (pasSubject aag)) \<Longrightarrow> \<exists>d. d \<in> subjectAffects (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) \<and> d \<in> subjectReads (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma ev_add_pre:
  "equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_inv I A (P and Q) f" apply (rule equiv_valid_guard_imp) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_inv I A (P and Q) f proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_inv I A ?Q f
 2. \<And>s. \<lbrakk>equiv_valid_inv I A P f; (P and Q) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_valid_inv I A P f; (P and Q) s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma silc_inv_refl:
  "silc_inv aag st s \<Longrightarrow> silc_inv aag s s" by (fastforce simp: silc_inv_def silc_dom_equiv_def equiv_for_refl
              intro!: silc_inv_no_transferableD')

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

lemma Fin_big_step_adt:
  "Fin (big_step_adt A R evmap) = Fin A" by (simp add: big_step_adt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Fin (big_step_adt A R evmap) = Fin A
theory Noninterference

lemma small_step_reachable:
  "ni.reachable s \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s" apply (rule reachable_big_step_adt) apply (simp add: big_step_ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> system.reachable (big_step_adt (ADT_A_if utf) ?R ?exmap) s0 s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma reachable_invs_if:
  "ni.reachable s \<Longrightarrow> invs_if s" apply (rule ADT_A_if_reachable_invs_if) apply (erule small_step_reachable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma pas_refined_if:
  "ni.reachable  s \<Longrightarrow> pas_refined_if s" apply (drule reachable_invs_if) apply (simp add: invs_if_def Invs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> pas_refined_if s proof (prove)
goal (1 subgoal):
 1. invs_if s \<Longrightarrow> pas_refined_if s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma guarded_pas_domain_if:
  "ni.reachable  s \<Longrightarrow> guarded_pas_domain_if s" apply (drule reachable_invs_if) apply (simp add: invs_if_def Invs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> guarded_pas_domain_if s proof (prove)
goal (1 subgoal):
 1. invs_if s \<Longrightarrow> guarded_pas_domain_if s proof (prove)
goal:
No subgoals!