From 04d50580f1ce3914a09220d68ac8df9721d825b0 Mon Sep 17 00:00:00 2001
From: Evan Johnson <e5johnso@ucsd.edu>
Date: Tue, 7 Apr 2026 13:42:44 -0700
Subject: [PATCH] adjust tock so that flux-core Result spec doesn't break it

---
 arch/rv32i/src/pmp.rs                   |  3 +++
 flux_support/src/extern_specs/result.rs | 10 ++++++++++
 kernel/src/syscall_driver.rs            |  1 +
 3 files changed, 14 insertions(+)

diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
index 3e09752338..b4ec93541d 100644
--- a/arch/rv32i/src/pmp.rs
+++ b/arch/rv32i/src/pmp.rs
@@ -1300,6 +1300,7 @@ impl<const MAX_REGIONS: usize, P: TORUserPMP<MAX_REGIONS> + 'static> kernel::pla
     // type MpuConfig = PMPUserMPUConfig<MAX_REGIONS>;
     type Region = PMPUserRegion<MAX_REGIONS>;
 
+    #[flux_rs::trusted]
     fn enable_app_mpu(&self) -> MpuEnabledCapability {
         // TODO: This operation may fail when the PMP is not exclusively used
         // for userspace. Instead of panicing, we should handle this case more
@@ -1360,6 +1361,8 @@ pub mod test {
             Ok(())
         }
 
+        // #[flux_rs::sig(fn (x: usize) -> u32[x] requires x <= u32::MAX)]
+        #[flux_rs::sig(fn (&Self) -> Result<(), ()>[true])]
         fn enable_user_pmp(&self) -> Result<(), ()> {
             Ok(())
         } // The kernel's MPU trait requires
diff --git a/flux_support/src/extern_specs/result.rs b/flux_support/src/extern_specs/result.rs
index 77fae5ae98..277f1abfdf 100644
--- a/flux_support/src/extern_specs/result.rs
+++ b/flux_support/src/extern_specs/result.rs
@@ -14,4 +14,14 @@ impl<T, E> Result<T, E> {
 
     #[sig(fn(&Result<T,E>[@b]) -> bool[!b])]
     const fn is_err(&self) -> bool;
+
+    #[sig(fn(Result<T, E>[true]) -> T)]
+    fn unwrap(self) -> T
+    where
+        E: core::fmt::Debug;
+
+    #[sig(fn(Result<T, E>[false]) -> E)]
+    fn unwrap_err(self) -> E
+    where
+        T: core::fmt::Debug;
 }
diff --git a/kernel/src/syscall_driver.rs b/kernel/src/syscall_driver.rs
index e37f3f239b..5ae60c6cf2 100644
--- a/kernel/src/syscall_driver.rs
+++ b/kernel/src/syscall_driver.rs
@@ -81,6 +81,7 @@ impl CommandReturn {
 }
 
 impl From<Result<(), ErrorCode>> for CommandReturn {
+    #[flux_rs::trusted]
     fn from(rc: Result<(), ErrorCode>) -> Self {
         match rc {
             Ok(()) => CommandReturn::success(),