theory Finalise_IF

lemma possible_switch_to_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (pas_refined aag and pas_cur_domain aag
                                               and (\<lambda>s. is_subject aag (cur_thread s)))
                              (possible_switch_to tptr)" apply (simp add: possible_switch_to_def ethread_get_def) apply (case_tac "aag_can_read aag tptr \<or> aag_can_affect aag l tptr") apply (wp hoare_weak_lift_imp tcb_sched_action_reads_respects | wpc | simp)+ apply (clarsimp simp: get_etcb_def) apply ((intro conjI impI allI
          | elim aag_can_read_self reads_equivE affects_equivE equiv_forE conjE disjE
          | force)+)[1] apply clarsimp apply (wp (once), rename_tac cur_dom) apply (simp add: equiv_valid_def2) apply (rule_tac W="\<top>\<top>" and Q="\<lambda>tcb. pas_refined aag and K (tcb_domain tcb \<noteq> cur_dom)"
                  in equiv_valid_rv_bind) prefer 3 apply wp apply (monad_eq simp: get_etcb_def equiv_valid_2_def) apply (rule gen_asm_ev2') apply (simp add: equiv_valid_def2[symmetric]) apply (wp tcb_sched_action_reads_respects) apply (simp add: reads_equiv_def) apply (wp gets_cur_domain_ev)+ apply (clarsimp simp: get_etcb_def pas_refined_def tcb_domain_map_wellformed_aux_def) apply (frule_tac x="(tptr, tcb_domain y)" in bspec, force intro: domtcbs) apply (erule notE) apply (fastforce dest: domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (possible_switch_to tptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read aag tptr \<or> aag_can_affect aag l tptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 2. \<not> (aag_can_read aag tptr \<or> aag_can_affect aag l tptr) \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag tptr \<or> aag_can_affect aag l tptr; pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_etcb tptr s = get_etcb tptr t) \<and> ((\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t))
 2. \<not> (aag_can_read aag tptr \<or> aag_can_affect aag l tptr) \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read aag tptr \<or> aag_can_affect aag l tptr; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> ekheap s tptr = ekheap t tptr) \<and> ((\<exists>y. ekheap s tptr = Some y) \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t))
 2. \<not> (aag_can_read aag tptr \<or> aag_can_affect aag l tptr) \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) proof (prove)
goal (1 subgoal):
 1. \<not> (aag_can_read aag tptr \<or> aag_can_affect aag l tptr) \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) (do cur_dom <- gets cur_domain;
tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q154 cur_dom) (do tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>?Q154\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q154 cur_dom) (do tcb <- gets_the (get_etcb tptr);
action <- gets scheduler_action;
if tcb_domain tcb \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>?Q154\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (6 subgoals):
 1. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (?Q154 cur_dom) (gets_the (get_etcb tptr))
 2. \<And>cur_dom rv rv'. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (pas_refined aag and K (tcb_domain rv \<noteq> cur_dom)) (pas_refined aag and K (tcb_domain rv' \<noteq> cur_dom)) (do action <- gets scheduler_action;
if tcb_domain rv \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) (do action <- gets scheduler_action;
if tcb_domain rv' \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 3. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?Q154 cur_dom\<rbrace> gets_the (get_etcb tptr) \<lbrace>\<lambda>tcb. pas_refined aag and K (tcb_domain tcb \<noteq> cur_dom)\<rbrace>
 4. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 5. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>?Q154\<rbrace>
 6. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (6 subgoals):
 1. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?Q154 cur_dom\<rbrace> gets_the (get_etcb tptr) \<lbrace>\<lambda>tcb. pas_refined aag and K (tcb_domain tcb \<noteq> cur_dom)\<rbrace>
 2. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (?Q154 cur_dom) (gets_the (get_etcb tptr))
 3. \<And>cur_dom rv rv'. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (pas_refined aag and K (tcb_domain rv \<noteq> cur_dom)) (pas_refined aag and K (tcb_domain rv' \<noteq> cur_dom)) (do action <- gets scheduler_action;
if tcb_domain rv \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) (do action <- gets scheduler_action;
if tcb_domain rv' \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 4. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 5. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>?Q154\<rbrace>
 6. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (5 subgoals):
 1. \<And>cur_dom. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s) (gets_the (get_etcb tptr))
 2. \<And>cur_dom rv rv'. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (pas_refined aag and K (tcb_domain rv \<noteq> cur_dom)) (pas_refined aag and K (tcb_domain rv' \<noteq> cur_dom)) (do action <- gets scheduler_action;
if tcb_domain rv \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) (do action <- gets scheduler_action;
if tcb_domain rv' \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 4. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s\<rbrace>
 5. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom rv rv'. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (pas_refined aag and K (tcb_domain rv \<noteq> cur_dom)) (pas_refined aag and K (tcb_domain rv' \<noteq> cur_dom)) (do action <- gets scheduler_action;
if tcb_domain rv \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) (do action <- gets scheduler_action;
if tcb_domain rv' \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom rv rv'. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; True; tcb_domain rv \<noteq> cur_dom; tcb_domain rv' \<noteq> cur_dom\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (pas_refined aag) (pas_refined aag) (do action <- gets scheduler_action;
if tcb_domain rv \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od) (do action <- gets scheduler_action;
if tcb_domain rv' \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od)
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom rv rv'. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; tcb_domain rv \<noteq> cur_dom; tcb_domain rv' \<noteq> cur_dom\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag) (do action <- gets scheduler_action;
tcb_sched_action tcb_sched_enqueue tptr
od)
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom rv rv' s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; tcb_domain rv \<noteq> cur_dom; tcb_domain rv' \<noteq> cur_dom; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t) \<and> pas_refined aag s
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 3. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s\<rbrace>
 4. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> reads_respects aag l ?P'154 (gets cur_domain)
 2. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> \<lbrace>?P''154\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_dom)) s\<rbrace>
 3. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'154 s \<and> ?P''154 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; (pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> True \<and> (get_etcb tptr s \<noteq> None \<longrightarrow> (pas_refined aag and K (tcb_domain (the (get_etcb tptr s)) \<noteq> cur_domain s)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pas_cur_domain aag s; is_subject aag (cur_thread s); ekheap s tptr = Some y; tcb_domain y = cur_domain s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pas_cur_domain aag s; is_subject aag (cur_thread s); ekheap s tptr = Some y; tcb_domain y = cur_domain s; case (tptr, tcb_domain y) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag tptr \<notin> subjectReads (pasPolicy aag) l; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pas_cur_domain aag s; is_subject aag (cur_thread s); ekheap s tptr = Some y; tcb_domain y = cur_domain s; case (tptr, tcb_domain y) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> aag_can_read aag tptr proof (prove)
goal:
No subgoals!