theory Noninterference

lemma check_active_irq_A_if_confidentiality:
  "\<lbrakk> (s, t) \<in> uwr PSched; (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 \<rbrakk>
     \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y
                  \<longrightarrow> (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s))" apply (subgoal_tac "silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s')") apply (blast dest!: check_active_irq_A_if_confidentiality_helper) apply (case_tac s', simp) apply (case_tac a, simp) apply (clarsimp simp: check_active_irq_A_if_def) apply (erule use_valid) apply (wp check_active_irq_if_wp) apply (fastforce simp: invs_if_def Invs_def current_aag_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched 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\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>uwr2 s PSched 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; silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s')\<rbrakk> \<Longrightarrow> x = y \<and> (snd s' = f x \<and> snd t' = f y \<longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t')
 2. \<lbrakk>uwr2 s PSched 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\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s PSched 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\<rbrakk> \<Longrightarrow> silc_inv (current_aag (internal_state_if s')) s0_internal (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>uwr2 s PSched 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, a) \<in> check_active_irq_A_if; (fst t, y, fst t') \<in> check_active_irq_A_if; s' = (a, b)\<rbrakk> \<Longrightarrow> silc_inv (current_aag (snd a)) s0_internal (snd a) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>uwr2 s PSched 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, aa, ba) \<in> check_active_irq_A_if; (fst t, y, fst t') \<in> check_active_irq_A_if; s' = ((aa, ba), b); a = (aa, ba)\<rbrakk> \<Longrightarrow> silc_inv (current_aag ba) s0_internal ba proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa xa ya xaa yaa xb yb. \<lbrakk>uwr2 s PSched 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); s' = ((aa, baa), ba); fst s = (xa, ya); ((x, aa), baa) \<in> fst (check_active_irq_if xa ya); fst t = (xaa, yaa); fst t' = (xb, yb); ((y, xb), yb) \<in> fst (check_active_irq_if xaa yaa)\<rbrakk> \<Longrightarrow> silc_inv (current_aag baa) s0_internal baa proof (prove)
goal (2 subgoals):
 1. \<And>ba aa baa x ya xa yaa xb yb. \<lbrakk>uwr2 s PSched 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); s' = ((aa, baa), ba); fst s = (x, ya); fst t = (xa, yaa); fst t' = (xb, yb); ((y, xb), yb) \<in> fst (check_active_irq_if xa yaa)\<rbrakk> \<Longrightarrow> \<lbrace>?P219 ba aa baa x ya xa yaa xb yb\<rbrace> check_active_irq_if x \<lbrace>\<lambda>a b. silc_inv (current_aag b) s0_internal b\<rbrace>
 2. \<And>ba aa baa x ya xa yaa xb yb. \<lbrakk>uwr2 s PSched 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); s' = ((aa, baa), ba); fst s = (x, ya); fst t = (xa, yaa); fst t' = (xb, yb); ((y, xb), yb) \<in> fst (check_active_irq_if xa yaa)\<rbrakk> \<Longrightarrow> ?P219 ba aa baa x ya xa yaa xb yb ya proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa x ya xa yaa xb yb. \<lbrakk>uwr2 s PSched 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); s' = ((aa, baa), ba); fst s = (x, ya); fst t = (xa, yaa); fst t' = (xb, yb); ((y, xb), yb) \<in> fst (check_active_irq_if xa yaa)\<rbrakk> \<Longrightarrow> silc_inv (current_aag (ya\<lparr>machine_state := machine_state ya\<lparr>irq_state := irq_state_of_state ya + 1\<rparr>\<rparr>)) s0_internal (ya\<lparr>machine_state := machine_state ya\<lparr>irq_state := irq_state_of_state ya + 1\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!