theory Finalise_IF

lemma tcb_sched_action_reads_respects:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag l (pas_refined aag) (tcb_sched_action action t)" apply (simp add: tcb_sched_action_def get_tcb_queue_def) apply (subst gets_apply) apply (case_tac "aag_can_read aag t \<or> aag_can_affect aag l t") apply (simp add: ethread_get_def) apply wp apply (rule_tac Q="\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv)"
                      in equiv_valid_guard_imp) apply (wp gets_apply_ev') apply (fastforce simp: reads_equiv_def affects_equiv_def equiv_for_def states_equiv_for_def) apply (wp | simp)+ apply (intro conjI impI allI
          | fastforce simp: get_etcb_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="(t, 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 t}" and L'="{pasObjectAbs aag t}"
                     in ev2_invisible[OF domains_distinct]) 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 (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 (force intro: domtcbs simp: get_etcb_def pas_refined_def tcb_domain_map_wellformed_aux_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag) (tcb_sched_action action t) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queues <- gets ready_queues;
set_tcb_queue d prio (action t (queues d prio))
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od)
 2. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (pas_refined aag) (do tcb <- gets_the (get_etcb t);
tcba <- gets_the (get_etcb t);
a <- gets_apply ready_queues (tcb_domain tcb);
set_tcb_queue (tcb_domain tcb) (tcb_priority tcba) (action t (a (tcb_priority tcba)))
od)
 2. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (?P'4 rv rva) (gets_apply ready_queues (tcb_domain rv))
 2. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<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 aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (?P'3 rv) (gets_the (get_etcb t))
 4. \<And>rv. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 5. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l ?P'2 (gets_the (get_etcb t))
 6. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 7. \<And>s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 8. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv))
 2. \<And>rv rva s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<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 aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (?P'3 rv) (gets_the (get_etcb t))
 5. \<And>rv. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l ?P'2 (gets_the (get_etcb t))
 7. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (9 subgoals):
 1. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<forall>s ta. reads_equiv aag s ta \<and> affects_equiv aag l s ta \<and> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv) \<and> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv) \<longrightarrow> ready_queues s (tcb_domain rv) = ready_queues ta (tcb_domain rv)
 2. \<And>rv rva s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv)
 3. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<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 aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (?P'3 rv) (gets_the (get_etcb t))
 5. \<And>rv. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 6. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l ?P'2 (gets_the (get_etcb t))
 7. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 8. \<And>s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 9. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; ?P'4 rv rva s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain rv)
 2. \<And>rv rva. aag_can_read aag t \<or> aag_can_affect aag l t \<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 aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l (?P'3 rv) (gets_the (get_etcb t))
 4. \<And>rv. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>
 5. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> reads_respects aag l ?P'2 (gets_the (get_etcb t))
 6. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<lbrace>?P''2\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. ?P'3 rv s \<and> ?P''3 rv s\<rbrace>
 7. \<And>s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s
 8. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s ta. reads_equiv aag s ta \<and> affects_equiv aag l s ta \<longrightarrow> get_etcb t s = get_etcb t ta) \<and> ((\<exists>y. get_etcb t s = Some y) \<longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (get_etcb t s))))
 2. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; pas_refined aag s; \<exists>y. get_etcb t s = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (get_etcb t s)))
 2. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; get_etcb t 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 t \<in> pasDomainAbs aag (tcb_domain y)
 2. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; get_etcb t 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; (t, tcb_domain y) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain y)
 2. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (1 subgoal):
 1. \<not> (aag_can_read aag t \<or> aag_can_affect aag l t) \<Longrightarrow> reads_respects aag l (pas_refined aag) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
a <- gets_apply ready_queues d;
set_tcb_queue d prio (action t (a prio))
od) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (pas_refined aag) (do tcb <- gets_the (get_etcb t);
tcba <- gets_the (get_etcb t);
a <- gets_apply ready_queues (tcb_domain tcb);
set_tcb_queue (tcb_domain tcb) (tcb_priority tcba) (action t (a (tcb_priority tcba)))
od) proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W184 (pas_refined aag) (gets_the (get_etcb t))
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); ?W184 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q184 rv) (?Q184 rv') (do tcb <- gets_the (get_etcb t);
a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority tcb) (action t (a (tcb_priority tcb)))
od) (do tcb <- gets_the (get_etcb t);
a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority tcb) (action t (a (tcb_priority tcb)))
od)
 3. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>?Q184\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q184 rv) (?Q184 rv') (do tcb <- gets_the (get_etcb t);
a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority tcb) (action t (a (tcb_priority tcb)))
od) (do tcb <- gets_the (get_etcb t);
a <- gets_apply ready_queues (tcb_domain rv');
set_tcb_queue (tcb_domain rv') (tcb_priority tcb) (action t (a (tcb_priority tcb)))
od)
 2. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>?Q184\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; ?R'193 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q193 rv rv' rva) (?Q'193 rv rv' rv'a) (do a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (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 t (a (tcb_priority rv'a)))
od)
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'193 rv rv') (?P'196 rv) (?P'196 rv') (gets_the (get_etcb t)) (gets_the (get_etcb t))
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>?Q193 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>?Q'193 rv rv'\<rbrace>
 5. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. ?P'196 rv s \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'193 rv rv') (?P'196 rv) (?P'196 rv') (gets_the (get_etcb t)) (gets_the (get_etcb t))
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; ?R'193 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q193 rv rv' rva) (?Q'193 rv rv' rv'a) (do a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (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 t (a (tcb_priority rv'a)))
od)
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>?Q193 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>?Q'193 rv rv'\<rbrace>
 5. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. ?P'196 rv s \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q193 rv rv' rva) (?Q'193 rv rv' rv'a) (do a <- gets_apply ready_queues (tcb_domain rv);
set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (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 t (a (tcb_priority rv'a)))
od)
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>?Q193 rv rv'\<rbrace>
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>?Q'193 rv rv'\<rbrace>
 4. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'207 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q207 rv rv' rva rv'a rvb) (?Q'207 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva)))) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))))
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'207 rv rv' rva rv'a) (?P208 rv rv' rva) (?P'210 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 t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>?Q207 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>?Q'207 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 6. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
 7. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'207 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag t}
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'207 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag t}
 3. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'207 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag t} (?Q217 rv rv' rva rv'a rvb) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva))))
 4. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'207 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag t} (?Q'218 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))))
 5. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; ?R'207 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<forall>s ta. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))) ta). rva = rvb)
 6. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'207 rv rv' rva rv'a) (?P208 rv rv' rva) (?P'210 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 t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and ?Q217 rv rv' rva rv'a rvb\<rbrace>
 8. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and ?Q'218 rv rv' rva rv'a rv'b\<rbrace>
 9. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 10. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' rva rv'a rvb. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag t} (?Q217 rv rv' rva rv'a rvb) (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva))))
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; labels_are_invisible aag l {pasObjectAbs aag t}\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag t} (?Q'218 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))))
 3. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; labels_are_invisible aag l {pasObjectAbs aag t}\<rbrakk> \<Longrightarrow> \<forall>s ta. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))) ta). rva = rvb)
 4. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rvb rv'b. labels_are_invisible aag l {pasObjectAbs aag t}) (?P208 rv rv' rva) (?P'210 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 5. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 rv rv' rva\<rbrace> gets_apply ready_queues (tcb_domain rv) \<lbrace>\<lambda>rvb. (\<lambda>_. True) and ?Q217 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and ?Q'218 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 8. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
 9. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; labels_are_invisible aag l {pasObjectAbs aag t}\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag t} (?Q'218 rv rv' rva rv'a rv'b) (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))))
 2. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; labels_are_invisible aag l {pasObjectAbs aag t}\<rbrakk> \<Longrightarrow> \<forall>s ta. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))) ta). rva = rvb)
 3. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rvb rv'b. labels_are_invisible aag l {pasObjectAbs aag t}) (?P208 rv rv' rva) (?P'210 rv rv' rv'a) (gets_apply ready_queues (tcb_domain rv)) (gets_apply ready_queues (tcb_domain rv'))
 4. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 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 t} \<noteq> {})\<rbrace>
 5. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 rv rv' rv'a\<rbrace> gets_apply ready_queues (tcb_domain rv') \<lbrace>\<lambda>rv'b. (\<lambda>_. True) and ?Q'218 rv rv' rva rv'a rv'b\<rbrace>
 6. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 7. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
 8. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True; labels_are_invisible aag l {pasObjectAbs aag t}\<rbrakk> \<Longrightarrow> \<forall>s ta. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_tcb_queue (tcb_domain rv) (tcb_priority rva) (action t (rvb (tcb_priority rva))) s). \<forall>(rvb, t')\<in>fst (set_tcb_queue (tcb_domain rv') (tcb_priority rv'a) (action t (rv'b (tcb_priority rv'a))) ta). rva = rvb)
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rvb rv'b. labels_are_invisible aag l {pasObjectAbs aag t}) (?P208 rv rv' rva) (?P'210 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 t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 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 t} \<noteq> {})\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 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 t} \<noteq> {})\<rbrace>
 5. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 6. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
 7. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rvb rv'b. labels_are_invisible aag l {pasObjectAbs aag t}) (?P208 rv rv' rva) (?P'210 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 t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 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 t} \<noteq> {})\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 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 t} \<noteq> {})\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 5. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
 6. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S209 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 t} \<noteq> {})\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'211 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 t} \<noteq> {})\<rbrace>
 3. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rva s. ?P208 rv rv' rva s \<and> ?S209 rv rv' rva s\<rbrace>
 4. \<And>rv rv'. \<lbrakk>pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'197 rv'\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv'a s. ?P'210 rv rv' rv'a s \<and> ?S'211 rv rv' rv'a s\<rbrace>
 5. pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>rv s. True \<and> ?S'197 rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pas_refined aag s; pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l; get_etcb t s = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain y) proof (prove)
goal:
No subgoals!