theory Noninterference

lemma tcb_sched_action_reads_respects_g':
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "equiv_valid (reads_equiv_g aag)
               (\<lambda>s s'. affects_equiv aag (l :: 'a subject_label) s s' \<and>
                       arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
               (\<lambda>s s'. affects_equiv aag l s s' \<and>
                       arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
               (pas_refined aag) (tcb_sched_action action thread)" apply (simp add: tcb_sched_action_def get_tcb_queue_def) apply (subst gets_apply) apply (case_tac "aag_can_read aag thread \<or> aag_can_affect aag l thread") apply (simp add: ethread_get_def) apply (wp set_tcb_queue_reads_respects_g') apply (rule_tac Q="\<lambda>s. pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)"
                      in equiv_valid_guard_imp) apply (wp gets_apply_ev') apply (clarsimp simp: reads_equiv_g_def) apply (elim reads_equivE affects_equivE equiv_forE) apply (clarsimp simp: disjoint_iff_not_equal) apply metis  (* only one that works *)
          apply (wp | simp)+ apply (intro conjI impI allI
          | fastforce simp: get_etcb_def reads_equiv_g_def
                      elim: reads_equivE affects_equivE equiv_forE)+ apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def split: option.splits) apply (erule_tac x="(thread, tcb_domain y)" in ballE, force) apply (force intro: domtcbs simp: get_etcb_def) apply (simp add: equiv_valid_def2 ethread_get_def) apply (rule equiv_valid_rv_bind) apply (wp equiv_valid_rv_trivial', simp) apply (rule equiv_valid_2_bind) prefer 2 apply (wp equiv_valid_rv_trivial, simp) apply (rule equiv_valid_2_bind) apply (rule_tac P="\<top>" and P'="\<top>" and L="{pasObjectAbs aag thread}" and
                                              L'="{pasObjectAbs aag thread}" in ev2_invisible') apply (blast | simp add: labels_are_invisible_def)+ apply (rule set_tcb_queue_modifies_at_most) apply (rule set_tcb_queue_modifies_at_most) apply (rule doesnt_touch_globalsI | simp | wp)+ apply (clarsimp simp: equiv_valid_2_def gets_apply_def get_def bind_def return_def
                             labels_are_invisible_def) apply wpsimp+ apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) apply (erule_tac x="(thread, tcb_domain y)" in ballE) apply force apply (force intro: domtcbs simp: get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (tcb_sched_action action thread) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queues <- gets ready_queues;
set_tcb_queue d prio (action thread (queues d prio))
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od)
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do tcb <- gets_the (get_etcb thread);
tcba <- gets_the (get_etcb thread);
a <- gets_apply ready_queues (tcb_domain tcb);
set_tcb_queue (tcb_domain tcb) (tcb_priority tcba) (action thread (a (tcb_priority tcba)))
od)
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'4 rv rva) (gets_apply ready_queues (tcb_domain rv))
 2. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 3. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 5. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 7. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 8. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (\<lambda>s. pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv))
 2. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 5. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 7. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<forall>s t. reads_equiv_g aag s t \<and> (affects_equiv aag l s t \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state t)) \<and> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv) \<and> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv) \<longrightarrow> ready_queues s (tcb_domain rv) = ready_queues t (tcb_domain rv)
 2. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 5. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 7. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv s t. \<lbrakk>aag_can_read_or_affect aag l thread; reads_equiv aag s t; globals_equiv s t; affects_equiv aag l s t; arch_globals_equiv_strengthener (machine_state s) (machine_state t); pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)\<rbrakk> \<Longrightarrow> ready_queues s (tcb_domain rv) = ready_queues t (tcb_domain rv)
 2. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 5. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 7. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv s t. \<lbrakk>aag_can_read_or_affect aag l thread; globals_equiv s t; arch_globals_equiv_strengthener (machine_state s) (machine_state t); pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv); equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state t); equiv_asids (aag_can_read_asid aag) s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); equiv_machine_state (aag_can_affect aag l) (machine_state s) (machine_state t); equiv_asids (aag_can_affect_asid aag l) s t; \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap t x; \<And>x. (aag_can_read aag \<circ> fst) x \<Longrightarrow> cdt s x = cdt t x; \<And>x. (aag_can_read aag \<circ> fst) x \<Longrightarrow> cdt_list s x = cdt_list t x; \<And>x. aag_can_read aag x \<Longrightarrow> ekheap s x = ekheap t x; \<And>x. (aag_can_read aag \<circ> fst) x \<Longrightarrow> is_original_cap s x = is_original_cap t x; \<And>x. aag_can_read_irq aag x \<Longrightarrow> interrupt_states s x = interrupt_states t x; \<And>x. aag_can_read_irq aag x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x; \<And>x. aag_can_read_domain aag x \<Longrightarrow> ready_queues s x = ready_queues t x; \<And>x. aag_can_affect aag l x \<Longrightarrow> kheap s x = kheap t x; \<And>x. (aag_can_affect aag l \<circ> fst) x \<Longrightarrow> cdt s x = cdt t x; \<And>x. (aag_can_affect aag l \<circ> fst) x \<Longrightarrow> cdt_list s x = cdt_list t x; \<And>x. aag_can_affect aag l x \<Longrightarrow> ekheap s x = ekheap t x; \<And>x. (aag_can_affect aag l \<circ> fst) x \<Longrightarrow> is_original_cap s x = is_original_cap t x; \<And>x. aag_can_affect_irq aag l x \<Longrightarrow> interrupt_states s x = interrupt_states t x; \<And>x. aag_can_affect_irq aag l x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x; \<And>x. aag_can_affect_domain aag l x \<Longrightarrow> ready_queues s x = ready_queues t x\<rbrakk> \<Longrightarrow> ready_queues s (tcb_domain rv) = ready_queues t (tcb_domain rv)
 2. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 5. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 7. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv s t. \<lbrakk>aag_can_read_or_affect aag l thread; globals_equiv s t; arch_globals_equiv_strengthener (machine_state s) (machine_state t); pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv); equiv_asids (aag_can_read_asid aag) s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); equiv_asids (aag_can_affect_asid aag l) s t; \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap t x; \<And>a b. aag_can_read aag a \<Longrightarrow> cdt s (a, b) = cdt t (a, b); \<And>a b. aag_can_read aag a \<Longrightarrow> cdt_list s (a, b) = cdt_list t (a, b); \<And>x. aag_can_read aag x \<Longrightarrow> ekheap s x = ekheap t x; \<And>a b. aag_can_read aag a \<Longrightarrow> is_original_cap s (a, b) = is_original_cap t (a, b); \<And>x. aag_can_read_irq aag x \<Longrightarrow> interrupt_states s x = interrupt_states t x; \<And>x. aag_can_read_irq aag x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x; \<And>x. \<exists>x\<in>pasDomainAbs aag x. x \<in> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> ready_queues s x = ready_queues t x; \<And>x. aag_can_affect aag l x \<Longrightarrow> kheap s x = kheap t x; \<And>a b. aag_can_affect aag l a \<Longrightarrow> cdt s (a, b) = cdt t (a, b); \<And>a b. aag_can_affect aag l a \<Longrightarrow> cdt_list s (a, b) = cdt_list t (a, b); \<And>x. aag_can_affect aag l x \<Longrightarrow> ekheap s x = ekheap t x; \<And>a b. aag_can_affect aag l a \<Longrightarrow> is_original_cap s (a, b) = is_original_cap t (a, b); \<And>x. aag_can_affect_irq aag l x \<Longrightarrow> interrupt_states s x = interrupt_states t x; \<And>x. aag_can_affect_irq aag l x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node t x; \<And>x. aag_can_affect_label aag l \<and> (\<exists>x\<in>pasDomainAbs aag x. x \<in> subjectReads (pasPolicy aag) l) \<Longrightarrow> ready_queues s x = ready_queues t x; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state t); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state t); equiv_for (aag_can_affect aag l) underlying_memory (machine_state s) (machine_state t); equiv_for (aag_can_affect aag l) device_state (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> ready_queues s (tcb_domain rv) = ready_queues t (tcb_domain rv)
 2. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 5. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 7. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 2. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 3. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 5. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 7. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 8. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva s. \<lbrakk>aag_can_read_or_affect aag l thread; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain rv)
 2. \<And>rv rva. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb _. True\<rbrace>
 3. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (?P'3 rv) (gets_the (get_etcb thread))
 4. \<And>rv. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 5. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag ?P'2 (gets_the (get_etcb thread))
 6. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 7. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 8. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state t) \<longrightarrow> get_etcb thread s = get_etcb thread t) \<and> ((\<exists>y. get_etcb thread s = Some y) \<longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain (the (get_etcb thread s))))
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l thread; pas_refined aag s; \<exists>y. get_etcb thread s = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain (the (get_etcb thread s)))
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>aag_can_read_or_affect aag l thread; get_etcb thread s = Some y; 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> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y)
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>aag_can_read_or_affect aag l thread; get_etcb thread s = Some y; 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; (thread, tcb_domain y) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y)
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_equiv_valid_g_inv (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) aag (pas_refined aag) (do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action thread (a prio))
od) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> equiv_valid_rv_inv (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (pas_refined aag) (do tcb <- gets_the (get_etcb thread);
tcba <- gets_the (get_etcb thread);
a <- gets_apply ready_queues (tcb_domain tcb);
set_tcb_queue (tcb_domain tcb) (tcb_priority tcba) (action thread (a (tcb_priority tcba)))
od) proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> equiv_valid_rv_inv (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) ?W124 (pas_refined aag) (gets_the (get_etcb thread))
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ?W124 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (?Q124 rv) (?Q124 rv') (do tcb <- gets_the (get_etcb thread);
a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority tcb) (action thread (a (tcb_priority tcb)))
od) (do tcb <- gets_the (get_etcb thread);
a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority tcb) (action thread (a (tcb_priority tcb)))
od)
 3. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q124\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (?Q124 rv) (?Q124 rv') (do tcb <- gets_the (get_etcb thread);
a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority tcb) (action thread (a (tcb_priority tcb)))
od) (do tcb <- gets_the (get_etcb thread);
a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority tcb) (action thread (a (tcb_priority tcb)))
od)
 2. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q124\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; ?R'133 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (?Q133 rv rv' rva) (?Q'133 rv rv' rv'a) (do a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (a (tcb_priority rva)))
od) (do a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (a (tcb_priority rv'a)))
od)
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (?R'133 rv rv') (?P'136 rv) (?P'136 rv') (gets_the (get_etcb thread)) (gets_the (get_etcb thread))
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q133 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q'133 rv rv'\<rbrace>
 5. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'136 rv s \<and> ?S'137 rv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (?R'133 rv rv') (?P'136 rv) (?P'136 rv') (gets_the (get_etcb thread)) (gets_the (get_etcb thread))
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; ?R'133 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (?Q133 rv rv' rva) (?Q'133 rv rv' rv'a) (do a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (a (tcb_priority rva)))
od) (do a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (a (tcb_priority rv'a)))
od)
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q133 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q'133 rv rv'\<rbrace>
 5. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. ?P'136 rv s \<and> ?S'137 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (?Q133 rv rv' rva) (?Q'133 rv rv' rv'a) (do a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (a (tcb_priority rva)))
od) (do a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (a (tcb_priority rv'a)))
od)
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q133 rv rv'\<rbrace>
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>?Q'133 rv rv'\<rbrace>
 4. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. True \<and> ?S'137 rv s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (=) (?Q147 rv rv' rva rv'a rvb) (?Q'147 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva)))) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (?R'147 rv rv' rva rv'a) (?P148 rv rv' rva) (?P'150 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 3. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S149 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>?Q147 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'151 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>?Q'147 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P148 rv rv' rva s \<and> ?S149 rv rv' rva s\<rbrace>
 6. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv'a s. ?P'150 rv rv' rv'a s \<and> ?S'151 rv rv' rv'a s\<rbrace>
 7. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. True \<and> ?S'137 rv s\<rbrace> proof (prove)
goal (16 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> pas_domains_distinct aag
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag thread}
 3. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag thread}
 4. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (?Q157 rv rv' rva rv'a rvb) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))))
 5. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (?Q'158 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 6. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> doesnt_touch_globals (?Q157 rv rv' rva rv'a rvb) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))))
 7. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> doesnt_touch_globals (?Q'158 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 8. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 9. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 10. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'147 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) t). rva = rvb)
A total of 16 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rv' rva rv'a rvb. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); pas_domains_distinct aag\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (?Q157 rv rv' rva rv'a rvb) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))))
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (?Q'158 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 3. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> doesnt_touch_globals (?Q157 rv rv' rva rv'a rvb) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))))
 4. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> doesnt_touch_globals (?Q'158 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 5. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 6. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 7. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) t). rva = rvb)
 8. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>rvb rv'b. pas_domains_distinct aag) (?P148 rv rv' rva) (?P'150 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 9. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S149 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and ?Q157 rv rv' rva rv'a rvb\<rbrace>
 10. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'151 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and ?Q'158 rv rv' rva rv'a rv'b\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (?Q'158 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> doesnt_touch_globals (\<lambda>s. pasDomainAbs aag (tcb_domain rv) \<inter> {pasObjectAbs aag thread} \<noteq> {}) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))))
 3. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> doesnt_touch_globals (?Q'158 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 4. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 5. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 6. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) t). rva = rvb)
 7. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>rvb rv'b. pas_domains_distinct aag) (?P148 rv rv' rva) (?P'150 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 8. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S149 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv) \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 9. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'151 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and ?Q'158 rv rv' rva rv'a rv'b\<rbrace>
 10. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P148 rv rv' rva s \<and> ?S149 rv rv' rva s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> doesnt_touch_globals (\<lambda>s. pasDomainAbs aag (tcb_domain rv) \<inter> {pasObjectAbs aag thread} \<noteq> {}) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))))
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> doesnt_touch_globals (\<lambda>s. pasDomainAbs aag (tcb_domain rv') \<inter> {pasObjectAbs aag thread} \<noteq> {}) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))))
 3. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 4. \<And>rv rv' rva rv'a rvb rv'b st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace> set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) \<lbrace>\<lambda>_ s. arch_globals_equiv_strengthener (machine_state st) (machine_state s)\<rbrace>
 5. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True; pas_domains_distinct aag\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action thread (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action thread (rv'b (tcb_priority rv'a))) t). rva = rvb)
 6. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>rvb rv'b. pas_domains_distinct aag) (?P148 rv rv' rva) (?P'150 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 7. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S149 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv) \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 8. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'151 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv') \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 9. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P148 rv rv' rva s \<and> ?S149 rv rv' rva s\<rbrace>
 10. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv'a s. ?P'150 rv rv' rv'a s \<and> ?S'151 rv rv' rv'a s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> equiv_valid_2 (reads_equiv_g aag) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>rvb rv'b. pas_domains_distinct aag) (?P148 rv rv' rva) (?P'150 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S149 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv) \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'151 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv') \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P148 rv rv' rva s \<and> ?S149 rv rv' rva s\<rbrace>
 5. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv'a s. ?P'150 rv rv' rv'a s \<and> ?S'151 rv rv' rv'a s\<rbrace>
 6. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. True \<and> ?S'137 rv s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a s t. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l; ?P148 rv rv' rva s; ?P'150 rv rv' rv'a t; reads_equiv_g aag s t; affects_equiv aag l s t; arch_globals_equiv_strengthener (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> pas_domains_distinct aag
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S149 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv) \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'151 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and (\<lambda>s. pasDomainAbs aag (tcb_domain rv') \<inter> {pasObjectAbs aag thread} \<noteq> {})\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rva s. ?P148 rv rv' rva s \<and> ?S149 rv rv' rva s\<rbrace>
 5. \<And>rv rv'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'137 rv'\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv'a s. ?P'150 rv rv' rv'a s \<and> ?S'151 rv rv' rv'a s\<rbrace>
 6. pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb thread) \<lbrace>\<lambda>rv s. True \<and> ?S'137 rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pas_refined aag s; pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l; get_etcb thread s = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l; get_etcb thread s = Some y; 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> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l; get_etcb thread s = Some y; 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 (thread, tcb_domain y) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y)
 2. \<And>s y. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l; get_etcb thread s = Some y; 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; (thread, tcb_domain y) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l; get_etcb thread s = Some y; 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; (thread, tcb_domain y) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag thread \<in> pasDomainAbs aag (tcb_domain y) proof (prove)
goal:
No subgoals!