theory Noninterference

lemma choose_thread_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_g aag (l :: 'a subject_label)
           ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and
                 einvs and valid_queues and pas_cur_domain aag and pas_refined aag)
           choose_thread" apply (simp add: choose_thread_def) apply (wp guarded_switch_to_reads_respects_g) apply (rule conjI) apply (fastforce simp: reads_equiv_g_def reads_equiv_def) apply (rule conjI) apply (clarsimp simp: reads_equiv_g_def reads_equiv_def2
                         states_equiv_for_def equiv_for_def disjoint_iff_not_equal) apply (metis reads_lrefl) apply (simp add: invs_valid_idle) 
  (* everything from here clagged from Syscall_AC.choose_thread_respects *)
   apply (clarsimp simp: pas_refined_def) apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) apply (erule_tac x="(hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s)"
                in ballE) apply (fastforce dest: domains_distinct[THEN pas_domains_distinct_inj]) apply (clarsimp simp: valid_queues_def is_etcb_at_def) apply (erule_tac x="cur_domain s" in allE) apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE) apply clarsimp apply (erule_tac x="hd (max_non_empty_queue (ready_queues s (cur_domain s)))" in ballE) apply (clarsimp) apply (erule notE, rule domtcbs) apply force apply (simp add: etcb_at_def) apply (simp add: max_non_empty_queue_def) apply (erule_tac P="hd A \<in> B" for A B in notE) apply (rule Max_prop) apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) choose_thread proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) (do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> (\<forall>sa t. reads_equiv_g aag sa t \<and> affects_equiv aag l sa t \<longrightarrow> ready_queues sa (cur_domain s) = ready_queues t (cur_domain s)) \<and> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>sa. is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> \<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t
 2. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> (\<forall>sa t. reads_equiv_g aag sa t \<and> affects_equiv aag l sa t \<longrightarrow> ready_queues sa (cur_domain s) = ready_queues t (cur_domain s)) \<and> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>sa. is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> (\<forall>sa t. reads_equiv_g aag sa t \<and> affects_equiv aag l sa t \<longrightarrow> ready_queues sa (cur_domain s) = ready_queues t (cur_domain s)) \<and> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>sa. is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> \<forall>sa t. reads_equiv_g aag sa t \<and> affects_equiv aag l sa t \<longrightarrow> ready_queues sa (cur_domain s) = ready_queues t (cur_domain s)
 2. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>sa. is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; valid_queues s; pas_cur_domain aag s; pas_refined aag s; \<forall>x. aag_can_read aag x \<longrightarrow> kheap sa x = kheap t x; \<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory (machine_state sa) x = underlying_memory (machine_state t) x; \<forall>x. aag_can_read aag x \<longrightarrow> device_state (machine_state sa) x = device_state (machine_state t) x; \<forall>a. aag_can_read aag a \<longrightarrow> (\<forall>b. cdt sa (a, b) = cdt t (a, b)); \<forall>x. aag_can_read aag x \<longrightarrow> ekheap sa x = ekheap t x; \<forall>a. aag_can_read aag a \<longrightarrow> (\<forall>b. cdt_list sa (a, b) = cdt_list t (a, b)); \<forall>a. aag_can_read aag a \<longrightarrow> (\<forall>b. is_original_cap sa (a, b) = is_original_cap t (a, b)); \<forall>x. aag_can_read_irq aag x \<longrightarrow> interrupt_states sa x = interrupt_states t x; \<forall>x. aag_can_read_irq aag x \<longrightarrow> interrupt_irq_node sa x = interrupt_irq_node t x; \<forall>x. (\<exists>x\<in>pasDomainAbs aag x. x \<in> subjectReads (pasPolicy aag) (pasSubject aag)) \<longrightarrow> ready_queues sa x = ready_queues t x; equiv_asids (aag_can_read_asid aag) sa t; cur_thread sa = cur_thread t; cur_domain sa = cur_domain t; scheduler_action sa = scheduler_action t; work_units_completed sa = work_units_completed t; equiv_irq_state (machine_state sa) (machine_state t); globals_equiv sa t; affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> ready_queues sa (cur_domain s) = ready_queues t (cur_domain s)
 2. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>sa. is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and valid_queues and pas_cur_domain aag and pas_refined aag) s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>sa. is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> valid_queues s \<and> pas_cur_domain aag s \<and> pas_refined aag s \<Longrightarrow> (\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> valid_queues s \<and> pas_cur_domain aag s \<and> pas_refined aag s \<Longrightarrow> (\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; valid_queues s; pas_cur_domain aag s; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_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; ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; valid_queues s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; valid_queues s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; case (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s))))
 2. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; valid_queues s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; valid_queues s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; \<forall>p. (\<forall>t\<in>set (ready_queues s (cur_domain s) p). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) p)\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; \<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); (\<exists>y. ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s))))
 2. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s prio y. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s))))
 2. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (3 subgoals):
 1. \<And>s prio y. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some (?etcb93 s prio y)
 2. \<And>s prio y. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain (?etcb93 s prio y)
 3. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s prio y. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain y
 2. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> is_subject aag (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) \<in> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) proof (prove)
goal (2 subgoals):
 1. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<in> {prio. ready_queues s (cur_domain s) prio \<noteq> []}\<rbrakk> \<Longrightarrow> hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) \<in> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))
 2. \<And>s prio. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; 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; ready_queues s (cur_domain s) prio \<noteq> []; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<noteq> {} proof (prove)
goal:
No subgoals!