theory Noninterference

lemma kernel_entry_scheduler_equiv_2:
  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'. snd 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'))
                       (kernel_entry_if Interrupt uc) (kernel_entry_if Interrupt uc')" apply (simp add: kernel_entry_if_def) apply (simp add: bind_assoc[symmetric]) apply (rule equiv_valid_2_bind_pre[where R'="(=)"]) apply (rule_tac P="\<top>" and P'="\<top>" in return_ev2) apply simp apply (rule equiv_valid_2_bind_pre[where R'="(=)"]) apply (rule equiv_valid_2) apply simp apply (wp del: no_irq add: handle_interrupt_reads_respects_scheduler[where st=st]
                                      dmo_getActive_IRQ_reads_respect_scheduler
                  | wpc
                  | simp add: imp_conjR all_conj_distrib  arch_tcb_update_aux2
                  | wp (once) hoare_drop_imps)+ apply (rule context_update_cur_thread_snippit) apply (wp thread_set_invs_trivial guarded_pas_domain_lift
                   thread_set_pas_refined thread_set_not_state_valid_sched
                | simp add: tcb_cap_cases_def arch_tcb_update_aux2)+ apply (fastforce simp: silc_inv_not_cur_thread cur_thread_idle)+ 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'. snd 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) (kernel_entry_if Interrupt 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'. snd 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) (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) (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 (1 subgoal):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. snd 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) (do r <- do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od;
return (r, uc)
od) (do r <- do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od;
return (r, uc')
od) proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. snd r = uc \<and> snd r' = uc') (?Q rv) (?Q' rv') (return (rv, uc)) (return (rv', uc'))
 2. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P ?P' (do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od) (do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od)
 3. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>?Q\<rbrace>
 4. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>?Q'\<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>rv = rv'; True; True; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> snd (rv, uc) = uc \<and> snd (rv', uc') = uc'
 2. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P ?P' (do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od) (do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od)
 3. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P ?P' (do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od) (do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od)
 2. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S s
 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (10 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (?Q9 rv) (?Q'9 rv') (liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)) (liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt))
 2. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P9 ?P'9 (gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>)) (gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
 3. \<lbrace>?S9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) \<lbrace>?Q9\<rbrace>
 4. \<lbrace>?S'9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) \<lbrace>?Q'9\<rbrace>
 5. \<And>s. ?P s \<Longrightarrow> ?P9 s \<and> ?S9 s
 6. \<And>s. ?P' s \<Longrightarrow> ?P'9 s \<and> ?S'9 s
 7. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (10 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q17 (liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt))
 2. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P9 ?P'9 (gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>)) (gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
 3. \<lbrace>?S9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv. ?Q17\<rbrace>
 4. \<lbrace>?S'9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv'. ?Q17\<rbrace>
 5. \<And>s. ?P s \<Longrightarrow> ?P9 s \<and> ?S9 s
 6. \<And>s. ?P' s \<Longrightarrow> ?P'9 s \<and> ?S'9 s
 7. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (10 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q17 (liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt))
 2. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P9 ?P'9 (gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>)) (gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
 3. \<lbrace>?S9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv. ?Q17\<rbrace>
 4. \<lbrace>?S'9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv'. ?Q17\<rbrace>
 5. \<And>s. ?P s \<Longrightarrow> ?P9 s \<and> ?S9 s
 6. \<And>s. ?P' s \<Longrightarrow> ?P'9 s \<and> ?S'9 s
 7. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (9 subgoals):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?P9 ?P'9 (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')))
 2. \<lbrace>?S9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv s. irq_masks_of_state ?st41 = irq_masks_of_state s \<and> True \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s \<and> True\<rbrace>
 3. \<lbrace>?S'9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv' s. irq_masks_of_state ?st41 = irq_masks_of_state s \<and> True \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s \<and> True\<rbrace>
 4. \<And>s. ?P s \<Longrightarrow> ?P9 s \<and> ?S9 s
 5. \<And>s. ?P' s \<Longrightarrow> ?P'9 s \<and> ?S'9 s
 6. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 7. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (8 subgoals):
 1. \<lbrace>?S9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv s. irq_masks_of_state ?st41 = irq_masks_of_state s \<and> True \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s \<and> True\<rbrace>
 2. \<lbrace>?S'9\<rbrace> gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>) \<lbrace>\<lambda>rv' s. irq_masks_of_state ?st41 = irq_masks_of_state s \<and> True \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> valid_sched s \<and> domain_sep_inv False st s \<and> True\<rbrace>
 3. \<And>s. ?P s \<Longrightarrow> (invs and silc_inv aag ?st88 and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<and> ?S9 s
 4. \<And>s. ?P' s \<Longrightarrow> (invs and silc_inv aag ?st88 and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<and> ?S'9 s
 5. \<lbrace>?S\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv _. True\<rbrace>
 6. \<lbrace>?S'\<rbrace> do y <- gets cur_thread >>= thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>);
liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
od \<lbrace>\<lambda>rv' _. True\<rbrace>
 7. \<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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P s \<and> ?S s
 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> pas_refined aag s \<and> guarded_pas_domain aag s \<and> domain_sep_inv False st s \<and> silc_inv aag st' s \<and> irq_masks_of_state st = irq_masks_of_state s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> (reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') \<Longrightarrow> silc_inv aag ?st88 s \<and> irq_masks_of_state ?st41 = irq_masks_of_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state 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. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')) s \<Longrightarrow> (invs s \<and> silc_inv aag ?st88 s \<and> guarded_pas_domain aag s \<and> (reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') \<and> (ct_idle s \<longrightarrow> uc' = idle_context s) \<and> irq_masks_of_state ?st41 = irq_masks_of_state s \<and> invs s \<and> guarded_pas_domain aag s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_sched s \<and> domain_sep_inv False st s) \<and> True proof (prove)
goal:
No subgoals!