CAVEATS: verification update; remove clang problem

- add new platforms supported by verification
- remove 32-bit imx8mm with FPU (proof out of date)
- add AArch64 integrity
- add FPU where covered
- remove caveat on lazy FPU and VCPU switching (fixed)
- remove caveat on SMP lock with clang (fixed)

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

CAVEATS.md

@@ -9,18 +9,44 @@
 ## Implementation Correctness
 
 The following seL4 architectures have platforms with a C-level functional
-correctness proof. Proof support for further platforms within these
-architectures is on the roadmap and expected in 2025.
+correctness proof. Proof support for further platforms for RISC-V is on
+the roadmap and expected in 2026.
 
-- AArch32: Armv7-a with and without hypervisor extensions, no SMMU, with
+- AArch32: Armv7-a with and without hypervisor extensions, no SMMU, no FPU, with
   fast path
-  - Platforms (non-hyp): `sabre` (no FPU), `imx8mm-evk` (with FPU)
-  - Platforms (hyp, no FPU): `tk1`, `exynos5`
-- AArch64: Armv8-a with hypervisor extensions only, no SMMU, with fast path
-  - Platforms: `tx2`, `zynqmp`, `bcm2711` (rpi4)
-- RISC-V: 64-bit only, no fast path
+  - Platforms (non-hyp):
+    - `sabre`
+    - `am335x`
+    - `bcm2837`
+    - `exynos4`
+    - `exynos5410`
+    - `exynos5422`
+    - `hikey`
+    - `imx8mm`
+    - `omap3`
+    - `tk1`
+    - `zynq7000`
+    - `zynqmp`
+  - Platforms (hyp): `tk1`, `exynos5`, `exynos5410`
+- AArch64: Armv8-a with hypervisor extensions only, no SMMU, with FPU, with fast path
+  - Platforms:
+    - `tx2`
+    - `bcm2711`
+    - `hikey`
+    - `imx8mm`
+    - `imx8mq`
+    - `imx93`
+    - `maaxboard`
+    - `odroidc2`
+    - `odroidc4`
+    - `rockpro64`
+    - `tqma`
+    - `tx1`
+    - `ultra96v2`
+    - `zynqmp`
+- RISC-V: 64-bit only, no FPU, no fast path
   - Platforms: `hifive`
-- x64: without VT-x and VT-d, no fast path
+- x64: without VT-x and VT-d, with FPU, no fast path
   - Platforms: `pc99`
 
 This proof covers the functional behaviour of the C code of the kernel. It does
@@ -45,15 +71,17 @@ The security property proofs depend on additional assumptions on the correct
 configuration of the system. See the [l4v] repository on GitHub for more
 details.
 
-Similar proofs for AArch64 with hypervisor extensions are in progress.
+For AArch64 with hypervisor extensions and with FPU, the following security
+properties hold:
+
+- integrity (no write without authority)
+
+Confidentiality and non-interference proofs for AArch64 with hypervisor
+extensions are in progress.
 
 For AArch32, there additionally exist proofs for correct user-level system
 initialisation. See the [l4v] repository for details.
 
-Note that seL4 currently performs lazy FPU and VCPU switching, which can
-introduce information flow timing channels. An API-change proposal ([RFC]) to
-improve this behaviour is currently in progress.
-
 ## Verified Configurations
 
 For the precise configuration of the verified platforms above, see the
@@ -99,10 +127,7 @@ values.
 ## SMP
 
 A symmetric multi-processor (SMP) configuration for seL4 exists and is supported
-by the seL4 Foundation, but currently without formal verification. While
-generally stable, there are a small number of known open issues, in particular
-when the kernel is compiled with `clang`. We recommend `gcc` for working with
-SMP configurations of seL4.
+by the seL4 Foundation, but currently without formal verification.
 
 The combination of SMP and hypervisor extensions is supported and should be
 generally stable, but like the plain SMP configuration it is not formally