theory Noninterference

lemma kernel_entry_if_reads_respects_f_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f_g aag l (ct_active and silc_inv aag st and einvs
                                             and only_timer_irq_inv irq st'
                                             and schact_is_rct and pas_refined aag
                                             and pas_cur_domain aag and guarded_pas_domain aag
                                             and K (ev \<noteq> Interrupt \<and> \<not> pasMaySendIrqs aag))
                            (kernel_entry_if ev tc)" apply (simp add: kernel_entry_if_def) apply (wp handle_event_reads_respects_f_g thread_set_tcb_context_update_reads_respects_f_g
            thread_set_tcb_context_update_silc_inv only_timer_irq_inv_pres[where P="\<top>" and Q="\<top>"]
            thread_set_invs_trivial thread_set_not_state_valid_sched thread_set_pas_refined
         | simp add: tcb_cap_cases_def arch_tcb_update_aux2)+ apply (elim conjE) apply (frule (1) ct_active_cur_thread_not_idle_thread[OF invs_valid_idle]) apply (clarsimp simp: ct_in_state_def runnable_eq_active) apply (rule conjI) apply (fastforce dest: requiv_g_cur_thread_eq simp: reads_equiv_f_g_def) apply (clarsimp simp: guarded_pas_domain_def) apply (fastforce simp: only_timer_irq_inv_def invs_valid_idle
                   dest: domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (ct_active and silc_inv aag st and einvs and only_timer_irq_inv irq st' and schact_is_rct and pas_refined aag and pas_cur_domain aag and guarded_pas_domain aag and K (ev \<noteq> Interrupt \<and> \<not> pasMaySendIrqs aag)) (kernel_entry_if ev tc) proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (ct_active and silc_inv aag st and einvs and only_timer_irq_inv irq st' and schact_is_rct and pas_refined aag and pas_cur_domain aag and guarded_pas_domain aag and (\<lambda>y. ev \<noteq> Interrupt \<and> \<not> pasMaySendIrqs aag)) (do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event ev;
return (r, tc)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_active s \<and> silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> schact_is_rct s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> guarded_pas_domain aag s \<and> ev \<noteq> Interrupt \<and> \<not> pasMaySendIrqs aag \<Longrightarrow> (\<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> silc_inv aag (?st7 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ct_active s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; guarded_pas_domain aag s; ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> silc_inv aag (?st7 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ct_active s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; guarded_pas_domain aag s; ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> silc_inv aag (?st7 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at active (cur_thread s) s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; guarded_pas_domain aag s; ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> silc_inv aag (?st7 (cur_thread s)) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at active (cur_thread s) s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; guarded_pas_domain aag s; ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t
 2. \<And>s. \<lbrakk>st_tcb_at active (cur_thread s) s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; guarded_pas_domain aag s; ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> silc_inv aag (?st7 (cur_thread s)) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at active (cur_thread s) s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; guarded_pas_domain aag s; ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> silc_inv aag (?st7 (cur_thread s)) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at active (cur_thread s) s; silc_inv aag st s; invs s; valid_list s; valid_sched s; only_timer_irq_inv irq st' s; schact_is_rct s; pas_refined aag s; pas_cur_domain aag s; pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); ev \<noteq> Interrupt; \<not> pasMaySendIrqs aag; cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> silc_inv aag (?st7 (cur_thread s)) s \<and> silc_inv aag (?st48 (cur_thread s) ()) s \<and> only_timer_irq_inv (?irq49 (cur_thread s) ()) (?st'50 (cur_thread s) ()) s \<and> is_subject aag (cur_thread s) \<and> domain_sep_inv False (?st'50 (cur_thread s) ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!