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

1use vstd::{modes::tracked_swap, prelude::*, simple_pptr::PointsTo};
2use vstd_extra::{ghost_tree::*, ownership::*};
3
4use crate::specs::{
5    arch::*,
6    mm::{
7        frame::{mapping::*, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners},
8        page_table::*,
9    },
10};
11
12use crate::arch::mm::PagingConsts;
13use crate::mm::{
14    Paddr, PagingConstsTrait, PagingLevel, Vaddr,
15    frame::meta::{
16        MetaSlot, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED, mapping::meta_to_frame,
17    },
18    page_prop::PageProperty,
19    page_table::*,
20};
21use core::marker::PhantomData;
22
23verus! {
24
25/// # Verification Design
26/// The proof-side snapshot for a page table leaf: a frame mapped in a node. Asterinas
27/// supports huge pages, so it is not necessarily at level 1.
28/// - `mapped_pa` is the physical address of the mapped frame.
29/// - `prop` is a bitfield tracking the properties of the page ([`PageProperty`])
30pub tracked struct FrameEntryOwner<C: PageTableConfig> {
31    pub ghost mapped_pa: usize,
32    pub ghost prop: PageProperty,
33    pub permission: Option<C::Perm>,
34}
35
36pub tracked enum EntryOwnerKind<C: PageTableConfig> {
37    Node(NodeOwner<C>),
38    Frame(FrameEntryOwner<C>),
39    /// Translation-only / borrowed-sub-tree variant.
40    ///
41    /// Present when the slot's PTE references a sub-tree owned by *another*
42    /// page-table configuration (e.g. a user PT's kernel-half slot
43    /// pointing at a kernel-owned sub-table). The ghost `Set<Mapping>`
44    /// records the mappings reachable through that sub-tree so the
45    /// embedding can reason about what the borrowed translation provides
46    /// without descending into a sub-tree it does not own. Mutually
47    /// exclusive with `node`, `frame`, and `absent` by construction.
48    Borrowed(ghost Set<Mapping>),
49    Absent,
50}
51
52pub tracked struct EntryOwner<C: PageTableConfig> {
53    pub kind: EntryOwnerKind<C>,
54    pub ghost path: TreePath<NR_ENTRIES>,
55    pub ghost parent_level: PagingLevel,
56}
57
58impl<C: PageTableConfig> EntryOwner<C> {
59    #[verifier::inline]
60    pub open spec fn is_node(self) -> bool {
61        self.kind is Node
62    }
63
64    #[verifier::inline]
65    pub open spec fn is_frame(self) -> bool {
66        self.kind is Frame
67    }
68
69    #[verifier::inline]
70    pub open spec fn is_absent(self) -> bool {
71        self.kind is Absent
72    }
73
74    #[verifier::inline]
75    pub open spec fn is_borrowed(self) -> bool {
76        self.kind is Borrowed
77    }
78
79    pub open spec fn node(self) -> NodeOwner<C> {
80        self.kind->Node_0
81    }
82
83    pub open spec fn frame(self) -> FrameEntryOwner<C> {
84        self.kind->Frame_0
85    }
86
87    pub open spec fn frame_permission(self) -> Option<C::Perm>
88        recommends
89            self.is_frame(),
90    {
91        self.frame().permission
92    }
93
94    pub open spec fn frame_is_tracked(self) -> bool
95        recommends
96            self.is_frame(),
97    {
98        self.frame_permission() is Some
99    }
100
101    pub open spec fn borrowed(self) -> Set<Mapping> {
102        self.kind->Borrowed_0
103    }
104
105    pub open spec fn new_absent(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> Self {
106        EntryOwner { kind: EntryOwnerKind::Absent, path, parent_level }
107    }
108
109    pub open spec fn new_frame(
110        paddr: Paddr,
111        path: TreePath<NR_ENTRIES>,
112        parent_level: PagingLevel,
113        prop: PageProperty,
114        permission: Option<C::Perm>,
115    ) -> Self {
116        EntryOwner {
117            kind: EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa: paddr, prop, permission }),
118            path,
119            parent_level,
120        }
121    }
122
123    pub open spec fn new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> Self {
124        EntryOwner {
125            kind: EntryOwnerKind::Node(node),
126            path,
127            parent_level: (node.level() + 1) as PagingLevel,
128        }
129    }
130
131    pub proof fn tracked_new_absent(
132        path: TreePath<NR_ENTRIES>,
133        parent_level: PagingLevel,
134    ) -> tracked Self
135        returns
136            Self::new_absent(path, parent_level),
137    {
138        Self { kind: EntryOwnerKind::Absent, path, parent_level }
139    }
140
141    pub proof fn tracked_take_node(tracked &mut self) -> (tracked res: NodeOwner<C>)
142        requires
143            old(self).kind is Node,
144        ensures
145            res == old(self).node(),
146            *final(self) == (EntryOwner { kind: EntryOwnerKind::Absent, ..*old(self) }),
147    {
148        let tracked mut tmp = EntryOwnerKind::Absent;
149        tracked_swap(&mut self.kind, &mut tmp);
150        match tmp {
151            EntryOwnerKind::Node(node) => node,
152            _ => { proof_from_false() },
153        }
154    }
155
156    pub proof fn tracked_put_node(tracked &mut self, tracked node: NodeOwner<C>)
157        ensures
158            *final(self) == (EntryOwner { kind: EntryOwnerKind::Node(node), ..*old(self) }),
159    {
160        self.kind = EntryOwnerKind::Node(node);
161    }
162
163    pub proof fn tracked_borrow_node(tracked &self) -> (tracked res: &NodeOwner<C>)
164        requires
165            self.kind is Node,
166        ensures
167            *res == self.node(),
168    {
169        match self.kind {
170            EntryOwnerKind::Node(ref node) => node,
171            _ => { proof_from_false() },
172        }
173    }
174
175    pub proof fn tracked_borrow_mut_node(tracked &mut self) -> (tracked res: &mut NodeOwner<C>)
176        requires
177            old(self).kind is Node,
178        ensures
179            *res == old(self).node(),
180            *final(self) == (EntryOwner { kind: EntryOwnerKind::Node(*final(res)), ..*old(self) }),
181    {
182        match self.kind {
183            EntryOwnerKind::Node(ref mut node) => node,
184            _ => { proof_from_false() },
185        }
186    }
187
188    pub proof fn tracked_set_frame_prop(tracked &mut self, prop: PageProperty)
189        requires
190            old(self).kind is Frame,
191        ensures
192            *final(self) == (EntryOwner {
193                kind: EntryOwnerKind::Frame(FrameEntryOwner { prop, ..old(self).frame() }),
194                ..*old(self)
195            }),
196    {
197        let tracked mut old_kind = EntryOwnerKind::Absent;
198        tracked_swap(&mut self.kind, &mut old_kind);
199        match old_kind {
200            EntryOwnerKind::Frame(frame) => {
201                let ghost mapped_pa = frame.mapped_pa;
202                let tracked permission = frame.permission;
203                self.kind = EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa, prop, permission });
204            },
205            _ => proof_from_false(),
206        }
207    }
208
209    pub proof fn tracked_take_frame_permission(tracked &mut self) -> (tracked res: Option<C::Perm>)
210        requires
211            old(self).is_frame(),
212        ensures
213            res == old(self).frame_permission(),
214            *final(self) == (EntryOwner {
215                kind: EntryOwnerKind::Frame(
216                    FrameEntryOwner { permission: None, ..old(self).frame() },
217                ),
218                ..*old(self)
219            }),
220    {
221        let tracked mut old_kind = EntryOwnerKind::Absent;
222        tracked_swap(&mut self.kind, &mut old_kind);
223        match old_kind {
224            EntryOwnerKind::Frame(frame) => {
225                let ghost mapped_pa = frame.mapped_pa;
226                let ghost prop = frame.prop;
227                let tracked permission = frame.permission;
228                self.kind = EntryOwnerKind::Frame(
229                    FrameEntryOwner { mapped_pa, prop, permission: None },
230                );
231                permission
232            },
233            _ => proof_from_false(),
234        }
235    }
236
237    pub proof fn tracked_put_frame_permission(
238        tracked &mut self,
239        tracked permission: Option<C::Perm>,
240    )
241        requires
242            old(self).is_frame(),
243            old(self).frame_permission() is None,
244        ensures
245            *final(self) == (EntryOwner {
246                kind: EntryOwnerKind::Frame(FrameEntryOwner { permission, ..old(self).frame() }),
247                ..*old(self)
248            }),
249    {
250        let tracked mut old_kind = EntryOwnerKind::Absent;
251        tracked_swap(&mut self.kind, &mut old_kind);
252        match old_kind {
253            EntryOwnerKind::Frame(frame) => {
254                let ghost mapped_pa = frame.mapped_pa;
255                let ghost prop = frame.prop;
256                self.kind = EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa, prop, permission });
257            },
258            _ => proof_from_false(),
259        }
260    }
261
262    pub proof fn tracked_new_frame(
263        paddr: Paddr,
264        path: TreePath<NR_ENTRIES>,
265        parent_level: PagingLevel,
266        prop: PageProperty,
267        tracked permission: Option<C::Perm>,
268    ) -> tracked Self
269        returns
270            Self::new_frame(paddr, path, parent_level, prop, permission),
271    {
272        Self {
273            kind: EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa: paddr, prop, permission }),
274            path,
275            parent_level,
276        }
277    }
278
279    /// Creates an untracked physical mapping without counted metadata ownership.
280    /// The mapped address may belong to ordinary RAM or MMIO.
281    /// The actual mapping correctness is guaranteed by the caller's `unsafe` contract.
282    ///
283    /// The `requires` reflect properties established by `collect_largest_pages` and the page-table
284    /// configuration model, allowing this checked constructor to build an invariant-safe,
285    /// untracked entry owner.
286    pub proof fn tracked_new_untracked_frame(
287        paddr: Paddr,
288        parent_level: PagingLevel,
289        prop: PageProperty,
290    ) -> (tracked res: Self)
291        requires
292            valid_frame_paddr(paddr),
293            1 <= parent_level < NR_LEVELS,
294            paddr % page_size::<PagingConsts>(parent_level) == 0,
295            paddr + page_size::<PagingConsts>(parent_level) <= MAX_PADDR,
296            C::raw_item_well_formed((paddr, parent_level, prop, Tracked(None))),
297            C::E::new_page_req(paddr, parent_level, prop),
298        ensures
299            res.is_frame(),
300            res.frame().mapped_pa == paddr,
301            res.frame().prop == prop,
302            !res.frame_is_tracked(),
303            res.parent_level == parent_level,
304            res.path.inv(),
305            res.inv(),
306            crate::mm::page_table::Child::<C>::Frame(paddr, parent_level, prop).wf(res),
307    {
308        Self {
309            kind: EntryOwnerKind::Frame(
310                FrameEntryOwner { mapped_pa: paddr, prop, permission: None },
311            ),
312            path: TreePath(Seq::empty()),
313            parent_level,
314        }
315    }
316
317    pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
318        &&& valid_frame_paddr(pte.paddr())
319        &&& !pte.is_present() ==> {
320            &&& self.is_absent()
321            &&& parent_level > 1 ==> !pte.is_last(parent_level)
322        }
323        &&& pte.is_present() && !pte.is_last(parent_level) ==> {
324            &&& self.is_node()
325            &&& meta_to_frame(self.node().slot_vaddr()) == pte.paddr()
326        }
327        &&& pte.is_present() && pte.is_last(parent_level) ==> {
328            &&& self.is_frame()
329            &&& self.frame().mapped_pa == pte.paddr()
330            &&& self.frame().prop == pte.prop()
331        }
332    }
333
334    /// PTE-shape constraint for a borrowed / translation-only entry. The
335    /// PTE must be a node-PTE (present and non-leaf at `parent_level`),
336    /// since the borrowed sub-table is accessed only via the MMU walk.
337    /// Unlike [`match_pte`], we do *not* pin the PTE's target paddr to
338    /// any owned `NodeOwner` — the sub-table is owned by a different
339    /// page-table configuration and the embedding doesn't track its
340    /// address here.
341    pub open spec fn borrowed_match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
342        &&& self.is_borrowed()
343        &&& valid_frame_paddr(pte.paddr())
344        &&& pte.is_present()
345        &&& !pte.is_last(parent_level)
346    }
347
348    pub proof fn huge_frame_split_child_at(self, regions: MetaRegionOwners, idx: usize)
349        requires
350            self.inv(),
351            self.is_frame(),
352            regions.inv(),
353            1 < self.parent_level < NR_LEVELS,
354            idx < NR_ENTRIES,
355        ensures
356            self.frame().mapped_pa + idx * page_size::<PagingConsts>(
357                (self.parent_level - 1) as PagingLevel,
358            ) < MAX_PADDR,
359            ((self.frame().mapped_pa + idx * page_size::<PagingConsts>(
360                (self.parent_level - 1) as PagingLevel,
361            )) as Paddr) % page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel) == 0,
362            ((self.frame().mapped_pa + idx * page_size::<PagingConsts>(
363                (self.parent_level - 1) as PagingLevel,
364            )) as Paddr) + page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel)
365                <= MAX_PADDR,
366            ((self.frame().mapped_pa + idx * page_size::<PagingConsts>(
367                (self.parent_level - 1) as PagingLevel,
368            )) as Paddr) % PAGE_SIZE == 0,
369    {
370        let pa = self.frame().mapped_pa;
371        let child_pa = (pa + idx * page_size::<PagingConsts>(
372            (self.parent_level - 1) as PagingLevel,
373        )) as Paddr;
374        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_spec_values();
375        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
376        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_base::<
377            PagingConsts,
378        >();
379        vstd::arithmetic::power2::lemma2_to64();
380        if self.parent_level == 2 {
381            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_divides::<
382                PagingConsts,
383            >(1, 2);
384            assert(child_pa + page_size::<PagingConsts>(1) <= MAX_PADDR) by {
385                assert(idx * 4096 + 4096 <= 2097152);
386            };
387        } else {
388            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_va_align_page_size::<
389                PagingConsts,
390            >(pa, 2);
391            vstd::arithmetic::div_mod::lemma_mod_multiples_basic(
392                idx as int,
393                page_size::<PagingConsts>(2) as int,
394            );
395            vstd::arithmetic::div_mod::lemma_add_mod_noop(
396                pa as int,
397                (idx * page_size::<PagingConsts>(2)) as int,
398                page_size::<PagingConsts>(2) as int,
399            );
400        }
401    }
402
403    pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool {
404        if self.is_node() {
405            let idx = frame_to_index(self.meta_slot_paddr()->0);
406            &&& regions.ref_count(idx) != REF_COUNT_UNUSED
407            &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
408            &&& regions.slot_owners[idx].slot_vaddr == self.node().slot_vaddr()
409            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
410            &&& regions.slot_owners[idx].paths_in_pt == set![self.path]
411            &&& self.node().metaregion_sound_node(regions)
412        } else if self.is_frame() {
413            let idx = frame_to_index(self.meta_slot_paddr()->0);
414            &&& regions.slots.contains_key(idx)
415            &&& regions.slots[idx].addr() == index_to_meta(idx)
416            &&& regions.slots[idx].is_init()
417            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
418            &&& self.frame_is_tracked() ==> {
419                &&& regions.slot_owners[idx].usage !is PageTable
420                &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
421                &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)
422            }
423            &&& C::perm_well_formed_with_region(
424                self.frame().mapped_pa,
425                Tracked(self.frame_permission()),
426                regions,
427            )
428        } else {
429            true
430        }
431    }
432
433    /// An active page-table node cannot occupy a metadata slot whose refcount is
434    /// still `REF_COUNT_UNUSED`.
435    pub proof fn lemma_active_entry_not_in_free_pool(
436        entry: Self,
437        regions: MetaRegionOwners,
438        free_idx: int,
439    )
440        requires
441            regions.inv(),
442            entry.inv(),
443            entry.is_node(),
444            entry.metaregion_sound(regions),
445            regions.slots.contains_key(free_idx),
446            regions.ref_count(free_idx) == REF_COUNT_UNUSED,
447        ensures
448            frame_to_index(entry.meta_slot_paddr()->0) != free_idx,
449    {
450        let idx = frame_to_index(entry.meta_slot_paddr().unwrap());
451        if idx == free_idx {
452            assert(false);
453        }
454    }
455
456    pub open spec fn meta_slot_paddr(self) -> Option<Paddr> {
457        if self.is_node() {
458            Some(meta_to_frame(self.node().slot_vaddr()))
459        } else if self.is_frame() {
460            Some(self.frame().mapped_pa)
461        } else {
462            None
463        }
464    }
465
466    /// Physical-slot exclusion for owning entries; raw mappings impose no exclusion.
467    pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool {
468        (self.is_node() || (self.is_frame() && self.frame_is_tracked())) && (other.is_node() || (
469        other.is_frame() && other.frame_is_tracked())) ==> {
470            self.meta_slot_paddr() is Some ==> other.meta_slot_paddr() is Some
471                ==> self.meta_slot_paddr()->0 != other.meta_slot_paddr()->0
472        }
473    }
474
475    /// An untracked mapping needs no counted ownership of its physical slot.
476    pub proof fn lemma_untracked_frame_metaregion_sound(self, regions: MetaRegionOwners)
477        requires
478            self.inv(),
479            self.is_frame(),
480            !self.frame_is_tracked(),
481            regions.inv(),
482        ensures
483            self.metaregion_sound(regions),
484    {
485        regions.lemma_contains_valid_frame_paddr(self.frame().mapped_pa);
486        C::lemma_none_perm_well_formed(self.frame().mapped_pa, regions);
487    }
488
489    /// `metaregion_sound` transfers when `slot_owners` matches and `slots` is a superset.
490    /// For nodes: only `slot_owners` matters. For frames: `slots.contains_key` and `slots[idx]`
491    /// must be preserved, which holds when `slots` is a superset with values unchanged.
492    pub proof fn metaregion_sound_slot_owners_only(self, r0: MetaRegionOwners, r1: MetaRegionOwners)
493        requires
494            self.inv(),
495            self.metaregion_sound(r0),
496            r0.slot_owners == r1.slot_owners,
497            forall|k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
498            forall|k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
499        ensures
500            self.metaregion_sound(r1),
501    {
502        if self.is_frame() {
503            let pa = self.frame().mapped_pa;
504            let idx = frame_to_index(pa);
505            assert(r0.slots[idx] == r1.slots[idx]);
506            assert(r0.slot_owners[idx].metadata_perm.id()
507                == r1.slot_owners[idx].metadata_perm.id());
508            C::lemma_perm_well_formed_with_region_preserved(
509                pa,
510                Tracked(self.frame_permission()),
511                r0,
512                r1,
513            );
514        }
515    }
516
517    /// Updating frame paths preserves metadata access and node ownership paths.
518    pub proof fn lemma_metaregion_sound_frame_paths_changed(
519        self,
520        r0: MetaRegionOwners,
521        r1: MetaRegionOwners,
522    )
523        requires
524            self.inv(),
525            self.metaregion_sound(r0),
526            r0.inv(),
527            r1.inv(),
528            r0.slots == r1.slots,
529            forall|i: int|
530                #![trigger r1.slot_owners[i]]
531                r0.slot_owners.contains_key(i) ==> {
532                    &&& r1.slot_owners[i].same_permissions(r0.slot_owners[i])
533                    &&& r1.slot_owners[i].usage == r0.slot_owners[i].usage
534                    &&& r1.slot_owners[i].slot_vaddr == r0.slot_owners[i].slot_vaddr
535                    &&& r0.slot_owners[i].paths_in_pt.subset_of(r1.slot_owners[i].paths_in_pt)
536                    &&& r0.slot_owners[i].usage is PageTable ==> r1.slot_owners[i].paths_in_pt
537                        == r0.slot_owners[i].paths_in_pt
538                },
539        ensures
540            self.metaregion_sound(r1),
541    {
542        if self.is_frame() {
543            C::lemma_perm_well_formed_with_region_preserved(
544                self.frame().mapped_pa,
545                Tracked(self.frame_permission()),
546                r0,
547                r1,
548            );
549        }
550    }
551
552    /// Changing only a leaf PTE's page properties preserves its relationship
553    /// to the metadata region. The counting permission, physical address and
554    /// page-table path remain unchanged.
555    pub proof fn metaregion_sound_frame_prop_changed(self, other: Self, regions: MetaRegionOwners)
556        requires
557            regions.inv(),
558            self.inv(),
559            other.inv(),
560            self.is_frame(),
561            other.is_frame(),
562            self.metaregion_sound(regions),
563            other.frame().mapped_pa == self.frame().mapped_pa,
564            other.path == self.path,
565            other.parent_level == self.parent_level,
566            other.frame_permission() == self.frame_permission(),
567            other.frame_is_tracked() == self.frame_is_tracked(),
568        ensures
569            other.metaregion_sound(regions),
570    {
571    }
572
573    /// If `metaregion_sound(r0)` holds and `r1` differs from `r0` only at one slot index
574    /// that this entry does not reference, then `metaregion_sound(r1)` also holds.
575    pub proof fn lemma_metaregion_sound_one_slot_changed(
576        self,
577        r0: MetaRegionOwners,
578        r1: MetaRegionOwners,
579        changed_idx: int,
580    )
581        requires
582            self.inv(),
583            self.metaregion_sound(r0),
584            forall|i: int|
585                #![trigger r1.slot_owners[i]]
586                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
587            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
588            // slots preserved at the entry's index (frames read from slots)
589            forall|k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
590            forall|k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
591            self.is_node() || (self.is_frame() && self.frame_is_tracked())
592                ==> self.meta_slot_paddr() is Some ==> frame_to_index(self.meta_slot_paddr()->0)
593                != changed_idx,
594            self.meta_slot_paddr() is Some && frame_to_index(self.meta_slot_paddr()->0)
595                == changed_idx ==> r1.inv(),
596        ensures
597            self.metaregion_sound(r1),
598    {
599        if self.is_frame() && !self.frame_is_tracked() && frame_to_index(self.meta_slot_paddr()->0)
600            == changed_idx {
601            self.lemma_untracked_frame_metaregion_sound(r1);
602        } else if self.meta_slot_paddr() is Some {
603            let idx = frame_to_index(self.meta_slot_paddr()->0);
604            assert(idx != changed_idx);
605            assert(r0.slot_owners[idx] == r1.slot_owners[idx]);
606            assert(r0.slots.contains_key(idx));
607            assert(r1.slots.contains_key(idx));
608            assert(r0.slots[idx] == r1.slots[idx]);
609            if self.is_frame() {
610                assert(r0.slot_owners[idx].metadata_perm.id()
611                    == r1.slot_owners[idx].metadata_perm.id());
612                C::lemma_perm_well_formed_with_region_preserved(
613                    self.frame().mapped_pa,
614                    Tracked(self.frame_permission()),
615                    r0,
616                    r1,
617                );
618            }
619            if self.is_node() {
620                assert(self.node().meta_wf(r1));
621                assert(self.node().metaregion_sound_node(r1));
622            }
623        }
624    }
625}
626
627impl<C: PageTableConfig> Inv for EntryOwner<C> {
628    /// Structural invariant of an entry owner.
629    open spec fn inv(self) -> bool {
630        &&& self.is_node() ==> {
631            &&& self.node().inv()
632            &&& self.parent_level == self.node().level() + 1
633        }
634        &&& self.is_frame() ==> {
635            // The current mapping model supports 4K, 2M and 1G leaves. A level-4
636            // leaf spans 512 GiB, exceeding the modeled physical-address bound.
637            &&& 1 <= self.parent_level < NR_LEVELS
638            &&& valid_frame_paddr(self.frame().mapped_pa)
639            &&& self.frame().mapped_pa % page_size::<PagingConsts>(self.parent_level) == 0
640            &&& self.frame().mapped_pa + page_size::<PagingConsts>(self.parent_level) <= MAX_PADDR
641            &&& C::raw_item_well_formed(
642                (
643                    self.frame().mapped_pa,
644                    self.parent_level,
645                    self.frame().prop,
646                    Tracked(self.frame_permission()),
647                ),
648            )
649            &&& C::E::new_page_req(self.frame().mapped_pa, self.parent_level, self.frame().prop)
650        }
651        &&& self.path.inv()
652    }
653}
654
655impl<'a, 'rcu, C: PageTableConfig> OwnerOf for Entry<'a, 'rcu, C> {
656    type Owner = EntryOwner<C>;
657
658    open spec fn wf(self, owner: Self::Owner) -> bool {
659        &&& self.idx < NR_ENTRIES
660        &&& owner.match_pte(self.pte, owner.parent_level)
661    }
662}
663
664} // verus!
ostd/specs/mm/page_table/node/entry_owners.rs

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