theory ArchInterrupt_AI

lemma invoke_irq_handler_invs'[Interrupt_AI_asms]:
  assumes dmo_ex_inv[wp]: "\<And>f. \<lbrace>invs and ex_inv\<rbrace> do_machine_op f \<lbrace>\<lambda>rv::unit. ex_inv\<rbrace>"
  assumes cap_insert_ex_inv[wp]: "\<And>cap src dest.
  \<lbrace>ex_inv and invs and K (src \<noteq> dest)\<rbrace>
      cap_insert cap src dest
  \<lbrace>\<lambda>_.ex_inv\<rbrace>"
  assumes cap_delete_one_ex_inv[wp]: "\<And>cap.
   \<lbrace>ex_inv and invs\<rbrace> cap_delete_one cap \<lbrace>\<lambda>_.ex_inv\<rbrace>"
 shows
  "\<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>" proof - have
   cap_insert_invs_ex_invs[wp]: "\<And>cap src dest. \<lbrace>ex_inv and (invs  and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and
   tcb_cap_valid cap dest and
   ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and
   (\<lambda>s. \<forall>r\<in>obj_refs cap.
           \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow>
                cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) and
   (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and
   (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s)
         src s) and
   (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow>
            st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and
   K (\<not> is_master_reply_cap cap))\<rbrace>
  cap_insert cap src dest \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>" apply wp apply (auto simp: cte_wp_at_caps_of_state) done show ?thesis apply (cases i, simp_all) apply (wp maskInterrupt_invs_ARCH) apply simp apply (rename_tac irq cap prod) apply (rule hoare_pre) apply (wp valid_cap_typ [OF cap_delete_one_typ_at]) apply (strengthen real_cte_tcb_valid) apply (wp real_cte_at_typ_valid [OF cap_delete_one_typ_at]) apply (rule_tac Q="\<lambda>rv s. is_ntfn_cap cap \<and> invs s
                              \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s"
                in hoare_post_imp) apply (clarsimp simp: is_cap_simps is_derived_def cte_wp_at_caps_of_state) apply (simp split: if_split_asm) apply (simp add: cap_master_cap_def split: cap.split_asm) apply (drule cte_wp_valid_cap [OF caps_of_state_cteD] | clarsimp)+ apply (clarsimp simp: cap_master_cap_simps valid_cap_def obj_at_def is_ntfn is_tcb is_cap_table
                     split: option.split_asm dest!:cap_master_cap_eqDs) apply (wp cap_delete_one_still_derived) apply simp apply (wp get_irq_slot_ex_cte get_irq_slot_different_ARCH hoare_drop_imps) apply (clarsimp simp: valid_state_def invs_def appropriate_cte_cap_def
                            is_cap_simps) apply (erule cte_wp_at_weakenE, simp add: is_derived_use_interrupt_ARCH) apply (wp| simp add: )+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap src dest. \<lbrace>ex_inv and (invs and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap cap))\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap src dest s. (ex_inv and (invs and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap cap))) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and tcb_cap_valid cap dest and ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and (\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap cap)) s \<and> (ex_inv and invs and K (src \<noteq> dest)) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ex_inv and (invs and cte_wp_at (\<lambda>c. c = NullCap) ?dest and valid_cap ?cap and tcb_cap_valid ?cap ?dest and ex_cte_cap_wp_to (appropriate_cte_cap ?cap) ?dest and (\<lambda>s. \<forall>r\<in>obj_refs ?cap. \<forall>p'. ?dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie ?cap) and (\<lambda>s. cte_wp_at (is_derived (cdt s) ?src ?cap) ?src s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs ?cap - cap_irqs cap'. irq_issued irq s) ?src s) and (\<lambda>s. \<forall>t R. ?cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap ?cap))\<rbrace> cap_insert ?cap ?src ?dest \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. i = ACKIrq x1 \<Longrightarrow> \<lbrace>invs and ex_inv and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive)\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>
 2. \<And>x21 x22 x23. i = SetIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)\<rbrace> do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>
 3. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1 s. \<lbrakk>i = ACKIrq x1; (invs and ex_inv and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive)) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. \<not> False \<longrightarrow> interrupt_states s x1 \<noteq> IRQInactive)) s \<and> (invs and ex_inv) s
 2. \<And>x21 x22 x23. i = SetIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)\<rbrace> do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>
 3. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23. i = SetIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)\<rbrace> do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>
 2. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)\<rbrace> do irq_slot <- get_irq_slot irq;
y <- cap_delete_one irq_slot;
cap_insert cap prod irq_slot
od \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>
 2. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> do irq_slot <- get_irq_slot irq;
y <- cap_delete_one irq_slot;
cap_insert cap prod irq_slot
od \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>
 2. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 3. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'31 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. tcb_cap_valid cap irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. irq_slot \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) prod s \<and> (\<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> K (\<not> is_master_reply_cap cap) s\<rbrace>
 2. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> ?P'31 irq cap prod irq_slot s\<rbrace>
 3. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 4. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'31 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>r s. real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. irq_slot \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) prod s \<and> (\<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> K (\<not> is_master_reply_cap cap) s\<rbrace>
 2. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> ?P'31 irq cap prod irq_slot s\<rbrace>
 3. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 4. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. (\<forall>r\<in>obj_refs cap. \<forall>p'. irq_slot \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) prod s \<and> (\<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> K (\<not> is_master_reply_cap cap) s\<rbrace>
 2. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 3. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 4. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>irq cap prod irq_slot rv s. \<lbrakk>i = SetIRQHandler irq cap prod; is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs cap. \<forall>p'. irq_slot \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) prod s \<and> (\<forall>t R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> K (\<not> is_master_reply_cap cap) s
 2. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrace>
 3. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 4. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 5. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>irq a b aa ba s bb R capa ab bc ra bd n. \<lbrakk>i = SetIRQHandler irq (NotificationCap ra bb R) (a, b); invs s; caps_of_state s (a, b) = Some capa; \<forall>r b n. capa \<noteq> Zombie r b n; if \<exists>dev r bits f. capa = UntypedCap dev r bits f then cap_master_cap capa = cap_master_cap (NotificationCap ra bb R) \<and> descendants_of (a, b) (cdt s) = {} else cap_master_cap capa = cap_master_cap (NotificationCap ra bb R) \<and> (cap_badge capa, Some bb) \<in> capBadge_ordering False; \<forall>x R. capa \<noteq> ReplyCap x True R; vs_cap_ref (NotificationCap ra bb R) = vs_cap_ref capa \<or> (\<exists>dev p R sz m. capa = ArchObjectCap (PageCap dev p R sz m)); \<forall>x R. capa \<noteq> ReplyCap x False R; aa = ab \<longrightarrow> ba \<noteq> bc; caps_of_state s (ab, bc) = Some (Zombie ra bd n)\<rbrakk> \<Longrightarrow> False
 2. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrace>
 3. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 4. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 5. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>irq a b aa ba s bb R capa ab bc ra bd n dev r bits f. \<lbrakk>vs_cap_ref (NotificationCap ra bb R) = vs_cap_ref (UntypedCap dev r bits f); aa = ab \<longrightarrow> ba \<noteq> bc; caps_of_state s (ab, bc) = Some (Zombie ra bd n); i = SetIRQHandler irq (NotificationCap ra bb R) (a, b); invs s; caps_of_state s (a, b) = Some (UntypedCap dev r bits f); capa = UntypedCap dev r bits f; cap_master_cap (UntypedCap dev r bits f) = cap_master_cap (NotificationCap ra bb R) \<and> descendants_of (a, b) (cdt s) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>irq a b aa ba s bb R capa ab bc ra bd n. \<lbrakk>\<forall>x R. capa \<noteq> ReplyCap x True R; vs_cap_ref (NotificationCap ra bb R) = vs_cap_ref capa \<or> (\<exists>dev p R sz m. capa = ArchObjectCap (PageCap dev p R sz m)); \<forall>x R. capa \<noteq> ReplyCap x False R; aa = ab \<longrightarrow> ba \<noteq> bc; caps_of_state s (ab, bc) = Some (Zombie ra bd n); i = SetIRQHandler irq (NotificationCap ra bb R) (a, b); invs s; caps_of_state s (a, b) = Some capa; \<forall>r b n. capa \<noteq> Zombie r b n; \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; cap_master_cap capa = cap_master_cap (NotificationCap ra bb R) \<and> (cap_badge capa, Some bb) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> False
 3. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrace>
 4. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 5. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 6. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>irq a b aa ba s bb R capa ab bc ra bd n. \<lbrakk>\<forall>x R. capa \<noteq> ReplyCap x True R; vs_cap_ref (NotificationCap ra bb R) = vs_cap_ref capa \<or> (\<exists>dev p R sz m. capa = ArchObjectCap (PageCap dev p R sz m)); \<forall>x R. capa \<noteq> ReplyCap x False R; aa = ab \<longrightarrow> ba \<noteq> bc; caps_of_state s (ab, bc) = Some (Zombie ra bd n); i = SetIRQHandler irq (NotificationCap ra bb R) (a, b); invs s; caps_of_state s (a, b) = Some capa; \<forall>r b n. capa \<noteq> Zombie r b n; \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; cap_master_cap capa = cap_master_cap (NotificationCap ra bb R) \<and> (cap_badge capa, Some bb) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> False
 2. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrace>
 3. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 4. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 5. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>irq a b aa ba s bb R capa ab bc ra bd n. \<lbrakk>\<forall>x R. capa \<noteq> ReplyCap x True R; vs_cap_ref (NotificationCap ra bb R) = vs_cap_ref capa \<or> (\<exists>dev p R sz m. capa = ArchObjectCap (PageCap dev p R sz m)); \<forall>x R. capa \<noteq> ReplyCap x False R; aa = ab \<longrightarrow> ba \<noteq> bc; i = SetIRQHandler irq (NotificationCap ra bb R) (a, b); invs s; \<forall>r b n. capa \<noteq> Zombie r b n; \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; s \<turnstile> Zombie ra bd n; s \<turnstile> capa; cap_master_cap capa = cap_master_cap (NotificationCap ra bb R); (cap_badge capa, Some bb) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> False
 2. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrace>
 3. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 4. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 5. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irq cap prod irq_slot. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?P'51 irq cap prod irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. is_ntfn_cap cap \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s\<rbrace>
 2. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> ?P'51 irq cap prod irq_slot s\<rbrace>
 3. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 4. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. (ex_inv and invs) s \<and> (invs and emptyable irq_slot) s \<and> True \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> is_ntfn_cap cap \<and> (invs and emptyable irq_slot) s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> irq_slot \<noteq> prod \<and> valid_mdb s\<rbrace>
 2. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 3. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irq cap prod. i = SetIRQHandler irq cap prod \<Longrightarrow> \<lbrace>?Q8 irq cap prod\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot s. ex_inv s \<and> invs s \<and> emptyable irq_slot s \<and> s \<turnstile> cap \<and> real_cte_at irq_slot s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) irq_slot s \<and> is_ntfn_cap cap \<and> invs s \<and> emptyable irq_slot s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> irq_slot \<noteq> prod \<and> valid_mdb s\<rbrace>
 2. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ?Q8 irq cap prod s
 3. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>irq cap prod s. \<lbrakk>i = SetIRQHandler irq cap prod; (invs and ex_inv and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap prod s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) prod s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap)) s\<rbrakk> \<Longrightarrow> ex_inv s \<and> invs s \<and> invs s \<and> s \<turnstile> cap \<and> invs s \<and> (\<exists>ptr. cte_wp_at ((=) (IRQHandlerCap irq)) ptr s \<and> appropriate_cte_cap cap (IRQHandlerCap irq)) \<and> is_ntfn_cap cap \<and> invs s \<and> invs s \<and> cte_wp_at (is_derived (cdt s) prod cap) prod s \<and> (valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap prod s) \<and> valid_mdb s
 2. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>irq a b s aa ba r bb R. \<lbrakk>i = SetIRQHandler irq (NotificationCap r bb R) (a, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_inv s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; cte_wp_at (interrupt_derived (NotificationCap r bb R)) (a, b) s; s \<turnstile> NotificationCap r bb R\<rbrakk> \<Longrightarrow> cte_wp_at (is_derived (cdt s) (a, b) (NotificationCap r bb R)) (a, b) s
 2. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>invs and ex_inv\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>

goal:
No subgoals!