ostd/mm/page_table/node/
entry.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module provides accessors to the page table entries in a node.
3use vstd::prelude::*;
4
5use vstd::simple_pptr::{self, PPtr, PointsTo};
6
7use vstd_extra::cast_ptr;
8use vstd_extra::ghost_tree::*;
9use vstd_extra::ownership::*;
10use vstd_extra::undroppable::NeverDrop;
11
12use crate::mm::frame::meta::mapping::{frame_to_index, meta_to_frame};
13use crate::mm::frame::{Frame, FrameRef};
14use crate::mm::page_table::*;
15use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
16use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
17use crate::specs::arch::paging_consts::PagingConsts;
18use crate::specs::mm::frame::meta_owners::MetaSlotOwner;
19use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
20use crate::specs::task::InAtomicMode;
21
22use core::marker::PhantomData;
23use core::mem::ManuallyDrop;
24
25use crate::{
26    mm::{nr_subpage_per_huge, page_prop::PageProperty},
27    //    sync::RcuDrop,
28    //    task::atomic_mode::InAtomicMode,
29};
30
31use super::*;
32
33verus! {
34
35/// A reference to a page table node.
36pub type PageTableNodeRef<'a, C> = FrameRef<'a, PageTablePageMeta<C>>;
37
38/// A guard that holds the lock of a page table node.
39#[rustc_has_incoherent_inherent_impls]
40pub struct PageTableGuard<'rcu, C: PageTableConfig> {
41    pub inner: PageTableNodeRef<'rcu, C>,
42}
43
44impl<'rcu, C: PageTableConfig> core::ops::Deref for PageTableGuard<'rcu, C> {
45    type Target = PageTableNodeRef<'rcu, C>;
46
47    #[verus_spec(ensures returns self.inner)]
48    fn deref(&self) -> &Self::Target {
49        &self.inner
50    }
51}
52
53#[rustc_has_incoherent_inherent_impls]
54pub struct Entry<'rcu, C: PageTableConfig> {
55    /// The page table entry.
56    ///
57    /// We store the page table entry here to optimize the number of reads from
58    /// the node. We cannot hold a `&mut E` reference to the entry because that
59    /// other CPUs may modify the memory location for accessed/dirty bits. Such
60    /// accesses will violate the aliasing rules of Rust and cause undefined
61    /// behaviors.
62    pub pte: C::E,
63    /// The index of the entry in the node.
64    pub idx: usize,
65    /// The node that contains the entry.
66    pub node: PPtr<PageTableGuard<'rcu, C>>,
67}
68
69impl<'rcu, C: PageTableConfig> Entry<'rcu, C> {
70    pub open spec fn new_spec(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self {
71        Self { pte, idx, node }
72    }
73
74    #[verifier::when_used_as_spec(new_spec)]
75    pub fn new(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self {
76        Self { pte, idx, node }
77    }
78}
79
80#[verus_verify]
81impl<'a, 'rcu, C: PageTableConfig> Entry<'rcu, C> {
82    /// Returns if the entry does not map to anything.
83    #[rustc_allow_incoherent_impl]
84    #[verus_spec]
85    pub fn is_none(&self) -> bool {
86        !self.pte.is_present()
87    }
88
89    /// Returns if the entry maps to a page table node.
90    #[rustc_allow_incoherent_impl]
91    #[verus_spec(
92        with Tracked(owner): Tracked<EntryOwner<C>>,
93            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
94            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
95    )]
96    pub fn is_node(&self) -> bool
97        requires
98            owner.inv(),
99            self.wf(owner),
100            guard_perm.addr() == self.node.addr(),
101            parent_owner.relate_guard_perm(*guard_perm),
102            parent_owner.inv(),
103    {
104        let guard = self.node.borrow(Tracked(guard_perm));
105
106        self.pte.is_present() && !self.pte.is_last(
107            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
108            guard.level(),
109        )
110    }
111
112    /// Gets a reference to the child.
113    #[verus_spec(
114        with Tracked(owner): Tracked<&EntryOwner<C>>,
115            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
116            Tracked(regions): Tracked<&mut MetaRegionOwners>,
117            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
118    )]
119    pub fn to_ref(&self) -> (res: ChildRef<'rcu, C>)
120        requires
121            self.wf(*owner),
122            owner.inv(),
123            old(regions).inv(),
124            parent_owner.level == owner.parent_level,
125            guard_perm.addr() == self.node.addr(),
126            guard_perm.is_init(),
127            guard_perm.value().inner.inner@.ptr.addr() == parent_owner.meta_perm.addr(),
128            guard_perm.value().inner.inner@.ptr.addr() == parent_owner.meta_perm.points_to.addr(),
129            guard_perm.value().inner.inner@.wf(*parent_owner),
130            parent_owner.meta_perm.is_init(),
131            parent_owner.meta_perm.wf(),
132            parent_owner.inv(),
133            owner.is_node() ==> owner.node.unwrap().relate_region(*old(regions)),
134        ensures
135            regions.inv(),
136            res.wf(*owner),
137            owner.is_node() ==> owner.node.unwrap().relate_region(*regions),
138    {
139        let guard = self.node.borrow(Tracked(guard_perm));
140
141        assert(parent_owner.level == parent_owner.meta_perm.value().level) by { admit() };
142
143        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
144        let level = guard.level();
145
146        // SAFETY:
147        //  - The PTE outlives the reference (since we have `&self`).
148        //  - The level matches the current node.
149        #[verus_spec(with Tracked(regions), Tracked(owner))]
150        let res = ChildRef::from_pte(&self.pte, level);
151
152        assert(owner.is_node() ==> owner.node.unwrap().relate_region(*regions)) by { admit() };
153        res
154    }
155
156    /// Operates on the mapping properties of the entry.
157    ///
158    /// It only modifies the properties if the entry is present.
159    #[verus_spec(
160        with Tracked(owner) : Tracked<&mut EntryOwner<C>>,
161            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
162            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>,
163    )]
164    pub fn protect(&mut self, op: impl FnOnce(PageProperty) -> PageProperty)
165        requires
166            old(owner).inv(),
167            old(self).wf(*old(owner)),
168            old(parent_owner).inv(),
169            old(self).node.addr() == old(guard_perm).addr(),
170            old(parent_owner).relate_guard_perm(*old(guard_perm)),
171            op.requires((old(self).pte.prop(),)),
172            old(owner).is_frame()
173        ensures
174            owner.inv(),
175            self.wf(*owner),
176            parent_owner.inv(),
177            parent_owner.relate_guard_perm(*guard_perm),
178            guard_perm.addr() == old(guard_perm).addr(),
179            owner.is_frame(),
180    {
181        let ghost pte0 = self.pte;
182
183        if !self.pte.is_present() {
184            return ;
185        }
186        let prop = self.pte.prop();
187        let new_prop = op(prop);
188
189        /*if prop == new_prop {
190            return;
191        }*/
192
193        proof {
194            self.pte.set_prop_properties(new_prop);
195        }
196        self.pte.set_prop(new_prop);
197
198        assert(self.pte.paddr() == pte0.paddr()) by { admit() };
199
200        let mut guard = self.node.take(Tracked(guard_perm));
201
202        // SAFETY:
203        //  1. The index is within the bounds.
204        //  2. We replace the PTE with a new one, which differs only in
205        //     `PageProperty`, so the level still matches the current
206        //     page table node.
207        #[verus_spec(with Tracked(parent_owner))]
208        guard.write_pte(self.idx, self.pte);
209
210        proof {
211            let tracked mut frame_owner = owner.frame.tracked_take();
212            frame_owner.prop = new_prop;
213            owner.frame = Some(frame_owner);
214        }
215        assert(owner.match_pte(self.pte, owner.parent_level));
216
217        self.node.put(Tracked(guard_perm), guard);
218    }
219
220    /// Replaces the entry with a new child.
221    ///
222    /// The old child is returned.
223    ///
224    /// # Panics
225    ///
226    /// The method panics if the level of the new child does not match the
227    /// current node.
228    #[verus_spec(
229        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
230            Tracked(owner): Tracked<&EntryOwner<C>>,
231            Tracked(new_owner): Tracked<&EntryOwner<C>>,
232            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
233            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
234    )]
235    pub fn replace(&mut self, new_child: Child<C>) -> (res: Child<C>)
236        requires
237            old(self).wf(*owner),
238            owner.inv(),
239            new_child.wf(*new_owner),
240            new_owner.inv(),
241            old(parent_owner).inv(),
242            old(regions).inv(),
243            owner.is_node() ==> owner.node.unwrap().relate_region(*old(regions)),
244            old(guard_perm).addr() == old(self).node.addr(),
245            old(parent_owner).relate_guard_perm(*old(guard_perm)),
246        ensures
247            parent_owner.inv(),
248            parent_owner.relate_guard_perm(*guard_perm),
249            guard_perm.pptr() == old(guard_perm).pptr(),
250            guard_perm.value().inner.inner@.ptr.addr() == old(guard_perm).value().inner.inner@.ptr.addr(),
251            regions.inv(),
252            self.wf(*new_owner),
253            new_owner.inv(),
254            res.wf(*owner),
255            owner.is_node() ==> owner.node.unwrap().relate_region(*regions),
256    {
257        /* match &new_child {
258            Child::PageTable(node) => {
259                assert_eq!(node.level(), self.node.level() - 1);
260            }
261            Child::Frame(_, level, _) => {
262                assert_eq!(*level, self.node.level());
263            }
264            Child::None => {}
265        }*/
266        let mut guard = self.node.take(Tracked(guard_perm));
267
268        // SAFETY:
269        //  - The PTE is not referenced by other `ChildRef`s (since we have `&mut self`).
270        //  - The level matches the current node.
271        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
272        let level = guard.level();
273
274        #[verus_spec(with Tracked(regions), Tracked(&owner))]
275        let old_child = Child::from_pte(self.pte, level);
276
277        if old_child.is_none() && !new_child.is_none() {
278            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
279            let nr_children = guard.nr_children_mut();
280            let _tmp = nr_children.take(Tracked(&mut parent_owner.meta_own.nr_children));
281            assert(_tmp < NR_ENTRIES()) by { admit() };
282            nr_children.put(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
283        } else if !old_child.is_none() && new_child.is_none() {
284            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
285            let nr_children = guard.nr_children_mut();
286            let _tmp = nr_children.take(Tracked(&mut parent_owner.meta_own.nr_children));
287            assert(_tmp > 0) by { admit() };
288            nr_children.put(Tracked(&mut parent_owner.meta_own.nr_children), _tmp - 1);
289        }
290        #[verus_spec(with Tracked(&new_owner), Tracked(regions))]
291        let new_pte = new_child.into_pte();
292
293        assert(new_child.wf(*new_owner));
294        assert(owner.is_node() ==> owner.node.unwrap().relate_region(*regions)) by { admit() };
295        // SAFETY:
296        //  1. The index is within the bounds.
297        //  2. The new PTE is a valid child whose level matches the current page table node.
298        //  3. The ownership of the child is passed to the page table node.
299        #[verus_spec(with Tracked(parent_owner))]
300        guard.write_pte(self.idx, new_pte);
301
302        self.node.put(Tracked(guard_perm), guard);
303
304        self.pte = new_pte;
305
306        old_child
307    }
308
309    /// Allocates a new child page table node and replaces the entry with it.
310    ///
311    /// If the old entry is not none, the operation will fail and return `None`.
312    /// Otherwise, the lock guard of the new child page table node is returned.
313    #[verifier::external_body]
314    #[verus_spec(res =>
315        with Tracked(owner): Tracked<&mut OwnerSubtree<C>>,
316            Tracked(regions): Tracked<&mut MetaRegionOwners>,
317            Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
318            Tracked(parent_guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
319            -> guard_perm: Tracked<Option<GuardPerm<'rcu, C>>>
320        requires
321            old(owner).inv(),
322            old(self).wf(old(owner).value),
323            old(regions).inv(),
324        ensures
325            old(owner).value.is_absent() ==> {
326                &&& res is Some
327                &&& owner.value.is_node()
328                &&& guard_perm@ is Some
329                &&& guard_perm@.unwrap().addr() == res.unwrap().addr()
330                &&& owner.level == old(owner).level
331                &&& owner.value.parent_level == old(owner).value.parent_level
332                &&& owner.value.node.unwrap().relate_guard_perm(guard_perm@.unwrap())
333            },
334            !old(owner).value.is_absent() ==> {
335                &&& res is None
336                &&& *owner == *old(owner)
337            },
338            forall |i: usize| old(guards).lock_held(i) ==> guards.lock_held(i),
339            parent_guard_perm.addr() == old(parent_guard_perm).addr(),
340            parent_guard_perm.is_init(),
341            parent_guard_perm.value().inner.inner@.ptr.addr() == old(parent_guard_perm).value().inner.inner@.ptr.addr(),
342            owner.inv(),
343            regions.inv(),
344    )]
345    pub fn alloc_if_none<A: InAtomicMode>(&mut self, guard: &'rcu A)
346    -> (res: Option<PPtr<PageTableGuard<'rcu, C>>>) {
347        let mut parent_guard = self.node.take(Tracked(parent_guard_perm));
348
349        if !(self.is_none() && parent_guard.level() > 1) {
350            proof_with!{|= Tracked(None)}
351            None
352        } else {
353
354        let level = parent_guard.level();
355        let new_page = /*RcuDrop::new(*/PageTableNode::<C>::alloc(level - 1)/*)*/;
356
357        let paddr = new_page.start_paddr();
358        // SAFETY: The page table won't be dropped before the RCU grace period
359        // ends, so it outlives `'rcu`.
360        let pt_ref = unsafe { PageTableNodeRef::borrow_paddr(paddr) };
361
362        proof_decl! {
363            let tracked mut guard_perm: Tracked<GuardPerm<'rcu, C>>;
364        }
365
366        // Lock before writing the PTE, so no one else can operate on it.
367        #[verus_spec(with Tracked(guards) => Tracked(guard_perm))]
368        let pt_lock_guard = pt_ref.lock(guard);
369
370        self.pte = Child::PageTable(new_page).into_pte();
371
372        // SAFETY:
373        //  1. The index is within the bounds.
374        //  2. The new PTE is a child in `C` and at the correct paging level.
375        //  3. The ownership of the child is passed to the page table node.
376        unsafe { parent_guard.write_pte(self.idx, self.pte) };
377
378        let nr_children = parent_guard.nr_children_mut();
379        //nr_children += 1;
380
381        self.node.put(Tracked(parent_guard_perm), parent_guard);
382
383        proof_with!{|= Tracked(Some(guard_perm))}
384        Some(pt_lock_guard)
385        }
386    }
387
388    /// Splits the entry to smaller pages if it maps to a huge page.
389    ///
390    /// If the entry does map to a huge page, it is split into smaller pages
391    /// mapped by a child page table node. The new child page table node
392    /// is returned.
393    ///
394    /// If the entry does not map to a untracked huge page, the method returns
395    /// `None`.
396    #[verus_spec(res =>
397        with Tracked(owner) : Tracked<&mut OwnerSubtree<C>>,
398            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
399            Tracked(regions): Tracked<&mut MetaRegionOwners>,
400            Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
401            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
402        requires
403            old(regions).inv(),
404            old(owner).inv(),
405            old(self).wf(old(owner).value),
406            old(self).node.addr() == old(guard_perm).addr(),
407            old(guard_perm).is_init(),
408            old(parent_owner).relate_guard_perm(*old(guard_perm)),
409            old(parent_owner).inv(),
410        ensures
411            old(owner).value.is_frame() ==> {
412                &&& res is Some
413                &&& owner.value.is_node()
414                &&& owner.level == old(owner).level
415                &&& parent_owner.relate_guard_perm(*guard_perm)
416                &&& guards.guards.contains_key(res.unwrap().addr())
417                &&& guards.guards[res.unwrap().addr()] is Some
418                &&& guards.guards[res.unwrap().addr()].unwrap().pptr() == res.unwrap()
419                &&& owner.value.node.unwrap().relate_guard_perm(guards.guards[res.unwrap().addr()].unwrap())
420                &&& owner.value.node.unwrap().meta_perm.addr() == res.unwrap().addr()
421            },
422            !old(owner).value.is_frame() ==> {
423                &&& res is None
424                &&& *owner == *old(owner)
425            },
426            owner.inv(),
427            regions.inv(),
428            parent_owner.inv(),
429            guard_perm.pptr() == old(guard_perm).pptr(),
430            guard_perm.value().inner.inner@.ptr.addr() == old(guard_perm).value().inner.inner@.ptr.addr(),
431    )]
432    #[verifier::external_body]
433    pub fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A) -> (res: Option<PPtr<PageTableGuard<'rcu, C>>>) {
434        let mut node_guard = self.node.take(Tracked(guard_perm));
435
436        assert(parent_owner.meta_perm.value().level <= NR_LEVELS()) by { admit() };
437
438        #[verus_spec(with Tracked(&mut parent_owner.meta_perm))]
439        let level = node_guard.level();
440
441        if !(self.pte.is_last(level) && level > 1) {
442            assert(!owner.value.is_frame()) by { admit() };
443            self.node.put(Tracked(guard_perm), node_guard);
444
445            return None;
446        }
447        //        #[verus_spec(with Tracked(&mut parent_owner.as_node.meta_perm))]
448
449        let pa = self.pte.paddr();
450        let prop = self.pte.prop();
451
452        proof_decl!{
453            let tracked mut new_owner: OwnerSubtree<C>;
454        }
455
456        #[verus_spec(with Tracked(regions) => Tracked(new_owner))]
457        let new_page =   /*RcuDrop::new(*/
458        PageTableNode::<C>::alloc(level - 1)  /*)*/
459        ;
460
461        assert(regions.inv());
462        assert(new_owner.value.is_node()) by { admit() };
463        assert(new_owner.inv()) by { admit() };
464
465        assert(new_page.ptr.addr() == parent_owner.meta_perm.points_to.addr()) by { admit() };
466        assert(FRAME_METADATA_RANGE().start <= new_page.ptr.addr() < FRAME_METADATA_RANGE().end)
467            by { admit() };
468        assert(new_page.ptr.addr() % META_SLOT_SIZE() == 0) by { admit() };
469
470        #[verus_spec(with Tracked(&mut parent_owner.meta_perm.points_to))]
471        let paddr = new_page.start_paddr();
472
473        assert(paddr < MAX_PADDR()) by { admit() };
474        assert(!regions.slots.contains_key(frame_to_index(paddr))) by { admit() };
475        assert(regions.dropped_slots.contains_key(frame_to_index(paddr))) by { admit() };
476
477        // SAFETY: The page table won't be dropped before the RCU grace period
478        // ends, so it outlives `'rcu`.
479        #[verus_spec(with Tracked(regions), Tracked(&parent_owner.meta_perm))]
480        let pt_ref = PageTableNodeRef::borrow_paddr(paddr);
481
482        proof_decl! {
483            let tracked mut guard_perm: Tracked<GuardPerm<'rcu, C>>;
484        }
485
486        // Lock before writing the PTE, so no one else can operate on it.
487        #[verus_spec(with Tracked(guards) => Tracked(guard_perm))]
488        let pt_lock_guard = pt_ref.lock(guard);
489
490        assert(1 < level < NR_LEVELS()) by { admit() };
491
492        for i in 0..nr_subpage_per_huge::<C>()
493            invariant
494                1 < level < NR_LEVELS(),
495                owner.inv(),
496                regions.inv(),
497                parent_owner.inv(),
498                new_owner.value.is_node(),
499                new_owner.inv(),
500        {
501            assert(i < NR_ENTRIES()) by { admit() };
502
503            let tracked mut new_owner_node = new_owner.value.node.tracked_take();
504
505            assert(pa + i * page_size((level - 1) as u8) < MAX_PADDR()) by { admit() };
506            let small_pa = pa + i * page_size(level - 1);
507
508            let tracked child_owner = EntryOwner::new_frame(
509                small_pa,
510                (level - 1) as PagingLevel,
511                prop,
512            );
513            assert(Child::Frame(small_pa, (level - 1) as PagingLevel, prop).wf(child_owner)) by {
514                admit()
515            };
516            assert(new_owner.children[i as int].unwrap().value.inv()) by { admit() };
517            assert(new_owner_node.relate_guard_perm(guard_perm)) by { admit() };
518            assert(guard_perm.addr() == pt_lock_guard.addr()) by { admit() };
519            assert(new_owner.children[i as int].unwrap().value.match_pte(
520                new_owner_node.children_perm.value()[i as int],
521                new_owner_node.level,
522            )) by { admit() };
523
524            #[verus_spec(with Tracked(&new_owner_node), Tracked(&new_owner.children.tracked_borrow(i as int).tracked_borrow().value), Tracked(&guard_perm))]
525            let mut entry = PageTableGuard::entry(pt_lock_guard, i);
526
527            assert(!regions.slots.contains_key(frame_to_index(entry.pte.paddr()))) by { admit() };
528            assert(regions.dropped_slots.contains_key(frame_to_index(entry.pte.paddr()))) by {
529                admit()
530            };
531            assert(parent_owner.relate_guard_perm(guard_perm)) by { admit() };
532
533            assert(child_owner.inv()) by { admit() };
534            #[verus_spec(with Tracked(regions), Tracked(&owner.value), Tracked(&child_owner),
535                Tracked(&mut new_owner_node), Tracked(&mut guard_perm))]
536            let old = entry.replace(Child::Frame(small_pa, level - 1, prop));
537            //debug_assert!(old.is_none());
538            proof {
539                new_owner.value.node = Some(new_owner_node);
540            }
541        }
542
543        self.pte = (#[verus_spec(with Tracked(&new_owner.value), Tracked(regions))]
544        Child::PageTable(new_page).into_pte());
545
546        assert(owner.value.is_node()) by { admit() };
547
548        let tracked mut node_owner = owner.value.node.tracked_take();
549        assert(node_owner.inv()) by { admit() };
550
551        // SAFETY:
552        //  1. The index is within the bounds.
553        //  2. The new PTE is a child in `C` and at the correct paging level.
554        //  3. The ownership of the child is passed to the page table node.
555        #[verus_spec(with Tracked(&mut node_owner))]
556        node_guard.write_pte(self.idx, self.pte);
557
558        proof {
559            owner.value.node = Some(node_owner);
560            admit();
561        }
562
563        self.node.put(Tracked(&mut guard_perm), node_guard);
564
565        Some(pt_lock_guard)
566    }
567
568    /// Create a new entry at the node with guard.
569    ///
570    /// # Safety
571    ///
572    /// The caller must ensure that the index is within the bounds of the node.
573    #[verus_spec(
574        with Tracked(owner): Tracked<&EntryOwner<C>>,
575            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
576            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
577    )]
578    pub fn new_at(guard: PPtr<PageTableGuard<'rcu, C>>, idx: usize) -> (res: Self)
579        requires
580            owner.inv(),
581            parent_owner.inv(),
582            guard_perm.addr() == guard.addr(),
583            parent_owner.relate_guard_perm(*guard_perm),
584            idx < NR_ENTRIES(),
585            owner.match_pte(parent_owner.children_perm.value()[idx as int], owner.parent_level),
586        ensures
587            res.wf(*owner),
588            res.node.addr() == guard_perm.addr(),
589    {
590        // SAFETY: The index is within the bound.
591        let guard_val = guard.borrow(Tracked(guard_perm));
592        #[verus_spec(with Tracked(parent_owner))]
593        let pte = guard_val.read_pte(idx);
594        Self { pte, idx, node: guard }
595    }
596}
597
598} // verus!
ostd/mm/page_table/node/entry.rs

ostd/mm/page_table/node/
entry.rs
