From 9ac07adc7d0c47af08923d689f63bfb66f627ab0 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Wed, 18 Dec 2024 10:37:31 +1100
Subject: [PATCH] aarch64 abstract+machine squash: PR suggestions

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 spec/abstract/AARCH64/FPU_A.thy     |  2 +-
 spec/abstract/Schedule_A.thy        |  2 +-
 spec/abstract/Tcb_A.thy             |  2 +-
 spec/machine/AARCH64/MachineOps.thy | 29 ++++++++++++++++++++++-------
 4 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/spec/abstract/AARCH64/FPU_A.thy b/spec/abstract/AARCH64/FPU_A.thy
index 9d6fd6cffc..c80272e463 100644
--- a/spec/abstract/AARCH64/FPU_A.thy
+++ b/spec/abstract/AARCH64/FPU_A.thy
@@ -25,7 +25,7 @@ definition load_fpu_state :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad
      do_machine_op (writeFpuState fpu_state)
    od"
 
-\<comment> \<open>FIXME: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
+\<comment> \<open>FIXME FPU: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
 definition switch_local_fpu_owner :: "obj_ref option \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "switch_local_fpu_owner new_owner \<equiv> do
      do_machine_op enableFpu;
diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy
index 699733490d..a2f83b4c29 100644
--- a/spec/abstract/Schedule_A.thy
+++ b/spec/abstract/Schedule_A.thy
@@ -167,7 +167,7 @@ end
 instantiation unit :: state_ext_sched
 begin
 
-\<comment> \<open>FIXME: update this comment to mention the state that might be
+\<comment> \<open>FIXME FPU: update this comment to mention the state that might be
   saved as part of @{term arch_prepare_next_domain}\<close>
 text \<open>
   The scheduler is heavily underspecified.
diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy
index 645277fab0..5e2a4b70b8 100644
--- a/spec/abstract/Tcb_A.thy
+++ b/spec/abstract/Tcb_A.thy
@@ -273,7 +273,7 @@ definition
      when (tptr = cur) reschedule_required
    od"
 
- \<comment> \<open>FIXME: @{term arch_prepare_set_domain} shouldn't be an extended op. Fixing this will require either
+ \<comment> \<open>FIXME FPU: @{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.\<close>
 definition invoke_domain:: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad" where
   "invoke_domain thread domain \<equiv>
diff --git a/spec/machine/AARCH64/MachineOps.thy b/spec/machine/AARCH64/MachineOps.thy
index e3abc34952..db6b3ac03a 100644
--- a/spec/machine/AARCH64/MachineOps.thy
+++ b/spec/machine/AARCH64/MachineOps.thy
@@ -168,17 +168,22 @@ definition setNextPC :: "machine_word \<Rightarrow> unit user_monad" where
 
 subsection "FPU-related"
 
-\<comment> \<open>FIXME: Should this modify @{term fpu_enabled}? The C doesn't update isFPUEnabledCached when this is called directly.\<close>
-consts' enableFpuEL01_impl :: "unit machine_rest_monad"
-definition enableFpuEL01 :: "unit machine_monad" where
-  "enableFpuEL01 \<equiv> machine_op_lift enableFpuEL01_impl"
-
 definition getFPUState :: "fpu_state user_monad" where
   "getFPUState \<equiv> gets fpu_state"
 
 definition setFPUState :: "fpu_state \<Rightarrow> unit user_monad" where
   "setFPUState fc \<equiv> modify (\<lambda>s. UserContext fc (user_regs s))"
 
+\<comment> \<open>This function touches the CPACR_EL1 register, which is used to enable/disable the FPU for EL0
+   and EL1 and is generally controlled by the VM. seL4 only modifies it by unconditionally enabling
+   it when disabling a VCPU, it instead toggles CPTR_EL2 to enable or disable the FPU for native
+   tasks.\<close>
+\<comment> \<open>FIXME FPU: The underlying register is saved and restored when switching between VCPUs, so this
+     will probably need to be moved out of machine\_rest\_monad.\<close>
+consts' enableFpuEL01_impl :: "unit machine_rest_monad"
+definition enableFpuEL01 :: "unit machine_monad" where
+  "enableFpuEL01 \<equiv> machine_op_lift enableFpuEL01_impl"
+
 consts' readFpuState_val :: "machine_state_rest \<Rightarrow> fpu_state"
 definition readFpuState :: "fpu_state machine_monad" where
   "readFpuState \<equiv>  do
@@ -193,11 +198,21 @@ definition writeFpuState :: "fpu_state \<Rightarrow> unit machine_monad" where
      machine_op_lift $ writeFpuState_impl val
    od"
 
+\<comment> \<open>FIXME FPU: on AArch64 with hypervisor support this actually calls disableTrapFpu to enable the
+     FPU. Do we want to model that as well or are we happy to abstract it away?\<close>
+consts' enableFpu_impl :: "unit machine_rest_monad"
 definition enableFpu :: "unit machine_monad" where
-  "enableFpu \<equiv> modify (\<lambda>s. s\<lparr>fpu_enabled := True \<rparr>)"
+  "enableFpu \<equiv> do
+     machine_op_lift enableFpu_impl;
+     modify (\<lambda>s. s\<lparr>fpu_enabled := True \<rparr>)
+   od"
 
+consts' disableFpu_impl :: "unit machine_rest_monad"
 definition disableFpu :: "unit machine_monad" where
-  "disableFpu \<equiv> modify (\<lambda>s. s\<lparr>fpu_enabled := False \<rparr>)"
+  "disableFpu \<equiv> do
+     machine_op_lift disableFpu_impl;
+     modify (\<lambda>s. s\<lparr>fpu_enabled := False \<rparr>)
+   od"
 
 definition isFpuEnable :: "bool machine_monad" where
   "isFpuEnable \<equiv> gets fpu_enabled"