diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy
index 73159d12cf..909316b470 100644
--- a/lib/Word_Lib/Word_Lemmas_Internal.thy
+++ b/lib/Word_Lib/Word_Lemmas_Internal.thy
@@ -838,4 +838,180 @@ lemma ucast_ucast_mask_id:
    UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n" for x :: "'a::len word"
   by (simp add: ucast_ucast_len[OF eq_mask_less])
 
+lemma msb_le_mono:
+  fixes v w :: "'a::len word"
+  shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w"
+  by (simp add: msb_big)
+
+lemma neg_msb_le_mono:
+  fixes v w :: "'a::len word"
+  shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v"
+  by (simp add: msb_big)
+
+lemmas msb_less_mono = msb_le_mono[OF less_imp_le]
+lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le]
+
+lemma word_sless_iff_less:
+  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w"
+  by (simp add: word_sless_alt sint_eq_uint word_less_alt)
+
+lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2]
+lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2]
+
+lemma to_bool_if:
+  "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
+  by (auto simp: to_bool_def)
+
+lemma word_sle_iff_le:
+  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w"
+  apply (simp add: word_sle_def sint_eq_uint word_le_def)
+  by (metis sint_eq_uint word_sle.rep_eq word_sle_eq)
+
+lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2]
+lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2]
+
+lemma word_upcast_shiftr:
+  assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
+  shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
+  apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast)
+  apply (drule test_bit_size)
+  using assms by (simp add: word_size)
+
+lemma word_upcast_neg_msb:
+  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)"
+  unfolding ucast_eq msb_word_of_int
+  by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)
+
+lemma word_upcast_0_sle:
+  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
+  by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
+
+lemma scast_ucast_up_eq_ucast:
+  assumes "LENGTH('a::len) < LENGTH('b::len)"
+  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
+  using assms
+  apply (subst scast_eq_ucast; simp)
+  apply (simp only: ucast_eq msb_word_of_int)
+   apply (metis bin_nth_uint_imp decr_length_less_iff numeral_nat(7) verit_comp_simplify1(3))
+  by (metis less_or_eq_imp_le ucast_nat_def unat_ucast_up_simp)
+
+lemmas not_max_word_iff_less = word_order.not_eq_extremum
+
+lemma ucast_increment:
+  assumes "w \<noteq> max_word"
+  shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)"
+  apply (cases "LENGTH('b) \<le> LENGTH('a)")
+   apply (simp add: ucast_down_add is_down)
+  apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)")
+   apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)")
+    apply (subst word_uint_eq_iff)
+    apply (simp add: uint_arith_simps uint_up_ucast is_up)
+   apply (erule less_trans, rule power_strict_increasing, simp, simp)
+  apply (subst less_diff_eq[symmetric])
+  using assms
+  apply (simp add: not_max_word_iff_less word_less_alt)
+  apply (erule less_le_trans)
+  apply simp
+  done
+
+lemma max_word_gt_0:
+  "0 < max_word"
+  by (simp add: le_neq_trans[OF max_word_max])
+
+lemma and_not_max_word:
+  "m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word"
+  by (simp add: not_max_word_iff_less word_and_less')
+
+lemma mask_not_max_word:
+  "m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)"
+  by (simp add: mask_eq_exp_minus_1)
+
+lemmas and_mask_not_max_word =
+  and_not_max_word[OF mask_not_max_word]
+
+lemma shiftr_not_max_word:
+  "0 < n \<Longrightarrow> w >> n \<noteq> max_word"
+  by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)
+
+lemma word_sandwich1:
+  fixes a b c :: "'a::len word"
+  assumes "a < b"
+  assumes "b <= c"
+  shows "0 < b - a \<and> b - a <= c"
+  using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le
+        word_le_less_eq word_neq_0_conv
+  by metis
+
+lemma word_sandwich2:
+  fixes a b :: "'a::len word"
+  assumes "0 < a"
+  assumes "a <= b"
+  shows "b - a < b"
+  using assms less_le_trans word_diff_less
+  by blast
+
+lemma unat_and_mask_less_2p:
+  fixes w :: "'a::len word"
+  shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m"
+  by (simp add: unat_less_helper  and_mask_less')
+
+lemma unat_shiftr_less_2p:
+  fixes w :: "'a::len word"
+  shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m"
+  by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3)
+
+lemma nat_div_less_mono:
+  fixes m n :: nat
+  shows "m div d < n div d \<Longrightarrow> m < n"
+  by (meson div_le_mono not_less)
+
+lemma word_shiftr_less_mono:
+  fixes w :: "'a::len word"
+  shows "w >> n < v >> n \<Longrightarrow> w < v"
+  by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono)
+
+lemma word_shiftr_less_mask:
+  fixes w :: "'a::len word"
+  shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)"
+  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
+
+lemma word_shiftr_le_mask:
+  fixes w :: "'a::len word"
+  shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)"
+  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
+
+lemma word_shiftr_eq_mask:
+  fixes w :: "'a::len word"
+  shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)"
+  by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq)
+
+lemmas word_shiftr_cmp_mask =
+  word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask
+
+lemma if_if_if_same_output:
+  "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)"
+  by (simp split: if_splits)
+
+lemma word_le_split_mask:
+  "(w \<le> v) \<longleftrightarrow> (w >> n < v >> n \<or> w >> n = v >> n \<and> w && mask n \<le> v && mask n)"
+  apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask)
+  apply (rule subst[where P="\<lambda>c. c \<le> d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]])
+  apply (rule subst[where P="\<lambda>c. d \<le> c = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]])
+  by (metis (no_types) Orderings.order_eq_iff and_not_eq_minus_and bit.double_compl linorder_linear
+                       neg_mask_mono_le word_and_le2 word_le_minus_cancel word_not_le
+                       word_plus_and_or_coroll2)
+
+lemma uint_minus_1_less_le_eq:
+  "0 < n \<Longrightarrow> (uint (n - 1) < m) = (uint n \<le> m)"
+  by uint_arith
+
+lemma scast_ucast_up_minus_1_ucast:
+  assumes "LENGTH('a::len) < LENGTH('b::len)"
+  assumes "0 < w"
+  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w - 1) = UCAST('a \<rightarrow> 'c::len) (w - 1)"
+  using assms
+  apply (subst scast_eq_ucast; simp)
+   apply (metis gt0_iff_gem1 msb_less_mono ucast_less_ucast_weak unsigned_0 word_upcast_neg_msb)
+  by (metis less_le ucast_nat_def ucast_up_preserves_not0 unat_minus_one unat_ucast_up_simp)
+
 end
diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy
index 2541e8510b..f4fa88eae1 100644
--- a/proof/crefine/Move_C.thy
+++ b/proof/crefine/Move_C.thy
@@ -143,180 +143,6 @@ lemma cteSizeBits_le_cte_level_bits[simp]:
   "cteSizeBits \<le> cte_level_bits"
   by (simp add: cte_level_bits_def cteSizeBits_def)
 
-lemma msb_le_mono:
-  fixes v w :: "'a::len word"
-  shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w"
-  by (simp add: msb_big)
-
-lemma neg_msb_le_mono:
-  fixes v w :: "'a::len word"
-  shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v"
-  by (simp add: msb_big)
-
-lemmas msb_less_mono = msb_le_mono[OF less_imp_le]
-lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le]
-
-lemma word_sless_iff_less:
-  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w"
-  by (simp add: word_sless_alt sint_eq_uint word_less_alt)
-
-lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2]
-lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2]
-
-lemma word_sle_iff_le:
-  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w"
-  by (simp add: word_sle_def sint_eq_uint word_le_def)
-
-lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2]
-lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2]
-
-lemma to_bool_if:
-  "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
-  by (auto simp: to_bool_def)
-
-(* FIXME: move to Word_Lib *)
-lemma word_upcast_shiftr:
-  assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
-  shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
-  apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast)
-  apply (drule test_bit_size)
-  using assms by (simp add: word_size)
-
-lemma word_upcast_neg_msb:
-  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)"
-  unfolding ucast_def msb_word_of_int
-  by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)
-
-(* FIXME: move to Word_Lib *)
-lemma word_upcast_0_sle:
-  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
-  by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
-
-(* FIXME: move to Word_Lib *)
-lemma scast_ucast_up_eq_ucast:
-  assumes "LENGTH('a::len) < LENGTH('b::len)"
-  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
-  using assms
-  apply (subst scast_eq_ucast; simp)
-  apply (simp only: ucast_def msb_word_of_int)
-   apply (metis bin_nth_uint_imp decr_length_less_iff numeral_nat(7) verit_comp_simplify1(3))
-  by (metis less_or_eq_imp_le ucast_nat_def unat_ucast_up_simp)
-
-lemma not_max_word_iff_less:
-  "w \<noteq> max_word \<longleftrightarrow> w < max_word"
-  by (simp add: order_less_le)
-
-lemma ucast_increment:
-  assumes "w \<noteq> max_word"
-  shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)"
-  apply (cases "LENGTH('b) \<le> LENGTH('a)")
-   apply (simp add: ucast_down_add is_down)
-  apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)")
-   apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)")
-    apply (subst word_uint_eq_iff)
-    apply (simp add: uint_arith_simps uint_up_ucast is_up)
-   apply (erule less_trans, rule power_strict_increasing, simp, simp)
-  apply (subst less_diff_eq[symmetric])
-  using assms
-  apply (simp add: not_max_word_iff_less word_less_alt)
-  apply (erule less_le_trans)
-  apply simp
-  done
-
-lemma max_word_gt_0:
-  "0 < max_word"
-  by (simp add: le_neq_trans[OF max_word_max])
-
-lemma and_not_max_word:
-  "m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word"
-  by (simp add: not_max_word_iff_less word_and_less')
-
-lemma mask_not_max_word:
-  "m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)"
-  by (simp add: mask_eq_exp_minus_1)
-
-lemmas and_mask_not_max_word =
-  and_not_max_word[OF mask_not_max_word]
-
-lemma shiftr_not_max_word:
-  "0 < n \<Longrightarrow> w >> n \<noteq> max_word"
-  by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)
-
-lemma word_sandwich1:
-  fixes a b c :: "'a::len word"
-  assumes "a < b"
-  assumes "b <= c"
-  shows "0 < b - a \<and> b - a <= c"
-  using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le
-        word_le_less_eq word_neq_0_conv
-  by metis
-
-lemma word_sandwich2:
-  fixes a b :: "'a::len word"
-  assumes "0 < a"
-  assumes "a <= b"
-  shows "b - a < b"
-  using assms less_le_trans word_diff_less
-  by blast
-
-lemma unat_and_mask_less_2p:
-  fixes w :: "'a::len word"
-  shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m"
-  by (simp add: unat_less_helper  and_mask_less')
-
-lemma unat_shiftr_less_2p:
-  fixes w :: "'a::len word"
-  shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m"
-  by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3)
-
-lemma nat_div_less_mono:
-  fixes m n :: nat
-  shows "m div d < n div d \<Longrightarrow> m < n"
-  by (meson div_le_mono not_less)
-
-lemma word_shiftr_less_mono:
-  fixes w :: "'a::len word"
-  shows "w >> n < v >> n \<Longrightarrow> w < v"
-  by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono)
-
-lemma word_shiftr_less_mask:
-  fixes w :: "'a::len word"
-  shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)"
-  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
-
-lemma word_shiftr_le_mask:
-  fixes w :: "'a::len word"
-  shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)"
-  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
-
-lemma word_shiftr_eq_mask:
-  fixes w :: "'a::len word"
-  shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)"
-  by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq)
-
-lemmas word_shiftr_cmp_mask =
-  word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask
-
-lemma if_if_if_same_output:
-  "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)"
-  by (simp split: if_splits)
-
-lemma word_le_split_mask:
-  "(w \<le> v) \<longleftrightarrow> (w >> n < v >> n \<or> w >> n = v >> n \<and> w && mask n \<le> v && mask n)"
-  apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask)
-  apply (rule subst[where P="\<lambda>c. c \<le> d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]])
-  apply (rule subst[where P="\<lambda>c. d \<le> c = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]])
-  apply (rule iffI)
-   apply safe
-     apply (fold_subgoals (prefix))[2]
-    apply (subst atomize_conj)
-    apply (rule context_conjI)
-     apply (metis AND_NOT_mask_plus_AND_mask_eq neg_mask_mono_le word_le_less_eq)
-    apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_4)
-   apply (metis Groups.add_ac(2) neg_mask_mono_le word_le_less_eq word_not_le word_plus_and_or_coroll2)
-  apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_3)
-  done
-
 lemma unat_ucast_prio_mask_simp[simp]:
   "unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)"
   by (simp add: ucast_and_mask)
@@ -325,19 +151,11 @@ lemma unat_ucast_prio_shiftr_simp[simp]:
   "unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)"
   by simp
 
-lemma from_bool_to_bool_and_1 [simp]:
-  assumes r_size: "1 < size r"
-  shows "from_bool (to_bool (r && 1)) = r && 1"
-proof -
-  from r_size have "r && 1 < 2"
-    by (simp add: and_mask_less_size [where n=1, unfolded mask_def, simplified])
-  thus ?thesis
-    by (fastforce simp add: from_bool_def to_bool_def dest: word_less_cases)
-qed
-
 lemma wb_gt_2:
   "2 < word_bits" by (simp add: word_bits_conv)
 
+declare from_bool_to_bool_and_1[simp]
+
 (* NOTE: unused. *)
 lemma inj_on_option_map:
  "inj_on (map_option f o m) (dom m) \<Longrightarrow> inj_on m (dom m)"
diff --git a/proof/crefine/X64/ADT_C.thy b/proof/crefine/X64/ADT_C.thy
index 049d7689c0..82672f5287 100644
--- a/proof/crefine/X64/ADT_C.thy
+++ b/proof/crefine/X64/ADT_C.thy
@@ -539,6 +539,10 @@ end
 
 context state_rel begin
 
+definition
+  "ioapic_nirqs_to_H cstate \<equiv>
+     \<lambda>x. if x \<le> of_nat maxNumIOAPIC then ioapic_nirqs_' cstate.[unat x] else 0"
+
 definition
   "carch_state_to_H cstate \<equiv>
    X64KernelState
@@ -553,6 +557,7 @@ definition
       x64KSKernelVSpace_C
       (cioport_bitmap_to_H (the (clift (t_hrs_' cstate) (Ptr (symbol_table ''x86KSAllocatedIOPorts'')))))
       (ucast (num_ioapics_' cstate))
+      (ioapic_nirqs_to_H cstate)
       \<comment> \<open>Map IRQ states to their Haskell equivalent, and out-of-bounds entries to X64IRQFree\<close>
       (case_option X64IRQFree id \<circ>
           (array_map_conv
@@ -582,6 +587,8 @@ lemma carch_state_to_H_correct:
   using valid[simplified valid_arch_state'_def]
   apply (fastforce simp: valid_asid_table'_def)
   apply (simp add: ccr3_relation_def split: cr3.splits)
+  apply (rule conjI)
+   apply (solves \<open>clarsimp simp: global_ioport_bitmap_relation_def\<close>)
   apply (rule conjI)
    prefer 2
    apply (rule ext)
@@ -589,7 +596,10 @@ lemma carch_state_to_H_correct:
                          array_to_map_def)
    using valid[simplified valid_arch_state'_def valid_x64_irq_state'_def]
    apply (case_tac "x \<le> maxIRQ"; fastforce split: option.split)
-  apply (clarsimp simp: global_ioport_bitmap_relation_def)
+  apply (clarsimp simp: array_relation_def ioapic_nirqs_to_H_def)
+  apply (rule ext)
+  using valid[simplified valid_arch_state'_def valid_ioapic_def]
+  apply (clarsimp simp: not_le)
   done
 
 end
diff --git a/proof/crefine/X64/Interrupt_C.thy b/proof/crefine/X64/Interrupt_C.thy
index 4f21490401..cb5bced472 100644
--- a/proof/crefine/X64/Interrupt_C.thy
+++ b/proof/crefine/X64/Interrupt_C.thy
@@ -530,32 +530,61 @@ lemma ccorres_pre_gets_x64KSNumIOAPICs_ksArchState:
   apply clarsimp
   done
 
+lemma ccorres_pre_gets_x64KSIOAPICnIRQs_ksArchState:
+  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
+  shows   "ccorres r xf
+                   (\<lambda>s. (\<forall>rv. x64KSIOAPICnIRQs (ksArchState s) = rv  \<longrightarrow> P rv s))
+                   {s. \<forall>rv. s \<in> P' rv } hs
+                   (gets (x64KSIOAPICnIRQs \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
+  apply (rule ccorres_guard_imp)
+    apply (rule ccorres_symb_exec_l)
+       defer
+       apply wp[1]
+      apply (rule gets_sp)
+     apply (clarsimp simp: empty_fail_def simpler_gets_def)
+    apply assumption
+   apply clarsimp
+   defer
+   apply (rule ccorres_guard_imp)
+     apply (rule cc)
+    apply clarsimp
+   apply assumption
+  apply clarsimp
+  done
+
+lemma rf_sr_x64KSIOAPICnIRQs:
+  "\<lbrakk> (s,s') \<in> rf_sr; i < of_nat maxNumIOAPIC \<rbrakk> \<Longrightarrow>
+   ioapic_nirqs_' (globals s').[unat i] = x64KSIOAPICnIRQs (ksArchState s) i"
+  by (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def
+                     array_relation_def)
+
 lemma ioapic_decode_map_pin_to_vector_ccorres:
   "ccorres (intr_and_se_rel \<currency> dc)
      (liftxf errstate id (K ()) ret__unsigned_long_')
-     \<top>
-     (UNIV
-           \<inter> {s. ioapic___unsigned_long_' s = ioapic}
-           \<inter> {s. pin___unsigned_long_' s = pin}
-           \<inter> {s. level___unsigned_long_' s = level}
-           \<inter> {s. polarity_' s = polarity})
+     valid_ioapic
+     (\<lbrace>\<acute>ioapic___unsigned_long = ioapic\<rbrace> \<inter>
+      \<lbrace>\<acute>pin___unsigned_long = pin\<rbrace> \<inter>
+      \<lbrace>\<acute>level___unsigned_long = level\<rbrace> \<inter>
+      \<lbrace>\<acute>polarity = polarity\<rbrace>)
      hs
      (doE numIOAPICs <- liftE (gets (x64KSNumIOAPICs \<circ> ksArchState));
+          ioapic_nirqs <- liftE (gets (x64KSIOAPICnIRQs \<circ> ksArchState));
           whenE (numIOAPICs = 0) (throwError (Inl IllegalOperation));
           whenE (uint (numIOAPICs - 1) < uint ioapic)
-                     (throwError (Inl (RangeError 0 (numIOAPICs - 1))));
-          whenE (uint (ioapicIRQLines - 1) < uint pin)
-                     (throwError (Inl (RangeError 0 (ioapicIRQLines - 1))));
+                (throwError (Inl (RangeError 0 (numIOAPICs - 1))));
+          whenE (uint (ucast (ioapic_nirqs ioapic - 1) :: machine_word) < uint pin)
+                (throwError (Inl (RangeError 0 (ucast (ioapic_nirqs ioapic - 1)))));
           whenE (1 < uint level) (throwError (Inl (RangeError 0 1)));
           whenE (1 < uint polarity) (throwError (Inl (RangeError 0 1)))
        odE)
-    (Call ioapic_decode_map_pin_to_vector_'proc)"
-  supply Collect_const[simp del]
+     (Call ioapic_decode_map_pin_to_vector_'proc)"
+  supply Collect_const[simp del] word_less_1[simp del] (* for uniform array guard on ioapic_nirqs *)
   apply (cinit' lift: ioapic___unsigned_long_' pin___unsigned_long_' level___unsigned_long_'
                       polarity_')
    apply (simp add: ioapicIRQLines_def cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (clarsimp simp: liftE_bindE)
    apply (rule ccorres_pre_gets_x64KSNumIOAPICs_ksArchState)
+   apply (rule ccorres_pre_gets_x64KSIOAPICnIRQs_ksArchState)
    apply (rule_tac Q="\<lambda>s. x64KSNumIOAPICs (ksArchState s) = numIOAPICs" and Q'=\<top>
                    in ccorres_split_when_throwError_cond)
       apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def)
@@ -573,23 +602,55 @@ lemma ioapic_decode_map_pin_to_vector_ccorres:
                             EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def syscall_error_rel_def)
       apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def)
       apply (subst ucast_sub_ucast; fastforce simp: lt1_neq0)
+     apply (rule_tac P="numIOAPICs \<le> of_nat maxNumIOAPIC" in ccorres_gen_asm)
+     apply (clarsimp simp: not_less word_le_def[symmetric])
+     apply (prop_tac "ioapic < of_nat maxNumIOAPIC",
+            solves \<open>simp add: le_m1_iff_lt[THEN iffD1] word_neq_0_conv\<close>)
+     apply (rule ccorres_prove_guard)
+      (* array guard where array dimension is maxNumIOAPIC *)
+      apply (solves \<open>simp add: Kernel_Config.maxNumIOAPIC_def\<close>)
+     apply ccorres_rewrite
+     apply (rename_tac ioapic_nirqs)
+     apply (rule_tac Q="\<lambda>s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \<and>
+                            0 < x64KSIOAPICnIRQs (ksArchState s) ioapic" and
+                     Q'=\<top>
+                     in ccorres_split_when_throwError_cond)
+        apply (fastforce simp: word_le_def scast_ucast_up_eq_ucast uint_up_ucast is_up
+                               rf_sr_x64KSIOAPICnIRQs
+                               uint_minus_1_less_le_eq)
+      (* Need to VCG it as the range error depends on the global state *)
+      apply (rule_tac P="\<lambda>s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \<and>
+                             numIOAPICs \<le> of_nat maxNumIOAPIC \<and>
+                             0 < x64KSIOAPICnIRQs (ksArchState s) ioapic \<and>
+                             x64KSIOAPICnIRQs (ksArchState s) ioapic \<le> ucast ioapicIRQLines"
+                  and P'="UNIV" in ccorres_from_vcg_throws)
+      apply (rule allI, rule conseqPre, vcg)
+      apply (clarsimp simp: fst_throwError_returnOk syscall_error_to_H_cases
+                            EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def syscall_error_rel_def)
+      apply (simp add: rf_sr_x64KSIOAPICnIRQs
+                       scast_ucast_up_eq_ucast ioapicIRQLines_def sint_ucast_eq_uint is_down
+                       scast_ucast_up_minus_1_ucast)
+      apply (rule conjI, uint_arith)
+      apply (rule conjI, uint_arith)
+      (* array guard where array dimension is maxNumIOAPIC *)
+      apply (solves \<open>simp add: Kernel_Config.maxNumIOAPIC_def\<close>)
      apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_split_when_throwError_cond)
-        apply (fastforce simp: word_le_def add1_zle_eq[symmetric])
+        apply clarsimp
+        apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1
+                     word_neq_0_conv word_sub_less_iff)
        apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n)
-      apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_split_when_throwError_cond)
+      apply (rule_tac Q=\<top> and Q'=\<top>
+                      in ccorres_split_when_throwError_cond[where b="returnOk ()", simplified])
          apply clarsimp
          apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1
                       word_neq_0_conv word_sub_less_iff)
         apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n)
-       apply (rule_tac Q=\<top> and Q'=\<top>
-                       in ccorres_split_when_throwError_cond[where b="returnOk ()", simplified])
-          apply clarsimp
-          apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1
-                       word_neq_0_conv word_sub_less_iff)
-         apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n)
-        apply (ctac add: ccorres_return_CE)
-       apply vcg+
-  apply fastforce
+       apply (ctac add: ccorres_return_CE)
+      apply vcg+
+  apply (clarsimp simp: not_less)
+  apply (prop_tac "ioapic < x64KSNumIOAPICs (ksArchState s)")
+   apply (meson word_leq_minus_one_le word_less_eq_iff_unsigned)
+  apply (fastforce simp: valid_ioapic_def)
   done
 
 (* Bundle of definitions for minIRQ, maxIRQ, minUserIRQ, etc *)
@@ -867,11 +928,8 @@ from assms show ?thesis
                                     invs_sch_act_wf' ct_in_state'_def cte_wp_at_weakenE'
                                     pred_tcb'_weakenE invs_pspace_aligned' invs_pspace_distinct')
               apply (subst pred_tcb'_weakenE, assumption, fastforce)+
-              apply (rule conjI)
-               apply (rule TrueI)
-              apply (rule conjI)
-               apply (rule impI)
-               apply (rule TrueI)
+              apply (rule conjI, fastforce)
+              apply clarsimp
               apply (rule_tac irq1="yf" in irq64_helper_two)
               apply (simp only: unat_def)
              apply (vcg exspec=isIRQActive_modifies)
diff --git a/proof/crefine/X64/SR_lemmas_C.thy b/proof/crefine/X64/SR_lemmas_C.thy
index e5103dbdf9..8b00610a92 100644
--- a/proof/crefine/X64/SR_lemmas_C.thy
+++ b/proof/crefine/X64/SR_lemmas_C.thy
@@ -1065,7 +1065,6 @@ lemma cstate_relation_only_t_hrs:
   ksCurThread_' s = ksCurThread_' t;
   ksIdleThread_' s = ksIdleThread_' t;
   ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t;
-  intStateIRQNode_' s = intStateIRQNode_' t;
   intStateIRQTable_' s = intStateIRQTable_' t;
   x86KSASIDTable_' s = x86KSASIDTable_' t;
   x64KSCurrentUserCR3_' s = x64KSCurrentUserCR3_' t;
@@ -1075,6 +1074,7 @@ lemma cstate_relation_only_t_hrs:
   ksCurDomain_' s = ksCurDomain_' t;
   ksDomainTime_' s = ksDomainTime_' t;
   num_ioapics_' s = num_ioapics_' t;
+  ioapic_nirqs_' s = ioapic_nirqs_' t;
   x86KSIRQState_' s = x86KSIRQState_' t
   \<rbrakk>
   \<Longrightarrow> cstate_relation a s = cstate_relation a t"
@@ -1091,7 +1091,6 @@ lemma rf_sr_upd:
     "(ksCurThread_' (globals x)) = (ksCurThread_' (globals y))"
     "(ksIdleThread_' (globals x)) = (ksIdleThread_' (globals y))"
     "(ksWorkUnitsCompleted_' (globals x)) = (ksWorkUnitsCompleted_' (globals y))"
-    "intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)"
     "intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)"
     "x86KSASIDTable_' (globals x) = x86KSASIDTable_' (globals y)"
     "x64KSCurrentUserCR3_' (globals x) = x64KSCurrentUserCR3_' (globals y)"
@@ -1101,6 +1100,7 @@ lemma rf_sr_upd:
     "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)"
     "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)"
     "num_ioapics_' (globals x) = num_ioapics_' (globals y)"
+    "ioapic_nirqs_' (globals x) = ioapic_nirqs_' (globals y)"
     "x86KSIRQState_' (globals x) = x86KSIRQState_' (globals y)"
   shows "((a, x) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
   unfolding rf_sr_def using assms
@@ -1114,7 +1114,6 @@ lemma rf_sr_upd_safe[simp]:
   and     sa: "(ksSchedulerAction_' (globals (g y))) = (ksSchedulerAction_' (globals y))"
   and     ct: "(ksCurThread_' (globals (g y))) = (ksCurThread_' (globals y))"
   and     it: "(ksIdleThread_' (globals (g y))) = (ksIdleThread_' (globals y))"
-  and     isn: "intStateIRQNode_'(globals (g y)) = intStateIRQNode_' (globals y)"
   and     ist: "intStateIRQTable_'(globals (g y)) = intStateIRQTable_' (globals y)"
   and     dsi: "ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)"
   and     cdom: "ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)"
@@ -1124,11 +1123,12 @@ lemma rf_sr_upd_safe[simp]:
     "x64KSCurrentUserCR3_' (globals (g y)) = x64KSCurrentUserCR3_' (globals y)"
     "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)"
     "num_ioapics_' (globals (g y)) = num_ioapics_' (globals y)"
+    "ioapic_nirqs_' (globals (g y)) = ioapic_nirqs_' (globals y)"
     "x86KSIRQState_' (globals (g y)) = x86KSIRQState_' (globals y)"
   and    gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)"
   and     wu:  "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))"
   shows "((a, (g y)) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
-  using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd)
+  using assms by - (rule rf_sr_upd)
 
 (* More of a well-formed lemma, but \<dots> *)
 lemma valid_mdb_cslift_next:
diff --git a/proof/crefine/X64/StateRelation_C.thy b/proof/crefine/X64/StateRelation_C.thy
index 0701acd80b..0f17b0fbc4 100644
--- a/proof/crefine/X64/StateRelation_C.thy
+++ b/proof/crefine/X64/StateRelation_C.thy
@@ -191,6 +191,7 @@ where
     global_ioport_bitmap_relation (clift (t_hrs_' cstate)) (x64KSAllocatedIOPorts astate) \<and>
     fpu_null_state_relation (t_hrs_' cstate) \<and>
     x64KSNumIOAPICs astate = UCAST (32 \<rightarrow> 64) (num_ioapics_' cstate) \<and>
+    array_relation (=) (of_nat Kernel_Config.maxNumIOAPIC) (x64KSIOAPICnIRQs astate) (ioapic_nirqs_' cstate) \<and>
     array_relation x64_irq_state_relation maxIRQ (x64KSIRQState astate) (x86KSIRQState_' cstate) \<and>
     carch_globals astate"
 
diff --git a/proof/crefine/lib/Ctac.thy b/proof/crefine/lib/Ctac.thy
index f07db59f25..e5b71f8994 100644
--- a/proof/crefine/lib/Ctac.thy
+++ b/proof/crefine/lib/Ctac.thy
@@ -1949,6 +1949,18 @@ lemmas ccorres_move_const_guards
     = ccorres_move_const_guard
       ccorres_move_const_guard[unfolded Collect_const]
 
+lemma ccorres_prove_guard_direct:
+  "\<lbrakk> G; ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c) \<rbrakk> \<Longrightarrow>
+   ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (Guard F \<lbrace>G\<rbrace> c)"
+  by (rule ccorres_guard_imp, erule ccorres_move_const_guard; simp)
+
+lemma ccorres_prove_guard_seq:
+  "\<lbrakk> G; ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c;; d) \<rbrakk> \<Longrightarrow>
+   ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (Guard F \<lbrace>G\<rbrace> c;; d)"
+  by (rule ccorres_guard_imp, erule ccorres_move_const_guard; simp)
+
+lemmas ccorres_prove_guard = ccorres_prove_guard_direct ccorres_prove_guard_seq
+
 lemma liftM_exs_valid:
   "\<lbrace>P\<rbrace> m \<exists>\<lbrace>\<lambda>rv. Q (f rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<exists>\<lbrace>Q\<rbrace>"
   unfolding liftM_def exs_valid_def
diff --git a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy
index ac133c90da..5be572964a 100644
--- a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy
+++ b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy
@@ -20,8 +20,7 @@ where
                     real_cte_at dest_slot and
                     (\<lambda>s. ioapic < x64_num_ioapics (arch_state s)) and
                     K (minUserIRQ \<le> irq \<and> irq \<le> maxUserIRQ \<and>
-                       pin < ioapicIRQLines \<and> level < 2 \<and>
-                       polarity < 2))"
+                       level < 2 \<and> polarity < 2))"
 | "arch_irq_control_inv_valid_real (IssueIRQHandlerMSI irq dest_slot src_slot bus dev func handle)
       = (cte_wp_at ((=) NullCap) dest_slot and
                     cte_wp_at ((=) IRQControlCap) src_slot and
diff --git a/proof/refine/X64/ADT_H.thy b/proof/refine/X64/ADT_H.thy
index b83baca500..d736b254d3 100644
--- a/proof/refine/X64/ADT_H.thy
+++ b/proof/refine/X64/ADT_H.thy
@@ -1949,13 +1949,14 @@ where
 
 definition
   "absArchState s' \<equiv>
-   case s' of X64KernelState asid_tbl gpm gpdpts gpds gpts ccr3 kvspace kports num_ioapics irq_states \<Rightarrow>
+   case s' of X64KernelState asid_tbl gpm gpdpts gpds gpts ccr3 kvspace kports num_ioapics ioapics_nirqs irq_states \<Rightarrow>
      \<lparr>x64_asid_table = asid_tbl \<circ> ucast, x64_global_pml4 = gpm,
       x64_kernel_vspace = kvspace, x64_global_pts = gpts,
       x64_global_pdpts = gpdpts, x64_global_pds = gpds,
       x64_current_cr3 = absCR3 ccr3,
       x64_allocated_io_ports = kports,
       x64_num_ioapics = num_ioapics,
+      x64_ioapic_nirqs = ioapics_nirqs,
       x64_irq_state = x64irqstate_to_abstract \<circ> irq_states\<rparr>"
 
 lemma cr3_expand_unexpand[simp]: "cr3 (cr3_base_address a) (cr3_pcid a) = a"
diff --git a/proof/refine/X64/Init_R.thy b/proof/refine/X64/Init_R.thy
index b129d1dc9a..844799594f 100644
--- a/proof/refine/X64/Init_R.thy
+++ b/proof/refine/X64/Init_R.thy
@@ -41,6 +41,7 @@ definition zeroed_arch_abstract_state ::
     x64_current_cr3        = cr3 0 0 ,
     x64_allocated_io_ports = \<bottom>,
     x64_num_ioapics        = 0,
+    x64_ioapic_nirqs       = K 0,
     x64_irq_state          = K IRQFree\<rparr>"
 
 definition zeroed_main_abstract_state ::
@@ -83,7 +84,7 @@ definition zeroed_arch_intermediate_state ::
   Arch.kernel_state
   where
   "zeroed_arch_intermediate_state \<equiv> X64KernelState Map.empty 0 [] [] [] (CR3 0 0)
-     (K X64VSpaceUserRegion) \<bottom> 0 (K X64IRQFree)"
+     (K X64VSpaceUserRegion) \<bottom> 0 (K 0) (K X64IRQFree)"
 
 definition zeroed_intermediate_state ::
   global.kernel_state
diff --git a/proof/refine/X64/Interrupt_R.thy b/proof/refine/X64/Interrupt_R.thy
index 9c696b7625..f797f8fdd3 100644
--- a/proof/refine/X64/Interrupt_R.thy
+++ b/proof/refine/X64/Interrupt_R.thy
@@ -200,6 +200,10 @@ lemmas irq_const_defs =
   maxIRQ_def minIRQ_def
   X64.maxUserIRQ_def X64.minUserIRQ_def X64_H.maxUserIRQ_def X64_H.minUserIRQ_def
 
+lemma corres_gets_ioapic_nirqs [corres]:
+  "corres (=) \<top> \<top> (gets (x64_ioapic_nirqs \<circ> arch_state)) (gets (x64KSIOAPICnIRQs \<circ> ksArchState))"
+  by (simp add: state_relation_def arch_state_relation_def)
+
 lemma arch_decodeIRQControlInvocation_corres:
   "list_all2 cap_relation caps caps' \<Longrightarrow>
    corres (ser \<oplus> arch_irq_control_inv_relation)
@@ -257,12 +261,13 @@ lemma arch_decodeIRQControlInvocation_corres:
          apply (rule corres_splitEE[OF ensureEmptySlot_corres])
             apply simp
            apply (rule corres_split[OF corres_gets_num_ioapics])
-             apply (rule whenE_throwError_corres, ((simp add: ioapicIRQLines_def)+)[2])+
-             apply (rule corres_returnOkTT)
-             apply (clarsimp simp: arch_irq_control_inv_relation_def )
-            apply (wpsimp wp: isIRQActive_inv
-                        simp: invs_valid_objs invs_psp_aligned invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
-                   | wp (once) hoare_drop_imps)+
+             apply (rule corres_split[OF corres_gets_ioapic_nirqs])
+               apply (rule whenE_throwError_corres, ((simp add: ioapicIRQLines_def)+)[2])+
+               apply (rule corres_returnOkTT)
+               apply (clarsimp simp: arch_irq_control_inv_relation_def )
+              apply (wpsimp wp: isIRQActive_inv
+                          simp: invs_valid_objs invs_psp_aligned invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
+                     | wp (once) hoare_drop_imps)+
   by (auto split: arch_invocation_label.splits invocation_label.splits)
 
 lemma irqhandler_simp[simp]:
diff --git a/proof/refine/X64/Invariants_H.thy b/proof/refine/X64/Invariants_H.thy
index 892e995337..b237e71d45 100644
--- a/proof/refine/X64/Invariants_H.thy
+++ b/proof/refine/X64/Invariants_H.thy
@@ -1178,9 +1178,20 @@ definition
 where
   "valid_x64_irq_state' irqState \<equiv> \<forall>irq > maxIRQ. irqState irq = X64IRQFree"
 
-definition
-  valid_arch_state' :: "kernel_state \<Rightarrow> bool"
-where
+definition valid_ioapic_2 :: "machine_word \<Rightarrow> (machine_word \<Rightarrow> 8 word) \<Rightarrow> bool" where
+  "valid_ioapic_2 num_ioapics ioapic_nirqs \<equiv>
+    num_ioapics \<le> of_nat Kernel_Config.maxNumIOAPIC \<and>
+    (\<forall>ioapic < num_ioapics. 0 < ioapic_nirqs ioapic) \<and>
+    (\<forall>ioapic < num_ioapics. ioapic_nirqs ioapic \<le> ucast ioapicIRQLines) \<and>
+    (\<forall>ioapic > of_nat Kernel_Config.maxNumIOAPIC. ioapic_nirqs ioapic = 0)"
+
+abbreviation valid_ioapic where
+  "valid_ioapic s \<equiv>
+     valid_ioapic_2 (x64KSNumIOAPICs (ksArchState s)) (x64KSIOAPICnIRQs (ksArchState s))"
+
+lemmas valid_ioapic_def = valid_ioapic_2_def
+
+definition valid_arch_state' :: "kernel_state \<Rightarrow> bool" where
   "valid_arch_state' \<equiv> \<lambda>s.
   valid_asid_table' (x64KSASIDTable (ksArchState s)) s \<and>
   valid_cr3' (x64KSCurrentUserCR3 (ksArchState s)) \<and>
@@ -1188,7 +1199,8 @@ where
   valid_global_pds' (x64KSSKIMPDs (ksArchState s)) s \<and>
   valid_global_pdpts' (x64KSSKIMPDPTs (ksArchState s)) s \<and>
   valid_global_pts' (x64KSSKIMPTs (ksArchState s)) s \<and>
-  valid_x64_irq_state' (x64KSIRQState (ksArchState s))"
+  valid_x64_irq_state' (x64KSIRQState (ksArchState s)) \<and>
+  valid_ioapic s"
 
 definition
   irq_issued' :: "irq \<Rightarrow> kernel_state \<Rightarrow> bool"
@@ -3461,6 +3473,10 @@ lemma invs_valid_global'[elim!]:
   "invs' s \<Longrightarrow> valid_global_refs' s"
   by (fastforce simp: invs'_def valid_state'_def)
 
+lemma invs_valid_ioapic[elim!]:
+  "invs' s \<Longrightarrow> valid_ioapic s"
+  by (simp add: invs'_def valid_state'_def valid_arch_state'_def)
+
 lemma invs'_invs_no_cicd:
   "invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s"
   by (simp add: invs'_to_invs_no_cicd'_def)
diff --git a/proof/refine/X64/StateRelation.thy b/proof/refine/X64/StateRelation.thy
index 1df131c221..f8b3c00bd3 100644
--- a/proof/refine/X64/StateRelation.thy
+++ b/proof/refine/X64/StateRelation.thy
@@ -556,6 +556,7 @@ where
        \<and> x64_kernel_vspace s = x64KSKernelVSpace s'
        \<and> x64_allocated_io_ports s = x64KSAllocatedIOPorts s'
        \<and> x64_num_ioapics s = x64KSNumIOAPICs s'
+       \<and> x64_ioapic_nirqs s = x64KSIOAPICnIRQs s'
        \<and> x64_irq_relation (x64_irq_state s) (x64KSIRQState s')}"
 
 definition
diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy
index 1dbddd19a0..24a8aa9b3b 100644
--- a/spec/abstract/X64/ArchDecode_A.thy
+++ b/spec/abstract/X64/ArchDecode_A.thy
@@ -68,13 +68,11 @@ definition
         dest_slot \<leftarrow> lookup_target_slot cnode (data_to_cptr index) (unat depth);
         ensure_empty dest_slot;
 
-       \<comment> \<open>Following should be wrapped in to a function like what c did
-          since it is pc99 related, problem is where to put this function\<close>
-
         numIOAPICs \<leftarrow> liftE $ gets (x64_num_ioapics \<circ> arch_state);
+        ioapic_nirqs \<leftarrow> liftE $ gets (x64_ioapic_nirqs \<circ> arch_state);
         whenE (numIOAPICs = 0) $ throwError IllegalOperation;
         whenE (ioapic > numIOAPICs - 1) $ throwError (RangeError 0 (numIOAPICs-1));
-        whenE (pin > ioapicIRQLines - 1) $ throwError (RangeError 0 (ioapicIRQLines-1));
+        whenE (pin > ucast (ioapic_nirqs ioapic - 1)) $ throwError (RangeError 0 (ucast (ioapic_nirqs ioapic - 1)));
         whenE (level > 1) $ throwError (RangeError 0 1);
         whenE (polarity > 1) $ throwError (RangeError 0 1);
 
diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy
index 7b23358337..8d35283924 100644
--- a/spec/abstract/X64/Arch_Structs_A.thy
+++ b/spec/abstract/X64/Arch_Structs_A.thy
@@ -310,6 +310,7 @@ record arch_state =
   x64_current_cr3           :: "X64_A.cr3"
   x64_allocated_io_ports    :: "X64_A.io_port \<Rightarrow> bool"
   x64_num_ioapics           :: "64 word"
+  x64_ioapic_nirqs          :: "machine_word \<Rightarrow> 8 word"
   x64_irq_state             :: "8 word \<Rightarrow> X64_A.X64IRQState"
 
 (* FIXME x64-vtd:
diff --git a/spec/abstract/X64/Init_A.thy b/spec/abstract/X64/Init_A.thy
index 1d78c1a7de..45e1f95c65 100644
--- a/spec/abstract/X64/Init_A.thy
+++ b/spec/abstract/X64/Init_A.thy
@@ -56,6 +56,7 @@ definition
     x64_current_cr3 = cr3 0 0,
     x64_allocated_io_ports = \<lambda>_. False,
     x64_num_ioapics = 1,
+    x64_ioapic_nirqs = \<lambda>_. ucast ioapicIRQLines,
     x64_irq_state = K IRQFree
    \<rparr>"
 
diff --git a/spec/cspec/c/gen-config-thy.py b/spec/cspec/c/gen-config-thy.py
index 730489b7a3..3a9746508c 100755
--- a/spec/cspec/c/gen-config-thy.py
+++ b/spec/cspec/c/gen-config-thy.py
@@ -170,6 +170,7 @@
     'CONFIG_CTZ_64': (bool, None),
     'CONFIG_CLZ_NO_BUILTIN': (bool, None),
     'CONFIG_CTZ_NO_BUILTIN': (bool, None),
+    'CONFIG_MAX_NUM_IOAPIC': (nat, 'maxNumIOAPIC'),
 }
 
 
diff --git a/spec/haskell/src/SEL4/Model/StateData/X64.lhs b/spec/haskell/src/SEL4/Model/StateData/X64.lhs
index 73659eeeb5..7e99bd1d79 100644
--- a/spec/haskell/src/SEL4/Model/StateData/X64.lhs
+++ b/spec/haskell/src/SEL4/Model/StateData/X64.lhs
@@ -16,6 +16,7 @@ This module contains the architecture-specific kernel global data for the X86-64
 > import SEL4.Object.Structures.X64
 
 > import Data.Array
+> import Data.Word(Word8)
 
 \end{impdetails}
 
@@ -32,17 +33,17 @@ This module contains the architecture-specific kernel global data for the X86-64
 > gdteBits = 3
 
 > data KernelState = X64KernelState {
->     x64KSASIDTable      :: Array ASID (Maybe (PPtr ASIDPool)),
->     x64KSSKIMPML4       :: PPtr PML4E,
->     x64KSSKIMPDPTs      :: [PPtr PDPTE],
->     x64KSSKIMPDs        :: [PPtr PDE],
->     x64KSSKIMPTs        :: [PPtr PTE],
->     x64KSCurrentUserCR3 :: CR3,
->     x64KSKernelVSpace :: PPtr Word -> X64VSpaceRegionUse,
+>     x64KSASIDTable        :: Array ASID (Maybe (PPtr ASIDPool)),
+>     x64KSSKIMPML4         :: PPtr PML4E,
+>     x64KSSKIMPDPTs        :: [PPtr PDPTE],
+>     x64KSSKIMPDs          :: [PPtr PDE],
+>     x64KSSKIMPTs          :: [PPtr PTE],
+>     x64KSCurrentUserCR3   :: CR3,
+>     x64KSKernelVSpace     :: PPtr Word -> X64VSpaceRegionUse,
 >     x64KSAllocatedIOPorts :: Array IOPort Bool,
->     x64KSNumIOAPICs :: Word,
->     x64KSIRQState :: Array IRQ X64IRQState}
+>     x64KSNumIOAPICs       :: Word,
+>     x64KSIOAPICnIRQs      :: Word -> Word8,
+>     x64KSIRQState         :: Array IRQ X64IRQState}
 
 > newKernelState :: PAddr -> (KernelState, [PAddr])
 > newKernelState _ = error "No initial state defined for x64"
-
diff --git a/spec/haskell/src/SEL4/Object/Interrupt/X64.lhs b/spec/haskell/src/SEL4/Object/Interrupt/X64.lhs
index 6135fbc618..0e3ccfe14c 100644
--- a/spec/haskell/src/SEL4/Object/Interrupt/X64.lhs
+++ b/spec/haskell/src/SEL4/Object/Interrupt/X64.lhs
@@ -59,14 +59,14 @@ This module defines the machine-specific interrupt handling routines for x64.
 >
 >             -- from ioapic_map_pin_to_vector
 >             numIOAPICs <- withoutFailure $ gets (x64KSNumIOAPICs . ksArchState)
+>             ioAPICnIRQs <- withoutFailure $ gets (x64KSIOAPICnIRQs . ksArchState)
 >             when (numIOAPICs == 0) $ throw IllegalOperation
 >             rangeCheck ioapic 0 (numIOAPICs - 1)
->             rangeCheck pin 0 (Arch.ioapicIRQLines - 1)
+>             rangeCheck pin 0 (ioAPICnIRQs ioapic - 1)
 >             rangeCheck level (0::Word) 1
 >             rangeCheck polarity (0::Word) 1
 >
->             -- FIXME check semantics against toEnum, we might want == 0 here
->             let vector = (fromIntegral $ fromEnum irq) + Arch.irqIntOffset
+>             let vector = fromIntegral (fromEnum irq) + Arch.irqIntOffset
 >             return $ ArchInv.IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic
 >                 pin level polarity vector
 >