kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference

lemma set_tcb_queue_reads_respects_g':
  "equiv_valid (reads_equiv_g aag)
               (\<lambda>s s'. affects_equiv aag l s s' \<and>
                       arch_globals_equiv_strengthener  (machine_state s) (machine_state s'))
               (\<lambda>s s'. affects_equiv aag l s s' \<and>
                       arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
               \<top> (set_tcb_queue d prio queue)" unfolding equiv_valid_def2 equiv_valid_2_def supply if_cong[cong] apply (clarsimp simp: set_tcb_queue_def bind_def modify_def put_def get_def) by ((rule conjI
       | rule affects_equiv_ready_queues_update reads_equiv_ready_queues_update, assumption
       | clarsimp simp: reads_equiv_g_def
       | fastforce elim!: affects_equivE reads_equivE
                    simp: equiv_for_def globals_equiv_def idle_equiv_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (\<lambda>_. True) (set_tcb_queue d prio queue) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> reads_equiv_g aag s t \<and> affects_equiv aag l s t \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state t) \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue d prio queue s). \<forall>(rvb, t')\<in>fst (set_tcb_queue d prio queue t). rva = rvb \<and> reads_equiv_g aag s' t' \<and> affects_equiv aag l s' t' \<and> arch_globals_equiv_strengthener (machine_state s') (machine_state t')) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> reads_equiv_g aag s t \<and> affects_equiv aag l s t \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state t) \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue d prio queue s). \<forall>(rvb, t')\<in>fst (set_tcb_queue d prio queue t). rva = rvb \<and> reads_equiv_g aag s' t' \<and> affects_equiv aag l s' t' \<and> arch_globals_equiv_strengthener (machine_state s') (machine_state t')) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv_g aag s t; affects_equiv aag l s t; arch_globals_equiv_strengthener (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> reads_equiv_g aag (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t) \<and> affects_equiv aag l (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues t d' p) t)
theory Noninterference

lemma set_tcb_queue_globals_equiv[wp]:
  "set_tcb_queue d prio queue \<lbrace>globals_equiv st\<rbrace>" by (simp add: set_tcb_queue_def modify_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> set_tcb_queue d prio queue \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Noninterference

lemma guarded_switch_to_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_g aag (l :: 'a subject_label)
                          (pas_refined aag and valid_idle and (\<lambda>s. is_subject aag t))
                          (guarded_switch_to t)" apply (simp add: guarded_switch_to_def) apply (wp switch_to_thread_reads_respects_g get_thread_state_reads_respects_g gts_wp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and valid_idle and (\<lambda>s. is_subject aag t)) (guarded_switch_to t) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and valid_idle and (\<lambda>s. is_subject aag t)) (do ts <- get_thread_state t;
y <- assert (runnable ts);
switch_to_thread t
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and valid_idle and (\<lambda>s. is_subject aag t)) s \<Longrightarrow> (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) s \<and> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> True \<and> (runnable st \<longrightarrow> (pas_refined aag and (\<lambda>s. is_subject aag t)) s)) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma cur_thread_update_idle_reads_respects_g':
  "reads_respects_g aag (l :: 'a subject_label) (\<lambda>s. t = idle_thread s) (modify (cur_thread_update (\<lambda>_. t)))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) apply (clarsimp simp: reads_equiv_g_def reads_equiv_def2
                        affects_equiv_def2 globals_equiv_def idle_equiv_def) apply (fastforce intro: states_equiv_for_sym arch_globals_equiv_threads_eq) 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) (modify (cur_thread_update (\<lambda>_. 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) (modify (cur_thread_update (\<lambda>_. t))) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>reads_equiv_g aag s ta; affects_equiv aag l s ta; t = idle_thread s; t = idle_thread ta\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv_g aag (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) \<and> affects_equiv aag l (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) s ta; t = idle_thread ta; states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s ta; cur_domain s = cur_domain ta; scheduler_action s = scheduler_action ta; work_units_completed s = work_units_completed ta; equiv_irq_state (machine_state s) (machine_state ta); arch_globals_equiv (cur_thread ta) (idle_thread ta) (kheap s) (kheap ta) (arch_state s) (arch_state ta) (machine_state s) (machine_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; cur_thread s = cur_thread ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta))\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) (s\<lparr>cur_thread := idle_thread ta\<rparr>) ta \<and> arch_globals_equiv (idle_thread ta) (idle_thread ta) (kheap s) (kheap ta) (arch_state s) (arch_state ta) (machine_state s) (machine_state ta) \<and> states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) (s\<lparr>cur_thread := idle_thread ta\<rparr>) ta proof (prove)
goal:
No subgoals!
theory Noninterference

lemma switch_to_idle_thread_reads_respects_g[wp]:
  "reads_respects_g aag (l :: 'a subject_label) \<top> (switch_to_idle_thread)" apply (simp add: switch_to_idle_thread_def) apply (wp cur_thread_update_idle_reads_respects_g') apply (fastforce simp: reads_equiv_g_def globals_equiv_idle_thread_ptr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) switch_to_idle_thread proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True \<and> idle_thread s = idle_thread s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma gets_app_rewrite:
  "(gets y >>= (\<lambda>x. g (f x))) = (gets (\<lambda>s. f (y s)) >>= g)" apply (rule ext) apply (simp add: gets_def bind_def get_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- gets y;
g (f x)
od = gets (\<lambda>s. f (y s)) >>= g proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- gets y;
g (f x)
od) x = (gets (\<lambda>s. f (y s)) >>= g) x proof (prove)
goal:
No subgoals!
theory Noninterference

lemma gets_domain_time_zero_ev:
  "equiv_valid_inv I A (\<lambda>s. domain_time s > 0) (gets (\<lambda>s. domain_time s = 0))" apply (rule gets_ev'') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. 0 < domain_time s) (gets (\<lambda>s. domain_time s = 0)) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. I s t \<and> A s t \<and> 0 < domain_time s \<and> 0 < domain_time t \<longrightarrow> (domain_time s = 0) = (domain_time t = 0) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma reads_equiv_valid_g_inv_schedule_switch_thread_fastfail:
  "reads_equiv_valid_g_inv (affects_equiv aag l) aag
     ((\<lambda>s. ct \<noteq> it \<longrightarrow> is_subject aag (ct)))
     (schedule_switch_thread_fastfail ct it ct_prio target_prio)" unfolding schedule_switch_thread_fastfail_def by (wpsimp wp: reads_respects_g_from_inv[OF reads_respects_ethread_get])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. ct \<noteq> it \<longrightarrow> is_subject aag ct) (schedule_switch_thread_fastfail ct it ct_prio target_prio) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. ct \<noteq> it \<longrightarrow> is_subject aag ct) (if ct \<noteq> it then return (target_prio < ct_prio) else return True)
theory Noninterference

lemma reads_respects_is_highest_prio:
  "reads_respects aag l (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag d)
                  (gets (\<lambda>s. is_highest_prio d p s))" by (fastforce simp: is_highest_prio_def intro: reads_respects_gets_ready_queues)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag d) (gets (is_highest_prio d p))
theory Noninterference

lemma reads_respects_ethread_get_when:
  "reads_respects aag l (\<lambda>_. b \<longrightarrow> is_subject aag thread) (ethread_get_when b f thread)" apply (simp add: ethread_get_when_def) apply (rule conjI; clarsimp) apply (rule reads_respects_ethread_get) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. b \<longrightarrow> is_subject aag thread) (ethread_get_when b f thread) proof (prove)
goal (1 subgoal):
 1. (b \<longrightarrow> reads_respects aag l (\<lambda>_. is_subject aag thread) (ethread_get f thread)) \<and> (\<not> b \<longrightarrow> reads_respects aag l (\<lambda>_. True) (return undefined)) proof (prove)
goal (2 subgoals):
 1. b \<Longrightarrow> reads_respects aag l (\<lambda>_. is_subject aag thread) (ethread_get f thread)
 2. \<not> b \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (return undefined) proof (prove)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (return undefined) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma valid_sched_action_switch_is_subject:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "\<lbrakk> scheduler_action s = switch_thread t ; valid_sched_action s ;
           valid_etcbs s ; pas_refined aag s ; pas_cur_domain aag s \<rbrakk>
           \<Longrightarrow> is_subject aag t" by (fastforce dest: valid_sched_action_switch_subject_thread
                      domains_distinct[THEN pas_domains_distinct_inj])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_action s = switch_thread t; valid_sched_action s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s\<rbrakk> \<Longrightarrow> is_subject aag t
theory Noninterference

lemma schedule_if_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct pas"
  shows "reads_respects_g pas (l :: 'a subject_label)
           (einvs and pas_cur_domain pas and guarded_pas_domain pas
                  and (\<lambda>s. domain_time s > 0) and pas_refined pas) (schedule_if tc)" apply (simp add: schedule_if_def) apply (wp schedule_reads_respects_g activate_thread_reads_respects_g) apply (rule_tac Q="\<lambda>rv s. guarded_pas_domain pas s \<and> invs s \<and> pas_cur_domain pas s"
                in hoare_strengthen_post) apply (wp schedule_guarded_pas_domain schedule_cur_domain
           | simp add: guarded_pas_domain_def
           | fastforce dest: domains_distinct[THEN pas_domains_distinct_inj])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv pas l) pas (einvs and pas_cur_domain pas and guarded_pas_domain pas and (\<lambda>s. 0 < domain_time s) and pas_refined pas) (schedule_if tc) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv pas l) pas (einvs and pas_cur_domain pas and guarded_pas_domain pas and (\<lambda>s. 0 < domain_time s) and pas_refined pas) (do y <- schedule;
y <- activate_thread;
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> schedule \<lbrace>\<lambda>rv s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) \<and> invs s \<and> True\<rbrace>
 2. \<And>s. (einvs and pas_cur_domain pas and guarded_pas_domain pas and (\<lambda>s. 0 < domain_time s) and pas_refined pas) s \<Longrightarrow> ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) and einvs and pas_cur_domain pas and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined pas) s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P''\<rbrace> schedule \<lbrace>\<lambda>rv s. guarded_pas_domain pas s \<and> invs s \<and> pas_cur_domain pas s\<rbrace>
 2. \<And>rv s. guarded_pas_domain pas s \<and> invs s \<and> pas_cur_domain pas s \<Longrightarrow> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) \<and> invs s \<and> True
 3. \<And>s. (einvs and pas_cur_domain pas and guarded_pas_domain pas and (\<lambda>s. 0 < domain_time s) and pas_refined pas) s \<Longrightarrow> ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject pas (cur_thread s)) and einvs and pas_cur_domain pas and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined pas) s \<and> ?P'' s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma globals_equiv_globals_equiv_scheduler[elim]:
  "globals_equiv s t \<Longrightarrow> globals_equiv_scheduler s t" by (auto simp: globals_equiv_def globals_equiv_scheduler_def)

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

lemma flow_then_affect:
  "(Partition x, Partition l) \<in> policyFlows (pasPolicy initial_aag)
   \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy initial_aag) x" by (erule policyFlows.cases, simp_all add: partsSubjectAffects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Partition x, Partition l) \<in> policyFlows (pasPolicy initial_aag) \<Longrightarrow> Partition l \<in> partsSubjectAffects (pasPolicy initial_aag) x
theory Noninterference

lemma check_active_irq_if_reads_respects_g:
  "reads_respects_g aag (l :: 'a subject_label)
     (invs and only_timer_irq_inv irq st) (check_active_irq_if tc)" apply (simp add: check_active_irq_if_def) apply (wp dmo_getActiveIRQ_reads_respects_g| blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and only_timer_irq_inv irq st) (check_active_irq_if tc) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and only_timer_irq_inv irq st) (do irq <- do_machine_op (getActiveIRQ False);
return (irq, tc)
od) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma partitionIntegrity_cur_domain:
  "partitionIntegrity aag s s' \<Longrightarrow> cur_domain s = cur_domain s'" by (clarsimp simp: partitionIntegrity_def domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partitionIntegrity aag s s' \<Longrightarrow> cur_domain s = cur_domain s'
theory Noninterference

lemma use_ev:
  "\<lbrakk> equiv_valid I A B P 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> rv' = rv \<and> I s' t' \<and> B s' t'" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid I A B P 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> rv' = rv \<and> I s' t' \<and> B s' t'
theory Noninterference

lemma uwr_PSched_cur_domain:
  "(s,t) \<in> uwr PSched \<Longrightarrow> cur_domain (internal_state_if s) = cur_domain (internal_state_if t)" by (fastforce simp: uwr_def sameFor_def sameFor_scheduler_def domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uwr2 s PSched t \<Longrightarrow> cur_domain (internal_state_if s) = cur_domain (internal_state_if t)
theory Noninterference

lemma uwr_PSched_cur_domain':
  "(((sx, s), sm), ((tx, t), tm)) \<in> uwr PSched \<Longrightarrow> cur_domain s = cur_domain t" by (fastforce dest: uwr_PSched_cur_domain)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uwr2 ((sx, s), sm) PSched ((tx, t), tm) \<Longrightarrow> cur_domain s = cur_domain t
theory Noninterference

lemma part_not_PSched_sys_mode_of_not_KernelSchedule_True:
  "part s \<noteq> PSched \<Longrightarrow> sys_mode_of s \<noteq> KernelSchedule True" apply (erule contrapos_nn) apply (simp add: part_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. part s \<noteq> PSched \<Longrightarrow> sys_mode_of s \<noteq> KernelSchedule True proof (prove)
goal (1 subgoal):
 1. sys_mode_of s = KernelSchedule True \<Longrightarrow> part s = PSched proof (prove)
goal:
No subgoals!
theory Noninterference

lemma check_active_irq_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; (part s, u) \<in> policyFlows (pasPolicy initial_aag);
    part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s);
    ((fst s),x,(fst s')) \<in> check_active_irq_A_if; ((fst t),y,(fst t')) \<in> check_active_irq_A_if;
    snd s' = (case x of None \<Rightarrow> InIdleMode | Some xx \<Rightarrow> KernelEntry Interrupt);
    snd t' = (case y of None \<Rightarrow> InIdleMode | Some yy \<Rightarrow> KernelEntry Interrupt) \<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: check_active_irq_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; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s); (fst s, x, fst s') \<in> check_active_irq_A_if; (fst t, y, fst t') \<in> check_active_irq_A_if; snd s' = (case x of None \<Rightarrow> InIdleMode | Some xx \<Rightarrow> KernelEntry Interrupt); snd t' = (case y of None \<Rightarrow> InIdleMode | Some yy \<Rightarrow> KernelEntry Interrupt)\<rbrakk> \<Longrightarrow> x = y \<and> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t'
theory Noninterference

lemma check_active_irq_A_if_retval_eq:
  "\<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; (part s, u) \<in> policyFlows (pasPolicy initial_aag);
     part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s);
     ((fst s),x,s') \<in> check_active_irq_A_if; ((fst t),y,t') \<in> check_active_irq_A_if \<rbrakk>
     \<Longrightarrow> x = y" apply simp apply (drule_tac s'="(s',undefined)" and t'="(t',undefined)" and u=u
                in check_active_irq_A_if_confidentiality, simp+) apply (elim conjE, assumption) 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; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; user_modes (sys_mode_of s); (fst s, x, s') \<in> check_active_irq_A_if; (fst t, y, t') \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched t; XX = s; YY = t; uwr2 s (part s) t; uwr2 s u 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, x, s') \<in> check_active_irq_A_if; (fst t, y, t') \<in> check_active_irq_A_if\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>XX = s; YY = t; uwr2 s (part s) t; uwr2 s u 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, x, s') \<in> check_active_irq_A_if; (fst t, y, t') \<in> check_active_irq_A_if; x = y \<and> (undefined = ?f1 x \<and> undefined = ?f1 y \<longrightarrow> uwr2 (s', undefined) u (t', undefined) \<and> uwr2 (s', undefined) PSched (t', undefined) \<and> uwr2 (s', undefined) (part s) (t', undefined))\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory Noninterference

lemma partitionIntegrity_irq_state_update[simp]:
  "partitionIntegrity aag y (y\<lparr>machine_state := (machine_state y)\<lparr>irq_state := X\<rparr>\<rparr>)" apply (cut_tac s=y and aag=aag in partitionIntegrity_refl) apply (clarsimp simp: partitionIntegrity_def integrity_subjects_def domain_fields_equiv_def
                        globals_equiv_scheduler_def silc_dom_equiv_def equiv_for_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partitionIntegrity aag y (y\<lparr>machine_state := machine_state y\<lparr>irq_state := X\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. partitionIntegrity aag y y \<Longrightarrow> partitionIntegrity aag y (y\<lparr>machine_state := machine_state y\<lparr>irq_state := X\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma invs_if_Invs:
  "invs_if s
   \<Longrightarrow> Invs (internal_state_if s) \<and>
       det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s)" by (simp add: invs_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if s \<Longrightarrow> Invs (internal_state_if s) \<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s)