From fab81ad1a91a33d72cf1c7b20895e2aa67fb2773 Mon Sep 17 00:00:00 2001
From: Evan Johnson <e5johnso@eng.ucsd.edu>
Date: Thu, 10 Oct 2024 10:31:22 -0700
Subject: [PATCH] refine mpu::Permissions

---
 kernel/src/platform/mpu.rs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs
index 14d007b608..b4b8310954 100644
--- a/kernel/src/platform/mpu.rs
+++ b/kernel/src/platform/mpu.rs
@@ -11,11 +11,17 @@ use flux_support::*;
 
 /// User mode access permissions.
 #[derive(Copy, Clone, Debug)]
+#[flux_rs::refined_by(r: bool, w: bool, x: bool)]
 pub enum Permissions {
+    #[flux::variant(Permissions[true, true, true])]
     ReadWriteExecute,
+    #[flux::variant(Permissions[true, true, false])]
     ReadWriteOnly,
+    #[flux::variant(Permissions[true, false, true])]
     ReadExecuteOnly,
+    #[flux::variant(Permissions[true, false, false])]
     ReadOnly,
+    #[flux::variant(Permissions[false, false, true])]
     ExecuteOnly,
 }