theory Finalise_R

lemma (in delete_one) deletingIRQHandler_corres:
  "corres dc (einvs) (invs')
          (deleting_irq_handler irq) (deletingIRQHandler irq)" apply (simp add: deleting_irq_handler_def deletingIRQHandler_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getIRQSlot_corres]) apply simp apply (rule_tac P'="cte_at' (cte_map slot)" in corres_symb_exec_r_conj) apply (rule_tac F="isNotificationCap rv \<or> rv = capability.NullCap"
             and P="cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot
                 and einvs"
             and P'="invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv)
                 (cte_map slot)" in corres_req) apply (clarsimp simp: cte_wp_at_caps_of_state state_relation_def) apply (drule caps_of_state_cteD) apply (drule(1) pspace_relation_cte_wp_at, clarsimp+) apply (auto simp: cte_wp_at_ctes_of is_cap_simps isCap_simps)[1] apply simp apply (rule corres_guard_imp, rule delete_one_corres[unfolded dc_def]) apply (auto simp: cte_wp_at_caps_of_state is_cap_simps can_fast_finalise_def)[1] apply (clarsimp simp: cte_wp_at_ctes_of) apply (wp getCTE_wp' | simp add: getSlotCap_def)+ apply (wp | simp add: get_irq_slot_def getIRQSlot_def
                           locateSlot_conv getInterruptState_def)+ apply (clarsimp simp: ex_cte_cap_wp_to_def interrupt_cap_null_or_ntfn) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc einvs invs' (deleting_irq_handler irq) (deletingIRQHandler irq) proof (prove)
goal (1 subgoal):
 1. corres dc einvs invs' (get_irq_slot irq >>= cap_delete_one) (do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne slot
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (get_irq_slot irq >>= cap_delete_one) (do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne slot
od)
 2. \<And>s. einvs s \<Longrightarrow> ?Q s
 3. \<And>s. invs' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>slot slota. slota = cte_map slot \<Longrightarrow> corres dc (?R4 slot) (?R'4 slota) (cap_delete_one slot) (do cap <- getSlotCap slota;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne slota
od)
 2. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>?R'4\<rbrace>
 4. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>slot. corres dc (?R4 slot) (?R'4 (cte_map slot)) (cap_delete_one slot) (do cap <- getSlotCap (cte_map slot);
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 2. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>?R'4\<rbrace>
 4. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>slot rv. corres dc (?R4 slot) (?R'9 slot rv) (cap_delete_one slot) (do y <- assert (isNotificationCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 2. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>?R'9 slot\<rbrace>
 3. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 5. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 7. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>slot rv s s'. \<lbrakk>(s, s') \<in> state_relation; (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) s; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) s'\<rbrakk> \<Longrightarrow> isNotificationCap rv \<or> rv = capability.NullCap
 2. \<And>slot rv. isNotificationCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) (cap_delete_one slot) (do y <- assert (isNotificationCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 3. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 4. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 6. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 8. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>a b rv s s' cap. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs' s'; cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (a, b)) s'; ekheap_relation (ekheap s) (ksPSpace s'); invs s; caps_of_state s (a, b) = Some cap; is_ntfn_cap cap \<or> cap = cap.NullCap; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (ksCurDomain s') (kheap s) (ksCurThread s') (ksIdleThread s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; rv \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> isNotificationCap rv
 2. \<And>slot rv. isNotificationCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) (cap_delete_one slot) (do y <- assert (isNotificationCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 3. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 4. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 6. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 8. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>a b rv s s' cap. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs' s'; cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (a, b)) s'; ekheap_relation (ekheap s) (ksPSpace s'); invs s; is_ntfn_cap cap \<or> cap = cap.NullCap; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (ksCurDomain s') (kheap s) (ksCurThread s') (ksIdleThread s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; rv \<noteq> capability.NullCap; cte_wp_at ((=) cap) (a, b) s\<rbrakk> \<Longrightarrow> isNotificationCap rv
 2. \<And>slot rv. isNotificationCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) (cap_delete_one slot) (do y <- assert (isNotificationCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 3. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 4. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 6. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 8. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>a b rv s s' cap. \<lbrakk>invs' s'; cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map (a, b)) s'; ekheap_relation (ekheap s) (ksPSpace s'); invs s; is_ntfn_cap cap \<or> cap = cap.NullCap; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (ksCurDomain s') (kheap s) (ksCurThread s') (ksIdleThread s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; rv \<noteq> capability.NullCap; cte_wp_at ((=) cap) (a, b) s; cte_wp_at' (\<lambda>cte. cap_relation cap (cteCap cte)) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> isNotificationCap rv
 2. \<And>slot rv. isNotificationCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) (cap_delete_one slot) (do y <- assert (isNotificationCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 3. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 4. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 6. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 8. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>slot rv. isNotificationCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres dc (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) (cap_delete_one slot) (do y <- assert (isNotificationCap rv \<or> rv = capability.NullCap);
cteDeleteOne (cte_map slot)
od)
 2. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 3. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 5. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 7. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>slot rv. isNotificationCap rv \<or> rv = capability.NullCap \<Longrightarrow> corres (\<lambda>a b. True) (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) (cap_delete_one slot) (cteDeleteOne (cte_map slot))
 2. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 3. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 5. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 7. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>slot rv s. \<lbrakk>isNotificationCap rv \<or> rv = capability.NullCap; (cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs) s\<rbrakk> \<Longrightarrow> (einvs and cte_wp_at can_fast_finalise slot) s
 2. \<And>slot rv s. \<lbrakk>isNotificationCap rv \<or> rv = capability.NullCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s
 3. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 4. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 5. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 6. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 8. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>slot rv s. \<lbrakk>isNotificationCap rv \<or> rv = capability.NullCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)) s\<rbrakk> \<Longrightarrow> (invs' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s
 2. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 3. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 5. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 7. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>slot. \<lbrace>?Q'11 (cte_map slot)\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv. invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) (cte_map slot)\<rbrace>
 2. \<And>slot s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> getSlotCap (cte_map slot) \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 3. \<And>slot s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (getSlotCap (cte_map slot))
 4. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot and einvs\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and ?Q'11 a\<rbrace>
 6. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_irq_slot irq \<lbrace>\<lambda>slot s. cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot s \<and> invs s \<and> valid_list s \<and> valid_sched s\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and (\<lambda>b. invs' b \<and> (\<forall>cte. cte_wp_at' ((=) cte) a b \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) a b))\<rbrace>
 3. \<And>s. einvs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> invs' s \<and> ((\<lambda>node a. \<forall>cte. cte_wp_at' ((=) cte) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) a \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) a) \<circ> intStateIRQNode) (ksInterruptState s) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> invs' s \<and> ((\<lambda>node a. \<forall>cte. cte_wp_at' ((=) cte) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) a \<longrightarrow> cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) a) \<circ> intStateIRQNode) (ksInterruptState s) s)) s proof (prove)
goal:
No subgoals!