fix

Author: hiroki-chen

ostd/specs/mm/page_table/node/entry_owners.rs

@@ -11,7 +11,6 @@ use crate::mm::frame::meta::REF_COUNT_UNUSED;
 use crate::mm::page_prop::PageProperty;
 use crate::mm::page_table::*;
 use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
-use crate::mm::frame::meta::REF_COUNT_UNUSED;
 use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
 use crate::specs::arch::paging_consts::PagingConsts;
 use crate::specs::arch::*;

ostd/specs/mm/page_table/node/owners.rs

@@ -106,7 +106,7 @@ impl<C: PageTableConfig> Inv for NodeOwner<C> {
 impl<C: PageTableConfig> NodeOwner<C> {
     /// Returns a NodeOwner with children_perm updated at the given index.
     /// Used to specify the state after storing a new PTE for an allocated child.
-    pub open spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
+    pub uninterp spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
 
     #[verifier::external_body]
     pub axiom fn set_children_perm_axiom(self, idx: usize, pte: C::E)