theory Noninterference

lemma preemption_interrupt_scheduler_invisible:
  assumes domains_distinct[wp]: "pas_domains_distinct (aag :: 'a subject_label PAS)"
  shows "equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l)
                       (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc')
                       (einvs and pas_refined aag and guarded_pas_domain aag
                              and domain_sep_inv False st and silc_inv aag st'
                              and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)
                              and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)
                              and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s))
                       (einvs and pas_refined aag and guarded_pas_domain aag
                              and domain_sep_inv False st and silc_inv aag st'
                              and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)
                              and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)
                              and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s))
                       (handle_preemption_if uc) (kernel_entry_if Interrupt uc')" apply (simp add: kernel_entry_if_def handle_preemption_if_def getActiveIRQ_no_non_kernel_IRQs) apply (rule equiv_valid_2_bind_right) apply (rule equiv_valid_2_bind_right) apply (simp add: liftE_def bind_assoc) apply (simp only: option.case_eq_if) apply (rule equiv_valid_2_bind_pre[where R'="(=)"]) apply (simp add: when_def split del: if_split) apply (subst if_swap) apply (simp split del: if_split) apply (rule equiv_valid_2_bind_pre[where R'="(=)" and Q="\<top>\<top>" and Q'="\<top>\<top>"]) apply (rule return_ev2) apply simp apply (rule equiv_valid_2) apply (wp handle_interrupt_reads_respects_scheduler[where st=st] | simp)+ apply (rule equiv_valid_2) apply (rule dmo_getActive_IRQ_reads_respect_scheduler) apply (wp dmo_getActiveIRQ_return_axiom[simplified try_some_magic]
                      | simp  add: imp_conjR arch_tcb_update_aux2
                      | elim conjE
                      | intro conjI
                      | wp (once) hoare_drop_imps)+ apply (subst thread_set_as_user2) apply (wp guarded_pas_domain_lift) apply ((simp add:  arch_tcb_update_aux2 | wp | force)+)[7] apply (fastforce simp: silc_inv_not_cur_thread cur_thread_idle guarded_pas_domain_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) (handle_preemption_if uc) (kernel_entry_if Interrupt uc') proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) (do irq <- do_machine_op (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return uc
od) (do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) t;
r <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
return (r, uc')
od) proof (prove)
goal (6 subgoals):
 1. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) (?Q1 rv) (do irq <- do_machine_op (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return uc
od) (do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv;
r <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
return (r, uc')
od)
 2. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 3. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 4. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
 6. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s proof (prove)
goal (11 subgoals):
 1. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) (?Q8 rv rva) (do irq <- do_machine_op (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return uc
od) (do r <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
return (r, uc')
od)
 2. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 3. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 4. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
 6. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 7. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 8. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) (?Q8 rv ()) (do irq <- do_machine_op (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return uc
od) (do x <- do_machine_op (getActiveIRQ False);
r <- case x of None \<Rightarrow> return () | Some x \<Rightarrow> handle_interrupt x;
return (Inr (), uc')
od)
 2. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 3. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 4. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
 6. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 7. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 8. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) (?Q8 rv ()) (do irq <- do_machine_op (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return uc
od) (do x <- do_machine_op (getActiveIRQ False);
r <- if x = None then return () else handle_interrupt (the x);
return (Inr (), uc')
od)
 2. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 3. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 4. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 5. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
 6. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 7. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 8. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
A total of 11 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rv'. rva = rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (?Q15 rv rva) (?Q'15 rv rv') (do y <- when (\<exists>y. rva = Some y) (handle_interrupt (the rva));
return uc
od) (do r <- if rv' = None then return () else handle_interrupt (the rv');
return (Inr (), uc')
od)
 2. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 3. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>?Q15 rv\<rbrace>
 4. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>?Q'15 rv\<rbrace>
 5. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 6. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
 7. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 8. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (?Q15 rv rva) (?Q'15 rv rva) (do y <- if \<exists>y. rva = Some y then handle_interrupt (the rva) else return ();
return uc
od) (do r <- if rva = None then return () else handle_interrupt (the rva);
return (Inr (), uc')
od)
 2. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 3. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>?Q15 rv\<rbrace>
 4. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>?Q'15 rv\<rbrace>
 5. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 6. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
 7. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 8. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (?Q23 rv rva (?rv23 rv rva) rva) (?Q'23 rv rva (?rv23 rv rva) rva) (do y <- if \<nexists>y. rva = Some y then return () else handle_interrupt (the rva);
return uc
od) (do r <- if rva = None then return () else handle_interrupt (the rva);
return (Inr (), uc')
od)
 2. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 3. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q23 rv rva (?rv23 rv rva) rva\<rbrace>
 4. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q'23 rv rva (?rv23 rv rva) rva\<rbrace>
 5. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 6. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
 7. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 8. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (?Q23 rv rva (?rv23 rv rva) rva) (?Q'23 rv rva (?rv23 rv rva) rva) (do y <- if rva = None then return () else handle_interrupt (the rva);
return uc
od) (do r <- if rva = None then return () else handle_interrupt (the rva);
return (Inr (), uc')
od)
 2. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 3. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q23 rv rva (?rv23 rv rva) rva\<rbrace>
 4. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q'23 rv rva (?rv23 rv rva) rva\<rbrace>
 5. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 6. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
 7. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 8. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 9. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 10. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
A total of 16 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rva rvb rv'. rvb = rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc') (\<lambda>_. True) (\<lambda>_. True) (return uc) (return (Inr (), uc'))
 2. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P26 rv rva) (?P'26 rv rva) (if rva = None then return () else handle_interrupt (the rva)) (if rva = None then return () else handle_interrupt (the rva))
 3. \<And>rv rva. \<lbrace>?S26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rva. \<lbrace>?S'26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rva s. ?Q23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P26 rv rva s \<and> ?S26 rv rva s
 6. \<And>rv rva s. ?Q'23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P'26 rv rva s \<and> ?S'26 rv rva s
 7. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 8. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q23 rv rva (?rv23 rv rva) rva\<rbrace>
 9. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q'23 rv rva (?rv23 rv rva) rva\<rbrace>
 10. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>rv rva rvb rv' s t. \<lbrakk>rvb = rv'; True; True; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> uc = uc \<and> snd (Inr (), uc') = uc'
 2. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P26 rv rva) (?P'26 rv rva) (if rva = None then return () else handle_interrupt (the rva)) (if rva = None then return () else handle_interrupt (the rva))
 3. \<And>rv rva. \<lbrace>?S26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rva. \<lbrace>?S'26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rva s. ?Q23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P26 rv rva s \<and> ?S26 rv rva s
 6. \<And>rv rva s. ?Q'23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P'26 rv rva s \<and> ?S'26 rv rva s
 7. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 8. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q23 rv rva (?rv23 rv rva) rva\<rbrace>
 9. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q'23 rv rva (?rv23 rv rva) rva\<rbrace>
 10. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
A total of 21 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rva. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P26 rv rva) (?P'26 rv rva) (if rva = None then return () else handle_interrupt (the rva)) (if rva = None then return () else handle_interrupt (the rva))
 2. \<And>rv rva. \<lbrace>?S26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv rva. \<lbrace>?S'26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rva s. ?Q23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P26 rv rva s \<and> ?S26 rv rva s
 5. \<And>rv rva s. ?Q'23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P'26 rv rva s \<and> ?S'26 rv rva s
 6. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 7. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q23 rv rva (?rv23 rv rva) rva\<rbrace>
 8. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q'23 rv rva (?rv23 rv rva) rva\<rbrace>
 9. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 10. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P26 rv rva) (if rva = None then return () else handle_interrupt (the rva))
 2. \<And>rv rva. \<lbrace>?S26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv rva. \<lbrace>?S'26 rv rva\<rbrace> if rva = None then return () else handle_interrupt (the rva) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rva s. ?Q23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P26 rv rva s \<and> ?S26 rv rva s
 5. \<And>rv rva s. ?Q'23 rv rva (?rv23 rv rva) rva s \<Longrightarrow> ?P26 rv rva s \<and> ?S'26 rv rva s
 6. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 7. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q23 rv rva (?rv23 rv rva) rva\<rbrace>
 8. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva. ?Q'23 rv rva (?rv23 rv rva) rva\<rbrace>
 9. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 10. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
A total of 20 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?P15 rv) (?P'15 rv) (do_machine_op (getActiveIRQ False)) (do_machine_op (getActiveIRQ False))
 2. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva a. (\<exists>y. rva = Some y) \<longrightarrow> invs a \<and> guarded_pas_domain aag a \<and> pas_refined aag a \<and> valid_sched a \<and> domain_sep_inv False st a \<and> the rva \<le> maxIRQ\<rbrace>
 3. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva a. (\<exists>y. rva = Some y) \<longrightarrow> invs a \<and> guarded_pas_domain aag a \<and> pas_refined aag a \<and> valid_sched a \<and> domain_sep_inv False st a \<and> the rva \<le> maxIRQ\<rbrace>
 4. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 5. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P'15 rv s \<and> ?S'15 rv s
 6. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 7. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 8. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
 10. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P15 rv) (do_machine_op (getActiveIRQ False))
 2. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva a. (\<exists>y. rva = Some y) \<longrightarrow> invs a \<and> guarded_pas_domain aag a \<and> pas_refined aag a \<and> valid_sched a \<and> domain_sep_inv False st a \<and> the rva \<le> maxIRQ\<rbrace>
 3. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva a. (\<exists>y. rva = Some y) \<longrightarrow> invs a \<and> guarded_pas_domain aag a \<and> pas_refined aag a \<and> valid_sched a \<and> domain_sep_inv False st a \<and> the rva \<le> maxIRQ\<rbrace>
 4. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P15 rv s \<and> ?S15 rv s
 5. \<And>rv s. ?Q8 rv () s \<Longrightarrow> ?P15 rv s \<and> ?S'15 rv s
 6. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 7. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 8. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
 10. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv. \<lbrace>?S15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva a. (\<exists>y. rva = Some y) \<longrightarrow> invs a \<and> guarded_pas_domain aag a \<and> pas_refined aag a \<and> valid_sched a \<and> domain_sep_inv False st a \<and> the rva \<le> maxIRQ\<rbrace>
 2. \<And>rv. \<lbrace>?S'15 rv\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rva a. (\<exists>y. rva = Some y) \<longrightarrow> invs a \<and> guarded_pas_domain aag a \<and> pas_refined aag a \<and> valid_sched a \<and> domain_sep_inv False st a \<and> the rva \<le> maxIRQ\<rbrace>
 3. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> irq_masks_of_state (?st50 rv) = irq_masks_of_state s \<and> ?S15 rv s
 4. \<And>rv s. ?Q8 rv () s \<Longrightarrow> irq_masks_of_state (?st50 rv) = irq_masks_of_state s \<and> ?S'15 rv s
 5. \<And>rv. \<lbrace>?S8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>?Q8 rv\<rbrace>
 6. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 7. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 8. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> ?S8 rv s \<and> ?S'8 rv s \<and> ?S''8 rv s
 9. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 10. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
A total of 14 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv. \<lbrace>?P'137 rv\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set uc')) rv \<lbrace>\<lambda>rv s. invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s\<rbrace>
 2. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 3. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> (irq_masks_of_state st = irq_masks_of_state s \<and> ?P'137 rv s) \<and> ?S'8 rv s \<and> ?S''8 rv s
 5. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 6. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 7. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 8. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
 10. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s proof (prove)
goal (10 subgoals):
 1. \<And>rv. \<lbrace>?P'141 rv rv\<rbrace> as_user rv (modify (\<lambda>_. uc')) \<lbrace>\<lambda>rv s. invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s\<rbrace>
 2. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 3. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> (irq_masks_of_state st = irq_masks_of_state s \<and> ?P'141 rv rv s) \<and> ?S'8 rv s \<and> ?S''8 rv s
 5. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 6. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 7. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 8. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
 10. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s proof (prove)
goal (9 subgoals):
 1. \<And>rv st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 2. \<And>rv st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''8 rv\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) rv \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>rv s. ?Q1 rv s \<Longrightarrow> ?P8 rv s \<and> (irq_masks_of_state st = irq_masks_of_state s \<and> invs s \<and> guarded_pas_domain aag s \<and> (pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag) s \<and> valid_sched s \<and> domain_sep_inv False st s) \<and> ?S'8 rv s \<and> ?S''8 rv s
 4. \<And>rv s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P8 rv s
 5. \<lbrace>?S1\<rbrace> gets cur_thread \<lbrace>?Q1\<rbrace>
 6. \<And>st. \<lbrace>scheduler_equiv aag st and scheduler_affects_equiv aag l st and ?S'1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>
 7. \<And>st. \<lbrace>scheduler_affects_equiv aag l st and scheduler_equiv aag st and ?S''1\<rbrace> gets cur_thread \<lbrace>\<lambda>r. scheduler_affects_equiv aag l st\<rbrace>
 8. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> ?S1 s \<and> ?S'1 s \<and> ?S''1 s
 9. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s \<and> (irq_masks_of_state st = irq_masks_of_state s \<and> invs s \<and> guarded_pas_domain aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s \<and> invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s) \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s)) \<and> ?S'1 s \<and> ?S''1 s
 2. \<And>s. (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s) and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s \<Longrightarrow> ?P1 s proof (prove)
goal:
No subgoals!