theory Scheduler_IF

lemma handle_interrupt_reads_respects_scheduler:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_scheduler aag l (invs and guarded_pas_domain aag and pas_refined aag and
                                     valid_sched and domain_sep_inv False st and K (irq \<le> maxIRQ))
                              (handle_interrupt irq)" apply (simp add: handle_interrupt_def ) apply (rule conjI; rule impI ) apply (rule gen_asm_ev) apply simp apply (wp modify_wp | simp )+ apply (rule ackInterrupt_reads_respects_scheduler) apply (rule_tac Q="rv = IRQTimer \<or> rv = IRQInactive" in gen_asm_ev(2)) apply (elim disjE) apply (wpsimp wp: timer_tick_reads_respects_scheduler ackInterrupt_reads_respects_scheduler
                         get_irq_state_reads_respects_scheduler_trivial irq_inactive_or_timer
                         dmo_resetTimer_reads_respects_scheduler fail_ev)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and K (irq \<le> maxIRQ)) (handle_interrupt irq) proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od))) \<and> (\<not> maxIRQ < irq \<longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) (do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od)) proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od))
 2. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) (do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>maxIRQ < irq; irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od))
 2. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) (do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) proof (prove)
goal (1 subgoal):
 1. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) (do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) proof (prove)
goal (6 subgoals):
 1. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q22 rv ()) (do_machine_op (ackInterrupt irq))
 2. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'22 rv) (case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq)
 3. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''22 rv\<rbrace> case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq \<lbrace>?Q22 rv\<rbrace>
 4. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'21 (get_irq_state irq)
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''21\<rbrace> get_irq_state irq \<lbrace>\<lambda>rv s. ?P'22 rv s \<and> ?P''22 rv s\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) s\<rbrakk> \<Longrightarrow> ?P'21 s \<and> ?P''21 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'22 rv) (case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq)
 2. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''22 rv\<rbrace> case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'21 (get_irq_state irq)
 4. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''21\<rbrace> get_irq_state irq \<lbrace>\<lambda>rv s. ?P'22 rv s \<and> ?P''22 rv s\<rbrace>
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) s\<rbrakk> \<Longrightarrow> ?P'21 s \<and> ?P''21 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>\<not> maxIRQ < irq; rv = IRQTimer \<or> rv = IRQInactive\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P24 rv) (case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq)
 2. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''22 rv\<rbrace> case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'21 (get_irq_state irq)
 4. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''21\<rbrace> get_irq_state irq \<lbrace>\<lambda>rv s. (?P24 rv and K (rv = IRQTimer \<or> rv = IRQInactive)) s \<and> ?P''22 rv s\<rbrace>
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) s\<rbrakk> \<Longrightarrow> ?P'21 s \<and> ?P''21 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. \<lbrakk>\<not> maxIRQ < irq; rv = IRQTimer\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P24 rv) (case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq)
 2. \<And>rv. \<lbrakk>\<not> maxIRQ < irq; rv = IRQInactive\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P24 rv) (case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq)
 3. \<And>rv. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''22 rv\<rbrace> case rv of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<not> maxIRQ < irq \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'21 (get_irq_state irq)
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?P''21\<rbrace> get_irq_state irq \<lbrace>\<lambda>rv s. (?P24 rv and K (rv = IRQTimer \<or> rv = IRQInactive)) s \<and> ?P''22 rv s\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and (\<lambda>y. irq \<le> maxIRQ)) s\<rbrakk> \<Longrightarrow> ?P'21 s \<and> ?P''21 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s; guarded_pas_domain aag s; pas_refined aag s; valid_sched s; domain_sep_inv False st s; irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> domain_sep_inv False ?st340 s \<and> domain_sep_inv False ?st343 s proof (prove)
goal:
No subgoals!