From 050a3e3e87350315e65c5c43d9d22eadc3f3a858 Mon Sep 17 00:00:00 2001
From: rikosellic <64517311+rikosellic@users.noreply.github.com>
Date: Tue, 14 Apr 2026 15:24:32 +0800
Subject: [PATCH] Make `PageTableConfig::TOP_LEVEL_CAN_UNMAP` be associated
 const

---
 ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs |  2 +-
 ostd/src/mm/kspace/mod.rs                          | 11 +----------
 ostd/src/mm/page_table/cursor/mod.rs               |  8 ++++----
 ostd/src/mm/page_table/mod.rs                      |  9 +--------
 ostd/src/mm/vm_space.rs                            |  8 --------
 5 files changed, 7 insertions(+), 31 deletions(-)

diff --git a/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs b/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs
index bae8d6a2d..716012b91 100644
--- a/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs
+++ b/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs
@@ -83,7 +83,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
         ||| self.inner.va >= self.inner.barrier_va.end
         ||| C::item_into_raw(item).1 > C::HIGHEST_TRANSLATION_LEVEL()
         ||| C::item_into_raw(item).1 >= self.inner.guard_level
-        ||| (!C::TOP_LEVEL_CAN_UNMAP_spec() && C::item_into_raw(item).1 >= NR_LEVELS)
+        ||| (!C::TOP_LEVEL_CAN_UNMAP && C::item_into_raw(item).1 >= NR_LEVELS)
         ||| self.inner.va % page_size(C::item_into_raw(item).1) != 0
         ||| self.inner.va + page_size(C::item_into_raw(item).1) > self.inner.barrier_va.end
     }
diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs
index 6386c99bb..18d884993 100644
--- a/ostd/src/mm/kspace/mod.rs
+++ b/ostd/src/mm/kspace/mod.rs
@@ -169,16 +169,7 @@ unsafe impl PageTableConfig for KernelPtConfig {
         256..512
     }
 
-    open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool {
-        false
-    }
-
-    fn TOP_LEVEL_CAN_UNMAP() -> (b: bool)
-        ensures
-            b == Self::TOP_LEVEL_CAN_UNMAP_spec(),
-    {
-        false
-    }
+    const TOP_LEVEL_CAN_UNMAP: bool = false;
 
     type E = PageTableEntry;
     type C = PagingConsts;
diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs
index 01d75269c..064f3a868 100644
--- a/ostd/src/mm/page_table/cursor/mod.rs
+++ b/ostd/src/mm/page_table/cursor/mod.rs
@@ -775,7 +775,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
 
             match cur_child {
                 ChildRef::PageTable(pt) => {
-                    if find_unmap_subtree && cur_entry_fits_range && (C::TOP_LEVEL_CAN_UNMAP()
+                    if find_unmap_subtree && cur_entry_fits_range && (C::TOP_LEVEL_CAN_UNMAP
                         || self.level != C::NR_LEVELS()) {
 
                         proof {
@@ -3214,7 +3214,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                 CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
             ),
             // panic
-            !C::TOP_LEVEL_CAN_UNMAP_spec() ==> old(owner).level < NR_LEVELS,
+            !C::TOP_LEVEL_CAN_UNMAP ==> old(owner).level < NR_LEVELS,
         ensures
             final(owner)@.mappings == old(owner)@.mappings - PageTableOwner(
                 old(owner).cur_subtree(),
@@ -3696,8 +3696,8 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
             },
             Child::PageTable(pt) => {
                 // debug_assert_eq!(pt.level(), level - 1);
-                if !C::TOP_LEVEL_CAN_UNMAP() {
-                    assert(!C::TOP_LEVEL_CAN_UNMAP_spec());
+                if !C::TOP_LEVEL_CAN_UNMAP {
+                    assert(!C::TOP_LEVEL_CAN_UNMAP);
                     if level as usize == NR_LEVELS {
                         assert(owner.level == NR_LEVELS);
 
diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs
index 899c14c2d..8fc96d656 100644
--- a/ostd/src/mm/page_table/mod.rs
+++ b/ostd/src/mm/page_table/mod.rs
@@ -124,14 +124,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static {
     /// This is for the kernel page table, whose second-top-level page
     /// tables need `'static` lifetime to be shared with user page tables.
     /// Other page tables do not need to set this to `false`.
-    open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool {
-        true
-    }
-
-    fn TOP_LEVEL_CAN_UNMAP() -> (b: bool)
-        ensures
-            b == Self::TOP_LEVEL_CAN_UNMAP_spec(),
-    ;
+    const TOP_LEVEL_CAN_UNMAP: bool = true;
 
     /// The type of the page table entry.
     type E: PageTableEntryTrait;
diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs
index ce299d4b0..21fc7cf6f 100644
--- a/ostd/src/mm/vm_space.rs
+++ b/ostd/src/mm/vm_space.rs
@@ -1433,18 +1433,10 @@ unsafe impl PageTableConfig for UserPtConfig {
         0..MAX_USERSPACE_VADDR
     }
 
-    open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> (b: bool) {
-        true
-    }
-
     fn TOP_LEVEL_INDEX_RANGE() -> Range<usize> {
         0..256
     }
 
-    fn TOP_LEVEL_CAN_UNMAP() -> (b: bool) {
-        true
-    }
-
     type E = PageTableEntry;
 
     type C = PagingConsts;