diff --git a/ostd/specs/mm/frame/frame_specs.rs b/ostd/specs/mm/frame/frame_specs.rs
index 36dc31ad7..32b420a4f 100644
--- a/ostd/specs/mm/frame/frame_specs.rs
+++ b/ostd/specs/mm/frame/frame_specs.rs
@@ -10,7 +10,7 @@ use crate::specs::{
     arch::*,
     mm::frame::{
         mapping::{frame_to_index, meta_to_index},
-        meta_owners::{FracMetadataPerm, MetadataPerm, PageUsage},
+        meta_owners::{FracMetadataPerm, MetaSlotStorage, MetadataPerm, PageUsage, typed_meta_wf},
         meta_region_owners::MetaRegionOwners,
     },
 };
@@ -80,6 +80,19 @@ impl<M: ?Sized> Frame<M> {
     }
 }
 
+impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M> {
+    /// Relates an externally stored metadata permission to this frame's slot permission.
+    pub open spec fn external_meta_wf(
+        self,
+        metadata_perm: MetadataPerm,
+        repr_perm: M::ReprPerm,
+    ) -> bool {
+        &&& self.ptr_inv()
+        &&& self.tracked_metadata_perm@ is None
+        &&& typed_meta_wf::<M>(self.slot_perm(), metadata_perm, repr_perm)
+    }
+}
+
 impl<M: ?Sized> Inv for Frame<M> {
     open spec fn inv(self) -> bool {
         &&& self.ptr_inv()
diff --git a/ostd/specs/mm/page_table/node/child.rs b/ostd/specs/mm/page_table/node/child.rs
index 1b7331307..040681efd 100644
--- a/ostd/specs/mm/page_table/node/child.rs
+++ b/ostd/specs/mm/page_table/node/child.rs
@@ -42,6 +42,7 @@ impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
                 &&& owner.is_node()
                 &&& node.inner@.ptr.addr() == owner.node().meta_vaddr()
                 &&& node.inner@.ptr_inv()
+                &&& node.inner@.external_meta_wf(owner.node().frame_permission.resource(), ())
             },
             Self::Frame(paddr, level, prop) => {
                 &&& owner.is_frame()
diff --git a/ostd/specs/mm/page_table/node/entry.rs b/ostd/specs/mm/page_table/node/entry.rs
index 1ba80a2ad..b850ed83c 100644
--- a/ostd/specs/mm/page_table/node/entry.rs
+++ b/ostd/specs/mm/page_table/node/entry.rs
@@ -30,8 +30,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
     ) -> bool {
         &&& parent_owner.level == owner.parent_level
         &&& parent_owner.inv()
-        &&& guard.inner.inner@.ptr.addr() == parent_owner.meta_vaddr()
-        &&& guard.inner.inner@.wf(parent_owner)
+        &&& parent_owner.relate_guard(guard)
         &&& owner.match_pte(parent_owner.children_perm.value()[self.idx as int], owner.parent_level)
     }
 
diff --git a/ostd/specs/mm/page_table/node/owners.rs b/ostd/specs/mm/page_table/node/owners.rs
index 6db1bb65a..3e86659cd 100644
--- a/ostd/specs/mm/page_table/node/owners.rs
+++ b/ostd/specs/mm/page_table/node/owners.rs
@@ -285,7 +285,7 @@ impl<C: PageTableConfig> NodeOwner<C> {
         )
     }
 
-    pub open spec fn meta_value(self, regions: MetaRegionOwners) -> PageTablePageMeta<C> {
+    pub open spec fn meta_value(self) -> PageTablePageMeta<C> {
         typed_meta_value::<PageTablePageMeta<C>>(self.frame_permission.resource(), ())
     }
 
@@ -297,11 +297,10 @@ impl<C: PageTableConfig> NodeOwner<C> {
         &&& regions.contains(idx)
         &&& self.frame_permission.id() == regions.slot_owners[idx].metadata_perm.id()
         &&& self.meta_wf(regions)
-        &&& self.meta_value(regions).wf(self.meta_own)
-        &&& self.level == self.meta_value(regions).level
-        &&& self.meta_own.nr_children.id() == self.meta_value(
-            regions,
-        ).nr_children.id()
+        &&& self.meta_value().wf(self.meta_own)
+        &&& self.level == self.meta_value().level
+        &&& self.meta_own.nr_children.id()
+            == self.meta_value().nr_children.id()
         // A page-table node's slot is tracked with `PageTable` usage (set at
         // allocation via `get_node_from_unused_spec`). This discriminates node
         // slots from data-frame slots (`Frame`/MMIO) by `usage` alone, so a
@@ -362,6 +361,7 @@ impl<'rcu, C: PageTableConfig> NodeOwner<C> {
     pub open spec fn relate_guard(self, guard: PageTableGuard<'rcu, C>) -> bool {
         &&& guard.inner.inner@.ptr.addr() == self.meta_vaddr()
         &&& guard.inner.inner@.wf(self)
+        &&& guard.inner.inner@.external_meta_wf(self.frame_permission.resource(), ())
     }
 }
 
diff --git a/ostd/src/mm/frame/frame_ref.rs b/ostd/src/mm/frame/frame_ref.rs
index 05e3842c9..3ce84c5c2 100644
--- a/ostd/src/mm/frame/frame_ref.rs
+++ b/ostd/src/mm/frame/frame_ref.rs
@@ -51,6 +51,9 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> FrameRef<'_, M> {
         ensures
             r.inner@.ptr.addr() == frame_to_meta(raw),
             r.inner@.ptr_inv(),
+            r.inner@.tracked_slot_perm@ == slot_perm,
+            r.inner@.tracked_metadata_perm@ is None,
+            MetaSlot::perms_related(r.inner@.slot_perm(), metadata_perm.resource()),
     )]
     pub(in crate::mm) unsafe fn borrow_paddr(raw: Paddr) -> Self {
         let frame = Frame::<M> {
diff --git a/ostd/src/mm/frame/mod.rs b/ostd/src/mm/frame/mod.rs
index 52d048b44..9d335c282 100644
--- a/ostd/src/mm/frame/mod.rs
+++ b/ostd/src/mm/frame/mod.rs
@@ -258,24 +258,40 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
     /// - By requiring the caller to provide a typed permission, we ensure that the metadata is of type `M`.
     /// While a non-verified caller cannot be trusted to obey this interface, all functions that return a `Frame<M>` also
     /// return an appropriate permission.
-    #[verus_spec(
+    #[verus_spec(ret =>
         with
-            Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
-            Tracked(metadata_perms): Tracked<&'a MetadataPerm>,
+            Tracked(metadata_perm): Tracked<Option<&'a MetadataPerm>>,
             Tracked(repr_perm): Tracked<&'a M::ReprPerm>,
         requires
-            self.ptr == points_to.pptr(),
-            typed_meta_wf::<M>(*points_to, *metadata_perms, *repr_perm),
-        returns
-            typed_meta_value::<M>(*metadata_perms, *repr_perm),
+            self.ptr_inv(),
+            {
+                self.inv() && metadata_perm is None
+                && typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), *repr_perm) ||
+                metadata_perm is Some
+                && self.external_meta_wf(*metadata_perm->0, *repr_perm)
+            },
+        ensures
+            {
+                let metadata_perm = if metadata_perm is Some {*metadata_perm -> 0} else
+                    { self.metadata_perm() };
+                ret == typed_meta_value::<M>(metadata_perm, *repr_perm)
+            },
     )]
     pub fn meta<'a>(&'a self) -> &'a M {
         // SAFETY: The type is tracked by the typed storage permission.
         //  unsafe { &*self.slot().as_meta_ptr::<M>() }
+        proof_decl! {
+            let tracked slot_perm = self.tracked_slot_perm.borrow();
+            let tracked metadata_perm = if metadata_perm is Some {
+                metadata_perm.tracked_borrow()
+            } else {
+                self.tracked_metadata_perm.tracked_borrow().tracked_borrow()
+            };
+        }
         borrow_meta(
             ReprPtr::<MetaSlotStorage, M>::from_pptr(PPtr::from_addr(self.ptr.addr())),
-            Tracked(points_to),
-            Tracked(metadata_perms),
+            Tracked(slot_perm),
+            Tracked(metadata_perm),
             Tracked(repr_perm),
         )
     }
@@ -473,6 +489,9 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M> {
         ensures
             res.inner@.ptr.addr() == self.ptr.addr(),
             res.inner@.ptr_inv(),
+            res.inner@.tracked_slot_perm@ == regions.slots[self.index()],
+            res.inner@.tracked_metadata_perm@ is None,
+            MetaSlot::perms_related(res.inner@.slot_perm(), frame_permission.resource()),
     )]
     pub(in crate::mm) fn borrow_with_permission<'a>(&self) -> FrameRef<'a, M> {
         unsafe {
diff --git a/ostd/src/mm/page_table/cursor/locking.rs b/ostd/src/mm/page_table/cursor/locking.rs
index 842bb4890..032c66eec 100644
--- a/ostd/src/mm/page_table/cursor/locking.rs
+++ b/ostd/src/mm/page_table/cursor/locking.rs
@@ -167,7 +167,7 @@ pub fn lock_range<'rcu, C: PageTableConfig, A: InAtomicMode>(
         assert(regions.contains(cont_slot_idx));
     }
     let tracked cont_node_owner = cont.entry_own.tracked_borrow_node();
-    #[verus_spec(with Tracked(cont_node_owner), Tracked(&*regions))]
+    #[verus_spec(with Tracked(cont_node_owner))]
     let guard_level = subtree_root.level();
     proof {
         cursor_own.guard_level = guard_level;
@@ -396,9 +396,7 @@ fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig, A: InAtomicMode>
 
         let tracked mut cont = cursor_own.continuations.tracked_remove(cursor_own.level - 1);
         let tracked node_owner = cont.entry_own.tracked_borrow_node();
-        let tracked meta_points_to = regions.slots.tracked_borrow(node_owner.slot_index);
         #[verus_spec(with
-            Tracked(meta_points_to),
             Tracked(node_owner.tracked_borrow_metadata_perm()),
             Tracked(&()),
             Ghost(node_owner.meta_own.stray.id())
@@ -483,9 +481,7 @@ fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig, A: InAtomicMode>
 
     let tracked mut cont = cursor_own.continuations.tracked_remove(cursor_own.level - 1);
     let tracked node_owner = cont.entry_own.tracked_borrow_node();
-    let tracked meta_points_to = regions.slots.tracked_borrow(node_owner.slot_index);
     #[verus_spec(with
-        Tracked(meta_points_to),
         Tracked(node_owner.tracked_borrow_metadata_perm()),
         Tracked(&()),
         Ghost(node_owner.meta_own.stray.id())
diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs
index 043fce201..d53c0d289 100644
--- a/ostd/src/mm/page_table/cursor/mod.rs
+++ b/ostd/src/mm/page_table/cursor/mod.rs
@@ -597,6 +597,8 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
                             EntryOwner::<C>::axiom_frame_is_tracked_iff_not_mmio(
                                 owner_before_permission_take.cur_entry_owner(),
                             );
+                            assert(regions.contains(idx));
+                            assert(old(regions).contains(idx));
                         }
                         owner_before_permission_take.lemma_cur_frame_clone_requires(
                             item,
@@ -1025,7 +1027,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
                         pt.make_guard_unchecked(rcu_guard)
                     };
 
-                    #[verus_spec(with Tracked(&mut child_node_owner), Tracked(&*regions))]
+                    #[verus_spec(with Tracked(&mut child_node_owner))]
                     let nr_children = pt_guard.nr_children();
 
                     // `nr_children()` requires `child_node_owner.metaregion_sound_node`,
diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs
index f9bfff2dc..411b96d63 100644
--- a/ostd/src/mm/page_table/node/entry.rs
+++ b/ostd/src/mm/page_table/node/entry.rs
@@ -119,21 +119,19 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
     #[verus_spec(
         with Tracked(owner): Tracked<EntryOwner<C>>,
              Tracked(parent_owner): Tracked<&NodeOwner<C>>,
-             Tracked(regions): Tracked<&MetaRegionOwners>,
         requires
             owner.inv(),
             self.wf(owner),
+            parent_owner.level == parent_owner.meta_value().level,
             parent_owner.relate_guard(*self.node),
             parent_owner.inv(),
             parent_owner.level == owner.parent_level,
-            regions.inv(),
-            parent_owner.metaregion_sound_node(*regions),
         returns
             owner.is_node(),
     )]
     pub(in crate::mm) fn is_node(&self) -> bool {
         self.pte.is_present() && !self.pte.is_last(
-            #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+            #[verus_spec(with Tracked(&*parent_owner))]
             self.node.level(),
         )
     }
@@ -160,7 +158,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
             final(regions).inv(),
     )]
     pub(in crate::mm) fn to_ref(&self) -> ChildRef<'rcu, C> {
-        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+        #[verus_spec(with Tracked(&*parent_owner))]
         let level = self.node.level();
 
         // SAFETY:
@@ -381,7 +379,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
         // SAFETY:
         //  - The PTE is not referenced by other `ChildRef`s (since we have `&mut self`).
         //  - The level matches the current node.
-        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+        #[verus_spec(with Tracked(&*parent_owner))]
         let level = self.node.level();
 
         let old_child = unsafe {
@@ -390,9 +388,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
         };
 
         if old_child.is_none() && !new_child.is_none() {
-            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
             #[verus_spec(with
-                Tracked(meta_points_to),
                 Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                     &parent_owner.frame_permission,
                 )),
@@ -405,9 +401,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
             }
             nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
         } else if !old_child.is_none() && new_child.is_none() {
-            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
             #[verus_spec(with
-                Tracked(meta_points_to),
                 Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                     &parent_owner.frame_permission,
                 )),
@@ -635,7 +629,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
         // For restoring `count_consistent` after adding the child below.
         let ghost cp0 = parent_owner.children_perm.value();
 
-        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+        #[verus_spec(with Tracked(&*parent_owner))]
         let level = self.node.level();
 
         if entry_is_present || level <= 1 {
@@ -706,9 +700,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
                 self.node.write_pte(self.idx, self.pte)
             };
 
-            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
             #[verus_spec(with
-                Tracked(meta_points_to),
                 Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                     &parent_owner.frame_permission,
                 )),
@@ -894,7 +886,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
     pub(in crate::mm) fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A) -> Option<
         PageTableGuard<'rcu, C>,
     > {
-        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+        #[verus_spec(with Tracked(&*parent_owner))]
         let level = self.node.level();
 
         if !(self.pte.is_last(level) && level > 1) {
@@ -1616,7 +1608,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
             self.read_pte(idx)
         };
 
-        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+        #[verus_spec(with Tracked(&*parent_owner))]
         let level = self.level();
 
         let old_child = unsafe {
@@ -1628,9 +1620,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
         let ghost cp0 = parent_owner.children_perm.value();
 
         if old_child.is_none() && !new_child.is_none() {
-            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
             #[verus_spec(with
-                Tracked(meta_points_to),
                 Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                     &parent_owner.frame_permission,
                 )),
@@ -1643,9 +1633,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
             }
             nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
         } else if !old_child.is_none() && new_child.is_none() {
-            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
             #[verus_spec(with
-                Tracked(meta_points_to),
                 Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                     &parent_owner.frame_permission,
                 )),
@@ -1846,7 +1834,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
         idx: usize,
         guard: &'rcu A,
     ) -> PageTableGuard<'rcu, C> {
-        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
+        #[verus_spec(with Tracked(&*parent_owner))]
         let level = self.level();
 
         let ghost old_path = owner.value().path;
@@ -1929,9 +1917,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
         // (`alloc` allocates a different slot, `write_pte` leaves regions
         // immutable).
 
-        let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
         #[verus_spec(with
-            Tracked(meta_points_to),
             Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                 &parent_owner.frame_permission,
             )),
@@ -2055,9 +2041,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
     ) {
         // For restoring `count_consistent` after the absent→frame install.
         let ghost cp0 = parent_owner.children_perm.value();
-        let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
         #[verus_spec(with
-            Tracked(meta_points_to),
             Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                 &parent_owner.frame_permission,
             )),
diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs
index b85e7a9ca..402c281cd 100644
--- a/ostd/src/mm/page_table/node/mod.rs
+++ b/ostd/src/mm/page_table/node/mod.rs
@@ -223,19 +223,16 @@ impl<C: PageTableConfig> PageTableNode<C> {
     #[verus_spec(
         with
             Tracked(owner): Tracked<&NodeOwner<C>>,
-            Tracked(regions): Tracked<&MetaRegionOwners>
     )]
     pub(super) fn level(&self) -> PagingLevel
         requires
-            self.ptr.addr() == regions.slots[owner.slot_index].addr(),
-            owner.metaregion_sound_node(*regions),
+            self.external_meta_wf(owner.frame_permission.resource(), ()),
+            owner.level == owner.meta_value().level,
         returns
             owner.level,
     {
-        let tracked points_to = regions.slots.tracked_borrow(owner.slot_index);
         #[verus_spec(with
-            Tracked(points_to),
-            Tracked(owner.tracked_borrow_metadata_perm()),
+            Tracked(Some(owner.tracked_borrow_metadata_perm())),
             Tracked(&())
         )]
         let meta = self.meta();
@@ -389,6 +386,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
             Tracked(guards): Tracked<&mut Guards>
         requires
             self.inner@.invariants(*owner),
+            self.inner@.external_meta_wf(owner.frame_permission.resource(), ()),
             old(guards).unlocked(owner.meta_vaddr()),
         ensures
             final(guards).lock_held(owner.meta_vaddr()),
@@ -414,6 +412,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
              Tracked(guards): Tracked<&mut Guards>,
         requires
             self.inner@.invariants(*owner),
+            self.inner@.external_meta_wf(owner.frame_permission.resource(), ()),
             old(guards).unlocked(owner.meta_vaddr()),
         ensures
             final(guards).lock_held(owner.meta_vaddr()),
@@ -485,19 +484,16 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
     /// - We require the caller to provide a permission token to ensure that this function is only called on a valid page table node.
     #[verus_spec(nr =>
         with Tracked(owner) : Tracked<&NodeOwner<C>>,
-             Tracked(regions): Tracked<&MetaRegionOwners>,
         requires
+            owner.meta_own.nr_children.id() == owner.meta_value().nr_children.id(),
             self.inner.inner@.invariants(*owner),
-            regions.inv(),
-            owner.metaregion_sound_node(*regions),
+            self.inner.inner@.external_meta_wf(owner.frame_permission.resource(), ()),
         returns
             owner.meta_own.nr_children.value(),
     )]
     pub fn nr_children(&self) -> u16 {
-        let tracked points_to = regions.slots.tracked_borrow(owner.slot_index);
         #[verus_spec(with
-            Tracked(points_to),
-            Tracked(owner.tracked_borrow_metadata_perm()),
+            Tracked(Some(owner.tracked_borrow_metadata_perm())),
             Tracked(&())
         )]
         let meta = self.meta();
@@ -508,17 +504,11 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
     /// Returns if the page table node is detached from its parent.
     #[verus_spec(res =>
         with
-            Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
             Tracked(metadata_perms): Tracked<&'a MetadataPerm>,
             Tracked(repr_perm): Tracked<&'a ()>,
             Ghost(stray_id): Ghost<vstd::cell::CellId>,
         requires
-            old(self).inner.inner@.ptr.addr() == points_to.addr(),
-            typed_meta_wf::<PageTablePageMeta<C>>(
-                *points_to,
-                *metadata_perms,
-                *repr_perm,
-            ),
+            old(self).inner.inner@.external_meta_wf(*metadata_perms, *repr_perm),
             typed_meta_value::<PageTablePageMeta<C>>(
                 *metadata_perms,
                 *repr_perm,
@@ -531,8 +521,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
     pub(super) fn stray_mut<'a>(&'a mut self) -> &'a pcell_maybe_uninit::PCell<bool> {
         // SAFETY: The lock is held so we have an exclusive access.
         #[verus_spec(with
-            Tracked(points_to),
-            Tracked(metadata_perms),
+            Tracked(Some(metadata_perms)),
             Tracked(repr_perm)
         )]
         let meta = self.meta();
@@ -628,12 +617,10 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
     /// Gets the mutable reference to the number of valid PTEs in the node.
     #[verus_spec(res =>
         with
-            Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
             Tracked(metadata_perms): Tracked<&'a MetadataPerm>,
             Ghost(nr_children_id): Ghost<vstd::cell::CellId>,
         requires
-            old(self).inner.inner@.ptr.addr() == points_to.addr(),
-            typed_meta_wf::<PageTablePageMeta<C>>(*points_to, *metadata_perms, ()),
+            old(self).inner.inner@.external_meta_wf(*metadata_perms, ()),
             typed_meta_value::<PageTablePageMeta<C>>(
                 *metadata_perms,
                 (),
@@ -646,8 +633,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
     fn nr_children_mut<'a>(&'a mut self) -> &'a pcell_maybe_uninit::PCell<u16> {
         // SAFETY: The lock is held so we have an exclusive access.
         #[verus_spec(with
-            Tracked(points_to),
-            Tracked(metadata_perms),
+            Tracked(Some(metadata_perms)),
             Tracked(&())
         )]
         let meta = self.meta();