theory Interrupt_DR

lemma dcorres_invoke_irq_handler:
  "dcorres dc \<top> (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs)
          (Interrupt_D.invoke_irq_handler
            (translate_irq_handler_invocation irq_handler_invocation))
          (Interrupt_A.invoke_irq_handler irq_handler_invocation)" apply (case_tac irq_handler_invocation) 
(* ACKIrq *)
     apply (clarsimp simp:Interrupt_D.invoke_irq_handler_def) apply (rule corres_dummy_return_r) apply (rule dcorres_symb_exec_r_strong) apply (rule corres_free_return[where P'=\<top> ]) apply wp apply (wp do_machine_op_wp,clarsimp) apply (wp maskInterrupt_underlying_memory|clarsimp simp:Interrupt_D.invoke_irq_handler_def)+ 
   (* SetIRQHandler *)
    apply (rule dcorres_expand_pfx) apply (clarsimp dest!:is_ntfn_capD simp:valid_cap_def) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_get_irq_slot]) apply (rule_tac F="irq_slot\<noteq> (a,b)" in corres_gen_asm2) apply simp apply (rule corres_split[OF delete_cap_simple_corres]) apply (subst alternative_com) apply (rule dcorres_insert_cap_combine,simp) apply wp apply (wp delete_one_deletes[unfolded op_eq_simp[symmetric]]) apply (wp cte_wp_at_neq_slot_cap_delete_one) apply simp apply (wp cte_wp_at_neq_slot_cap_delete_one) apply (strengthen invs_valid_idle invs_valid_objs) apply (wp delete_one_invs) apply (simp add:valid_cap_def) apply (wp get_irq_slot_not_idle_wp get_irq_slot_ex_cte_cap_wp_to) apply (wp get_irq_slot_different get_irq_slot_not_idle_wp) apply simp+ apply (clarsimp simp:invs_valid_idle interrupt_derived_def) apply (frule_tac p = "(a,b)" in if_unsafe_then_capD) apply clarsimp+ apply (clarsimp simp: cte_wp_at_caps_of_state invs_valid_global_refs is_cap_simps
                          cap_master_cap_simps interrupt_derived_def dest!:cap_master_cap_eqDs)+ apply (drule ex_cte_cap_wp_to_not_idle) apply clarsimp+ 
  (* ClearIRQHandler *)
   apply (clarsimp simp: Interrupt_D.invoke_irq_handler_def) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_get_irq_slot]) apply (clarsimp) apply (rule delete_cap_simple_corres) apply (wp get_irq_slot_not_idle_wp,clarsimp)+ apply (clarsimp simp:invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 2. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 2. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs) (return ()) (do_machine_op (maskInterrupt False x1))
 2. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs) (return ()) (do_machine_op (maskInterrupt False x1) >>= return)
 2. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (5 subgoals):
 1. \<And>x1 rv. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'5 x1 rv) (return ()) (return rv)
 2. \<And>x1. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>?Q'5 x1\<rbrace>
 3. \<And>x1 cs. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> \<lbrace>\<lambda>ps. (invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 5. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (4 subgoals):
 1. \<And>x1. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x1 cs. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> \<lbrace>\<lambda>ps. (invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 4. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x1 cs. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> \<lbrace>\<lambda>ps. (invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (4 subgoals):
 1. \<And>x1 m. irq_handler_invocation = ACKIrq x1 \<Longrightarrow> \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt False x1 \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>x1 cs s. \<lbrakk>irq_handler_invocation = ACKIrq x1; (invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive) and valid_etcbs) s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 3. \<And>x21 x22 x23. irq_handler_invocation = SetIRQHandler x21 x22 x23 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
 4. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b. irq_handler_invocation = SetIRQHandler x21 x22 (a, b) \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) (a, b) s \<and> s \<turnstile> x22 \<and> Structures_A.is_ntfn_cap x22) and valid_etcbs) (do irqslot <- gets (CSpace_D.get_irq_slot x21);
y <- delete_cap_simple irqslot;
insert_cap_child (transform_cap x22) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (transform_cap x22) (transform_cslot_ptr (a, b)) irqslot
od) (do irq_slot <- KHeap_A.get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 (a, b) irq_slot
od)
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b. irq_handler_invocation = SetIRQHandler x21 x22 (a, b) \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) (a, b) s \<and> s \<turnstile> x22 \<and> Structures_A.is_ntfn_cap x22) and valid_etcbs) (do irqslot <- gets (CSpace_D.get_irq_slot x21);
y <- delete_cap_simple irqslot;
insert_cap_child (transform_cap x22) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (transform_cap x22) (transform_cslot_ptr (a, b)) irqslot
od) (do irq_slot <- KHeap_A.get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 (a, b) irq_slot
od)
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s s'. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 x22 (a, b); s = transform s'; True; (invs and (\<lambda>s. ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) (a, b) s \<and> s \<turnstile> x22 \<and> Structures_A.is_ntfn_cap x22) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do irqslot <- gets (CSpace_D.get_irq_slot x21);
y <- delete_cap_simple irqslot;
insert_cap_child (transform_cap x22) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (transform_cap x22) (transform_cslot_ptr (a, b)) irqslot
od) (do irq_slot <- KHeap_A.get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 (a, b) irq_slot
od)
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do irqslot <- gets (CSpace_D.get_irq_slot x21);
y <- delete_cap_simple irqslot;
insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot
od) (do irq_slot <- KHeap_A.get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot
od)
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (4 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> dcorres dc (?Q48 x21 a b s' aa ba ptr bb rights) (?Q'48 x21 a b s' aa ba ptr bb rights) (do irqslot <- gets (CSpace_D.get_irq_slot x21);
y <- delete_cap_simple irqslot;
insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot
od) (do irq_slot <- KHeap_A.get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot
od)
 2. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ?Q48 x21 a b s' aa ba ptr bb rights s
 3. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ?Q'48 x21 a b s' aa ba ptr bb rights s
 4. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot\<rbrakk> \<Longrightarrow> dcorres dc (?R52 x21 a b s' aa ba ptr bb rights irqslot) (?R'52 x21 a b s' aa ba ptr bb rights irq_slot) (do y <- delete_cap_simple irqslot;
insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot
od) (do y <- cap_delete_one irq_slot;
cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot
od)
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>?R52 x21 a b s' aa ba ptr bb rights\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>?R'52 x21 a b s' aa ba ptr bb rights\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> dcorres dc (?R52 x21 a b s' aa ba ptr bb rights irqslot) (?P'58 x21 a b s' aa ba ptr bb rights irq_slot) (do y <- delete_cap_simple irqslot;
insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot \<sqinter> insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) irqslot
od) (do y <- cap_delete_one irq_slot;
cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot
od)
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>?R52 x21 a b s' aa ba ptr bb rights\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. ?P'58 x21 a b s' aa ba ptr bb rights irq_slot and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> dcorres dc (?R52 x21 a b s' aa ba ptr bb rights (transform_cslot_ptr irq_slot)) (?P'58 x21 a b s' aa ba ptr bb rights irq_slot) (do y <- delete_cap_simple (transform_cslot_ptr irq_slot);
insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) (transform_cslot_ptr irq_slot) \<sqinter> insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) (transform_cslot_ptr irq_slot)
od) (do y <- cap_delete_one irq_slot;
cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot
od)
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>?R52 x21 a b s' aa ba ptr bb rights\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. ?P'58 x21 a b s' aa ba ptr bb rights irq_slot and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (8 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b); dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R59 x21 a b s' aa ba ptr bb rights irqslot irq_slot y) (?R'59 x21 a b s' aa ba ptr bb rights irqslot irq_slot ya) (insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) (transform_cslot_ptr irq_slot) \<sqinter> insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) (transform_cslot_ptr irq_slot)) (cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot)
 2. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 x21 a b s' aa ba ptr bb rights (transform_cslot_ptr irq_slot)\<rbrace> delete_cap_simple (transform_cslot_ptr irq_slot) \<lbrace>?R59 x21 a b s' aa ba ptr bb rights irqslot irq_slot\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'64 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>?R'59 x21 a b s' aa ba ptr bb rights irqslot irq_slot\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>c. (\<lambda>_. True) and ?Q65 x21 a b s' aa ba ptr bb rights c\<rbrace>
 5. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and ?Q'64 x21 a b s' aa ba ptr bb rights irq_slot and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 6. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 7. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 8. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (8 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b); dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya (?x21.71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) a b (?s'71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?aa71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?ba71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) ptr bb rights (?irqslot71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) irq_slot (?y71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya)) (?R'71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya (?x21.71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) a b (?s'71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?aa71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?ba71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) ptr bb rights (?irqslot71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) irq_slot (?ya71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya)) (insert_cap_sibling (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) (transform_cslot_ptr irq_slot) \<sqinter> insert_cap_child (cdl_cap.NotificationCap ptr bb rights) (transform_cslot_ptr (a, b)) (transform_cslot_ptr irq_slot)) (cap_insert (cap.NotificationCap ptr bb rights) (a, b) irq_slot)
 2. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 x21 a b s' aa ba ptr bb rights (transform_cslot_ptr irq_slot)\<rbrace> delete_cap_simple (transform_cslot_ptr irq_slot) \<lbrace>?R59 x21 a b s' aa ba ptr bb rights irqslot irq_slot\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'64 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>?R'59 x21 a b s' aa ba ptr bb rights irqslot irq_slot\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>c. (\<lambda>_. True) and ?Q65 x21 a b s' aa ba ptr bb rights c\<rbrace>
 5. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and ?Q'64 x21 a b s' aa ba ptr bb rights irq_slot and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 6. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 7. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 8. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation)
flex-flex pairs:
\<lambda>x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya. ?R'71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya (?x21.71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) a b (?s'71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?aa71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?ba71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) ptr bb rights (?irqslot71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) irq_slot (?ya71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) \<equiv>\<^sup>? \<lambda>x21 a b s' aa ba ptr bb rights irqslot irq_slot y. ?R'59 x21 a b s' aa ba ptr bb rights irqslot irq_slot
\<lambda>x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya. ?R71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya (?x21.71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) a b (?s'71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?aa71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) (?ba71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) ptr bb rights (?irqslot71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) irq_slot (?y71 x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya) \<equiv>\<^sup>? \<lambda>x21 a b s' aa ba ptr bb rights irqslot irq_slot y ya. ?R59 x21 a b s' aa ba ptr bb rights irqslot irq_slot y proof (prove)
goal (7 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 x21 a b s' aa ba ptr bb rights (transform_cslot_ptr irq_slot)\<rbrace> delete_cap_simple (transform_cslot_ptr irq_slot) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'64 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>c d. cte_wp_at ((=) cap.NullCap) irq_slot d \<and> cte_wp_at (\<lambda>_. True) (a, b) d \<and> not_idle_thread (fst irq_slot) d \<and> not_idle_thread (fst (a, b)) d \<and> valid_mdb d \<and> valid_idle d \<and> valid_etcbs d \<and> valid_objs d \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>c. (\<lambda>_. True) and ?Q65 x21 a b s' aa ba ptr bb rights c\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and ?Q'64 x21 a b s' aa ba ptr bb rights irq_slot and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 7. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'64 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>c d. cte_wp_at ((=) cap.NullCap) irq_slot d \<and> cte_wp_at (\<lambda>_. True) (a, b) d \<and> not_idle_thread (fst irq_slot) d \<and> not_idle_thread (fst (a, b)) d \<and> valid_mdb d \<and> valid_idle d \<and> valid_etcbs d \<and> valid_objs d \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and ?Q'64 x21 a b s' aa ba ptr bb rights irq_slot and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?P'83 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>_. True) (a, b) s \<and> not_idle_thread (fst irq_slot) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_mdb s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_objs s \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> ?P'83 x21 a b s' aa ba ptr bb rights irq_slot c) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (7 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (a, b) \<noteq> irq_slot
 2. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?P'89 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. not_idle_thread (fst irq_slot) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_mdb s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_objs s \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> cte_wp_at (\<lambda>_. True) (a, b) c \<and> ?P'89 x21 a b s' aa ba ptr bb rights irq_slot c) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 7. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?P'89 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. not_idle_thread (fst irq_slot) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_mdb s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_objs s \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> cte_wp_at (\<lambda>_. True) (a, b) c \<and> ?P'89 x21 a b s' aa ba ptr bb rights irq_slot c) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?P'107 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv s. valid_idle s \<and> valid_etcbs s \<and> valid_objs s \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> cte_wp_at (\<lambda>_. True) (a, b) c \<and> not_idle_thread (fst irq_slot) c \<and> not_idle_thread (fst (a, b)) c \<and> (invs and emptyable irq_slot) c \<and> ?P'107 x21 a b s' aa ba ptr bb rights irq_slot c) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights irqslot irq_slot. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; irqslot = transform_cslot_ptr irq_slot; irq_slot \<noteq> (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?P'107 x21 a b s' aa ba ptr bb rights irq_slot\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>r s. invs s \<and> valid_etcbs s \<and> invs s \<and> cap_aligned (cap.NotificationCap ptr bb rights)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> cte_wp_at (\<lambda>_. True) (a, b) c \<and> not_idle_thread (fst irq_slot) c \<and> not_idle_thread (fst (a, b)) c \<and> (invs and emptyable irq_slot) c \<and> ?P'107 x21 a b s' aa ba ptr bb rights irq_slot c) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (5 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 x21 a b s' aa ba ptr bb rights\<rbrace> gets (CSpace_D.get_irq_slot x21) \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> cte_wp_at (\<lambda>_. True) (a, b) c \<and> not_idle_thread (fst irq_slot) c \<and> not_idle_thread (fst (a, b)) c \<and> (invs and emptyable irq_slot) c \<and> (invs and emptyable irq_slot) c \<and> valid_etcbs c \<and> (invs and emptyable irq_slot) c \<and> cap_aligned (cap.NotificationCap ptr bb rights)) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 3. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 4. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 5. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (4 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>irq_slot. invs and not_idle_thread (fst irq_slot) and valid_etcbs and (\<lambda>c. True \<and> cte_wp_at (\<lambda>_. True) (a, b) c \<and> not_idle_thread (fst irq_slot) c \<and> not_idle_thread (fst (a, b)) c \<and> (invs and emptyable irq_slot) c \<and> (invs and emptyable irq_slot) c \<and> valid_etcbs c \<and> (invs and emptyable irq_slot) c \<and> cap_aligned (cap.NotificationCap ptr bb rights)) and (\<lambda>s. irq_slot \<noteq> (a, b))\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 3. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'52 x21 a b s' aa ba ptr bb rights) s
 4. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (4 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> \<lbrace>?P'183 x21 a b s' aa ba ptr bb rights\<rbrace> KHeap_A.get_irq_slot x21 \<lbrace>\<lambda>rv s. rv \<noteq> (a, b)\<rbrace>
 2. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 3. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs s \<and> (valid_idle and valid_irq_node) s \<and> valid_etcbs s \<and> True \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> (valid_idle and valid_irq_node) s \<and> not_idle_thread (fst (a, b)) s \<and> invs s \<and> invs s \<and> invs s \<and> invs s \<and> valid_etcbs s \<and> invs s \<and> invs s \<and> cap_aligned (cap.NotificationCap ptr bb rights) \<and> ?P'183 x21 a b s' aa ba ptr bb rights s)) s
 4. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q52 x21 a b s' aa ba ptr bb rights) s
 2. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s'; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s'; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s'; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s'; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s'; ntfn_at ptr s'; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs s \<and> (valid_idle and valid_irq_node) s \<and> valid_etcbs s \<and> True \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> (valid_idle and valid_irq_node) s \<and> not_idle_thread (fst (a, b)) s \<and> invs s \<and> invs s \<and> invs s \<and> invs s \<and> valid_etcbs s \<and> invs s \<and> invs s \<and> cap_aligned (cap.NotificationCap ptr bb rights) \<and> valid_global_refs s \<and> ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s)) s
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 a b s' aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; s' = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_irq_node s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> valid_idle s \<and> valid_irq_node s \<and> not_idle_thread a s \<and> valid_global_refs s
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 a b aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> valid_irq_node s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> valid_irq_node s \<and> not_idle_thread a s \<and> valid_global_refs s
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (4 subgoals):
 1. \<And>x21 a b aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s
 2. \<And>x21 a b aa ba ptr bb rights s cap. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; interrupt_derived (cap.NotificationCap ptr bb rights) cap\<rbrakk> \<Longrightarrow> cap \<noteq> cap.NullCap
 3. \<And>x21 a b aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. interrupt_derived (cap.NotificationCap ptr bb rights) cap' \<and> appropriate_cte_cap cap' cap) (a, b) s\<rbrakk> \<Longrightarrow> valid_irq_node s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> valid_irq_node s \<and> not_idle_thread a s \<and> valid_global_refs s
 4. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (3 subgoals):
 1. \<And>x21 a b aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; interrupt_derived (cap.NotificationCap ptr bb rights) cap.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>x21 a b aa ba ptr bb rights s. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cte_wp_at ((=) (IRQHandlerCap x21)) (aa, ba) s; cte_wp_at (interrupt_derived (cap.NotificationCap ptr bb rights)) (a, b) s; cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. interrupt_derived (cap.NotificationCap ptr bb rights) cap' \<and> appropriate_cte_cap cap' cap) (a, b) s\<rbrakk> \<Longrightarrow> valid_irq_node s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> valid_irq_node s \<and> not_idle_thread a s \<and> valid_global_refs s
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x21 a b aa ba ptr bb rights s bdg rghts. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap.NotificationCap ptr 0 UNIV = cap_master_cap cap' \<and> (CSpaceInv_AI.cap_badge cap', Some bb) \<in> capBadge_ordering False \<and> appropriate_cte_cap cap' cap) (a, b) s; caps_of_state s (a, b) = Some (cap.NotificationCap ptr bdg rghts); bdg = 0 \<or> bdg = bb\<rbrakk> \<Longrightarrow> valid_irq_node s \<and> not_idle_thread a s
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (6 subgoals):
 1. \<And>x21 a b aa ba ptr bb rights s bdg rghts. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap.NotificationCap ptr 0 UNIV = cap_master_cap cap' \<and> (CSpaceInv_AI.cap_badge cap', Some bb) \<in> capBadge_ordering False \<and> appropriate_cte_cap cap' cap) (a, b) s; caps_of_state s (a, b) = Some (cap.NotificationCap ptr bdg rghts); bdg = 0 \<or> bdg = bb\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>x21 a b aa ba ptr bb rights s bdg rghts. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap.NotificationCap ptr 0 UNIV = cap_master_cap cap' \<and> (CSpaceInv_AI.cap_badge cap', Some bb) \<in> capBadge_ordering False \<and> appropriate_cte_cap cap' cap) (a, b) s; caps_of_state s (a, b) = Some (cap.NotificationCap ptr bdg rghts); bdg = 0 \<or> bdg = bb\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>x21 a b aa ba ptr bb rights s bdg rghts. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap.NotificationCap ptr 0 UNIV = cap_master_cap cap' \<and> (CSpaceInv_AI.cap_badge cap', Some bb) \<in> capBadge_ordering False \<and> appropriate_cte_cap cap' cap) (a, b) s; caps_of_state s (a, b) = Some (cap.NotificationCap ptr bdg rghts); bdg = 0 \<or> bdg = bb\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>x21 a b aa ba ptr bb rights s bdg rghts. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap.NotificationCap ptr 0 UNIV = cap_master_cap cap' \<and> (CSpaceInv_AI.cap_badge cap', Some bb) \<in> capBadge_ordering False \<and> appropriate_cte_cap cap' cap) (a, b) s; caps_of_state s (a, b) = Some (cap.NotificationCap ptr bdg rghts); bdg = 0 \<or> bdg = bb\<rbrakk> \<Longrightarrow> valid_irq_node s
 5. \<And>x21 a b aa ba ptr bb rights s bdg rghts. \<lbrakk>irq_handler_invocation = SetIRQHandler x21 (cap.NotificationCap ptr bb rights) (a, b); invs s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); cap_aligned (cap.NotificationCap ptr bb rights); valid_etcbs s; ntfn_at ptr s; AllowGrant \<notin> rights; AllowGrantReply \<notin> rights; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap.NotificationCap ptr 0 UNIV = cap_master_cap cap' \<and> (CSpaceInv_AI.cap_badge cap', Some bb) \<in> capBadge_ordering False \<and> appropriate_cte_cap cap' cap) (a, b) s; caps_of_state s (a, b) = Some (cap.NotificationCap ptr bdg rghts); bdg = 0 \<or> bdg = bb; not_idle_thread (fst (a, b)) s\<rbrakk> \<Longrightarrow> valid_irq_node s \<and> not_idle_thread a s
 6. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_handler_inv_valid irq_handler_invocation and valid_etcbs) (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation irq_handler_invocation)) (Interrupt_A.invoke_irq_handler irq_handler_invocation) proof (prove)
goal (1 subgoal):
 1. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.invoke_irq_handler (ClearIrqHandler x3)) (KHeap_A.get_irq_slot x3 >>= cap_delete_one) proof (prove)
goal (1 subgoal):
 1. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.invoke_irq_handler (ClearIrqHandler x3)) (KHeap_A.get_irq_slot x3 >>= cap_delete_one) proof (prove)
goal (1 subgoal):
 1. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (gets (CSpace_D.get_irq_slot x3) >>= delete_cap_simple) (KHeap_A.get_irq_slot x3 >>= cap_delete_one) proof (prove)
goal (3 subgoals):
 1. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> dcorres dc (?Q235 x3) (?Q'235 x3) (gets (CSpace_D.get_irq_slot x3) >>= delete_cap_simple) (KHeap_A.get_irq_slot x3 >>= cap_delete_one)
 2. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; True\<rbrakk> \<Longrightarrow> ?Q235 x3 s
 3. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; (invs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'235 x3 s proof (prove)
goal (5 subgoals):
 1. \<And>x3 rv rv'. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R239 x3 rv) (?R'239 x3 rv') (delete_cap_simple rv) (cap_delete_one rv')
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>?Q239 x3\<rbrace> gets (CSpace_D.get_irq_slot x3) \<lbrace>?R239 x3\<rbrace>
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>?Q'239 x3\<rbrace> KHeap_A.get_irq_slot x3 \<lbrace>?R'239 x3\<rbrace>
 4. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q239 x3) s
 5. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; (invs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'239 x3) s proof (prove)
goal (5 subgoals):
 1. \<And>x3 a b aa ba. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> dcorres dc (?R239 x3 (transform_cslot_ptr (aa, ba))) (?R'239 x3 (aa, ba)) (delete_cap_simple (transform_cslot_ptr (aa, ba))) (cap_delete_one (aa, ba))
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>?Q239 x3\<rbrace> gets (CSpace_D.get_irq_slot x3) \<lbrace>?R239 x3\<rbrace>
 3. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>?Q'239 x3\<rbrace> KHeap_A.get_irq_slot x3 \<lbrace>?R'239 x3\<rbrace>
 4. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q239 x3) s
 5. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; (invs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'239 x3) s proof (prove)
goal (4 subgoals):
 1. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>?Q239 x3\<rbrace> gets (CSpace_D.get_irq_slot x3) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>x3. irq_handler_invocation = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>?Q'239 x3\<rbrace> KHeap_A.get_irq_slot x3 \<lbrace>\<lambda>a. invs and not_idle_thread (fst a) and valid_etcbs\<rbrace>
 3. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q239 x3) s
 4. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; (invs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'239 x3) s proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>irq_handler_invocation = ClearIRQHandler x3; (invs and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs s \<and> (valid_idle and valid_irq_node) s \<and> valid_etcbs s)) s proof (prove)
goal:
No subgoals!