theory Noninterference

lemma get_thread_state_reads_respects_g:
  "reads_respects_g aag l (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s))
                    (get_thread_state t)" apply (rule use_spec_ev) apply (case_tac "t = idle_thread st") apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) apply (drule_tac Q="\<lambda>rv s. s = st \<and> idle rv" in use_valid[OF _ gts_wp]) apply (simp add: valid_idle_def) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (drule_tac Q="\<lambda>rv s. s = ta \<and> idle rv" in use_valid[OF _ gts_wp]) apply (simp add: valid_idle_def) apply (fastforce simp: pred_tcb_at_def obj_at_def reads_equiv_g_def globals_equiv_idle_thread_ptr) apply (simp add: pred_tcb_at_def obj_at_def) apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) apply (frule aag_can_read_self) apply (frule get_thread_state_reads_respects_g[simplified equiv_valid_def2 equiv_valid_2_def,
                                                 rule_format, OF conjI, simplified]; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (2 subgoals):
 1. \<And>st. t = idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t)
 2. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (2 subgoals):
 1. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; (a, b) \<in> fst (get_thread_state (idle_thread st) st); (aa, ba) \<in> fst (get_thread_state (idle_thread st) ta); valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 2. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (3 subgoals):
 1. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; (aa, ba) \<in> fst (get_thread_state (idle_thread st) ta); valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) (idle_thread st) st \<longrightarrow> st = st \<and> idle sta
 2. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; (aa, ba) \<in> fst (get_thread_state (idle_thread st) ta); valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 3. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (3 subgoals):
 1. \<And>st ta aa ba. \<lbrakk>t = idle_thread_ptr; (aa, ba) \<in> fst (get_thread_state idle_thread_ptr ta); idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread st) st \<and> idle_thread st = idle_thread_ptr; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread ta) ta \<and> idle_thread ta = idle_thread_ptr; reads_equiv_g aag st ta; affects_equiv aag l st ta\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) idle_thread_ptr st \<longrightarrow> idle sta
 2. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; (aa, ba) \<in> fst (get_thread_state (idle_thread st) ta); valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 3. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (2 subgoals):
 1. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; (aa, ba) \<in> fst (get_thread_state (idle_thread st) ta); valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 2. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (3 subgoals):
 1. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) (idle_thread st) ta \<longrightarrow> ta = ta \<and> idle sta
 2. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a; ba = ta \<and> idle aa\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 3. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (3 subgoals):
 1. \<And>st ta a. \<lbrakk>t = idle_thread_ptr; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread st) st \<and> idle_thread st = idle_thread_ptr; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread ta) ta \<and> idle_thread ta = idle_thread_ptr; reads_equiv_g aag st ta; affects_equiv aag l st ta; idle a\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) idle_thread_ptr ta \<longrightarrow> idle st
 2. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a; ba = ta \<and> idle aa\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 3. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (2 subgoals):
 1. \<And>st ta a b aa ba. \<lbrakk>t = idle_thread st; valid_idle st; valid_idle ta; is_subject aag (idle_thread st) \<or> idle_thread st = idle_thread ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; b = st \<and> idle a; ba = ta \<and> idle aa\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba
 2. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. \<And>st. t \<noteq> idle_thread st \<Longrightarrow> spec_equiv_valid_inv st (reads_equiv_g aag) (affects_equiv aag l) (valid_idle and (\<lambda>s. is_subject aag t \<or> t = idle_thread s)) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. \<And>st ta a b aa ba. \<lbrakk>t \<noteq> idle_thread st; (a, b) \<in> fst (get_thread_state t st); (aa, ba) \<in> fst (get_thread_state t ta); valid_idle st; is_subject aag t; valid_idle ta; reads_equiv_g aag st ta; affects_equiv aag l st ta\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>st ta a b aa ba. \<lbrakk>t \<noteq> idle_thread st; (a, b) \<in> fst (get_thread_state t st); (aa, ba) \<in> fst (get_thread_state t ta); valid_idle st; is_subject aag t; valid_idle ta; reads_equiv_g aag st ta; affects_equiv aag l st ta; aag_can_read aag t\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal:
No subgoals!