theory ArchIRQMasks_IF

lemma handle_interrupt_irq_masks[IRQMasks_IF_assms]:
  notes no_irq[wp del]
  shows
    "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and K (irq \<le> maxIRQ)\<rbrace>
     handle_interrupt irq
     \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: handle_interrupt_def split del: if_split) apply (rule hoare_pre) apply (rule hoare_if) apply simp apply (wp dmo_wp
          | simp add: ackInterrupt_def maskInterrupt_def when_def split del: if_split
          | wpc
          | simp add: get_irq_state_def handle_reserved_irq_def
          | wp (once) hoare_drop_imp)+ apply (fastforce simp: domain_sep_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and K (irq \<le> maxIRQ)\<rbrace> handle_interrupt irq \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq \<le> maxIRQ \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> handle_interrupt irq \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq \<le> maxIRQ \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> if maxIRQ < irq then do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) else 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 \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. irq \<le> maxIRQ \<Longrightarrow> \<lbrace>?Q4\<rbrace> if maxIRQ < irq then do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) else 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 \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>s. \<lbrakk>irq \<le> maxIRQ; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>irq \<le> maxIRQ; maxIRQ < irq\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>
 2. \<lbrakk>irq \<le> maxIRQ; \<not> maxIRQ < irq\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> 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 \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>s. \<lbrakk>irq \<le> maxIRQ; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>irq \<le> maxIRQ; \<not> maxIRQ < irq\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> 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 \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>s. \<lbrakk>irq \<le> maxIRQ; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>irq \<le> maxIRQ; P (irq_masks_of_state s) \<and> domain_sep_inv False st s\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal \<longrightarrow> P (\<lambda>x. x \<noteq> irq \<longrightarrow> irq_masks_of_state s x) proof (prove)
goal:
No subgoals!