From f6ca1f883a859f6ca996a156126b0d358501d174 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 19 Sep 2024 21:46:56 +1000 Subject: [PATCH] aarch64 abstract+machine: update abstract to use semi-lazy FPU switching This includes extending the machine interface with new ops, adding the current owner of the FPU state to the kernel state, and adding the new seL4_TCB_Set_Flags syscall and related functions. Signed-off-by: Corey Lewis --- spec/abstract/AARCH64/ArchTcb_A.thy | 13 +++- spec/abstract/AARCH64/ArchVSpace_A.thy | 5 +- spec/abstract/AARCH64/Arch_A.thy | 6 +- spec/abstract/AARCH64/Arch_Structs_A.thy | 9 +++ spec/abstract/AARCH64/FPU_A.thy | 59 ++++++++++++++++++ spec/abstract/AARCH64/Hypervisor_A.thy | 18 +++--- spec/abstract/AARCH64/Init_A.thy | 4 +- spec/abstract/Decode_A.thy | 9 +++ spec/abstract/Invocations_A.thy | 1 + spec/abstract/KHeap_A.thy | 5 +- spec/abstract/Schedule_A.thy | 60 ++++++++++--------- spec/abstract/Structures_A.thy | 17 ++++++ spec/abstract/Tcb_A.thy | 22 ++++++- spec/design/m-skel/AARCH64/MachineTypes.thy | 2 + .../haskell/src/SEL4/API/InvocationLabels.lhs | 1 + spec/machine/AARCH64/MachineOps.thy | 44 +++++++------- 16 files changed, 203 insertions(+), 72 deletions(-) create mode 100644 spec/abstract/AARCH64/FPU_A.thy diff --git a/spec/abstract/AARCH64/ArchTcb_A.thy b/spec/abstract/AARCH64/ArchTcb_A.thy index ad486ad50f..8a5d36e05d 100644 --- a/spec/abstract/AARCH64/ArchTcb_A.thy +++ b/spec/abstract/AARCH64/ArchTcb_A.thy @@ -7,7 +7,7 @@ chapter \Architecture-specific TCB functions\ theory ArchTcb_A -imports KHeap_A +imports FPU_A begin context Arch begin arch_global_naming (A) @@ -26,5 +26,16 @@ definition arch_get_sanitise_register_info :: "obj_ref \ (bool, 'a:: definition arch_post_modify_registers :: "obj_ref \ obj_ref \ (unit, 'a::state_ext) s_monad" where "arch_post_modify_registers cur t \ return ()" +\ \The corresponding C code is not arch dependent and so is inline as part of invokeSetFlags\ +definition arch_post_set_flags :: "obj_ref \ tcb_flags \ (unit, 'a::state_ext) s_monad" where + "arch_post_set_flags t flags \ + when (ArchFlag FpuDisabled \ flags) (fpu_release t)" + +definition arch_prepare_set_domain :: "obj_ref \ domain \ unit det_ext_monad" where + "arch_prepare_set_domain t new_dom \ do + cur_domain \ gets cur_domain; + when (cur_domain \ new_dom) $ fpu_release t + od" + end end diff --git a/spec/abstract/AARCH64/ArchVSpace_A.thy b/spec/abstract/AARCH64/ArchVSpace_A.thy index 962540c8ec..ff31e855cb 100644 --- a/spec/abstract/AARCH64/ArchVSpace_A.thy +++ b/spec/abstract/AARCH64/ArchVSpace_A.thy @@ -395,12 +395,9 @@ definition in_user_frame :: "obj_ref \ 'z::state_ext state \ \sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))" -definition fpu_thread_delete :: "obj_ref \ (unit, 'z::state_ext) s_monad" where - "fpu_thread_delete thread_ptr \ do_machine_op (fpuThreadDeleteOp thread_ptr)" - definition prepare_thread_delete :: "obj_ref \ (unit,'z::state_ext) s_monad" where "prepare_thread_delete thread_ptr \ do - fpu_thread_delete thread_ptr; + fpu_release thread_ptr; t_vcpu \ arch_thread_get tcb_vcpu thread_ptr; case t_vcpu of Some v \ dissociate_vcpu_tcb v thread_ptr diff --git a/spec/abstract/AARCH64/Arch_A.thy b/spec/abstract/AARCH64/Arch_A.thy index 462642c0a4..b807ba1358 100644 --- a/spec/abstract/AARCH64/Arch_A.thy +++ b/spec/abstract/AARCH64/Arch_A.thy @@ -25,7 +25,8 @@ definition arch_switch_to_thread :: "obj_ref \ (unit,'z::state_ext) "arch_switch_to_thread t \ do tcb \ gets_the $ get_tcb t; vcpu_switch $ tcb_vcpu $ tcb_arch tcb; - set_vm_root t + set_vm_root t; + lazy_fpu_restore t od" definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where @@ -34,6 +35,9 @@ definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where set_global_user_vspace od" +definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where + "arch_prepare_next_domain \ switch_local_fpu_owner None" + definition arch_activate_idle_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where "arch_activate_idle_thread t \ return ()" diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy index 753e95142e..2098fc1cf0 100644 --- a/spec/abstract/AARCH64/Arch_Structs_A.thy +++ b/spec/abstract/AARCH64/Arch_Structs_A.thy @@ -333,6 +333,7 @@ record arch_state = arm_us_global_vspace :: "obj_ref" arm_current_vcpu :: "(obj_ref \ bool) option" arm_gicvcpu_numlistregs :: nat + arm_current_fpu_owner :: "obj_ref option" end_qualify @@ -369,6 +370,14 @@ record arch_tcb = tcb_context :: user_context tcb_vcpu :: "obj_ref option" +datatype arch_tcb_flag + = FpuDisabled + +definition word_from_arch_tcb_flag :: "arch_tcb_flag \ machine_word" where + "word_from_arch_tcb_flag flag \ + case flag of + FpuDisabled \ bit 0" + end_qualify context Arch begin arch_global_naming (A) diff --git a/spec/abstract/AARCH64/FPU_A.thy b/spec/abstract/AARCH64/FPU_A.thy new file mode 100644 index 0000000000..fc5b51c87b --- /dev/null +++ b/spec/abstract/AARCH64/FPU_A.thy @@ -0,0 +1,59 @@ +(* + * Copyright 2024, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +chapter "AARCH64 FPU Functions" + +theory FPU_A +imports + KHeap_A +begin + +context Arch begin arch_global_naming (A) + +definition save_fpu_state :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "save_fpu_state t \ do + fpu_state \ do_machine_op readFpuState; + as_user t (setFPUState fpu_state) + od" + +definition load_fpu_state :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "load_fpu_state t \ do + fpu_state \ as_user t getFPUState; + do_machine_op (writeFpuState fpu_state) + od" + +\ \FIXME: maybe use a case instead of the if (depends on if wpc or if_split is easier)\ +definition switch_local_fpu_owner :: "obj_ref option \ (unit,'z::state_ext) s_monad" where + "switch_local_fpu_owner new_owner \ do + do_machine_op enableFpu; + cur_fpu_owner \ gets (arm_current_fpu_owner \ arch_state); + when (cur_fpu_owner \ None) $ save_fpu_state (the cur_fpu_owner); + if (new_owner \ None) + then load_fpu_state (the new_owner) + else do_machine_op disableFpu; + modify (\s. s \arch_state := arch_state s\arm_current_fpu_owner := new_owner\\) + od" + +definition fpu_release :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "fpu_release thread_ptr \ do + cur_fpu_owner \ gets (arm_current_fpu_owner \ arch_state); + when (cur_fpu_owner = Some thread_ptr) $ switch_local_fpu_owner None + od" + +definition lazy_fpu_restore :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "lazy_fpu_restore thread_ptr \ do + flags \ thread_get tcb_flags thread_ptr; + if (ArchFlag FpuDisabled \ flags) + then do_machine_op disableFpu + else do + do_machine_op enableFpu; + switch_local_fpu_owner (Some thread_ptr) + od + od" + +end + +end \ No newline at end of file diff --git a/spec/abstract/AARCH64/Hypervisor_A.thy b/spec/abstract/AARCH64/Hypervisor_A.thy index b396cf8d64..46d5aa207b 100644 --- a/spec/abstract/AARCH64/Hypervisor_A.thy +++ b/spec/abstract/AARCH64/Hypervisor_A.thy @@ -14,17 +14,13 @@ context Arch begin arch_global_naming (A) fun handle_hypervisor_fault :: "machine_word \ hyp_fault_type \ (unit, 'z::state_ext) s_monad" where - "handle_hypervisor_fault thread (ARMVCPUFault hsr) = do - fpu_enabled \ do_machine_op isFpuEnable; - if \fpu_enabled - then fail - else if hsr = 0x2000000 \ \@{text UNKNOWN_FAULT}\ - then do - esr \ do_machine_op getESR; - handle_fault thread (UserException (esr && mask 32) 0) - od - else handle_fault thread (ArchFault $ VCPUFault (ucast hsr)) - od" + "handle_hypervisor_fault thread (ARMVCPUFault hsr) = + (if hsr = 0x2000000 \ \@{text UNKNOWN_FAULT}\ + then do + esr \ do_machine_op getESR; + handle_fault thread (UserException (esr && mask 32) 0) + od + else handle_fault thread (ArchFault $ VCPUFault (ucast hsr)))" end end diff --git a/spec/abstract/AARCH64/Init_A.thy b/spec/abstract/AARCH64/Init_A.thy index 9182f606e2..5cb9c5ea4e 100644 --- a/spec/abstract/AARCH64/Init_A.thy +++ b/spec/abstract/AARCH64/Init_A.thy @@ -52,7 +52,8 @@ definition init_arch_state :: arch_state where arm_next_vmid = 0, arm_us_global_vspace = arm_global_pt_ptr, arm_current_vcpu = None, - arm_gicvcpu_numlistregs = undefined + arm_gicvcpu_numlistregs = undefined, + arm_current_fpu_owner = None \" @@ -79,6 +80,7 @@ definition init_kheap :: kheap where tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, + tcb_flags = {}, tcb_arch = init_arch_tcb \, arm_global_pt_ptr \ ArchObj global_pt_obj diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index abe85ced52..69846bfc56 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -380,6 +380,14 @@ where returnOk (SetTLSBase (obj_ref_of cap) (ucast (args ! 0))) odE" +definition + decode_set_flags :: "data list \ cap \ (tcb_invocation,'z::state_ext) se_monad" +where + "decode_set_flags args cap \ doE + whenE (length args < 2) $ throwError TruncatedMessage; + returnOk (SetFlags (obj_ref_of cap) (word_to_tcb_flags (args ! 0)) (word_to_tcb_flags (args ! 1))) + odE" + definition decode_tcb_invocation :: "data \ data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ @@ -401,6 +409,7 @@ where | TCBBindNotification \ decode_bind_notification cap excs | TCBUnbindNotification \ decode_unbind_notification cap | TCBSetTLSBase \ decode_set_tls_base args cap + | TCBSetFlags \ decode_set_flags args cap | _ \ throwError IllegalOperation" definition diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index c8026c6755..4bb34913f4 100644 --- a/spec/abstract/Invocations_A.thy +++ b/spec/abstract/Invocations_A.thy @@ -48,6 +48,7 @@ datatype tcb_invocation = | Resume "obj_ref" | NotificationControl "obj_ref" "obj_ref option" | SetTLSBase obj_ref machine_word + | SetFlags obj_ref tcb_flags tcb_flags datatype irq_control_invocation = IRQControl irq cslot_ptr cslot_ptr diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy index 3d9a4542e1..c5ca951609 100644 --- a/spec/abstract/KHeap_A.thy +++ b/spec/abstract/KHeap_A.thy @@ -132,7 +132,10 @@ definition definition set_mcpriority :: "obj_ref \ priority \ (unit, 'z::state_ext) s_monad" where - "set_mcpriority ref mcp \ thread_set (\tcb. tcb\tcb_mcpriority:=mcp\) ref " + "set_mcpriority ref mcp \ thread_set (\tcb. tcb\tcb_mcpriority:=mcp\) ref" + +definition set_flags :: "obj_ref \ tcb_flags \ (unit, 'z::state_ext) s_monad" where + "set_flags ref flags \ thread_set (\tcb. tcb\tcb_flags:=flags\) ref" section "simple kernel objects" diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy index a541a1dc88..39afe19362 100644 --- a/spec/abstract/Schedule_A.thy +++ b/spec/abstract/Schedule_A.thy @@ -17,6 +17,7 @@ begin arch_requalify_consts (A) arch_switch_to_thread arch_switch_to_idle_thread + arch_prepare_next_domain abbreviation "idle st \ st = Structures_A.IdleThreadState" @@ -34,10 +35,7 @@ where text \Gets all schedulable threads in the system.\ definition allActiveTCBs :: "(obj_ref set,'z::state_ext) s_monad" where - "allActiveTCBs \ do - state \ get; - return {x. getActiveTCB x state \ None} - od" + "allActiveTCBs \ gets (\state. {x. getActiveTCB x state \ None})" text \Switches the current thread to the specified one.\ definition @@ -100,7 +98,10 @@ definition definition "schedule_choose_new_thread \ do dom_time \ gets domain_time; - when (dom_time = 0) next_domain; + when (dom_time = 0) $ do + arch_prepare_next_domain; + next_domain + od; choose_thread; set_scheduler_action resume_cur_thread od" @@ -166,37 +167,42 @@ end instantiation unit :: state_ext_sched begin - +\ \FIXME: update this comment to mention the state that might be + saved as part of arch_prepare_next_domain\ text \ The scheduler is heavily underspecified. It is allowed to pick any active thread or the idle thread. - If the thread the scheduler picked is the current thread, it - may omit the call to @{const switch_to_thread}. Likewise it - may omit the call to @{const switch_to_idle_thread} if the - idle thread is the current thread. -\ + If the current thread is active or is already the idle thread + then it may omit the call to @{const switch_to_thread} or + @{const switch_to_idle_thread} and do nothing.\ + +definition pre_choose_thread_unit :: "(unit,unit) s_monad" where + "pre_choose_thread_unit \ return () \ arch_prepare_next_domain" + +definition choose_thread_unit :: "(unit,unit) s_monad" where + "choose_thread_unit \ (do + threads \ allActiveTCBs; + thread \ select threads; + switch_to_thread thread + od) \ + switch_to_idle_thread" + definition schedule_unit :: "(unit,unit) s_monad" where -"schedule_unit \ (do - cur \ gets cur_thread; - threads \ allActiveTCBs; - thread \ select threads; - (if thread = cur then - return () \ switch_to_thread thread - else - switch_to_thread thread) - od) \ - (do - cur \ gets cur_thread; - idl \ gets idle_thread; - if idl = cur then - return () \ switch_to_idle_thread - else switch_to_idle_thread - od)" + "schedule \ (do + cur \ gets cur_thread; + cur_active \ gets (getActiveTCB cur); + idl \ gets idle_thread; + if cur_active \ None \ idl = cur then + return () \ (do pre_choose_thread_unit; choose_thread_unit od) + else + (do pre_choose_thread_unit; choose_thread_unit od) + od)" instance .. end lemmas schedule_def = schedule_det_ext_ext_def schedule_unit_def +lemmas schedule_def_all = schedule_def pre_choose_thread_unit_def choose_thread_unit_def allActiveTCBs_def end diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index b8c7a568ca..fdacc9ce84 100644 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -23,6 +23,7 @@ arch_requalify_types (A) arch_kernel_obj arch_state arch_tcb + arch_tcb_flag aa_type arch_requalify_consts (A) @@ -46,6 +47,7 @@ arch_requalify_consts (A) untyped_min_bits untyped_max_bits msg_label_bits + word_from_arch_tcb_flag text \ User mode can request these objects to be created by retype: @@ -367,6 +369,19 @@ datatype thread_state type_synonym priority = word8 +datatype tcb_flag + = ArchFlag arch_tcb_flag + +definition word_from_tcb_flag :: "tcb_flag \ machine_word" where + "word_from_tcb_flag flag \ + case flag of + ArchFlag arch_flag \ word_from_arch_tcb_flag arch_flag" + +type_synonym tcb_flags = "tcb_flag set" + +definition word_to_tcb_flags :: "machine_word \ tcb_flags" where + "word_to_tcb_flags w \ {flag. word_from_tcb_flag flag && w \ 0}" + record tcb = tcb_ctable :: cap tcb_vtable :: cap @@ -379,6 +394,7 @@ record tcb = tcb_fault :: "fault option" tcb_bound_notification :: "obj_ref option" tcb_mcpriority :: priority + tcb_flags :: tcb_flags tcb_arch :: arch_tcb (* arch_tcb must have a field for user context *) @@ -410,6 +426,7 @@ definition tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, + tcb_flags = {}, tcb_arch = default_arch_tcb\" text \ diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index 89fe35d96a..645277fab0 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -19,6 +19,8 @@ arch_requalify_consts (A) sanitise_register arch_get_sanitise_register_info arch_post_modify_registers + arch_post_set_flags + arch_prepare_set_domain section "Activating Threads" @@ -251,6 +253,15 @@ where return [] od)" +| "invoke_tcb (SetFlags tcb clearFlags setFlags) = + (liftE $ do + flags \ thread_get tcb_flags tcb; + new_flags \ return $ flags - clearFlags \ setFlags; + set_flags tcb new_flags; + arch_post_set_flags tcb new_flags; + return [] + od)" + definition set_domain :: "obj_ref \ domain \ unit det_ext_monad" where "set_domain tptr new_dom \ do @@ -262,10 +273,15 @@ definition when (tptr = cur) reschedule_required od" -definition invoke_domain:: "obj_ref \ domain \ (data list,'z::state_ext) p_monad" -where + \ \FIXME: @{term arch_prepare_set_domain} shouldn't be an extended op. Fixing this will require either + adding domains to the non-det spec, or removing the non-det spec completely.\ +definition invoke_domain:: "obj_ref \ domain \ (data list,'z::state_ext) p_monad" where "invoke_domain thread domain \ - liftE (do do_extended_op (set_domain thread domain); return [] od)" + liftE $ do + do_extended_op (arch_prepare_set_domain thread domain); + do_extended_op (set_domain thread domain); + return [] + od" text \Get all of the message registers, both from the sending thread's current register file and its IPC buffer.\ diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy index 64e4002243..8c518e2c8f 100644 --- a/spec/design/m-skel/AARCH64/MachineTypes.thy +++ b/spec/design/m-skel/AARCH64/MachineTypes.thy @@ -62,6 +62,7 @@ record irq_state :: nat underlying_memory :: "machine_word \ word8" device_state :: "machine_word \ word8 option" + fpu_enabled :: bool machine_state_rest :: AARCH64.machine_state_rest axiomatization @@ -109,6 +110,7 @@ definition irq_state = 0, underlying_memory = init_underlying_memory, device_state = Map.empty, + fpu_enabled = False, machine_state_rest = undefined \" #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64 ONLY \ diff --git a/spec/haskell/src/SEL4/API/InvocationLabels.lhs b/spec/haskell/src/SEL4/API/InvocationLabels.lhs index 9258f70047..3ad6a263b5 100644 --- a/spec/haskell/src/SEL4/API/InvocationLabels.lhs +++ b/spec/haskell/src/SEL4/API/InvocationLabels.lhs @@ -45,6 +45,7 @@ The following type enumerates all the kinds of invocations that clients can requ > | TCBBindNotification > | TCBUnbindNotification > | TCBSetTLSBase +> | TCBSetFlags > | CNodeRevoke > | CNodeDelete > | CNodeCancelBadgedSends diff --git a/spec/machine/AARCH64/MachineOps.thy b/spec/machine/AARCH64/MachineOps.thy index e5a5dde703..c778e280df 100644 --- a/spec/machine/AARCH64/MachineOps.thy +++ b/spec/machine/AARCH64/MachineOps.thy @@ -168,6 +168,7 @@ definition setNextPC :: "machine_word \ unit user_monad" where subsection "FPU-related" +\ \FIXME: Should this modify fpu_enabled? The C doesn't update isFPUEnabledCached when this is called directly.\ consts' enableFpuEL01_impl :: "unit machine_rest_monad" definition enableFpuEL01 :: "unit machine_monad" where "enableFpuEL01 \ machine_op_lift enableFpuEL01_impl" @@ -178,31 +179,28 @@ definition getFPUState :: "fpu_state user_monad" where definition setFPUState :: "fpu_state \ unit user_monad" where "setFPUState fc \ modify (\s. UserContext fc (user_regs s))" -consts' nativeThreadUsingFPU_impl :: "machine_word \ unit machine_rest_monad" -consts' nativeThreadUsingFPU_val :: "machine_state \ bool" -definition nativeThreadUsingFPU :: "machine_word \ bool machine_monad" where - "nativeThreadUsingFPU thread_ptr \ do - machine_op_lift (nativeThreadUsingFPU_impl thread_ptr); - gets nativeThreadUsingFPU_val - od" +consts' readFpuState_val :: "machine_state_rest \ fpu_state" +definition readFpuState :: "fpu_state machine_monad" where + "readFpuState \ do + state_assert fpu_enabled; + machine_rest_lift $ gets readFpuState_val + od" + +consts' writeFpuState_impl :: "fpu_state \ unit machine_rest_monad" +definition writeFpuState :: "fpu_state \ unit machine_monad" where + "writeFpuState val \ do + state_assert fpu_enabled; + machine_op_lift $ writeFpuState_impl val + od" + +definition enableFpu :: "unit machine_monad" where + "enableFpu \ modify (\s. s\fpu_enabled := True \)" + +definition disableFpu :: "unit machine_monad" where + "disableFpu \ modify (\s. s\fpu_enabled := False \)" -consts' switchFpuOwner_impl :: "machine_word \ machine_word \ unit machine_rest_monad" -definition switchFpuOwner :: "machine_word \ machine_word \ unit machine_monad" where - "switchFpuOwner new_owner cpu \ machine_op_lift (switchFpuOwner_impl new_owner cpu)" - -(* FIXME this is a very high-level FPU abstraction *) -consts' fpuThreadDeleteOp_impl :: "machine_word \ unit machine_rest_monad" -definition fpuThreadDeleteOp :: "machine_word \ unit machine_monad" where - "fpuThreadDeleteOp thread_ptr \ machine_op_lift (fpuThreadDeleteOp_impl thread_ptr)" - -(* FIXME this machine op is used to abstract the entire lazy FPU switch interrupt mechanism, - which can only trigger when the current thread's FPU is disabled and it performs an FPU - operation. We have no model for this mechanism or the state that it caches, so for - verification purposes we act as if the FPU is always enabled. - Future lazy FPU switch overhaul will involve the state that this operation reads, at which - point it should become a normal function. *) definition isFpuEnable :: "bool machine_monad" where - "isFpuEnable \ return True" + "isFpuEnable \ gets fpu_enabled" subsection "Fault Registers"