Make PageTableConfig::TOP_LEVEL_CAN_UNMAP be associated const

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
     }

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;

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);
 

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;

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;