theory Noninterference

lemma scheduler_action_switch_thread_is_subject:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "\<lbrakk> valid_sched s; pas_cur_domain aag s; pas_refined aag s \<rbrakk>
           \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> is_subject aag x" apply (clarsimp simp: valid_sched_def valid_sched_action_2_def
                        switch_in_cur_domain_2_def in_cur_domain_def) apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) apply (drule_tac x="(x,cur_domain s)" in bspec) apply (clarsimp simp: etcb_at_def) apply (clarsimp simp: weak_valid_sched_action_2_def) apply (clarsimp simp: valid_etcbs_def) apply (drule_tac x=x in spec) apply (simp add: st_tcb_weakenE) apply (simp add: is_etcb_at_def split: option.splits) apply (fastforce elim: domains_of_state_aux.intros) apply (fastforce dest: domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_sched s; pas_cur_domain aag s; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; pas_refined aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); st_tcb_at runnable x s; case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = is_etcb_at ptr s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); st_tcb_at runnable x s; case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); st_tcb_at runnable x s; case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; st_tcb_at (\<lambda>_. True) x s = is_etcb_at x s\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); st_tcb_at runnable x s; case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; is_etcb_at x s\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>x x2 y. \<lbrakk>valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pas_cur_domain aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); st_tcb_at runnable x s; y = x2; ekheap s x = Some x2; tcb_domain x2 = cur_domain s\<rbrakk> \<Longrightarrow> (x, cur_domain s) \<in> domains_of_state s
 2. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); weak_valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s); etcb_at (\<lambda>t. tcb_domain t = cur_domain s) x s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; scheduler_action s = switch_thread x; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (x, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal:
No subgoals!