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::{
8            mapping::{frame_to_index, index_to_meta, meta_to_index},
9            meta_owners::PageUsage,
10            meta_region_owners::MetaRegionOwners,
11        },
12        page_table::{node::entry_view::*, *},
13    },
14};
15
16use crate::arch::mm::PagingConsts;
17use crate::mm::{
18    Paddr, PagingConstsTrait, PagingLevel, Vaddr,
19    frame::meta::{
20        MetaSlot, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED, mapping::meta_to_frame,
21    },
22    page_prop::PageProperty,
23    page_table::*,
24};
25use core::marker::PhantomData;
26
27verus! {
28
29/// # Verification Design
30/// The proof-side snapshot for a page table leaf: a frame mapped in a node. Asterinas
31/// supports huge pages, so it is not necessarily at level 1.
32/// - `mapped_pa` is the physical address of the mapped frame.
33/// - `prop` is a bitfield tracking the properties of the page ([`PageProperty`])
34pub tracked struct FrameEntryOwner<C: PageTableConfig> {
35    pub ghost mapped_pa: usize,
36    pub ghost prop: PageProperty,
37    pub permission: Option<C::Perm>,
38}
39
40pub tracked enum EntryOwnerKind<C: PageTableConfig> {
41    Node(NodeOwner<C>),
42    Frame(FrameEntryOwner<C>),
43    /// Translation-only / borrowed-sub-tree variant.
44    ///
45    /// Present when the slot's PTE references a sub-tree owned by *another*
46    /// page-table configuration (e.g. a user PT's kernel-half slot
47    /// pointing at a kernel-owned sub-table). The ghost `Set<Mapping>`
48    /// records the mappings reachable through that sub-tree so the
49    /// embedding can reason about what the borrowed translation provides
50    /// without descending into a sub-tree it does not own. Mutually
51    /// exclusive with `node`, `frame`, and `absent` by construction.
52    Borrowed(ghost Set<Mapping>),
53    Absent,
54}
55
56pub tracked struct EntryOwner<C: PageTableConfig> {
57    pub kind: EntryOwnerKind<C>,
58    pub ghost path: TreePath<NR_ENTRIES>,
59    pub ghost parent_level: PagingLevel,
60}
61
62impl<C: PageTableConfig> EntryOwner<C> {
63    #[verifier::inline]
64    pub open spec fn is_node(self) -> bool {
65        self.kind is Node
66    }
67
68    #[verifier::inline]
69    pub open spec fn is_frame(self) -> bool {
70        self.kind is Frame
71    }
72
73    #[verifier::inline]
74    pub open spec fn is_absent(self) -> bool {
75        self.kind is Absent
76    }
77
78    #[verifier::inline]
79    pub open spec fn is_borrowed(self) -> bool {
80        self.kind is Borrowed
81    }
82
83    pub open spec fn node(self) -> NodeOwner<C> {
84        self.kind->Node_0
85    }
86
87    pub open spec fn frame(self) -> FrameEntryOwner<C> {
88        self.kind->Frame_0
89    }
90
91    pub open spec fn frame_permission(self) -> Option<C::Perm>
92        recommends
93            self.is_frame(),
94    {
95        self.frame().permission
96    }
97
98    pub open spec fn frame_is_tracked(self) -> bool
99        recommends
100            self.is_frame(),
101    {
102        self.frame_permission() is Some
103    }
104
105    pub open spec fn borrowed(self) -> Set<Mapping> {
106        self.kind->Borrowed_0
107    }
108
109    pub open spec fn new_absent(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> Self {
110        EntryOwner { kind: EntryOwnerKind::Absent, path, parent_level }
111    }
112
113    pub open spec fn new_frame(
114        paddr: Paddr,
115        path: TreePath<NR_ENTRIES>,
116        parent_level: PagingLevel,
117        prop: PageProperty,
118        permission: Option<C::Perm>,
119    ) -> Self {
120        EntryOwner {
121            kind: EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa: paddr, prop, permission }),
122            path,
123            parent_level,
124        }
125    }
126
127    pub open spec fn new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> Self {
128        EntryOwner {
129            kind: EntryOwnerKind::Node(node),
130            path,
131            parent_level: (node.level() + 1) as PagingLevel,
132        }
133    }
134
135    pub proof fn tracked_new_absent(
136        path: TreePath<NR_ENTRIES>,
137        parent_level: PagingLevel,
138    ) -> tracked Self
139        returns
140            Self::new_absent(path, parent_level),
141    {
142        Self { kind: EntryOwnerKind::Absent, path, parent_level }
143    }
144
145    pub proof fn tracked_take_node(tracked &mut self) -> (tracked res: NodeOwner<C>)
146        requires
147            old(self).kind is Node,
148        ensures
149            res == old(self).node(),
150            *final(self) == (EntryOwner { kind: EntryOwnerKind::Absent, ..*old(self) }),
151    {
152        let tracked mut tmp = EntryOwnerKind::Absent;
153        tracked_swap(&mut self.kind, &mut tmp);
154        match tmp {
155            EntryOwnerKind::Node(node) => node,
156            _ => { proof_from_false() },
157        }
158    }
159
160    pub proof fn tracked_put_node(tracked &mut self, tracked node: NodeOwner<C>)
161        ensures
162            *final(self) == (EntryOwner { kind: EntryOwnerKind::Node(node), ..*old(self) }),
163    {
164        self.kind = EntryOwnerKind::Node(node);
165    }
166
167    pub proof fn tracked_borrow_node(tracked &self) -> (tracked res: &NodeOwner<C>)
168        requires
169            self.kind is Node,
170        ensures
171            *res == self.node(),
172    {
173        match self.kind {
174            EntryOwnerKind::Node(ref node) => node,
175            _ => { proof_from_false() },
176        }
177    }
178
179    pub proof fn tracked_borrow_mut_node(tracked &mut self) -> (tracked res: &mut NodeOwner<C>)
180        requires
181            old(self).kind is Node,
182        ensures
183            *res == old(self).node(),
184            *final(self) == (EntryOwner { kind: EntryOwnerKind::Node(*final(res)), ..*old(self) }),
185    {
186        match self.kind {
187            EntryOwnerKind::Node(ref mut node) => node,
188            _ => { proof_from_false() },
189        }
190    }
191
192    pub proof fn tracked_set_frame_prop(tracked &mut self, prop: PageProperty)
193        requires
194            old(self).kind is Frame,
195        ensures
196            *final(self) == (EntryOwner {
197                kind: EntryOwnerKind::Frame(FrameEntryOwner { prop, ..old(self).frame() }),
198                ..*old(self)
199            }),
200    {
201        let tracked mut old_kind = EntryOwnerKind::Absent;
202        tracked_swap(&mut self.kind, &mut old_kind);
203        match old_kind {
204            EntryOwnerKind::Frame(frame) => {
205                let ghost mapped_pa = frame.mapped_pa;
206                let tracked permission = frame.permission;
207                self.kind = EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa, prop, permission });
208            },
209            _ => proof_from_false(),
210        }
211    }
212
213    pub proof fn tracked_take_frame_permission(tracked &mut self) -> (tracked res: Option<C::Perm>)
214        requires
215            old(self).is_frame(),
216        ensures
217            res == old(self).frame_permission(),
218            *final(self) == (EntryOwner {
219                kind: EntryOwnerKind::Frame(
220                    FrameEntryOwner { permission: None, ..old(self).frame() },
221                ),
222                ..*old(self)
223            }),
224    {
225        let tracked mut old_kind = EntryOwnerKind::Absent;
226        tracked_swap(&mut self.kind, &mut old_kind);
227        match old_kind {
228            EntryOwnerKind::Frame(frame) => {
229                let ghost mapped_pa = frame.mapped_pa;
230                let ghost prop = frame.prop;
231                let tracked permission = frame.permission;
232                self.kind = EntryOwnerKind::Frame(
233                    FrameEntryOwner { mapped_pa, prop, permission: None },
234                );
235                permission
236            },
237            _ => proof_from_false(),
238        }
239    }
240
241    pub proof fn tracked_put_frame_permission(
242        tracked &mut self,
243        tracked permission: Option<C::Perm>,
244    )
245        requires
246            old(self).is_frame(),
247            old(self).frame_permission() is None,
248        ensures
249            *final(self) == (EntryOwner {
250                kind: EntryOwnerKind::Frame(FrameEntryOwner { permission, ..old(self).frame() }),
251                ..*old(self)
252            }),
253    {
254        let tracked mut old_kind = EntryOwnerKind::Absent;
255        tracked_swap(&mut self.kind, &mut old_kind);
256        match old_kind {
257            EntryOwnerKind::Frame(frame) => {
258                let ghost mapped_pa = frame.mapped_pa;
259                let ghost prop = frame.prop;
260                self.kind = EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa, prop, permission });
261            },
262            _ => proof_from_false(),
263        }
264    }
265
266    pub proof fn tracked_new_frame(
267        paddr: Paddr,
268        path: TreePath<NR_ENTRIES>,
269        parent_level: PagingLevel,
270        prop: PageProperty,
271        tracked permission: Option<C::Perm>,
272    ) -> tracked Self
273        returns
274            Self::new_frame(paddr, path, parent_level, prop, permission),
275    {
276        Self {
277            kind: EntryOwnerKind::Frame(FrameEntryOwner { mapped_pa: paddr, prop, permission }),
278            path,
279            parent_level,
280        }
281    }
282
283    /// The frame's `is_tracked` flag is pinned to its paddr's range membership:
284    /// tracked frames map regular RAM (non-MMIO paddrs); untracked frames map
285    /// MMIO. Combined with `axiom_mmio_usage_iff_mmio_paddr`, this lets proofs
286    /// translate between the derived frame trackedness and `usage == MMIO`
287    /// on the corresponding meta slot.
288    pub broadcast axiom fn axiom_frame_is_tracked_iff_not_mmio(entry: Self)
289        requires
290            entry.is_frame(),
291            entry.inv_base(),
292        ensures
293            #[trigger] entry.frame_is_tracked()
294                != crate::specs::mm::frame::meta_owners::is_mmio_paddr(entry.frame().mapped_pa),
295    ;
296
297    /// Creates a ghost entry owner for mapping an untracked (device memory) frame.
298    /// Unlike `new_frame`, this does not consume a slot permission from the meta region,
299    /// since device memory PAs are outside the tracked frame allocator.
300    /// The actual mapping correctness is guaranteed by the caller's `unsafe` contract.
301    ///
302    /// The `requires` reflect properties established by `collect_largest_pages` and the page-table
303    /// configuration model, allowing this checked constructor to build an invariant-safe,
304    /// untracked entry owner.
305    pub proof fn tracked_new_untracked_frame(
306        paddr: Paddr,
307        parent_level: PagingLevel,
308        prop: PageProperty,
309    ) -> (tracked res: Self)
310        requires
311            valid_frame_paddr(paddr),
312            1 <= parent_level < NR_LEVELS,
313            paddr % page_size::<PagingConsts>(parent_level) == 0,
314            paddr + page_size::<PagingConsts>(parent_level) <= MAX_PADDR,
315            C::raw_item_well_formed((paddr, parent_level, prop, Tracked(None))),
316            C::E::new_page_req(paddr, parent_level, prop),
317        ensures
318            res.is_frame(),
319            res.frame().mapped_pa == paddr,
320            res.frame().prop == prop,
321            !res.frame_is_tracked(),
322            res.parent_level == parent_level,
323            res.path.inv(),
324            res.inv_base(),
325            crate::mm::page_table::Child::<C>::Frame(paddr, parent_level, prop).wf(res),
326    {
327        Self {
328            kind: EntryOwnerKind::Frame(
329                FrameEntryOwner { mapped_pa: paddr, prop, permission: None },
330            ),
331            path: TreePath(Seq::empty()),
332            parent_level,
333        }
334    }
335
336    pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
337        &&& valid_frame_paddr(pte.paddr())
338        &&& !pte.is_present() ==> {
339            &&& self.is_absent()
340            &&& parent_level > 1 ==> !pte.is_last(parent_level)
341        }
342        &&& pte.is_present() && !pte.is_last(parent_level) ==> {
343            &&& self.is_node()
344            &&& meta_to_frame(self.node().slot_vaddr()) == pte.paddr()
345        }
346        &&& pte.is_present() && pte.is_last(parent_level) ==> {
347            &&& self.is_frame()
348            &&& self.frame().mapped_pa == pte.paddr()
349            &&& self.frame().prop == pte.prop()
350        }
351    }
352
353    /// PTE-shape constraint for a borrowed / translation-only entry. The
354    /// PTE must be a node-PTE (present and non-leaf at `parent_level`),
355    /// since the borrowed sub-table is accessed only via the MMU walk.
356    /// Unlike [`match_pte`], we do *not* pin the PTE's target paddr to
357    /// any owned `NodeOwner` — the sub-table is owned by a different
358    /// page-table configuration and the embedding doesn't track its
359    /// address here.
360    pub open spec fn borrowed_match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
361        &&& self.is_borrowed()
362        &&& valid_frame_paddr(pte.paddr())
363        &&& pte.is_present()
364        &&& !pte.is_last(parent_level)
365    }
366
367    pub proof fn last_pte_implies_frame_match(self, pte: C::E, parent_level: PagingLevel)
368        requires
369            self.inv(),
370            self.match_pte(pte, parent_level),
371            1 < parent_level,
372            pte.is_last(parent_level),
373        ensures
374            self.is_frame(),
375            self.frame().mapped_pa == pte.paddr(),
376            self.frame().prop == pte.prop(),
377    {
378    }
379
380    pub proof fn huge_frame_split_child_at(self, regions: MetaRegionOwners, idx: usize)
381        requires
382            self.inv(),
383            self.is_frame(),
384            regions.inv(),
385            1 < self.parent_level < NR_LEVELS,
386            idx < NR_ENTRIES,
387        ensures
388            self.frame().mapped_pa + idx * page_size::<PagingConsts>(
389                (self.parent_level - 1) as PagingLevel,
390            ) < MAX_PADDR,
391            ((self.frame().mapped_pa + idx * page_size::<PagingConsts>(
392                (self.parent_level - 1) as PagingLevel,
393            )) as Paddr) % page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel) == 0,
394            ((self.frame().mapped_pa + idx * page_size::<PagingConsts>(
395                (self.parent_level - 1) as PagingLevel,
396            )) as Paddr) + page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel)
397                <= MAX_PADDR,
398            ((self.frame().mapped_pa + idx * page_size::<PagingConsts>(
399                (self.parent_level - 1) as PagingLevel,
400            )) as Paddr) % PAGE_SIZE == 0,
401    {
402        let pa = self.frame().mapped_pa;
403        let child_pa = (pa + idx * page_size::<PagingConsts>(
404            (self.parent_level - 1) as PagingLevel,
405        )) as Paddr;
406        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_spec_values();
407        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
408        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_base::<
409            PagingConsts,
410        >();
411        vstd::arithmetic::power2::lemma2_to64();
412        if self.parent_level == 2 {
413            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_divides::<
414                PagingConsts,
415            >(1, 2);
416            assert(child_pa + page_size::<PagingConsts>(1) <= MAX_PADDR) by {
417                assert(idx * 4096 + 4096 <= 2097152);
418            };
419        } else {
420            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_va_align_page_size::<
421                PagingConsts,
422            >(pa, 2);
423            vstd::arithmetic::div_mod::lemma_mod_multiples_basic(
424                idx as int,
425                page_size::<PagingConsts>(2) as int,
426            );
427            vstd::arithmetic::div_mod::lemma_add_mod_noop(
428                pa as int,
429                (idx * page_size::<PagingConsts>(2)) as int,
430                page_size::<PagingConsts>(2) as int,
431            );
432        }
433    }
434
435    /// Helper: sub-page validity is preserved when the only slot that changed is the
436    /// frame's own slot (and slots map and other slot owners are unchanged).
437    pub proof fn frame_sub_pages_valid_preserved_at_own_slot(
438        self,
439        r0: MetaRegionOwners,
440        r1: MetaRegionOwners,
441    )
442        requires
443            self.inv(),
444            r0.inv(),
445            self.is_frame(),
446            self.parent_level <= NR_LEVELS,
447            self.frame_sub_pages_valid(r0),
448            r0.slots == r1.slots,
449            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
450            forall|i: int|
451                #![trigger r1.slot_owners[i]]
452                i != frame_to_index(self.meta_slot_paddr()->0) && r0.slot_owners.contains_key(i)
453                    ==> r0.slot_owners[i] == r1.slot_owners[i],
454        ensures
455            self.frame_sub_pages_valid(r1),
456    {
457        if self.parent_level > 1 {
458            let pa = self.frame().mapped_pa;
459            let nr_pages = page_size::<PagingConsts>(self.parent_level) / PAGE_SIZE;
460            let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
461            C::lemma_huge_raw_item_untracked(
462                pa,
463                self.parent_level,
464                self.frame().prop,
465                Tracked(self.frame_permission()),
466            );
467            assert(!self.frame_is_tracked());
468            assert forall|j: usize|
469                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
470                0 < j < nr_pages implies {
471                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
472                &&& r1.slots.contains_key(sub_idx)
473                &&& self.frame_is_tracked() ==> {
474                    &&& r1.ref_count(sub_idx) != REF_COUNT_UNUSED
475                    &&& r1.ref_count(sub_idx) > 0
476                    &&& r1.ref_count(sub_idx) <= REF_COUNT_MAX
477                }
478            } by {
479                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
480                assert(r0.slots.contains_key(sub_idx));
481                assert(r1.slots.contains_key(sub_idx));
482                // From frame_sub_pages_valid(r0): slot existence is unconditional.
483                // sub_idx != self_idx by arithmetic: pa is PAGE_SIZE-aligned, so
484                // self_idx = pa / PAGE_SIZE, and sub_idx = (pa + j*PAGE_SIZE) / PAGE_SIZE
485                //         = pa/PAGE_SIZE + j = self_idx + j > self_idx (since j >= 1).
486                let pa_plus_int: int = pa + j * PAGE_SIZE;
487                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_ge_base::<
488                    PagingConsts,
489                >(self.parent_level);
490                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_div_mul_eq::<
491                    PagingConsts,
492                >(self.parent_level);
493                vstd::arithmetic::div_mod::lemma_div_multiples_vanish_quotient(
494                    j as int,
495                    pa as int,
496                    PAGE_SIZE as int,
497                );
498                // Slot equality at sub_idx carries usage and rc forward.
499            }
500        }
501    }
502
503    /// Sub-page slot validity for huge frames (fine-grained: all 4KB pages within).
504    ///
505    /// When a frame at this entry has `parent_level > 1`, it is a huge page covering
506    /// `page_size(parent_level)` bytes. Every 4KB sub-page within this range (excluding
507    /// the j = 0 case which coincides with the frame's own slot) must be allocated
508    /// (in the free pool) with `rc != UNUSED`.
509    ///
510    /// The fine-grained form (over `j * PAGE_SIZE` rather than `j * page_size(L-1)`) is
511    /// what enables the recursive split case in `split_if_mapped_huge`: when splitting a
512    /// 1GB frame into 2MB sub-frames, each 2MB sub-frame's own sub-page validity (over
513    /// its 511 4KB sub-sub-pages) follows from the 1GB frame's fine-grained validity over
514    /// the corresponding subrange of indices.
515    pub open spec fn frame_sub_pages_valid(self, regions: MetaRegionOwners) -> bool {
516        self.is_frame() && self.parent_level > 1 ==> {
517            let pa = self.frame().mapped_pa;
518            let nr_pages = page_size::<PagingConsts>(self.parent_level) / PAGE_SIZE;
519            forall|j: usize|
520                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
521                0 < j < nr_pages ==> {
522                    let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
523                    // Slot existence is unconditional — the metadata array spans all
524                    // phys memory at boot, so every valid sub-page PA has an allocated slot.
525                    &&& regions.slots.contains_key(
526                        sub_idx,
527                    )
528                    // A tracked huge mapping would own one reference to every
529                    // covered base page. Current configs only permit untracked
530                    // huge mappings, so this implication is normally vacuous.
531                    &&& self.frame_is_tracked() ==> {
532                        &&& regions.ref_count(sub_idx) != REF_COUNT_UNUSED
533                        &&& regions.ref_count(sub_idx) > 0
534                        &&& regions.ref_count(sub_idx) <= REF_COUNT_MAX
535                    }
536                }
537        }
538    }
539
540    pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool {
541        if self.is_node() {
542            let idx = frame_to_index(self.meta_slot_paddr()->0);
543            &&& regions.ref_count(idx) != REF_COUNT_UNUSED
544            &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
545            &&& regions.slot_owners[idx].slot_vaddr == self.node().slot_vaddr()
546            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
547            &&& regions.slot_owners[idx].paths_in_pt == set![self.path]
548            &&& self.node().metaregion_sound_node(regions)
549        } else if self.is_frame() {
550            let idx = frame_to_index(self.meta_slot_paddr()->0);
551            &&& regions.slots.contains_key(idx)
552            &&& regions.slots[idx].addr() == index_to_meta(idx)
553            &&& regions.slots[idx].is_init()
554            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
555            &&& regions.slot_owners[idx].usage !is PageTable
556            // Tracked vs MMIO discriminator is the slot's `usage`. MMIO slots
557            // stay in the free pool with `rc == UNUSED`; tracked slots have
558            // `rc > 0`. The slot's `usage == MMIO` is pinned by the paddr's
559            // range membership via `axiom_mmio_usage_iff_mmio_paddr`.
560            &&& regions.slot_owners[idx].usage !is MMIO ==> {
561                // A mapped (tracked) frame is SHARED.
562                &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
563            }
564            &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)
565            &&& self.frame_sub_pages_valid(regions)
566            &&& C::perm_well_formed_with_region(
567                self.frame().mapped_pa,
568                Tracked(self.frame_permission()),
569                regions,
570            )
571        } else {
572            true
573        }
574    }
575
576    /// An active page-table node cannot occupy a metadata slot whose refcount is
577    /// still `REF_COUNT_UNUSED`.
578    pub proof fn lemma_active_entry_not_in_free_pool(
579        entry: Self,
580        regions: MetaRegionOwners,
581        free_idx: int,
582    )
583        requires
584            regions.inv(),
585            entry.inv(),
586            entry.is_node(),
587            entry.metaregion_sound(regions),
588            regions.slots.contains_key(free_idx),
589            regions.ref_count(free_idx) == REF_COUNT_UNUSED,
590        ensures
591            frame_to_index(entry.meta_slot_paddr()->0) != free_idx,
592    {
593        let idx = frame_to_index(entry.meta_slot_paddr().unwrap());
594        if idx == free_idx {
595            assert(false);
596        }
597    }
598
599    pub open spec fn meta_slot_paddr(self) -> Option<Paddr> {
600        if self.is_node() {
601            Some(meta_to_frame(self.node().slot_vaddr()))
602        } else if self.is_frame() {
603            Some(self.frame().mapped_pa)
604        } else {
605            None
606        }
607    }
608
609    pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool {
610        self.meta_slot_paddr() is Some ==> other.meta_slot_paddr() is Some
611            ==> self.meta_slot_paddr()->0 != other.meta_slot_paddr()->0
612    }
613
614    /// `metaregion_sound` transfers when `slot_owners` matches and `slots` is a superset.
615    /// For nodes: only `slot_owners` matters. For frames: `slots.contains_key` and `slots[idx]`
616    /// must be preserved, which holds when `slots` is a superset with values unchanged.
617    pub proof fn metaregion_sound_slot_owners_only(self, r0: MetaRegionOwners, r1: MetaRegionOwners)
618        requires
619            self.inv(),
620            self.metaregion_sound(r0),
621            r0.slot_owners == r1.slot_owners,
622            forall|k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
623            forall|k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
624        ensures
625            self.metaregion_sound(r1),
626    {
627        if self.is_frame() {
628            let pa = self.frame().mapped_pa;
629            let idx = frame_to_index(pa);
630            assert(r0.slots[idx] == r1.slots[idx]);
631            assert(r0.slot_owners[idx].metadata_perm.id()
632                == r1.slot_owners[idx].metadata_perm.id());
633            C::lemma_perm_well_formed_with_region_preserved(
634                pa,
635                Tracked(self.frame_permission()),
636                r0,
637                r1,
638            );
639        }
640        if self.is_frame() && self.parent_level > 1 {
641            C::lemma_huge_raw_item_untracked(
642                self.frame().mapped_pa,
643                self.parent_level,
644                self.frame().prop,
645                Tracked(self.frame_permission()),
646            );
647            assert(!self.frame_is_tracked());
648        }
649    }
650
651    /// Changing only a leaf PTE's page properties preserves its relationship
652    /// to the metadata region. The counting permission, physical address and
653    /// page-table path remain unchanged.
654    pub proof fn metaregion_sound_frame_prop_changed(self, other: Self, regions: MetaRegionOwners)
655        requires
656            regions.inv(),
657            self.inv(),
658            other.inv(),
659            self.is_frame(),
660            other.is_frame(),
661            self.metaregion_sound(regions),
662            other.frame().mapped_pa == self.frame().mapped_pa,
663            other.path == self.path,
664            other.parent_level == self.parent_level,
665            other.frame_permission() == self.frame_permission(),
666            other.frame_is_tracked() == self.frame_is_tracked(),
667        ensures
668            other.metaregion_sound(regions),
669    {
670    }
671
672    /// If `metaregion_sound(r0)` holds and `r1` differs from `r0` only at one slot index
673    /// that this entry does not reference, then `metaregion_sound(r1)` also holds.
674    pub proof fn metaregion_sound_one_slot_changed(
675        self,
676        r0: MetaRegionOwners,
677        r1: MetaRegionOwners,
678        changed_idx: int,
679    )
680        requires
681            self.inv(),
682            self.metaregion_sound(r0),
683            forall|i: int|
684                #![trigger r1.slot_owners[i]]
685                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
686            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
687            // slots preserved at the entry's index (frames read from slots)
688            forall|k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
689            forall|k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
690            self.meta_slot_paddr() is Some ==> frame_to_index(self.meta_slot_paddr()->0)
691                != changed_idx,
692            // Huge frames: if changed_idx is one of this frame's 4KB sub-page slots and
693            // that sub-slot is non-MMIO, the sub-page validity at changed_idx must still
694            // hold in r1. MMIO sub-pages keep `usage == MMIO` and `rc == UNUSED`.
695            self.is_frame() && self.parent_level > 1 ==> {
696                let pa = self.frame().mapped_pa;
697                let nr_pages = page_size::<PagingConsts>(self.parent_level) / PAGE_SIZE;
698                forall|j: usize|
699                    0 < j < nr_pages ==> {
700                        let sub_idx = #[trigger] frame_to_index((pa + j * PAGE_SIZE) as usize);
701                        sub_idx != changed_idx || r1.slot_owners[sub_idx].usage is MMIO || (
702                        r1.slots.contains_key(sub_idx) && r1.ref_count(sub_idx) != REF_COUNT_UNUSED
703                            && r1.ref_count(sub_idx) > 0 && r1.ref_count(sub_idx) <= REF_COUNT_MAX)
704                    }
705            },
706        ensures
707            self.metaregion_sound(r1),
708    {
709        if self.meta_slot_paddr() is Some {
710            let idx = frame_to_index(self.meta_slot_paddr()->0);
711            assert(idx != changed_idx);
712            assert(r0.slot_owners[idx] == r1.slot_owners[idx]);
713            assert(r0.slots.contains_key(idx));
714            assert(r1.slots.contains_key(idx));
715            assert(r0.slots[idx] == r1.slots[idx]);
716            if self.is_frame() {
717                assert(r0.slot_owners[idx].metadata_perm.id()
718                    == r1.slot_owners[idx].metadata_perm.id());
719                C::lemma_perm_well_formed_with_region_preserved(
720                    self.frame().mapped_pa,
721                    Tracked(self.frame_permission()),
722                    r0,
723                    r1,
724                );
725            }
726            if self.is_node() {
727                assert(self.node().meta_wf(r1));
728                assert(self.node().metaregion_sound_node(r1));
729            }
730        }
731        if self.is_frame() && self.parent_level > 1 {
732            C::lemma_huge_raw_item_untracked(
733                self.frame().mapped_pa,
734                self.parent_level,
735                self.frame().prop,
736                Tracked(self.frame_permission()),
737            );
738            assert(!self.frame_is_tracked());
739        }
740    }
741}
742
743impl<C: PageTableConfig> EntryOwner<C> {
744    /// Structural invariant of an entry owner. This is the whole of `inv()`,
745    /// and is also used directly by `Child::invariants`.
746    pub open spec fn inv_base(self) -> bool {
747        &&& self.is_node() ==> {
748            &&& self.node().inv()
749            &&& self.parent_level == self.node().level() + 1
750        }
751        &&& self.is_frame() ==> {
752            // Architectural constraint: frames only exist at PT levels that the
753            // ISA actually supports as leaves (4K, 2M, 1G on x86). `parent_level
754            // == NR_LEVELS` would be a 512 GiB huge page, which no current arch
755            // permits — and `Mapping::inv` would reject its page_size.
756            &&& 1 <= self.parent_level < NR_LEVELS
757            &&& valid_frame_paddr(self.frame().mapped_pa)
758            &&& self.frame().mapped_pa % page_size::<PagingConsts>(self.parent_level) == 0
759            &&& self.frame().mapped_pa + page_size::<PagingConsts>(self.parent_level) <= MAX_PADDR
760            &&& C::raw_item_well_formed(
761                (
762                    self.frame().mapped_pa,
763                    self.parent_level,
764                    self.frame().prop,
765                    Tracked(self.frame_permission()),
766                ),
767            )
768            &&& C::E::new_page_req(self.frame().mapped_pa, self.parent_level, self.frame().prop)
769        }
770        &&& self.is_borrowed() ==> { true }
771        &&& self.path.inv()
772    }
773}
774
775impl<C: PageTableConfig> Inv for EntryOwner<C> {
776    open spec fn inv(self) -> bool {
777        self.inv_base()
778    }
779}
780
781impl<'a, 'rcu, C: PageTableConfig> OwnerOf for Entry<'a, 'rcu, C> {
782    type Owner = EntryOwner<C>;
783
784    open spec fn wf(self, owner: Self::Owner) -> bool {
785        &&& self.idx < NR_ENTRIES
786        &&& owner.match_pte(self.pte, owner.parent_level)
787        &&& valid_frame_paddr(self.pte.paddr())
788    }
789}
790
791} // verus!
ostd/specs/mm/page_table/node/entry_owners.rs

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