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

1use vstd::prelude::*;
2
3use vstd::cell;
4use vstd::simple_pptr::PointsTo;
5use vstd_extra::array_ptr;
6use vstd_extra::ghost_tree::*;
7use vstd_extra::ownership::*;
8
9use crate::mm::frame::meta::MetaSlot;
10use crate::mm::frame::meta::{REF_COUNT_MAX, REF_COUNT_UNUSED};
11use crate::mm::page_prop::PageProperty;
12use crate::mm::page_table::*;
13use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
14use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
15use crate::specs::arch::paging_consts::PagingConsts;
16use crate::specs::arch::*;
17use crate::specs::mm::frame::mapping::{frame_to_index, meta_addr, meta_to_frame};
18use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
19use crate::specs::mm::page_table::node::entry_view::*;
20use crate::specs::mm::page_table::*;
21use core::marker::PhantomData;
22
23verus! {
24
25pub tracked struct FrameEntryOwner {
26    pub mapped_pa: usize,
27    pub size: usize,
28    pub prop: PageProperty,
29    /// Whether the frame is ref-counted (Tracked) or raw MMIO (Untracked).
30    /// Determines whether the slot at `frame_to_index(mapped_pa)` carries a
31    /// non-zero refcount and participates in `metaregion_sound`'s rc check.
32    pub is_tracked: bool,
33}
34
35pub tracked struct EntryOwner<C: PageTableConfig> {
36    pub node: Option<NodeOwner<C>>,
37    pub frame: Option<FrameEntryOwner>,
38    pub locked: Option<Ghost<Seq<FrameView<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 `locked`.
48    pub borrowed: Option<Ghost<Set<Mapping>>>,
49    pub absent: bool,
50    pub in_scope: bool,
51    pub path: TreePath<NR_ENTRIES>,
52    pub parent_level: PagingLevel,
53}
54
55impl<C: PageTableConfig> EntryOwner<C> {
56    pub open spec fn is_node(self) -> bool {
57        self.node is Some
58    }
59
60    pub open spec fn is_frame(self) -> bool {
61        self.frame is Some
62    }
63
64    pub open spec fn is_locked(self) -> bool {
65        self.locked is Some
66    }
67
68    pub open spec fn is_absent(self) -> bool {
69        self.absent
70    }
71
72    pub open spec fn is_borrowed(self) -> bool {
73        self.borrowed is Some
74    }
75
76    pub open spec fn new_absent(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> Self {
77        EntryOwner {
78            node: None,
79            frame: None,
80            locked: None,
81            borrowed: None,
82            absent: true,
83            in_scope: true,
84            path,
85            parent_level,
86        }
87    }
88
89    pub open spec fn new_frame(
90        paddr: Paddr,
91        path: TreePath<NR_ENTRIES>,
92        parent_level: PagingLevel,
93        prop: PageProperty,
94        is_tracked: bool,
95    ) -> Self {
96        EntryOwner {
97            node: None,
98            frame: Some(
99                FrameEntryOwner {
100                    mapped_pa: paddr,
101                    size: page_size(parent_level),
102                    prop,
103                    is_tracked,
104                },
105            ),
106            locked: None,
107            borrowed: None,
108            absent: false,
109            in_scope: true,
110            path,
111            parent_level,
112        }
113    }
114
115    pub open spec fn new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> Self {
116        EntryOwner {
117            node: Some(node),
118            frame: None,
119            locked: None,
120            borrowed: None,
121            absent: false,
122            in_scope: true,
123            path,
124            parent_level: (node.level + 1) as PagingLevel,
125        }
126    }
127
128    /// Constructor spec for a translation-only / borrowed entry. See
129    /// [`EntryOwner`]'s `borrowed` field for semantics.
130    pub open spec fn new_borrowed(
131        path: TreePath<NR_ENTRIES>,
132        parent_level: PagingLevel,
133        mappings: Set<Mapping>,
134    ) -> Self {
135        EntryOwner {
136            node: None,
137            frame: None,
138            locked: None,
139            borrowed: Some(Ghost(mappings)),
140            absent: false,
141            in_scope: true,
142            path,
143            parent_level,
144        }
145    }
146
147    pub axiom fn tracked_new_borrowed(
148        path: TreePath<NR_ENTRIES>,
149        parent_level: PagingLevel,
150        mappings: Set<Mapping>,
151    ) -> tracked Self
152        returns
153            Self::new_borrowed(path, parent_level, mappings),
154    ;
155
156    pub axiom fn tracked_new_absent(
157        path: TreePath<NR_ENTRIES>,
158        parent_level: PagingLevel,
159    ) -> tracked Self
160        returns
161            Self::new_absent(path, parent_level),
162    ;
163
164    /// Rewrites the `path` field of a tracked `EntryOwner` in place. Used by
165    /// `rebase_freshly_allocated_children` to propagate the cursor path down
166    /// to a freshly-allocated PT node's children, whose paths come from
167    /// `PageTableNode::alloc` rooted at the empty path.
168    pub axiom fn set_path_axiom(tracked &mut self, path: TreePath<NR_ENTRIES>)
169        ensures
170            *final(self) == (EntryOwner { path, ..*old(self) }),
171    ;
172
173    pub axiom fn tracked_new_frame(
174        paddr: Paddr,
175        path: TreePath<NR_ENTRIES>,
176        parent_level: PagingLevel,
177        prop: PageProperty,
178        is_tracked: bool,
179    ) -> tracked Self
180        returns
181            Self::new_frame(paddr, path, parent_level, prop, is_tracked),
182    ;
183
184    /// Structural connection between a frame entry's recorded `is_tracked` flag and
185    /// the trackedness of the item that would be reconstructed by `item_from_raw_spec`.
186    ///
187    /// **Why this is sound:** every `FrameEntryOwner` was created via `new_frame(...,
188    /// is_tracked)`, and at every construction site the caller passes
189    /// `is_tracked = C::tracked(item)` where `item` is the item being mapped. By the
190    /// `item_from_raw / item_into_raw` round-trip law, re-reading the entry's
191    /// `(mapped_pa, parent_level, prop)` and reconstructing via `item_from_raw_spec`
192    /// gives back the original `item`. So `C::tracked` of the reconstructed item
193    /// equals the recorded `is_tracked`.
194    ///
195    /// Encoded as an axiom (rather than an `EntryOwner::inv_base` clause) because
196    /// adding it to `inv_base` would require discharging this connection at every
197    /// `new_frame` call site — a wide cascading refactor (attempted, abandoned in
198    /// the FrameEntryOwner is_tracked refactor session).
199    pub axiom fn axiom_frame_is_tracked_matches_item(entry: Self)
200        requires
201            entry.is_frame(),
202            entry.inv_base(),
203        ensures
204            entry.frame.unwrap().is_tracked == C::tracked(
205                C::item_from_raw_spec(
206                    entry.frame.unwrap().mapped_pa,
207                    entry.parent_level,
208                    entry.frame.unwrap().prop,
209                ),
210            ),
211    ;
212
213    /// The frame's `is_tracked` flag is pinned to its paddr's range membership:
214    /// tracked frames map regular RAM (non-MMIO paddrs); untracked frames map
215    /// MMIO. Combined with `axiom_mmio_usage_iff_mmio_paddr`, this lets proofs
216    /// translate between `is_tracked` on a `FrameEntryOwner` and `usage == MMIO`
217    /// on the corresponding meta slot.
218    pub broadcast axiom fn axiom_frame_is_tracked_iff_not_mmio(entry: Self)
219        requires
220            entry.is_frame(),
221            entry.inv_base(),
222        ensures
223            #[trigger] entry.frame.unwrap().is_tracked
224                != crate::specs::mm::frame::meta_owners::is_mmio_paddr(
225                entry.frame.unwrap().mapped_pa,
226            ),
227    ;
228
229    pub axiom fn tracked_new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> tracked Self
230        returns
231            Self::new_node(node, path),
232    ;
233
234    /// Creates a ghost entry owner for mapping an untracked (device memory) frame.
235    /// Unlike `new_frame`, this does not consume a slot permission from the meta region,
236    /// since device memory PAs are outside the tracked frame allocator.
237    /// The actual mapping correctness is guaranteed by the caller's `unsafe` contract.
238    ///
239    /// The `requires` reflect properties guaranteed by `collect_largest_pages` postconditions,
240    /// so this axiom is only ever called with values that satisfy them.
241    pub axiom fn new_untracked_frame(
242        paddr: Paddr,
243        parent_level: PagingLevel,
244        prop: PageProperty,
245    ) -> (tracked res: Self)
246        requires
247            paddr % PAGE_SIZE == 0,
248            paddr < MAX_PADDR,
249            1 <= parent_level,
250            parent_level <= NR_LEVELS,
251        ensures
252            res.is_frame(),
253            res.frame.unwrap().mapped_pa == paddr,
254            res.frame.unwrap().prop == prop,
255            res.frame.unwrap().size == page_size(parent_level),
256            res.frame.unwrap().is_tracked == false,
257            res.parent_level == parent_level,
258            res.path.inv(),
259            res.in_scope,
260            res.inv_base(),
261            crate::mm::page_table::Child::<C>::Frame(paddr, parent_level, prop).wf(res),
262    ;
263
264    pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
265        &&& pte.paddr() % PAGE_SIZE == 0
266        &&& pte.paddr() < MAX_PADDR
267        &&& !pte.is_present() ==> {
268            &&& self.is_absent()
269            &&& parent_level > 1 ==> !pte.is_last(parent_level)
270        }
271        &&& pte.is_present() && !pte.is_last(parent_level) ==> {
272            &&& self.is_node()
273            &&& meta_to_frame(self.node.unwrap().meta_addr_self()) == pte.paddr()
274        }
275        &&& pte.is_present() && pte.is_last(parent_level) ==> {
276            &&& self.is_frame()
277            &&& self.frame.unwrap().mapped_pa == pte.paddr()
278            &&& self.frame.unwrap().prop == pte.prop()
279        }
280    }
281
282    /// PTE-shape constraint for a borrowed / translation-only entry. The
283    /// PTE must be a node-PTE (present and non-leaf at `parent_level`),
284    /// since the borrowed sub-table is accessed only via the MMU walk.
285    /// Unlike [`match_pte`], we do *not* pin the PTE's target paddr to
286    /// any owned `NodeOwner` — the sub-table is owned by a different
287    /// page-table configuration and the embedding doesn't track its
288    /// address here.
289    pub open spec fn borrowed_match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
290        &&& self.is_borrowed()
291        &&& pte.paddr() % PAGE_SIZE == 0
292        &&& pte.paddr() < MAX_PADDR
293        &&& pte.is_present()
294        &&& !pte.is_last(parent_level)
295    }
296
297    /// When owner is absent and pte is the absent PTE with valid paddr, match_pte holds.
298    pub proof fn absent_match_pte(owner: Self, pte: C::E, parent_level: PagingLevel)
299        requires
300            owner.is_absent(),
301            pte == C::E::new_absent_spec(),
302            pte.paddr() % PAGE_SIZE == 0,
303            pte.paddr() < MAX_PADDR,
304        ensures
305            owner.match_pte(pte, parent_level),
306    {
307        C::E::new_properties();
308        assert(!pte.is_present());
309        if parent_level > 1 {
310            assert(!pte.is_last(parent_level));
311        }
312        if pte.is_present() && !pte.is_last(parent_level) {
313            assert(pte.is_present());
314            assert(!pte.is_present());
315        }
316        if pte.is_present() && pte.is_last(parent_level) {
317            assert(pte.is_present());
318            assert(!pte.is_present());
319        }
320    }
321
322    pub proof fn last_pte_implies_frame_match(self, pte: C::E, parent_level: PagingLevel)
323        requires
324            self.inv(),
325            self.match_pte(pte, parent_level),
326            1 < parent_level,
327            pte.is_last(parent_level),
328        ensures
329            self.is_frame(),
330            self.frame.unwrap().mapped_pa == pte.paddr(),
331            self.frame.unwrap().prop == pte.prop(),
332    {
333        if !pte.is_present() {
334            assert(self.is_absent());
335            assert(!pte.is_last(parent_level));
336            assert(false);
337        }
338        assert(self.is_frame());
339        assert(self.frame.unwrap().mapped_pa == pte.paddr());
340        assert(self.frame.unwrap().prop == pte.prop());
341    }
342
343    pub proof fn huge_frame_split_child_at(self, regions: MetaRegionOwners, idx: usize)
344        requires
345            self.inv(),
346            self.is_frame(),
347            regions.inv(),
348            1 < self.parent_level < NR_LEVELS,
349            idx < NR_ENTRIES,
350        ensures
351            self.frame.unwrap().mapped_pa + idx * page_size((self.parent_level - 1) as PagingLevel)
352                < MAX_PADDR,
353            ((self.frame.unwrap().mapped_pa + idx * page_size(
354                (self.parent_level - 1) as PagingLevel,
355            )) as Paddr) % page_size((self.parent_level - 1) as PagingLevel) == 0,
356            ((self.frame.unwrap().mapped_pa + idx * page_size(
357                (self.parent_level - 1) as PagingLevel,
358            )) as Paddr) + page_size((self.parent_level - 1) as PagingLevel) <= MAX_PADDR,
359            ((self.frame.unwrap().mapped_pa + idx * page_size(
360                (self.parent_level - 1) as PagingLevel,
361            )) as Paddr) % PAGE_SIZE == 0,
362    {
363        let pa = self.frame.unwrap().mapped_pa;
364        let child_pa = (pa + idx * page_size((self.parent_level - 1) as PagingLevel)) as Paddr;
365        assert(self.parent_level == 2 || self.parent_level == 3);
366        assert(NR_ENTRIES == 512) by {
367            crate::specs::arch::paging_consts::lemma_nr_subpage_per_huge_eq_nr_entries();
368        };
369        assert(crate::mm::nr_subpage_per_huge::<PagingConsts>() == 512usize) by {
370            crate::specs::arch::paging_consts::lemma_nr_subpage_per_huge_eq_nr_entries();
371        };
372        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
373        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_spec_level1();
374        assert(512usize.ilog2() == 9);
375        assert(crate::mm::nr_subpage_per_huge::<PagingConsts>().ilog2() == 512usize.ilog2());
376        vstd::arithmetic::power2::lemma2_to64();
377        if self.parent_level == 2 {
378            assert(page_size_spec(1) == 4096);
379            assert(page_size_spec(2) == (PAGE_SIZE * pow2(
380                (512usize.ilog2() * 1usize) as nat,
381            )) as usize);
382            assert(page_size_spec(2) == (4096 * pow2(9)) as usize);
383            assert(page_size_spec(2) == 2097152);
384            assert(pa % page_size(2) == 0);
385            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_divides(1, 2);
386            assert(child_pa % page_size(1) == 0);
387            assert(child_pa + page_size(1) <= MAX_PADDR) by {
388                assert(idx < 512);
389                assert(idx * 4096 + 4096 <= 2097152);
390                assert(child_pa + page_size(1) <= pa + page_size(2));
391            };
392        } else {
393            assert(self.parent_level == 3);
394            assert(page_size_spec(2) == (PAGE_SIZE * pow2(
395                (512usize.ilog2() * 1usize) as nat,
396            )) as usize);
397            assert(page_size_spec(2) == (4096 * pow2(9)) as usize);
398            assert(page_size_spec(2) == 2097152);
399            assert(page_size_spec(3) == (PAGE_SIZE * pow2(
400                (512usize.ilog2() * 2usize) as nat,
401            )) as usize);
402            assert(page_size_spec(3) == (4096 * pow2(18)) as usize);
403            assert(page_size_spec(3) == 1073741824);
404            assert(pa % page_size(3) == 0);
405            assert(pa % PAGE_SIZE == 0);
406            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_va_align_page_size(pa, 2);
407            assert(child_pa == pa + idx * page_size(2));
408            vstd::arithmetic::div_mod::lemma_mod_multiples_basic(idx as int, page_size(2) as int);
409            vstd::arithmetic::div_mod::lemma_add_mod_noop(
410                pa as int,
411                (idx * page_size(2)) as int,
412                page_size(2) as int,
413            );
414            assert(child_pa % page_size(2) == 0);
415            assert(child_pa + page_size(2) <= MAX_PADDR) by {
416                assert(idx < 512);
417                assert(idx * 2097152 + 2097152 <= 1073741824);
418                assert(child_pa + page_size(2) <= pa + page_size(3));
419            };
420        }
421        assert(child_pa < MAX_PADDR);
422        assert(child_pa % PAGE_SIZE == 0);
423    }
424
425    /// Helper: sub-page validity is preserved when the only slot that changed is the
426    /// frame's own slot (and slots map and other slot owners are unchanged).
427    pub proof fn frame_sub_pages_valid_preserved_at_own_slot(
428        self,
429        r0: MetaRegionOwners,
430        r1: MetaRegionOwners,
431    )
432        requires
433            self.inv(),
434            r0.inv(),
435            self.is_frame(),
436            self.parent_level <= NR_LEVELS,
437            self.frame_sub_pages_valid(r0),
438            r0.slots == r1.slots,
439            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
440            forall|i: usize|
441                #![trigger r1.slot_owners[i]]
442                i != frame_to_index(self.meta_slot_paddr().unwrap()) && r0.slot_owners.contains_key(
443                    i,
444                ) ==> r0.slot_owners[i] == r1.slot_owners[i],
445        ensures
446            self.frame_sub_pages_valid(r1),
447    {
448        if self.parent_level > 1 {
449            let pa = self.frame.unwrap().mapped_pa;
450            let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
451            let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
452            assert forall|j: usize|
453                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
454                0 < j < nr_pages implies {
455                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
456                &&& r1.slots.contains_key(sub_idx)
457                &&& r1.slot_owners[sub_idx].usage
458                    != crate::specs::mm::frame::meta_owners::PageUsage::MMIO ==> {
459                    &&& r1.slot_owners[sub_idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
460                    &&& r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
461                }
462            } by {
463                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
464                // From frame_sub_pages_valid(r0): slot existence is unconditional.
465                assert(r0.slots.contains_key(sub_idx));
466                // sub_idx != self_idx by arithmetic: pa is PAGE_SIZE-aligned, so
467                // self_idx = pa / PAGE_SIZE, and sub_idx = (pa + j*PAGE_SIZE) / PAGE_SIZE
468                //         = pa/PAGE_SIZE + j = self_idx + j > self_idx (since j >= 1).
469                let pa_plus_int: int = pa as int + (j as int) * (PAGE_SIZE as int);
470                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_ge_page_size(
471                self.parent_level);
472                assert((j as int) * (PAGE_SIZE as int) < (nr_pages as int) * (PAGE_SIZE as int))
473                    by {
474                    vstd::arithmetic::mul::lemma_mul_strict_inequality(
475                        j as int,
476                        nr_pages as int,
477                        PAGE_SIZE as int,
478                    );
479                };
480                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_div_mul_eq(
481                    self.parent_level,
482                );
483                assert(pa_plus_int < MAX_PADDR);
484                vstd::arithmetic::div_mod::lemma_div_multiples_vanish_quotient(
485                    j as int,
486                    pa as int,
487                    PAGE_SIZE as int,
488                );
489                assert(self_idx as int == pa as int / PAGE_SIZE as int);
490                assert(sub_idx != self_idx);
491                assert(r0.slot_owners.contains_key(sub_idx));
492                assert(r0.slot_owners[sub_idx] == r1.slot_owners[sub_idx]);
493                // Slot equality at sub_idx carries usage and rc forward.
494            }
495        }
496    }
497
498    /// Sub-page slot validity for huge frames (fine-grained: all 4KB pages within).
499    ///
500    /// When a frame at this entry has `parent_level > 1`, it is a huge page covering
501    /// `page_size(parent_level)` bytes. Every 4KB sub-page within this range (excluding
502    /// the j = 0 case which coincides with the frame's own slot) must be allocated
503    /// (in the free pool) with `rc != UNUSED`.
504    ///
505    /// The fine-grained form (over `j * PAGE_SIZE` rather than `j * page_size(L-1)`) is
506    /// what enables the recursive split case in `split_if_mapped_huge`: when splitting a
507    /// 1GB frame into 2MB sub-frames, each 2MB sub-frame's own sub-page validity (over
508    /// its 511 4KB sub-sub-pages) follows from the 1GB frame's fine-grained validity over
509    /// the corresponding subrange of indices.
510    pub open spec fn frame_sub_pages_valid(self, regions: MetaRegionOwners) -> bool {
511        self.is_frame() && self.parent_level > 1 ==> {
512            let pa = self.frame.unwrap().mapped_pa;
513            let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
514            forall|j: usize|
515                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
516                0 < j < nr_pages ==> {
517                    let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
518                    // Slot existence is unconditional — the metadata array spans all
519                    // phys memory at boot, so every valid sub-page PA has an allocated slot.
520                    &&& regions.slots.contains_key(
521                        sub_idx,
522                    )
523                    // RC bookkeeping (`rc != UNUSED`, `rc > 0`) applies only to non-MMIO
524                    // sub-pages. MMIO sub-page slots stay in the free pool with
525                    // `rc == UNUSED` and `usage == MMIO`.
526                    &&& regions.slot_owners[sub_idx].usage
527                        != crate::specs::mm::frame::meta_owners::PageUsage::MMIO ==> {
528                        &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value()
529                            != REF_COUNT_UNUSED
530                        &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
531                    }
532                }
533        }
534    }
535
536    pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool {
537        if self.is_node() {
538            let idx = frame_to_index(self.meta_slot_paddr().unwrap());
539            &&& regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
540            &&& 0 < regions.slot_owners[idx].inner_perms.ref_count.value() <= REF_COUNT_MAX
541            &&& regions.slot_owners[idx].self_addr == self.node.unwrap().meta_addr_self()
542            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
543            &&& regions.slot_owners[idx].paths_in_pt == set![self.path]
544            &&& self.node.unwrap().metaregion_sound_node(regions)
545        } else if self.is_frame() {
546            let idx = frame_to_index(self.meta_slot_paddr().unwrap());
547            &&& regions.slots.contains_key(idx)
548            &&& regions.slots[idx].addr() == meta_addr(idx)
549            &&& regions.slots[idx].is_init()
550            &&& regions.slots[idx].value().wf(
551                regions.slot_owners[idx],
552            )
553            // Tracked vs MMIO discriminator is the slot's `usage`. MMIO slots
554            // stay in the free pool with `rc == UNUSED`; tracked slots have
555            // `rc > 0`. The slot's `usage == MMIO` is pinned by the paddr's
556            // range membership via `axiom_mmio_usage_iff_mmio_paddr`.
557            &&& regions.slot_owners[idx].usage
558                != crate::specs::mm::frame::meta_owners::PageUsage::MMIO ==> {
559                &&& regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
560                &&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
561            }
562            &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)
563            &&& self.frame_sub_pages_valid(regions)
564        } else {
565            true
566        }
567    }
568
569    /// PointsTo uniqueness: if meta slot `free_idx` is in the free pool (`regions.slots`),
570    /// no active page table NODE entry can own a PointsTo at the same slot address.
571    /// Justified by Verus's linear ownership of `PointsTo<MetaSlot>`:
572    /// the node's PointsTo is either in `regions.slots` OR held by the node, never both.
573    /// (Frames no longer own their PointsTo — they read from `regions.slots` directly.)
574    pub axiom fn active_entry_not_in_free_pool(
575        entry: Self,
576        regions: MetaRegionOwners,
577        free_idx: usize,
578    )
579        requires
580            regions.inv(),
581            entry.inv(),
582            entry.is_node(),
583            entry.metaregion_sound(regions),
584            regions.slots.contains_key(free_idx),
585        ensures
586            frame_to_index(entry.meta_slot_paddr().unwrap()) != free_idx,
587    ;
588
589    pub axiom fn get_path(self) -> tracked TreePath<NR_ENTRIES>
590        returns
591            self.path,
592    ;
593
594    pub open spec fn meta_slot_paddr(self) -> Option<Paddr> {
595        if self.is_node() {
596            Some(meta_to_frame(self.node.unwrap().meta_addr_self()))
597        } else if self.is_frame() {
598            Some(self.frame.unwrap().mapped_pa)
599        } else {
600            None
601        }
602    }
603
604    pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool {
605        self.meta_slot_paddr() is Some ==> other.meta_slot_paddr() is Some
606            ==> self.meta_slot_paddr().unwrap() != other.meta_slot_paddr().unwrap()
607    }
608
609    /// `metaregion_sound` transfers when `slot_owners` matches and `slots` is a superset.
610    /// For nodes: only `slot_owners` matters. For frames: `slots.contains_key` and `slots[idx]`
611    /// must be preserved, which holds when `slots` is a superset with values unchanged.
612    pub proof fn metaregion_sound_slot_owners_only(self, r0: MetaRegionOwners, r1: MetaRegionOwners)
613        requires
614            self.inv(),
615            self.metaregion_sound(r0),
616            r0.slot_owners == r1.slot_owners,
617            forall|k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
618            forall|k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
619        ensures
620            self.metaregion_sound(r1),
621    {
622        if self.is_node() {
623            let slot_idx = self.node.unwrap().slot_index;
624            assert(r0.slots.contains_key(slot_idx));
625            assert(self.node.unwrap().meta_perm_of(r1) == self.node.unwrap().meta_perm_of(r0));
626        }
627    }
628
629    /// If `metaregion_sound(r0)` holds and `r1` differs from `r0` only at one slot index
630    /// that this entry does not reference, then `metaregion_sound(r1)` also holds.
631    pub proof fn metaregion_sound_one_slot_changed(
632        self,
633        r0: MetaRegionOwners,
634        r1: MetaRegionOwners,
635        changed_idx: usize,
636    )
637        requires
638            self.inv(),
639            self.metaregion_sound(r0),
640            forall|i: usize|
641                #![trigger r1.slot_owners[i]]
642                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
643            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
644            // slots preserved at the entry's index (frames read from slots)
645            forall|k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
646            forall|k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
647            self.meta_slot_paddr() is Some ==> frame_to_index(self.meta_slot_paddr().unwrap())
648                != changed_idx,
649            // Huge frames: if changed_idx is one of this frame's 4KB sub-page slots and
650            // that sub-slot is non-MMIO, the sub-page validity at changed_idx must still
651            // hold in r1. MMIO sub-pages keep `usage == MMIO` and `rc == UNUSED`.
652            self.is_frame() && self.parent_level > 1 ==> {
653                let pa = self.frame.unwrap().mapped_pa;
654                let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
655                forall|j: usize|
656                    0 < j < nr_pages ==> {
657                        let sub_idx = #[trigger] frame_to_index((pa + j * PAGE_SIZE) as usize);
658                        sub_idx != changed_idx || r1.slot_owners[sub_idx].usage
659                            == crate::specs::mm::frame::meta_owners::PageUsage::MMIO || (
660                        r1.slots.contains_key(sub_idx)
661                            && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
662                            != REF_COUNT_UNUSED
663                            && r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0)
664                    }
665            },
666        ensures
667            self.metaregion_sound(r1),
668    {
669        if self.is_node() {
670            let slot_idx = self.node.unwrap().slot_index;
671            let outer_idx = frame_to_index(self.meta_slot_paddr().unwrap());
672            assert(r0.slots.contains_key(slot_idx));
673            assert(slot_idx != changed_idx);
674            assert(r1.slot_owners[slot_idx] == r0.slot_owners[slot_idx]);
675            assert(self.node.unwrap().meta_perm_of(r1) == self.node.unwrap().meta_perm_of(r0));
676        }
677    }
678
679    /// `metaregion_sound` is preserved when only `paths_in_pt` changes at a slot,
680    /// `slots` is unchanged, and the new `paths_in_pt` is correct for any node at that index.
681    pub proof fn metaregion_sound_paths_in_pt_changed(
682        self,
683        r0: MetaRegionOwners,
684        r1: MetaRegionOwners,
685        changed_idx: usize,
686    )
687        requires
688            self.inv(),
689            r0.inv(),
690            self.metaregion_sound(r0),
691            r0.slots == r1.slots,
692            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
693            // All slots other than changed_idx are entirely unchanged.
694            forall|i: usize|
695                #![trigger r1.slot_owners[i]]
696                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
697            // At changed_idx, only paths_in_pt differs.
698            r1.slot_owners[changed_idx].inner_perms == r0.slot_owners[changed_idx].inner_perms,
699            r1.slot_owners[changed_idx].self_addr == r0.slot_owners[changed_idx].self_addr,
700            r1.slot_owners[changed_idx].usage == r0.slot_owners[changed_idx].usage,
701            // For nodes at changed_idx: the new paths_in_pt must match this entry's path.
702            self.is_node() && self.meta_slot_paddr() is Some && frame_to_index(
703                self.meta_slot_paddr().unwrap(),
704            ) == changed_idx ==> r1.slot_owners[changed_idx].paths_in_pt == set![self.path],
705            // For frames at changed_idx: the new paths_in_pt must still contain this entry's path.
706            self.is_frame() && self.meta_slot_paddr() is Some && frame_to_index(
707                self.meta_slot_paddr().unwrap(),
708            ) == changed_idx ==> r1.slot_owners[changed_idx].paths_in_pt.contains(self.path),
709            // For huge frames: if changed_idx is one of this frame's sub-page slots (j > 0),
710            // the new paths_in_pt at changed_idx must remain empty.
711            self.is_frame() && self.parent_level > 1 ==> {
712                let pa = self.frame.unwrap().mapped_pa;
713                let sub_level = (self.parent_level - 1) as PagingLevel;
714                forall|j: usize|
715                    0 < j < NR_ENTRIES ==> {
716                        let sub_idx = #[trigger] frame_to_index(
717                            (pa + j * page_size(sub_level)) as usize,
718                        );
719                        sub_idx != changed_idx || r1.slot_owners[changed_idx].paths_in_pt.is_empty()
720                    }
721            },
722        ensures
723            self.metaregion_sound(r1),
724    {
725        if self.meta_slot_paddr() is Some {
726            let eidx = frame_to_index(self.meta_slot_paddr().unwrap());
727            // Bridge `rc > 0` from r0 to r1: at `eidx == changed_idx` inner_perms
728            // are identical; elsewhere the entire slot_owner is identical.
729            if self.is_frame() {
730                if eidx == changed_idx {
731                    assert(r1.slot_owners[eidx].inner_perms == r0.slot_owners[eidx].inner_perms);
732                } else {
733                    assert(r1.slot_owners[eidx] == r0.slot_owners[eidx]);
734                }
735                // Sub-page validity for huge frames: slot existence (unconditional)
736                // plus `rc` bookkeeping when tracked.
737                if self.parent_level > 1 {
738                    let pa = self.frame.unwrap().mapped_pa;
739                    let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
740                    let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
741                    assert forall|j: usize|
742                        #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
743                        0 < j < nr_pages implies {
744                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
745                        &&& r1.slots.contains_key(sub_idx)
746                        &&& r1.slot_owners[sub_idx].usage
747                            != crate::specs::mm::frame::meta_owners::PageUsage::MMIO ==> {
748                            &&& r1.slot_owners[sub_idx].inner_perms.ref_count.value()
749                                != REF_COUNT_UNUSED
750                            &&& r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
751                        }
752                    } by {
753                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
754                        // From self.metaregion_sound(r0)'s frame arm (frame_sub_pages_valid(r0)).
755                        assert(r0.slots.contains_key(sub_idx));
756                        if sub_idx == changed_idx {
757                            assert(r1.slot_owners[sub_idx].inner_perms
758                                == r0.slot_owners[sub_idx].inner_perms);
759                            assert(r1.slot_owners[sub_idx].usage == r0.slot_owners[sub_idx].usage);
760                        } else {
761                            assert(r1.slot_owners[sub_idx] == r0.slot_owners[sub_idx]);
762                        }
763                    }
764                }
765            }
766        }
767    }
768
769    /// Two entries with the same physical address whose `paths_in_pt` matches their
770    /// respective paths must have the same path.
771    pub proof fn same_paddr_implies_same_path(self, other: Self, regions: MetaRegionOwners)
772        requires
773            self.meta_slot_paddr() is Some,
774            self.meta_slot_paddr() == other.meta_slot_paddr(),
775            regions.slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())].paths_in_pt
776                == set![self.path],
777            regions.slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())].paths_in_pt
778                == set![other.path],
779        ensures
780            self.path == other.path,
781    {
782        assert(set![self.path].contains(other.path));
783    }
784
785    /// `metaregion_sound` is preserved when only `ref_count.value()` changes at this entry's slot
786    /// and `slots` is unchanged.
787    pub proof fn metaregion_sound_rc_value_changed(self, r0: MetaRegionOwners, r1: MetaRegionOwners)
788        requires
789            self.inv(),
790            r0.inv(),
791            self.metaregion_sound(r0),
792            self.meta_slot_paddr() is Some,
793            r0.slots == r1.slots,
794            ({
795                let idx = frame_to_index(self.meta_slot_paddr().unwrap());
796                &&& r1.slot_owners[idx].inner_perms.ref_count.id()
797                    == r0.slot_owners[idx].inner_perms.ref_count.id()
798                &&& r1.slot_owners[idx].inner_perms.ref_count.value()
799                    != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
800                &&& r1.slot_owners[idx].inner_perms.ref_count.value()
801                    > 0
802                // Needed to re-establish the node branch's SHARED range (`<= MAX`).
803                &&& r1.slot_owners[idx].inner_perms.ref_count.value() <= REF_COUNT_MAX
804                &&& r1.slot_owners[idx].inner_perms.storage
805                    == r0.slot_owners[idx].inner_perms.storage
806                &&& r1.slot_owners[idx].inner_perms.vtable_ptr
807                    == r0.slot_owners[idx].inner_perms.vtable_ptr
808                &&& r1.slot_owners[idx].inner_perms.in_list
809                    == r0.slot_owners[idx].inner_perms.in_list
810                &&& r1.slot_owners[idx].self_addr == r0.slot_owners[idx].self_addr
811                &&& r1.slot_owners[idx].paths_in_pt == r0.slot_owners[idx].paths_in_pt
812            }),
813            // All other slot_owners unchanged: preserves sub-page validity for huge frames.
814            forall|i: usize|
815                #![trigger r1.slot_owners[i]]
816                i != frame_to_index(self.meta_slot_paddr().unwrap()) && r0.slot_owners.contains_key(
817                    i,
818                ) ==> r0.slot_owners[i] == r1.slot_owners[i],
819        ensures
820            self.metaregion_sound(r1),
821    {
822        if self.is_frame() && self.parent_level > 1 {
823            let pa = self.frame.unwrap().mapped_pa;
824            let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
825            let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
826            assert forall|j: usize|
827                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
828                0 < j < nr_pages implies {
829                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
830                &&& r1.slots.contains_key(sub_idx)
831                &&& r1.slot_owners[sub_idx].usage
832                    != crate::specs::mm::frame::meta_owners::PageUsage::MMIO ==> {
833                    &&& r1.slot_owners[sub_idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
834                    &&& r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
835                }
836            } by {
837                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
838                assert(r0.slots.contains_key(sub_idx));
839                let pa_plus_int: int = pa as int + (j as int) * (PAGE_SIZE as int);
840                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_ge_page_size(
841                self.parent_level);
842                assert((j as int) * (PAGE_SIZE as int) < (nr_pages as int) * (PAGE_SIZE as int))
843                    by {
844                    vstd::arithmetic::mul::lemma_mul_strict_inequality(
845                        j as int,
846                        nr_pages as int,
847                        PAGE_SIZE as int,
848                    );
849                };
850                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_div_mul_eq(
851                    self.parent_level,
852                );
853                assert(pa_plus_int < MAX_PADDR);
854                // sub_idx = (pa + j*PAGE_SIZE) / PAGE_SIZE = pa/PAGE_SIZE + j (since pa % PAGE_SIZE == 0).
855                vstd::arithmetic::div_mod::lemma_div_multiples_vanish_quotient(
856                    j as int,
857                    pa as int,
858                    PAGE_SIZE as int,
859                );
860                assert(self_idx as int == pa as int / PAGE_SIZE as int);
861                assert(sub_idx != self_idx);
862                assert(r0.slot_owners.contains_key(sub_idx));
863                assert(r0.slot_owners[sub_idx] == r1.slot_owners[sub_idx]);
864            }
865        }
866    }
867
868    /// Two nodes whose `paths_in_pt` matches their paths have different addresses
869    /// if they have different paths.
870    pub proof fn nodes_different_paths_different_addrs(self, other: Self, regions: MetaRegionOwners)
871        requires
872            self.is_node(),
873            other.is_node(),
874            self.meta_slot_paddr() is Some ==> regions.slot_owners[frame_to_index(
875                self.meta_slot_paddr().unwrap(),
876            )].paths_in_pt == set![self.path],
877            other.meta_slot_paddr() is Some ==> regions.slot_owners[frame_to_index(
878                other.meta_slot_paddr().unwrap(),
879            )].paths_in_pt == set![other.path],
880            self.path != other.path,
881        ensures
882            self.node.unwrap().meta_addr_self() != other.node.unwrap().meta_addr_self(),
883    {
884        let self_addr = self.node.unwrap().meta_addr_self();
885        let other_addr = other.node.unwrap().meta_addr_self();
886        let self_idx = frame_to_index(meta_to_frame(self_addr));
887        let other_idx = frame_to_index(meta_to_frame(other_addr));
888
889        if self_addr == other_addr {
890            assert(regions.slot_owners[self_idx].paths_in_pt == set![self.path]);
891            assert(regions.slot_owners[other_idx].paths_in_pt == set![other.path]);
892            assert(set![self.path].contains(other.path));
893            assert(self.path == other.path);
894            assert(false);  // Contradiction
895        }
896    }
897
898    /// Two node entries with `metaregion_sound` under the same regions cannot share
899    /// a meta slot paddr if their paths have different lengths.
900    ///
901    /// For nodes, `metaregion_sound` requires `paths_in_pt == set![path]` (singleton).
902    /// Equal slot indices would force equal singleton sets, hence equal paths —
903    /// contradicting the length difference.
904    pub proof fn nodes_different_path_lengths_neq_slot(self, other: Self, regions: MetaRegionOwners)
905        requires
906            self.is_node(),
907            other.is_node(),
908            self.metaregion_sound(regions),
909            other.metaregion_sound(regions),
910            self.path.len() != other.path.len(),
911        ensures
912            self.meta_slot_paddr_neq(other),
913    {
914        let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
915        let other_idx = frame_to_index(other.meta_slot_paddr().unwrap());
916        if self_idx == other_idx {
917            assert(regions.slot_owners[self_idx].paths_in_pt == set![self.path]);
918            assert(regions.slot_owners[other_idx].paths_in_pt == set![other.path]);
919            assert(set![self.path].contains(other.path));
920            assert(self.path == other.path);
921            assert(false);
922        }
923    }
924}
925
926impl<C: PageTableConfig> EntryOwner<C> {
927    /// Structural invariant without `!in_scope`. Used by `Child::invariants`
928    /// for entries that have been taken out of the tree (`in_scope == true`).
929    pub open spec fn inv_base(self) -> bool {
930        &&& self.node is Some ==> {
931            &&& self.frame is None
932            &&& self.locked is None
933            &&& self.borrowed is None
934            &&& self.node.unwrap().inv()
935            &&& !self.absent
936            &&& self.parent_level == self.node.unwrap().level + 1
937        }
938        &&& self.frame is Some ==> {
939            &&& self.node is None
940            &&& self.locked is None
941            &&& self.borrowed is None
942            &&& !self.absent
943            // Architectural constraint: frames only exist at PT levels that the
944            // ISA actually supports as leaves (4K, 2M, 1G on x86). `parent_level
945            // == NR_LEVELS` would be a 512 GiB huge page, which no current arch
946            // permits — and `Mapping::inv` would reject its page_size.
947            &&& 1 <= self.parent_level < NR_LEVELS
948            &&& self.frame.unwrap().mapped_pa % PAGE_SIZE == 0
949            &&& self.frame.unwrap().mapped_pa < MAX_PADDR
950            &&& self.frame.unwrap().size == page_size(self.parent_level)
951            &&& self.frame.unwrap().mapped_pa % page_size(self.parent_level) == 0
952            &&& self.frame.unwrap().mapped_pa + page_size(self.parent_level) <= MAX_PADDR
953        }
954        &&& self.locked is Some ==> {
955            &&& self.frame is None
956            &&& self.node is None
957            &&& self.borrowed is None
958            &&& !self.absent
959        }
960        &&& self.borrowed is Some ==> {
961            &&& self.node is None
962            &&& self.frame is None
963            &&& self.locked is None
964            &&& !self.absent
965        }
966        &&& self.path.inv()
967    }
968
969    pub open spec fn set_in_scope(self, in_scope: bool) -> Self {
970        EntryOwner { in_scope, ..self }
971    }
972}
973
974impl<C: PageTableConfig> Inv for EntryOwner<C> {
975    open spec fn inv(self) -> bool {
976        &&& !self.in_scope
977        &&& self.inv_base()
978    }
979}
980
981impl<C: PageTableConfig> View for EntryOwner<C> {
982    type V = EntryView<C>;
983
984    #[verifier::external_body]
985    open spec fn view(&self) -> <Self as View>::V {
986        if let Some(frame) = self.frame {
987            EntryView::Leaf {
988                leaf: LeafPageTableEntryView {
989                    map_va: vaddr(self.path) as int,
990                    //                    frame_pa: self.base_addr as int,
991                    //                    in_frame_index: self.index as int,
992                    map_to_pa: frame.mapped_pa as int,
993                    level: self.path.len() as u8,
994                    prop: frame.prop,
995                    phantom: PhantomData,
996                },
997            }
998        } else if let Some(node) = self.node {
999            EntryView::Intermediate {
1000                node: IntermediatePageTableEntryView {
1001                    map_va: vaddr(self.path) as int,
1002                    //                    frame_pa: self.base_addr as int,
1003                    //                    in_frame_index: self.index as int,
1004                    map_to_pa: meta_to_frame(node.meta_addr_self()) as int,
1005                    level: self.path.len() as u8,
1006                    phantom: PhantomData,
1007                },
1008            }
1009        } else if let Some(view) = self.locked {
1010            EntryView::LockedSubtree { views: view@ }
1011        } else {
1012            EntryView::Absent
1013        }
1014    }
1015}
1016
1017impl<C: PageTableConfig> InvView for EntryOwner<C> {
1018    proof fn view_preserves_inv(self) {
1019        // `EntryView::inv()` is trivially `true` (the view of an `EntryOwner`
1020        // is never inspected outside this trait obligation), so the
1021        // postcondition `self.view().inv()` discharges automatically.
1022    }
1023}
1024
1025impl<'a, 'rcu, C: PageTableConfig> OwnerOf for Entry<'a, 'rcu, C> {
1026    type Owner = EntryOwner<C>;
1027
1028    open spec fn wf(self, owner: Self::Owner) -> bool {
1029        &&& self.idx < NR_ENTRIES
1030        &&& owner.match_pte(self.pte, owner.parent_level)
1031        &&& self.pte.paddr() % PAGE_SIZE == 0
1032        &&& self.pte.paddr() < MAX_PADDR
1033    }
1034}
1035
1036} // verus!
ostd/specs/mm/page_table/node/entry_owners.rs

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