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

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

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