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

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

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