diff --git a/proof/crefine/ARM/Ctac_lemmas_C.thy b/proof/crefine/ARM/Ctac_lemmas_C.thy
index 2b42ab3a0c..c6e7f407ed 100644
--- a/proof/crefine/ARM/Ctac_lemmas_C.thy
+++ b/proof/crefine/ARM/Ctac_lemmas_C.thy
@@ -183,7 +183,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap]
 
 lemma array_assertion_abs_irq:
   "\<forall>s s'. (s, s') \<in> rf_sr \<and> True
-        \<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
+        \<and> (n s' \<le> 2^LENGTH(irq_len) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
     \<longrightarrow> (x s' = 0 \<or> array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))"
   apply (intro allI impI disjCI2)
   apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
diff --git a/proof/crefine/ARM/Interrupt_C.thy b/proof/crefine/ARM/Interrupt_C.thy
index 9432a06011..58bc21d17d 100644
--- a/proof/crefine/ARM/Interrupt_C.thy
+++ b/proof/crefine/ARM/Interrupt_C.thy
@@ -299,7 +299,9 @@ lemma invokeIRQControl_expanded_ccorres:
   apply (rule conjI, fastforce)+
   apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift
                         cap_to_H_def c_valid_cap_def cl_valid_cap_def irq_len_val ucast_and_mask)
-  apply word_eqI
+  (* if irq_len < 8, there may be an additional term in the goal *)
+  apply (rule conjI, word_eqI_solve)?
+  apply (word_eqI_solve dest: bit_imp_le_length)
   done
 
 lemma invokeIRQControl_ccorres:
diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy
index f072174c0c..563f15f7a2 100644
--- a/proof/crefine/ARM/Refine_C.thy
+++ b/proof/crefine/ARM/Refine_C.thy
@@ -36,7 +36,7 @@ lemma schedule_sch_act_wf:
   apply (rule schedule_invs')
   done
 
-(* On GICv2 and GICv3, irqInvalid is picked such it is outside the range of possible IRQs
+(* On Arm, irqInvalid is picked such it is outside the range of possible IRQs
    by type alone. *)
 lemma irq_type_never_invalid_left:
   "ucast irq \<noteq> irqInvalid" for irq::irq
diff --git a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy
index e099909f4e..f79b929cc6 100644
--- a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy
+++ b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy
@@ -186,7 +186,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap]
 
 lemma array_assertion_abs_irq:
   "\<forall>s s'. (s, s') \<in> rf_sr \<and> True
-        \<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
+        \<and> (n s' \<le> 2^LENGTH(irq_len) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
     \<longrightarrow> (x s' = 0 \<or> array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))"
   apply (intro allI impI disjCI2)
   apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
diff --git a/proof/crefine/ARM_HYP/Interrupt_C.thy b/proof/crefine/ARM_HYP/Interrupt_C.thy
index 88046147c6..8c8d9e1ac2 100644
--- a/proof/crefine/ARM_HYP/Interrupt_C.thy
+++ b/proof/crefine/ARM_HYP/Interrupt_C.thy
@@ -309,7 +309,9 @@ lemma invokeIRQControl_expanded_ccorres:
   apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift
                         cap_to_H_def c_valid_cap_def cl_valid_cap_def irq_len_val
                         word_bw_assocs mask_twice)
-  apply word_eqI
+  (* if irq_len < 8, there may be an additional term in the goal *)
+  apply (rule conjI, word_eqI_solve)?
+  apply (word_eqI_solve dest: bit_imp_le_length)
   done
 
 lemma invokeIRQControl_ccorres:
diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy
index 1c73871530..d6c0182dfb 100644
--- a/proof/crefine/ARM_HYP/Refine_C.thy
+++ b/proof/crefine/ARM_HYP/Refine_C.thy
@@ -30,7 +30,7 @@ lemma schedule_sch_act_wf:
   apply (rule schedule_invs')
   done
 
-(* On GICv2 and GICv3, irqInvalid is picked such it is outside the range of possible IRQs
+(* On Arm, irqInvalid is picked such it is outside the range of possible IRQs
    by type alone. *)
 lemma irq_type_never_invalid_left:
   "ucast irq \<noteq> irqInvalid" for irq::irq