theory Noninterference

lemma thread_get_tcb_context_reads_respects_g_helper:
  "equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l)
     (\<lambda>rv rv'. arch_tcb_context_get (tcb_arch rv) = arch_tcb_context_get (tcb_arch rv'))
     (\<lambda>s. t = idle_thread s \<or> is_subject aag t)
     (gets (get_tcb t) >>= assert_opt)" apply (clarsimp simp: equiv_valid_2_def in_monad reads_equiv_g_def) apply (erule disjE) apply (frule globals_equiv_idle_thread_ptr) apply (simp add: get_tcb_def split: kernel_object.splits option.splits) apply (fastforce simp: globals_equiv_def idle_equiv_def) apply (fastforce dest: requiv_get_tcb_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>rv rv'. arch_tcb_context_get (tcb_arch rv) = arch_tcb_context_get (tcb_arch rv')) (\<lambda>s. t = idle_thread s \<or> is_subject aag t) (gets (get_tcb t) >>= assert_opt) proof (prove)
goal (1 subgoal):
 1. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread s \<or> is_subject aag t; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa) proof (prove)
goal (2 subgoals):
 1. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; t = idle_thread s\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa)
 2. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; is_subject aag t\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa) proof (prove)
goal (2 subgoals):
 1. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; t = idle_thread s; idle_thread s = idle_thread ta\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa)
 2. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; is_subject aag t\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa) proof (prove)
goal (2 subgoals):
 1. \<And>s ta a aa x2 x2a x2b x2c. \<lbrakk>reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; t = idle_thread ta; idle_thread s = idle_thread ta; kheap s (idle_thread ta) = Some (TCB a); x2 = TCB a; x2a = a; kheap ta (idle_thread ta) = Some (TCB aa); x2b = TCB aa; x2c = aa\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa)
 2. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; is_subject aag t\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa) proof (prove)
goal (1 subgoal):
 1. \<And>s ta a aa. \<lbrakk>get_tcb t s = Some a; get_tcb t ta = Some aa; t = idle_thread ta \<or> is_subject aag t; reads_equiv aag s ta; globals_equiv s ta; affects_equiv aag l s ta; is_subject aag t\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch a) = arch_tcb_context_get (tcb_arch aa) proof (prove)
goal:
No subgoals!