theory Syscall_AC

lemma choose_thread_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and pas_cur_domain aag and einvs and valid_queues\<rbrace>
   choose_thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: choose_thread_def guarded_switch_to_def
         | wp switch_to_thread_respects' switch_to_idle_thread_respects gts_wp)+ apply (clarsimp simp: pas_refined_def) apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) 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 simp: etcb_at_def) 
  (* thread we're switching to is in cur_domain *)
   apply (rule_tac s = "cur_domain s" in subst) apply (clarsimp simp: max_non_empty_queue_def) apply (frule tcb_at_ekheap_dom[OF st_tcb_at_tcb_at]) apply (simp add: valid_sched_def) apply (clarsimp simp: max_non_empty_queue_def) apply (metis (mono_tags, lifting) setcomp_Max_has_prop hd_in_set) 
  (* pas_cur_domain *)
   apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and pas_cur_domain aag and einvs and valid_queues\<rbrace> choose_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> valid_queues s \<Longrightarrow> (\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s \<longrightarrow> runnable st \<longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta\<rbrakk> \<Longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta\<rbrakk> \<Longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag 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); ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta\<rbrakk> \<Longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; \<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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; (\<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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; \<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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))))))
 2. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> cur_domain s = tcb_domain (the (ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s))))))
 2. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal (2 subgoals):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable sta; 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> cur_domain s = tcb_domain (the (ekheap s (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})))))
 2. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal (3 subgoals):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable sta; 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> valid_etcbs s
 2. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable sta; 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> []})); \<exists>etcb. ekheap s (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) = Some etcb\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain (the (ekheap s (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})))))
 3. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal (2 subgoals):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable sta; 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> []})); \<exists>etcb. ekheap s (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) = Some etcb\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain (the (ekheap s (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})))))
 2. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal (2 subgoals):
 1. \<And>s prio sta etcb. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable sta; 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> []})); ekheap s (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) = Some etcb\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain etcb
 2. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal (1 subgoal):
 1. \<And>s prio sta. \<lbrakk>integrity aag X st 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; pas_cur_domain aag s; invs s; valid_list s; valid_sched s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) sta) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable sta; 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> pas_cur_domain aag s proof (prove)
goal:
No subgoals!