adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

x64: ainvs: refine: changes for IRQ invocations (VER-879)

This commit is contained in:
Michael Sproul 2018-05-07 15:41:55 +10:00 committed by Joel Beeren
parent 0b978bae61
commit 43f482ab26
10 changed files with 171 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/invariant-abstract/X64/ArchBCorres2_AI.thy
View File

@ -32,6 +32,8 @@ crunch (bcorres)bcorres[wp]: set_mcpriority,arch_tcb_set_ipc_buffer truncate_sta
crunch (bcorres)bcorres[wp, BCorres2_AI_assms]: arch_get_sanitise_register_info, arch_post_modify_registers truncate_state
crunch (bcorres)bcorres[wp]: updateIRQState truncate_state
lemma invoke_tcb_bcorres[wp]:
fixes a
shows "bcorres (invoke_tcb a) (invoke_tcb a)"

2
proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
View File

@ -18,7 +18,7 @@ named_theorems EmptyFail_AI_assms
crunch_ignore (empty_fail)
(add: invalidateTLBEntry_impl invalidateTranslationSingleASID_impl
invalidateASID_impl ioapicMapPinToVector_impl updateIRQState_impl
invalidateASID_impl ioapicMapPinToVector_impl
in8_impl in16_impl in32_impl out8_impl out16_impl out32_impl)
lemma invalidateLocalPageStructureCacheASID_ef[simp,wp]:

85
proof/invariant-abstract/X64/ArchInterrupt_AI.thy
View File

@ -22,7 +22,8 @@ where
cte_wp_at (op = IRQControlCap) src_slot and
ex_cte_cap_wp_to is_cnode_cap dest_slot and
real_cte_at dest_slot and
K (irq \<le> maxIRQ \<and> ioapic < numIOAPICs \<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))"
| "arch_irq_control_inv_valid_real (IssueIRQHandlerMSI irq dest_slot src_slot bus dev func handle)
@ -30,7 +31,8 @@ where
cte_wp_at (op = IRQControlCap) src_slot and
ex_cte_cap_wp_to is_cnode_cap dest_slot and
real_cte_at dest_slot and
K (irq \<le> maxIRQ \<and> bus \<le> maxPCIBus \<and> dev \<le> maxPCIDev \<and> func \<le> maxPCIFunc))"
K (minUserIRQ \<le> irq \<and> irq \<le> maxUserIRQ \<and>
bus \<le> maxPCIBus \<and> dev \<le> maxPCIDev \<and> func \<le> maxPCIFunc))"
defs arch_irq_control_inv_valid_def:
"arch_irq_control_inv_valid \<equiv> arch_irq_control_inv_valid_real"
@ -54,10 +56,26 @@ context begin
private method cap_hammer = (((drule_tac x="caps ! 0" in bspec)+, (rule nth_mem, fastforce)+),
solves \<open>(clarsimp simp: cte_wp_at_eq_simp)\<close>)
private method word_hammer = solves \<open>(clarsimp simp: not_less maxIRQ_def numIOAPICs_def ioapicIRQLines_def
private method word_hammer = solves \<open>(clarsimp simp: not_less maxIRQ_def ioapicIRQLines_def
maxPCIDev_def maxPCIBus_def maxPCIFunc_def,
(word_bitwise, auto?)?)[1]\<close>
lemma irq_plus_min_ge_min:
"irq \<le> maxUserIRQ - minUserIRQ \<Longrightarrow>
minUserIRQ \<le> irq + minUserIRQ"
apply (clarsimp simp: minUserIRQ_def maxUserIRQ_def)
apply (subst add.commute)
apply (rule no_olen_add_nat[THEN iffD2])
apply (clarsimp simp: unat_ucast word_le_nat_alt)
done
lemma irq_plus_min_le_max:
"irq \<le> maxUserIRQ - minUserIRQ \<Longrightarrow>
irq + minUserIRQ \<le> maxUserIRQ"
apply (clarsimp simp: minUserIRQ_def maxUserIRQ_def)
apply (subst add.commute)
apply (clarsimp simp: Word.le_plus)
done
lemma arch_decode_irq_control_valid[wp]:
"\<lbrace>\<lambda>s. invs s \<and> (\<forall>cap \<in> set caps. s \<turnstile> cap)
@ -72,10 +90,16 @@ lemma arch_decode_irq_control_valid[wp]:
cong: if_cong)
apply (rule hoare_pre)
apply (wp ensure_empty_stronger hoare_vcg_const_imp_lift_R hoare_vcg_const_imp_lift
| simp add: cte_wp_at_eq_simp split del: if_split
| wpc | wp_once hoare_drop_imps)+
apply clarsimp
by (safe; (cap_hammer | word_hammer))
| simp add: cte_wp_at_eq_simp split del: if_split
| wpc
| wp hoare_vcg_imp_lift_R[where P="\<lambda>rv s. \<not> x64_num_ioapics (arch_state s) - 1 < args ! 2"]
| wp hoare_vcg_imp_lift_R[where P="\<lambda>rv s. x64_num_ioapics (arch_state s) \<noteq> 0"]
| wp_once hoare_drop_imps)+
apply (safe; clarsimp simp: word_le_not_less[symmetric] minus_one_helper5
ucast_id irq_plus_min_ge_min irq_plus_min_le_max
| cap_hammer
| word_hammer)+
done
end
@ -199,22 +223,21 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]:
done
qed
crunch device_state_inv[wp]: updateIRQState, ioapicMapPinToVector "\<lambda>ms. P (device_state ms)"
crunch device_state_inv[wp]: ioapicMapPinToVector "\<lambda>ms. P (device_state ms)"
(* FIXME x64: move to Machine_AI *)
lemma no_irq_updateIRQState: "no_irq (updateIRQState vs asid)"
by (wp no_irq | clarsimp simp: no_irq_def updateIRQState_def)+
lemmas updateIRQState_irq_masks = no_irq[OF no_irq_updateIRQState]
lemma dmo_updateIRQState[wp]: "\<lbrace>invs\<rbrace> do_machine_op (updateIRQState irq b) \<lbrace>\<lambda>y. invs\<rbrace>"
apply (wp dmo_invs)
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply ((clarsimp simp: updateIRQState_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+)[3]
apply(erule (1) use_valid[OF _ updateIRQState_irq_masks])
lemma updateIRQState_invs[wp]:
"\<lbrace>invs and K (irq \<le> maxIRQ)\<rbrace>
updateIRQState irq state
\<lbrace>\<lambda>_. invs\<rbrace>"
apply (clarsimp simp: updateIRQState_def)
apply wp
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_global_refs_def
global_refs_def valid_arch_state_def valid_vspace_objs_def
valid_arch_caps_def valid_vs_lookup_def vs_lookup_def vs_lookup_pages_def
vs_lookup_pages1_def valid_table_caps_def empty_table_def second_level_tables_def
valid_global_objs_def valid_kernel_mappings_def valid_asid_map_def
valid_x64_irq_state_def valid_ioports_def all_ioports_issued_def
issued_ioports_def Word_Lemmas.word_not_le[symmetric])
done
lemma no_irq_ioapicMapPinToVector: "no_irq (ioapicMapPinToVector a b c d e)"
@ -232,6 +255,18 @@ lemma dmo_ioapicMapPinToVector[wp]: "\<lbrace>invs\<rbrace> do_machine_op (ioapi
apply(erule (1) use_valid[OF _ ioapicMapPinToVector_irq_masks])
done
crunches updateIRQState
for real_cte_at[wp]: "real_cte_at x"
and cte_wp_at[wp]: "\<lambda>s. P (cte_wp_at Q slot s)"
and cdt[wp]: "\<lambda>s. P (cdt s)"
and ex_cte_cap_wp_to[wp]: "ex_cte_cap_wp_to a b"
and valid_objs[wp]: "valid_objs"
and pspace_distinct[wp]: "pspace_distinct"
and pspace_aligned[wp]: "pspace_aligned"
and valid_mdb[wp]: "valid_mdb"
and kheap[wp]: "\<lambda>s. P (kheap s)"
(simp: ex_cte_cap_wp_to_def)
lemma arch_invoke_irq_control_invs[wp]:
"\<lbrace>invs and arch_irq_control_inv_valid i\<rbrace> arch_invoke_irq_control i \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: arch_invoke_irq_control_def)
@ -239,10 +274,12 @@ lemma arch_invoke_irq_control_invs[wp]:
apply (wp cap_insert_simple_invs | wpc
| simp add: IRQHandler_valid is_cap_simps no_cap_to_obj_with_diff_IRQHandler_ARCH
is_cap_simps safe_ioport_insert_triv
| strengthen real_cte_tcb_valid)+
| strengthen real_cte_tcb_valid
| wps)+
by (auto simp: cte_wp_at_caps_of_state IRQ_def arch_irq_control_inv_valid_def
is_simple_cap_def is_cap_simps is_pt_cap_def
safe_parent_for_def
maxUserIRQ_def maxIRQ_def order.trans
ex_cte_cap_to_cnode_always_appropriate_strg)
lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]:
@ -316,4 +353,4 @@ interpretation Interrupt_AI?: Interrupt_AI
case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?)
qed
end
end

8
proof/invariant-abstract/X64/ArchInvariants_AI.thy
View File

@ -1039,6 +1039,11 @@ where
"valid_ioports \<equiv> \<lambda>s. all_ioports_issued (caps_of_state s) (arch_state s) \<and>
ioports_no_overlap (caps_of_state s)"
definition
valid_x64_irq_state :: "(8 word \<Rightarrow> X64IRQState) \<Rightarrow> bool"
where
"valid_x64_irq_state irqState \<equiv> \<forall>irq > maxIRQ. irqState irq = IRQFree"
definition
valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
where
@ -1048,7 +1053,8 @@ where
\<and> valid_global_pts s
\<and> valid_global_pds s
\<and> valid_global_pdpts s
\<and> valid_cr3 (x64_current_cr3 (arch_state s))"
\<and> valid_cr3 (x64_current_cr3 (arch_state s))
\<and> valid_x64_irq_state (x64_irq_state (arch_state s))"
definition
vs_cap_ref_arch :: "arch_cap \<Rightarrow> vs_ref list option"

2
proof/invariant-abstract/X64/ArchKernelInit_AI.thy
View File

@ -293,7 +293,7 @@ lemma invs_A:
apply (clarsimp simp: valid_asid_table_def state_defs)
apply (simp add: valid_global_pts_def valid_global_pds_def valid_global_pdpts_def
valid_arch_state_def state_defs obj_at_def a_type_def
valid_cr3_def asid_wf_0)
valid_cr3_def valid_x64_irq_state_def asid_wf_0)
apply (rule conjI)
apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
is_cap_table_def wf_empty_bits

9
proof/refine/X64/ADT_H.thy
View File

@ -2056,11 +2056,14 @@ where
definition
"absArchState s' \<equiv>
case s' of X64KernelState asid_tbl gpm gpdpts gpds gpts ccr3 kvspace kports \<Rightarrow>
case s' of X64KernelState asid_tbl gpm gpdpts gpds gpts ccr3 kvspace kports num_ioapics 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\<rparr>"
x64_current_cr3 = absCR3 ccr3,
x64_allocated_io_ports = kports,
x64_num_ioapics = num_ioapics,
x64_irq_state = x64irqstate_to_abstract \<circ> irq_states\<rparr>"
lemma cr3_expand_unexpand[simp]: "cr3 (cr3_base_address a) (cr3_pcid a) = a"
by (cases a, simp)
@ -2075,7 +2078,7 @@ apply (subgoal_tac "(arch_state s, ksArchState s') \<in> arch_state_relation")
using rel
apply (simp add: state_relation_def)
apply (clarsimp simp add: arch_state_relation_def)
by (clarsimp simp add: absArchState_def absCR3_def cr3_relation_def
by (clarsimp simp add: absArchState_def absCR3_def cr3_relation_def x64_irq_relation_def
split: X64_H.kernel_state.splits cr3.splits)
definition absSchedulerAction where

8
proof/refine/X64/ArchAcc_R.thy
View File

@ -2177,5 +2177,13 @@ lemma dmo_clearMemory_invs'[wp]:
apply fastforce
done
lemma corres_gets_num_ioapics [corres]:
"corres (op =) \<top> \<top> (gets (x64_num_ioapics \<circ> arch_state)) (gets (x64KSNumIOAPICs \<circ> ksArchState))"
by (simp add: state_relation_def arch_state_relation_def)
lemma corres_gets_x64_irq_state [corres]:
"corres x64_irq_relation \<top> \<top> (gets (x64_irq_state \<circ> arch_state)) (gets (x64KSIRQState \<circ> ksArchState))"
by (simp add: state_relation_def arch_state_relation_def)
end
end

90
proof/refine/X64/Interrupt_R.thy
View File

@ -179,6 +179,10 @@ lemma unat_ucast_ucast_shenanigans[simp]:
apply (simp add: ucast_ucast_mask mask_def)
by (word_bitwise, auto)
lemmas irq_const_defs =
maxIRQ_def minIRQ_def
X64.maxUserIRQ_def X64.minUserIRQ_def X64_H.maxUserIRQ_def X64_H.minUserIRQ_def
(* FIXME x64: move *)
lemma whenE_throwError_corresK[corresK]:
"\<lbrakk>corres_underlyingK sr nf nf' F (frel \<oplus> rvr) Q Q' m m'\<rbrakk> \<Longrightarrow>
@ -215,11 +219,11 @@ lemma arch_decode_irq_control_corres:
-- "MSI"
apply (rule corres_guard_imp)
apply (rule whenE_throwError_corres)
apply (simp add: maxIRQ_def minIRQ_def)
apply (simp add: maxIRQ_def minIRQ_def ucast_nat_def)
apply (simp add: irq_const_defs)
apply (simp add: irq_const_defs)
apply (simp add: linorder_not_less )
apply (simp add: maxIRQ_def word_le_nat_alt)
apply (simp add: ucast_nat_def)
apply (simp add: irq_const_defs word_le_nat_alt ucast_id)
apply (simp add: ucast_nat_def Groups.ab_semigroup_add_class.add.commute)
apply (rule corres_split_eqr[OF _ is_irq_active_corres])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE[OF _ lsfc_corres])
@ -234,16 +238,17 @@ lemma arch_decode_irq_control_corres:
apply (rule conjI, clarsimp)
apply (rule corres_guard_imp)
apply (rule whenE_throwError_corres)
apply (simp add: maxIRQ_def minIRQ_def)
apply (simp add: maxIRQ_def minIRQ_def ucast_nat_def)
apply (simp add: irq_const_defs)
apply (simp add: irq_const_defs)
apply (simp add: linorder_not_less )
apply (simp add: maxIRQ_def word_le_nat_alt)
apply (simp add: ucast_nat_def)
apply (simp add: irq_const_defs word_le_nat_alt ucast_id)
apply (simp add: ucast_nat_def add.commute)
apply (rule corres_split_eqr[OF _ is_irq_active_corres])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE[OF _ lsfc_corres])
apply (rule corres_splitEE[OF _ ensure_empty_corres])
apply (rule whenE_throwError_corres, ((simp add: numIOAPICs_def ioapicIRQLines_def)+)[2])+
apply (rule corres_split[OF _ corres_gets_num_ioapics])
apply (rule whenE_throwError_corres, ((simp add: ucast_id ioapicIRQLines_def)+)[2])+
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply ((wpsimp wp: isIRQActive_inv
@ -313,7 +318,8 @@ lemma arch_decode_irq_control_valid'[wp]:
| wp whenE_throwError_wp isIRQActive_wp ensureEmptySlot_stronger
| wpc
| wp_once hoare_drop_imps)+
by (auto simp: invs_valid_objs' maxIRQ_def word_le_nat_alt unat_of_nat minIRQ_def)
apply (fastforce simp: invs_valid_objs' irq_const_defs unat_word_ariths word_le_nat_alt)
done
lemma decode_irq_control_valid'[wp]:
"\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' cap)
@ -462,10 +468,6 @@ lemma valid_mdb_interrupts'[simp]:
crunch valid_mdb'[wp]: setIRQState "valid_mdb'"
crunch cte_wp_at[wp]: setIRQState "cte_wp_at' P p"
(* FIXME x64: move *)
lemma no_fail_updateIRQState[wp]: "no_fail \<top> (updateIRQState a b)"
by (simp add: updateIRQState_def)
(* FIXME x64: move *)
lemma no_fail_ioapicMapPinToVector[wp]: "no_fail \<top> (ioapicMapPinToVector a b c d e) "
by (simp add: ioapicMapPinToVector_def)
@ -473,6 +475,32 @@ lemma no_fail_ioapicMapPinToVector[wp]: "no_fail \<top> (ioapicMapPinToVector a
method do_machine_op_corres
= (rule corres_machine_op, rule corres_Id, rule refl, simp)
lemma updateIRQState_corres[wp]:
"state = x64irqstate_to_abstract state' \<Longrightarrow>
corres dc \<top> \<top>
(X64_A.updateIRQState irq state)
(X64_H.updateIRQState irq state')"
apply (clarsimp simp: X64_A.updateIRQState_def X64_H.updateIRQState_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ corres_gets_x64_irq_state])
apply (rule corres_modify[where P=\<top> and P'=\<top>])
apply (auto simp: state_relation_def arch_state_relation_def x64_irq_relation_def)
done
crunches X64_H.updateIRQState
for pspace_distinct'[wp]: "pspace_distinct'"
and pspace_aligned'[wp]: "pspace_aligned'"
and cte_wp_at'[wp]: "cte_wp_at' a b"
and valid_mdb'[wp]: "valid_mdb'"
and ksPSpace[wp]: "\<lambda>s. P (ksPSpace s)"
and real_cte_at'[wp]: "real_cte_at' x"
and valid_cap'[wp]: "valid_cap' a"
and ctes_of[wp]: "\<lambda>s. P (ctes_of s a)"
and ksPSpace[wp]: "\<lambda>s. P (ksPSpace s)"
and inv[wp]: "\<lambda>s. P"
and ex_cte_cap_wp_to'[wp]: "ex_cte_cap_wp_to' a b"
(simp: ex_cte_cap_wp_to'_def valid_mdb'_def)
lemma arch_invoke_irq_control_corres:
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (intr \<oplus> dc)
(einvs and arch_irq_control_inv_valid x2)
@ -487,7 +515,7 @@ lemma arch_invoke_irq_control_corres:
apply (rule cins_corres_simple)
apply (wp | simp add: irq_state_relation_def
IRQHandler_valid IRQHandler_valid')+
apply (do_machine_op_corres | wpsimp)+
apply (do_machine_op_corres | wpsimp simp: IRQ_def | wps)+
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state
is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def
safe_parent_for_def)
@ -503,7 +531,7 @@ lemma arch_invoke_irq_control_corres:
apply (rule cins_corres_simple)
apply (wp | simp add: irq_state_relation_def
IRQHandler_valid IRQHandler_valid')+
apply (do_machine_op_corres | wpsimp)+
apply (do_machine_op_corres | wpsimp simp: IRQ_def | wps)+
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state
is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def
safe_parent_for_def)
@ -557,19 +585,23 @@ lemma setIRQState_issued[wp]:
apply clarsimp
done
(* FIXME x64: move*)
lemma no_irq_updateIRQState[wp]:
"no_irq (updateIRQState a b)"
by (simp add: updateIRQState_def)
lemma dmo_updateIRQState_invs'[wp]:
"\<lbrace>invs'\<rbrace> doMachineOp (updateIRQState a b) \<lbrace>\<lambda>_. invs'\<rbrace>"
apply (wp dmo_invs' no_irq_updateIRQState no_irq)
apply clarsimp
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
in use_valid[where P=P and Q="\<lambda>_. P" for P])
apply (simp add: updateIRQState_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+
lemma updateIRQState_invs'[wp]:
"\<lbrace>invs' and K (irq \<le> maxIRQ)\<rbrace>
X64_H.updateIRQState irq state
\<lbrace>\<lambda>_. invs'\<rbrace>"
apply (clarsimp simp: X64_H.updateIRQState_def)
apply wp
apply (fastforce simp: invs'_def valid_state'_def cur_tcb'_def
Invariants_H.valid_queues_def valid_queues'_def
valid_idle'_def valid_irq_node'_def
valid_arch_state'_def valid_global_refs'_def
global_refs'_def valid_machine_state'_def
if_unsafe_then_cap'_def ex_cte_cap_to'_def
valid_irq_handlers'_def irq_issued'_def
cteCaps_of_def valid_irq_masks'_def
bitmapQ_defs valid_queues_no_bitmap_def valid_x64_irq_state'_def
valid_ioports'_def all_ioports_issued'_def issued_ioports'_def
Word_Lemmas.word_not_le[symmetric])
done
(* FIXME x64: move*)

8
proof/refine/X64/Invariants_H.thy
View File

@ -1102,6 +1102,11 @@ definition
where
"valid_global_pdpts' pdpts \<equiv> \<lambda>s. \<forall>p \<in> set pdpts. pd_pointer_table_at' p s"
definition
valid_x64_irq_state' :: "(8 word \<Rightarrow> x64irqstate) \<Rightarrow> bool"
where
"valid_x64_irq_state' irqState \<equiv> \<forall>irq > maxIRQ. irqState irq = X64IRQFree"
definition
valid_arch_state' :: "kernel_state \<Rightarrow> bool"
where
@ -1111,7 +1116,8 @@ where
page_map_l4_at' (x64KSSKIMPML4 (ksArchState s)) s \<and>
valid_global_pds' (x64KSSKIMPDs (ksArchState s)) s \<and>
valid_global_pdpts' (x64KSSKIMPDPTs (ksArchState s)) s \<and>
valid_global_pts' (x64KSSKIMPTs (ksArchState s)) s"
valid_global_pts' (x64KSSKIMPTs (ksArchState s)) s \<and>
valid_x64_irq_state' (x64KSIRQState (ksArchState s))"
definition
irq_issued' :: "irq \<Rightarrow> kernel_state \<Rightarrow> bool"

18
proof/refine/X64/StateRelation.thy
View File

@ -470,6 +470,20 @@ definition
where
"cr3_relation c c' \<equiv> cr3_base_address c = cr3BaseAddress c' \<and> cr3_pcid c = cr3pcid c'"
fun
x64irqstate_to_abstract :: "x64irqstate \<Rightarrow> X64IRQState"
where
"x64irqstate_to_abstract X64IRQFree = IRQFree"
| "x64irqstate_to_abstract X64IRQReserved = IRQReserved"
| "x64irqstate_to_abstract (X64IRQMSI bus dev func handle) = (IRQMSI bus dev func handle)"
| "x64irqstate_to_abstract (X64IRQIOAPIC ioapic pin level polarity masked) =
(IRQIOAPIC ioapic pin level polarity masked)"
definition
x64_irq_relation :: "(8 word \<Rightarrow> X64IRQState) \<Rightarrow> (8 word \<Rightarrow> x64irqstate) \<Rightarrow> bool"
where
"x64_irq_relation irq_states irq_states' \<equiv> irq_states = x64irqstate_to_abstract o irq_states'"
definition
arch_state_relation :: "(arch_state \<times> X64_H.kernel_state) set"
where
@ -481,7 +495,9 @@ where
\<and> x64_global_pts s = x64KSSKIMPTs s'
\<and> cr3_relation (x64_current_cr3 s) (x64KSCurrentUserCR3 s')
\<and> x64_kernel_vspace s = x64KSKernelVSpace s'
\<and> x64_allocated_io_ports s = x64KSAllocatedIOPorts s'}"
\<and> x64_allocated_io_ports s = x64KSAllocatedIOPorts s'
\<and> x64_num_ioapics s = x64KSNumIOAPICs s'
\<and> x64_irq_relation (x64_irq_state s) (x64KSIRQState s')}"
definition
(* NOTE: this map discards the Ident right, needed on endpoints only *)