theory Noninterference

lemma schedule_if_partitionIntegrity:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "\<lbrace>partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and
          (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag\<rbrace>
         schedule_if tc
         \<lbrace>\<lambda>_. partitionIntegrity aag st\<rbrace>" apply (simp add: schedule_if_def) apply (rule_tac Q="\<lambda>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
                                      (scheduler_affects_globals_frame st) st s \<and>
                            domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and>
                            globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s"
               in hoare_strengthen_post) apply (wpsimp wp: activate_thread_integrity activate_thread_globals_equiv_scheduler
                     silc_dom_equiv_from_silc_inv_valid'[where P="\<top>"] schedule_integrity
                     hoare_vcg_all_lift domain_fields_equiv_lift[where Q="\<top>" and R="\<top>"]) apply (rule_tac Q="\<lambda>r s. guarded_pas_domain aag s \<and> pas_cur_domain aag s \<and>
                             domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and>
                             globals_equiv_scheduler st s \<and> silc_inv aag st s \<and>
                             silc_dom_equiv aag st s \<and> invs s" in hoare_strengthen_post) apply (wp schedule_guarded_pas_domain schedule_cur_domain
               silc_dom_equiv_from_silc_inv_valid'[where P="\<top>" and st=st]
               domain_fields_equiv_lift schedule_cur_domain schedule_domain_fields
            | simp add: silc_inv_def partitionIntegrity_def guarded_pas_domain_def
                        invs_valid_idle silc_dom_equiv_def)+ apply (fastforce simp: equiv_for_refl dest: domains_distinct[THEN pas_domains_distinct_inj]) apply (fastforce simp: partitionIntegrity_def globals_equiv_scheduler_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag\<rbrace> schedule_if tc \<lbrace>\<lambda>_. partitionIntegrity aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag\<rbrace> do y <- schedule;
y <- activate_thread;
return tc
od \<lbrace>\<lambda>_. partitionIntegrity aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag\<rbrace> do y <- schedule;
y <- activate_thread;
return tc
od \<lbrace>\<lambda>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s\<rbrace>
 2. \<And>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'31\<rbrace> schedule \<lbrace>\<lambda>rv s. valid_idle s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> valid_arch_state s \<and> valid_idle s \<and> silc_inv aag (?st24 ()) s \<and> silc_dom_equiv aag st s\<rbrace>
 2. \<And>s. (partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag) s \<Longrightarrow> (einvs and integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and pas_cur_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. domain_time s \<noteq> 0)) s \<and> ?P'31 s
 3. \<And>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'31\<rbrace> schedule \<lbrace>\<lambda>r s. guarded_pas_domain aag s \<and> pas_cur_domain aag s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_inv aag st s \<and> silc_dom_equiv aag st s \<and> invs s\<rbrace>
 2. \<And>rv s. guarded_pas_domain aag s \<and> pas_cur_domain aag s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_inv aag st s \<and> silc_dom_equiv aag st s \<and> invs s \<Longrightarrow> valid_idle s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> valid_arch_state s \<and> valid_idle s \<and> silc_inv aag (?st24 ()) s \<and> silc_dom_equiv aag st s
 3. \<And>s. (partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag) s \<Longrightarrow> (einvs and integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and pas_cur_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. domain_time s \<noteq> 0)) s \<and> ?P'31 s
 4. \<And>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (3 subgoals):
 1. \<And>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)) \<and> pas_cur_domain aag s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> SilcLabel \<noteq> pasSubject aag \<and> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s)) \<and> (\<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s \<and> (\<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s \<and> invs s \<Longrightarrow> (cur_thread s \<noteq> idle_thread st \<longrightarrow> is_subject aag (cur_thread s)) \<and> valid_arch_state s \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap (?st24 ()) s \<and> (\<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) (?st24 ())))
 2. \<And>s. (partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag) s \<Longrightarrow> (einvs and integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and pas_cur_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. domain_time s \<noteq> 0)) s \<and> (guarded_pas_domain aag and einvs and pas_refined aag) s \<and> (pas_cur_domain aag s \<and> domain_time s \<noteq> 0) \<and> (domain_fields_equiv st and (\<lambda>a. domain_time a \<noteq> 0) and (\<lambda>s. domain_time s \<noteq> 0)) s \<and> idle_thread s = idle_thread st \<and> (globals_equiv_scheduler st and invs) s \<and> silc_inv aag st s \<and> ((\<lambda>_. True) and silc_inv aag st and silc_dom_equiv aag st) s \<and> invs s
 3. \<And>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal (2 subgoals):
 1. \<And>s. (partitionIntegrity aag st and guarded_pas_domain aag and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv aag st and einvs and pas_refined aag) s \<Longrightarrow> (einvs and integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st and pas_refined (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and pas_cur_domain (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) and (\<lambda>s. domain_time s \<noteq> 0)) s \<and> (guarded_pas_domain aag and einvs and pas_refined aag) s \<and> (pas_cur_domain aag s \<and> domain_time s \<noteq> 0) \<and> (domain_fields_equiv st and (\<lambda>a. domain_time a \<noteq> 0) and (\<lambda>s. domain_time s \<noteq> 0)) s \<and> idle_thread s = idle_thread st \<and> (globals_equiv_scheduler st and invs) s \<and> silc_inv aag st s \<and> ((\<lambda>_. True) and silc_inv aag st and silc_dom_equiv aag st) s \<and> invs s
 2. \<And>rv s. integrity (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {} st s \<and> domain_fields_equiv st s \<and> idle_thread s = idle_thread st \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<Longrightarrow> partitionIntegrity aag st s proof (prove)
goal:
No subgoals!