theory Finalise_C

lemma deletingIRQHandler_ccorres:
  "ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
                   (UNIV \<inter> {s. irq_opt_relation (Some irq) (irq_' s)}) []
   (deletingIRQHandler irq) (Call deletingIRQHandler_'proc)" apply (cinit lift: irq_' cong: call_ignore_cong) apply (clarsimp simp: irq_opt_relation_def ptr_add_assertion_def
                   cong: call_ignore_cong ) apply (rule_tac r'="\<lambda>rv rv'. rv' = Ptr rv" and xf'="slot_'" in ccorres_split_nothrow) apply (rule ccorres_Guard_intStateIRQNode_array_Ptr) apply (rule ccorres_move_array_assertion_irq) apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def
                             locateSlot_conv) apply (simp add: bind_def simpler_gets_def return_def getIRQSlot_ccorres_stuff[simplified]) apply ceqv apply (rule ccorres_symb_exec_l) apply (rule ccorres_symb_exec_l) apply (rule ccorres_symb_exec_r) apply (ctac add: cteDeleteOne_ccorres[where w="scast cap_notification_cap"]) apply vcg apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def
                gs_set_assn_Delete_cstate_relation[unfolded o_def]) apply (wp getCTE_wp' | simp add: getSlotCap_def getIRQSlot_def locateSlot_conv
                                           getInterruptState_def)+ apply vcg apply (clarsimp simp: cap_get_tag_isCap ghost_assertion_data_get_def
                        ghost_assertion_data_set_def) apply (simp add: cap_tag_defs) apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem
                        irq_opt_relation_def Kernel_C.maxIRQ_def) apply (drule word_le_nat_alt[THEN iffD1]) apply (clarsimp simp: uint_0_iff unat_gt_0 uint_up_ucast is_up) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (UNIV \<inter> \<lbrace>irq_opt_relation (Some irq) \<acute>irq\<rbrace>) [] (deletingIRQHandler irq) (Call deletingIRQHandler_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>irqa. irq_opt_relation (Some irq) irqa \<Longrightarrow> ccorres dc xfdc (?Q203 irqa) (?Q'203 irqa) [SKIP] (do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>irqa = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irqa) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C)))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)))
 2. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q203 irqa s \<and> s' \<in> ?Q'203 irqa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q203 (UCAST(10 \<rightarrow> 32) irq)) (?Q'203 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)))
 2. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q203 irqa s \<and> s' \<in> ?Q'203 irqa proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = cte_Ptr rv) slot_' (?P230 (UCAST(10 \<rightarrow> 32) irq)) (?P'226 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (getIRQSlot irq) (Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))))
 2. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 6. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P230 irqa and ?R229 irqa) s \<and> s' \<in> ?P'226 irqa \<inter> ?R'225 irqa proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = cte_Ptr rv) slot_' (?P230 (UCAST(10 \<rightarrow> 32) irq)) (?P'226 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (getIRQSlot irq) (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)))))
 2. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 6. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P230 irqa and ?R229 irqa) s \<and> s' \<in> ?P'226 irqa \<inter> ?R'225 irqa proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = cte_Ptr rv) slot_' (?A236 (UCAST(10 \<rightarrow> 32) irq)) (?C'234 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (getIRQSlot irq) (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))
 2. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 6. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A236 irqa and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> ?C'234 irqa \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))) {s. \<exists>(rv, \<sigma>')\<in>fst (getIRQSlot irq \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> slot_' s = cte_Ptr rv}
 2. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 6. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (getIRQSlot irq \<sigma>). (\<sigma>', slot_'_update (\<lambda>_. cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)))) s) \<in> rf_sr \<and> cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr rv}
 2. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 6. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do x <- gets ksInterruptState;
return (intStateIRQNode x + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)) = rv
 2. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 6. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ceqv \<Gamma> slot_' rv' t t' (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(\<acute>slot)) (?d'223 rv')
 2. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (?d'223 rv')
 3. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 4. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 5. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 rv) (?Q'223 rv rv') [SKIP] (do cap <- getSlotCap rv;
y <- assert (isNotificationCap cap \<or> cap = capability.NullCap);
cteDeleteOne rv
od) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(rv'))
 2. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 3. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> ?Q'223 rv (slot_' s)}
 4. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q293 rv rv' rva) (?Q'293 rv rv' rva) [SKIP] (do y <- assert (isNotificationCap rva \<or> rva = capability.NullCap);
cteDeleteOne rv
od) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(rv'))
 2. \<And>rv rv' s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 rv\<rbrace> getSlotCap rv \<lbrace>?Q293 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 5. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 6. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> ?Q293 rv (slot_' s) rva sa \<longrightarrow> s' \<in> ?Q'293 rv (slot_' s) rva}}
 7. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (10 subgoals):
 1. \<And>rv rv' rva rvb. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q298 rv rv' rva rvb) (?Q'298 rv rv' rva rvb) [SKIP] (cteDeleteOne rv) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap));;
CALL cteDeleteOne_'proc(rv'))
 2. \<And>rv rv' rva s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 rv rv' rva\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>?Q298 rv rv' rva\<rbrace>
 4. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (assert (isNotificationCap rva \<or> rva = capability.NullCap))
 5. \<And>rv rv' s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 rv\<rbrace> getSlotCap rv \<lbrace>?Q293 rv rv'\<rbrace>
 7. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 8. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 9. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> ?Q293 rv (slot_' s) rva sa \<longrightarrow> s' \<in> {s'. \<forall>rvb sa. (sa, s') \<in> rf_sr \<and> ?Q298 rv (slot_' s) rva rvb sa \<longrightarrow> s' \<in> ?Q'298 rv (slot_' s) rva rvb}}}
 10. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rvb. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q298 rv rv' rva rvb) (?Q'303 rv rv' rva rvb) [SKIP] (cteDeleteOne rv) (CALL cteDeleteOne_'proc(rv'))
 2. \<And>rv rv' rva rvb. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'298 rv rv' rva rvb) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap)) (?Q'303 rv rv' rva rvb)
 3. \<And>rv rv' rva rvb s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv; ?Q298 rv rv' rva rvb s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'298 rv rv' rva rvb \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap)) {s'. (s, s') \<in> rf_sr}
 4. \<And>rv rv' rva s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 rv rv' rva\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>?Q298 rv rv' rva\<rbrace>
 6. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (assert (isNotificationCap rva \<or> rva = capability.NullCap))
 7. \<And>rv rv' s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 rv\<rbrace> getSlotCap rv \<lbrace>?Q293 rv rv'\<rbrace>
 9. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 10. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' rva rvb. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'298 rv rv' rva rvb) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap)) {s. slot_'_update (\<lambda>_. rv') s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = SCAST(32 signed \<rightarrow> 32) cap_notification_cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>}
 2. \<And>rv rv' rva rvb s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv; (invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'298 rv rv' rva rvb \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap)) {s'. (s, s') \<in> rf_sr}
 3. \<And>rv rv' rva s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 rv rv' rva\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>rvb. invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv\<rbrace>
 5. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (assert (isNotificationCap rva \<or> rva = capability.NullCap))
 6. \<And>rv rv' s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 rv\<rbrace> getSlotCap rv \<lbrace>?Q293 rv rv'\<rbrace>
 8. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 9. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 10. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> ?Q293 rv (slot_' s) rva sa \<longrightarrow> s' \<in> {s'. \<forall>rvb sa. (sa, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv) sa \<longrightarrow> s' \<in> ?Q'298 rv (slot_' s) rva rvb}}}
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv rv' rva rvb s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv; (invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<and> rv' = cte_Ptr rv\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap)) {s'. (s, s') \<in> rf_sr}
 2. \<And>rv rv' rva s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 rv rv' rva\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>rvb. invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv\<rbrace>
 4. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (assert (isNotificationCap rva \<or> rva = capability.NullCap))
 5. \<And>rv rv' s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 rv\<rbrace> getSlotCap rv \<lbrace>?Q293 rv rv'\<rbrace>
 7. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 8. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 9. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> ?Q293 rv (slot_' s) rva sa \<longrightarrow> s' \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv) sa \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<and> \<^bsup>s\<^esup>slot = cte_Ptr rv\<rbrace>}}}
 10. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' rva s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 rv rv' rva\<rbrace> assert (isNotificationCap rva \<or> rva = capability.NullCap) \<lbrace>\<lambda>rvb. invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv\<rbrace>
 3. \<And>rv rv' rva. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (assert (isNotificationCap rva \<or> rva = capability.NullCap))
 4. \<And>rv rv' s. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSlotCap rv \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> \<lbrace>?Q223 rv\<rbrace> getSlotCap rv \<lbrace>?Q293 rv rv'\<rbrace>
 6. \<And>rv rv'. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; rv' = cte_Ptr rv\<rbrakk> \<Longrightarrow> empty_fail (getSlotCap rv)
 7. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q223\<rbrace>
 8. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> s \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> ?Q293 rv (slot_' s) rva sa \<longrightarrow> s' \<in> {s'. \<forall>rva sa. (sa, s') \<in> rf_sr \<and> (invs' and cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv) sa \<longrightarrow> s' \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<and> \<^bsup>s\<^esup>slot = cte_Ptr rv\<rbrace>}}}
 9. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and ?R229 irqa) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F223\<^esub> (?R'225 (UCAST(10 \<rightarrow> 32) irq)) Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>UCAST(10 \<rightarrow> 32) irq = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>slot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C))))) {s. \<forall>rv. slot_' s = cte_Ptr rv \<longrightarrow> (\<exists>rva sa. (sa, s) \<in> rf_sr \<and> (isNotificationCap rva \<longrightarrow> invs' sa \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv sa) \<and> (rva = capability.NullCap \<longrightarrow> invs' sa \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv sa)) \<longrightarrow> (\<exists>sa. (sa, s) \<in> rf_sr \<and> invs' sa \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv sa) \<longrightarrow> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap) (\<lambda>x. apsnd (apsnd x)) (ghost'state_' (globals s))) = SCAST(32 signed \<rightarrow> 32) cap_notification_cap}
 2. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and (\<lambda>a. ((\<lambda>x a. \<forall>cte. cte_wp_at' ((=) cte) (x + 2 ^ cte_level_bits * irqa) a \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) (x + 2 ^ cte_level_bits * irqa) a) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) (x + 2 ^ cte_level_bits * irqa) a)) \<circ> intStateIRQNode) (ksInterruptState a) a)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> ?R'225 irqa proof (prove)
goal (1 subgoal):
 1. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True) and (\<lambda>a. ((\<lambda>x a. \<forall>cte. cte_wp_at' ((=) cte) (x + 2 ^ cte_level_bits * irqa) a \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) (x + 2 ^ cte_level_bits * irqa) a) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' a \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) (x + 2 ^ cte_level_bits * irqa) a)) \<circ> intStateIRQNode) (ksInterruptState a) a)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irq \<noteq> 0)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<longrightarrow> irqa = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> (\<forall>rv. cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr rv \<longrightarrow> (\<exists>rva sa. (sa, slot_'_update (\<lambda>_. cte_Ptr rv) s) \<in> rf_sr \<and> (isNotificationCap rva \<longrightarrow> invs' sa \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv sa) \<and> (rva = capability.NullCap \<longrightarrow> invs' sa \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv sa)) \<longrightarrow> (\<exists>sa. (sa, slot_'_update (\<lambda>_. cte_Ptr rv) s) \<in> rf_sr \<and> invs' sa \<and> cte_wp_at' (\<lambda>ct. SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) rv sa) \<longrightarrow> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (UCAST(32 signed \<rightarrow> 32) cap_notification_cap) (\<lambda>x. apsnd (apsnd x)) (ghost'state_' (globals s))) = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)} proof (prove)
goal (1 subgoal):
 1. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (irq_node' s + 2 ^ cte_level_bits * irqa) s \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (irq_node' s + 2 ^ cte_level_bits * irqa) s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (irq_node' s + 2 ^ cte_level_bits * irqa) s)) \<and> s' \<in> (if unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> 0 < unat irq) then UNIV else {}) \<and> (s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<longrightarrow> (irqa = 0 \<longrightarrow> (\<exists>rv s. (s, s') \<in> rf_sr \<and> (isNotificationCap rv \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (symbol_table ''intStateIRQNode'') s) \<and> (rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (symbol_table ''intStateIRQNode'') s)) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> invs' s \<and> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (symbol_table ''intStateIRQNode'') s) \<longrightarrow> UCAST(32 signed \<rightarrow> 32) cap_notification_cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap) \<and> (array_assertion intStateIRQNode_Ptr (unat irq) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> (\<exists>rv s. (s, s') \<in> rf_sr \<and> (isNotificationCap rv \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C))) s) \<and> (rv = capability.NullCap \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C))) s)) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> invs' s \<and> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = - 1 \<or> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C))) s) \<longrightarrow> UCAST(32 signed \<rightarrow> 32) cap_notification_cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap)) proof (prove)
goal (1 subgoal):
 1. \<And>irqa s s'. \<lbrakk>irq_opt_relation (Some irq) irqa; (s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (irq_node' s + 2 ^ cte_level_bits * irqa) s \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (irq_node' s + 2 ^ cte_level_bits * irqa) s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>ct. Ex (ccap_relation (cteCap ct)) \<longrightarrow> cteCap ct = capability.NullCap \<or> isNotificationCap (cteCap ct)) (irq_node' s + 2 ^ cte_level_bits * irqa) s)) \<and> s' \<in> (if unat irq \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> 0 < unat irq) then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; UCAST(10 \<rightarrow> 32) irq \<le> 0x9F\<rbrakk> \<Longrightarrow> unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; irq \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid; unat (UCAST(10 \<rightarrow> 32) irq) \<le> unat 0x9F\<rbrakk> \<Longrightarrow> unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq) proof (prove)
goal:
No subgoals!