theory Noninterference

lemma kernel_entry_if_partitionIntegrity:
  "\<lbrace>silc_inv aag st and pas_refined aag and einvs and schact_is_rct
                    and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st'
                    and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st\<rbrace>
   kernel_entry_if ev tc
   \<lbrace>\<lambda>_. partitionIntegrity (aag :: 'a subject_label PAS) st\<rbrace>" apply (rule_tac Q="\<lambda>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False,
                                                pasMayEditReadyQueues := False\<rparr>) X st s) \<and>
                            domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and>
                            idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s"
               in hoare_strengthen_post) apply (wp hoare_vcg_conj_lift) apply (rule hoare_vcg_all_lift[OF kernel_entry_if_integrity[where st'=st']]) apply (wp kernel_entry_if_cur_thread kernel_entry_if_globals_equiv_scheduler
              kernel_entry_if_cur_domain domain_fields_equiv_lift[where R="\<top>"]
              kernel_entry_if_domain_fields | simp)+ apply (rule_tac P="pas_refined aag and einvs and schact_is_rct and
                       is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and
                       (\<lambda> s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)"
                 in silc_dom_equiv_from_silc_inv_valid') apply (wp kernel_entry_silc_inv[where st'=st'], simp add: schact_is_rct_simple) apply (fastforce simp: pas_refined_pasMayActivate_update pas_refined_pasMayEditReadyQueues_update
                          globals_equiv_scheduler_refl silc_dom_equiv_def equiv_for_refl
                          domain_fields_equiv_def ct_active_not_idle') apply (fastforce simp: partitionIntegrity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>_. partitionIntegrity aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s\<rbrace>
 2. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P4\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>rv s. \<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s\<rbrace>
 2. \<lbrace>?P'4\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>rv s. domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s\<rbrace>
 3. \<And>s. (silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st) s \<Longrightarrow> ?P4 s \<and> ?P'4 s
 4. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'4\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>rv s. domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s\<rbrace>
 2. \<And>s. (silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st) s \<Longrightarrow> (\<forall>x. (einvs and schact_is_rct and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and is_subject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) st' and guarded_pas_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s) \<and> ?P'4 s
 3. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'22\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>rv. silc_dom_equiv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st) s \<Longrightarrow> (\<forall>x. (einvs and schact_is_rct and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and is_subject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) st' and guarded_pas_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s) \<and> (domain_fields_equiv st and K (ev \<noteq> Interrupt) and (\<lambda>_. True)) s \<and> (globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<and> idle_thread s = idle_thread st \<and> ?P'22 s
 3. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and silc_inv aag st\<rbrace> kernel_entry_if ev tc \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st) s \<Longrightarrow> (\<forall>x. (einvs and schact_is_rct and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and is_subject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) st' and guarded_pas_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s) \<and> (domain_fields_equiv st and K (ev \<noteq> Interrupt) and (\<lambda>_. True)) s \<and> (globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<and> idle_thread s = idle_thread st \<and> (pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and silc_inv aag ?st25 and silc_dom_equiv aag st) s
 3. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (2 subgoals):
 1. \<And>s. (silc_inv aag st and pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<and> ct_active s) and (=) st) s \<Longrightarrow> (\<forall>x. (einvs and schact_is_rct and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and is_subject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) st' and guarded_pas_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s) \<and> (domain_fields_equiv st and K (ev \<noteq> Interrupt) and (\<lambda>_. True)) s \<and> (globals_equiv_scheduler st and valid_arch_state and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<and> idle_thread s = idle_thread st \<and> (pas_refined aag and einvs and schact_is_rct and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and silc_inv aag ?st25 and silc_dom_equiv aag st) s
 2. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (\<forall>X. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) X st s) \<and> domain_fields_equiv st s \<and> globals_equiv_scheduler st s \<and> idle_thread s = idle_thread st \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal:
No subgoals!