theory Noninterference

lemma reads_equiv_g_ct_running_eq:
  "\<lbrakk> reads_equiv_g (current_aag bb) bd be; Invs bd; Invs be; current_aag bb = current_aag bd \<rbrakk>
     \<Longrightarrow> ct_running bd = ct_running be" apply (clarsimp simp: reads_equiv_f_g_def) apply (clarsimp simp: reads_equiv_g_def) apply (frule globals_equiv_idle_thread_ptr) apply (frule requiv_cur_thread_eq) apply (case_tac "cur_thread bd = idle_thread bd") apply (simp add: Invs_def) apply (elim conjE) apply (drule invs_valid_idle)+ apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def valid_idle_def) apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def) apply (fastforce simp: Invs_def guarded_pas_domain_def simp: current_aag_def
                   dest: is_subject_kheap_eq domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_g (current_aag bb) bd be; Invs bd; Invs be; current_aag bb = current_aag bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_g (current_aag bd) bd be; Invs bd; Invs be; current_aag bb = current_aag bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread bd = idle_thread bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be
 2. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread bd \<noteq> idle_thread bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs bd \<and> valid_list bd \<and> valid_sched_2 (ready_queues bd) (ekheap bd) (scheduler_action bd) (cur_domain bd) (kheap bd) (cur_thread be) (cur_thread be) \<and> only_timer_irq_inv timer_irq s0_internal bd \<and> silc_inv (current_aag bd) s0_internal bd \<and> domain_sep_inv False s0_internal bd \<and> pas_refined (current_aag bd) bd \<and> guarded_pas_domain (current_aag bd) bd \<and> idle_equiv s0_internal bd \<and> valid_domain_list bd \<and> valid_vspace_objs_if bd; invs be \<and> valid_list be \<and> valid_sched_2 (ready_queues be) (ekheap be) (scheduler_action be) (cur_domain be) (kheap be) (cur_thread be) (cur_thread be) \<and> only_timer_irq_inv timer_irq s0_internal be \<and> silc_inv (current_aag be) s0_internal be \<and> domain_sep_inv False s0_internal be \<and> pas_refined (current_aag be) be \<and> guarded_pas_domain (current_aag be) be \<and> idle_equiv s0_internal be \<and> valid_domain_list be \<and> valid_vspace_objs_if be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = cur_thread be; idle_thread be = cur_thread be; cur_thread bd = cur_thread be\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be
 2. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread bd \<noteq> idle_thread bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (2 subgoals):
 1. \<lbrakk>current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = cur_thread be; idle_thread be = cur_thread be; cur_thread bd = cur_thread be; invs bd; invs be; valid_list bd; valid_list be; valid_sched_2 (ready_queues bd) (ekheap bd) (scheduler_action bd) (cur_domain bd) (kheap bd) (cur_thread be) (cur_thread be); valid_sched_2 (ready_queues be) (ekheap be) (scheduler_action be) (cur_domain be) (kheap be) (cur_thread be) (cur_thread be); only_timer_irq_inv timer_irq s0_internal bd; only_timer_irq_inv timer_irq s0_internal be; silc_inv (current_aag bd) s0_internal bd; silc_inv (current_aag be) s0_internal be; domain_sep_inv False s0_internal bd; domain_sep_inv False s0_internal be; pas_refined (current_aag bd) bd; pas_refined (current_aag be) be; guarded_pas_domain (current_aag bd) bd; guarded_pas_domain (current_aag be) be; idle_equiv s0_internal bd; idle_equiv s0_internal be; valid_domain_list bd; valid_vspace_objs_if bd; valid_domain_list be; valid_vspace_objs_if be\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be
 2. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread bd \<noteq> idle_thread bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (2 subgoals):
 1. \<lbrakk>current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = cur_thread be; idle_thread be = cur_thread be; cur_thread bd = cur_thread be; valid_list bd; valid_list be; valid_sched_2 (ready_queues bd) (ekheap bd) (scheduler_action bd) (cur_domain bd) (kheap bd) (cur_thread be) (cur_thread be); valid_sched_2 (ready_queues be) (ekheap be) (scheduler_action be) (cur_domain be) (kheap be) (cur_thread be) (cur_thread be); only_timer_irq_inv timer_irq s0_internal bd; only_timer_irq_inv timer_irq s0_internal be; silc_inv (current_aag bd) s0_internal bd; silc_inv (current_aag be) s0_internal be; domain_sep_inv False s0_internal bd; domain_sep_inv False s0_internal be; pas_refined (current_aag bd) bd; pas_refined (current_aag be) be; guarded_pas_domain (current_aag bd) bd; guarded_pas_domain (current_aag be) be; idle_equiv s0_internal bd; idle_equiv s0_internal be; valid_domain_list bd; valid_vspace_objs_if bd; valid_domain_list be; valid_vspace_objs_if be; valid_idle bd; valid_idle be\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be
 2. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread bd \<noteq> idle_thread bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread bd \<noteq> idle_thread bd\<rbrakk> \<Longrightarrow> ct_running bd = ct_running be proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invs bd; Invs be; current_aag bb = current_aag bd; reads_equiv (current_aag bd) bd be; globals_equiv bd be; idle_thread bd = idle_thread be; cur_thread bd = cur_thread be; cur_thread be \<noteq> idle_thread be\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap bd (cur_thread be) = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_state tcb = Running)) = (\<exists>ko. kheap be (cur_thread be) = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_state tcb = Running)) proof (prove)
goal:
No subgoals!