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, meta_to_index},
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].ref_count() != REF_COUNT_UNUSED
435                    &&& r1.slot_owners[sub_idx].ref_count() > 0
436                    &&& r1.slot_owners[sub_idx].ref_count() <= 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].ref_count() != REF_COUNT_UNUSED
490                        &&& regions.slot_owners[sub_idx].ref_count() > 0
491                        &&& regions.slot_owners[sub_idx].ref_count() <= REF_COUNT_MAX
492                    }
493                }
494        }
495    }
496
497    pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool {
498        if self.is_node() {
499            let idx = frame_to_index(self.meta_slot_paddr()->0);
500            &&& regions.slot_owners[idx].ref_count() != REF_COUNT_UNUSED
501            &&& 0 < regions.slot_owners[idx].ref_count() <= REF_COUNT_MAX
502            &&& regions.slot_owners[idx].slot_vaddr == self.node().meta_vaddr()
503            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
504            &&& regions.slot_owners[idx].paths_in_pt == set![self.path]
505            &&& self.node().metaregion_sound_node(regions)
506        } else if self.is_frame() {
507            let idx = frame_to_index(self.meta_slot_paddr()->0);
508            &&& regions.slots.contains_key(idx)
509            &&& regions.slots[idx].addr() == index_to_meta(idx)
510            &&& regions.slots[idx].is_init()
511            &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
512            &&& regions.slot_owners[idx].usage !is PageTable
513            // Tracked vs MMIO discriminator is the slot's `usage`. MMIO slots
514            // stay in the free pool with `rc == UNUSED`; tracked slots have
515            // `rc > 0`. The slot's `usage == MMIO` is pinned by the paddr's
516            // range membership via `axiom_mmio_usage_iff_mmio_paddr`.
517            &&& regions.slot_owners[idx].usage !is MMIO ==> {
518                &&& regions.slot_owners[idx].ref_count() != REF_COUNT_UNUSED
519                &&& regions.slot_owners[idx].ref_count()
520                    > 0
521                // A mapped (tracked) frame is SHARED, never the UNIQUE sentinel
522                // (`rc <= MAX < REF_COUNT_UNIQUE`). Lets the UNIQUE-branch
523                // `paths_in_pt`-empty inv clause hold vacuously for mapped
524                // frames whose `paths_in_pt` is non-empty.
525                &&& regions.slot_owners[idx].ref_count() <= REF_COUNT_MAX
526            }
527            &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)
528            &&& self.frame_sub_pages_valid(regions)
529        } else {
530            true
531        }
532    }
533
534    /// An active page-table node cannot occupy a metadata slot whose refcount is
535    /// still `REF_COUNT_UNUSED`.
536    pub proof fn lemma_active_entry_not_in_free_pool(
537        entry: Self,
538        regions: MetaRegionOwners,
539        free_idx: int,
540    )
541        requires
542            regions.inv(),
543            entry.inv(),
544            entry.is_node(),
545            entry.metaregion_sound(regions),
546            regions.slots.contains_key(free_idx),
547            regions.slot_owners[free_idx].ref_count() == REF_COUNT_UNUSED,
548        ensures
549            frame_to_index(entry.meta_slot_paddr()->0) != free_idx,
550    {
551        let idx = frame_to_index(entry.meta_slot_paddr().unwrap());
552        if idx == free_idx {
553            assert(false);
554        }
555    }
556
557    pub open spec fn meta_slot_paddr(self) -> Option<Paddr> {
558        if self.is_node() {
559            Some(meta_to_frame(self.node().meta_vaddr()))
560        } else if self.is_frame() {
561            Some(self.frame().mapped_pa)
562        } else {
563            None
564        }
565    }
566
567    pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool {
568        self.meta_slot_paddr() is Some ==> other.meta_slot_paddr() is Some
569            ==> self.meta_slot_paddr()->0 != other.meta_slot_paddr()->0
570    }
571
572    /// `metaregion_sound` transfers when `slot_owners` matches and `slots` is a superset.
573    /// For nodes: only `slot_owners` matters. For frames: `slots.contains_key` and `slots[idx]`
574    /// must be preserved, which holds when `slots` is a superset with values unchanged.
575    pub proof fn metaregion_sound_slot_owners_only(self, r0: MetaRegionOwners, r1: MetaRegionOwners)
576        requires
577            self.inv(),
578            self.metaregion_sound(r0),
579            r0.slot_owners == r1.slot_owners,
580            forall|k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
581            forall|k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
582        ensures
583            self.metaregion_sound(r1),
584    {
585    }
586
587    /// If `metaregion_sound(r0)` holds and `r1` differs from `r0` only at one slot index
588    /// that this entry does not reference, then `metaregion_sound(r1)` also holds.
589    pub proof fn metaregion_sound_one_slot_changed(
590        self,
591        r0: MetaRegionOwners,
592        r1: MetaRegionOwners,
593        changed_idx: int,
594    )
595        requires
596            self.inv(),
597            self.metaregion_sound(r0),
598            forall|i: int|
599                #![trigger r1.slot_owners[i]]
600                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
601            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
602            // slots preserved at the entry's index (frames read from slots)
603            forall|k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
604            forall|k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
605            self.meta_slot_paddr() is Some ==> frame_to_index(self.meta_slot_paddr()->0)
606                != changed_idx,
607            // Huge frames: if changed_idx is one of this frame's 4KB sub-page slots and
608            // that sub-slot is non-MMIO, the sub-page validity at changed_idx must still
609            // hold in r1. MMIO sub-pages keep `usage == MMIO` and `rc == UNUSED`.
610            self.is_frame() && self.parent_level > 1 ==> {
611                let pa = self.frame().mapped_pa;
612                let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
613                forall|j: usize|
614                    0 < j < nr_pages ==> {
615                        let sub_idx = #[trigger] frame_to_index((pa + j * PAGE_SIZE) as usize);
616                        sub_idx != changed_idx || r1.slot_owners[sub_idx].usage is MMIO || (
617                        r1.slots.contains_key(sub_idx) && r1.slot_owners[sub_idx].ref_count()
618                            != REF_COUNT_UNUSED && r1.slot_owners[sub_idx].ref_count() > 0
619                            && r1.slot_owners[sub_idx].ref_count() <= REF_COUNT_MAX)
620                    }
621            },
622        ensures
623            self.metaregion_sound(r1),
624    {
625    }
626
627    /// `metaregion_sound` is preserved when only `paths_in_pt` changes at a slot,
628    /// `slots` is unchanged, and the new `paths_in_pt` is correct for any node at that index.
629    pub proof fn metaregion_sound_paths_in_pt_changed(
630        self,
631        r0: MetaRegionOwners,
632        r1: MetaRegionOwners,
633        changed_idx: int,
634    )
635        requires
636            self.inv(),
637            r0.inv(),
638            self.metaregion_sound(r0),
639            r0.slots == r1.slots,
640            r0.slot_owners.dom() =~= r1.slot_owners.dom(),
641            // All slots other than changed_idx are entirely unchanged.
642            forall|i: int|
643                #![trigger r1.slot_owners[i]]
644                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
645            // At changed_idx, only paths_in_pt differs.
646            r1.slot_owners[changed_idx].same_permissions(r0.slot_owners[changed_idx]),
647            r1.slot_owners[changed_idx].slot_vaddr == r0.slot_owners[changed_idx].slot_vaddr,
648            r1.slot_owners[changed_idx].usage == r0.slot_owners[changed_idx].usage,
649            // For nodes at changed_idx: the new paths_in_pt must match this entry's path.
650            self.is_node() && self.meta_slot_paddr() is Some && frame_to_index(
651                self.meta_slot_paddr()->0,
652            ) == changed_idx ==> r1.slot_owners[changed_idx].paths_in_pt == set![self.path],
653            // For frames at changed_idx: the new paths_in_pt must still contain this entry's path.
654            self.is_frame() && self.meta_slot_paddr() is Some && frame_to_index(
655                self.meta_slot_paddr()->0,
656            ) == changed_idx ==> r1.slot_owners[changed_idx].paths_in_pt.contains(self.path),
657            // For huge frames: if changed_idx is one of this frame's sub-page slots (j > 0),
658            // the new paths_in_pt at changed_idx must remain empty.
659            self.is_frame() && self.parent_level > 1 ==> {
660                let pa = self.frame().mapped_pa;
661                let sub_level = (self.parent_level - 1) as PagingLevel;
662                forall|j: int|
663                    0 < j < NR_ENTRIES ==> {
664                        let sub_idx = #[trigger] frame_to_index(
665                            (pa + j * page_size(sub_level)) as usize,
666                        );
667                        sub_idx != changed_idx || r1.slot_owners[changed_idx].paths_in_pt.is_empty()
668                    }
669            },
670        ensures
671            self.metaregion_sound(r1),
672    {
673        if self.meta_slot_paddr() is Some {
674            let eidx = frame_to_index(self.meta_slot_paddr().unwrap());
675            // Bridge `rc > 0` from r0 to r1: at `eidx == changed_idx` the
676            // permissions are preserved; elsewhere the entire slot owner is identical.
677            if self.is_frame() {
678                // Sub-page validity for huge frames: slot existence (unconditional)
679                // plus `rc` bookkeeping when tracked.
680                if self.parent_level > 1 {
681                    let pa = self.frame().mapped_pa;
682                    let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
683                    let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
684                    assert forall|j: usize|
685                        #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
686                        0 < j < nr_pages implies {
687                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
688                        &&& r1.slots.contains_key(sub_idx)
689                        &&& r1.slot_owners[sub_idx].usage !is MMIO ==> {
690                            &&& r1.slot_owners[sub_idx].ref_count() != REF_COUNT_UNUSED
691                            &&& r1.slot_owners[sub_idx].ref_count() > 0
692                            &&& r1.slot_owners[sub_idx].ref_count() <= REF_COUNT_MAX
693                        }
694                    } by {
695                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
696                        // From self.metaregion_sound(r0)'s frame arm (frame_sub_pages_valid(r0)).
697                    }
698                }
699            }
700        }
701    }
702
703    /// Two entries with the same physical address whose `paths_in_pt` matches their
704    /// respective paths must have the same path.
705    pub proof fn same_paddr_implies_same_path(self, other: Self, regions: MetaRegionOwners)
706        requires
707            self.meta_slot_paddr() is Some,
708            self.meta_slot_paddr() == other.meta_slot_paddr(),
709            regions.slot_owner(self.meta_slot_paddr()->0).paths_in_pt == set![self.path],
710            regions.slot_owner(other.meta_slot_paddr()->0).paths_in_pt == set![other.path],
711        ensures
712            self.path == other.path,
713    {
714        assert(set![self.path].contains(other.path));
715    }
716
717    /// `metaregion_sound` is preserved when only `ref_count.value()` changes at this entry's slot
718    /// and `slots` is unchanged.
719    pub proof fn metaregion_sound_rc_value_changed(self, r0: MetaRegionOwners, r1: MetaRegionOwners)
720        requires
721            self.inv(),
722            r0.inv(),
723            self.metaregion_sound(r0),
724            self.meta_slot_paddr() is Some,
725            r0.slots == r1.slots,
726            ({
727                let idx = frame_to_index(self.meta_slot_paddr()->0);
728                &&& r1.slot_owners.contains_key(idx)
729                &&& r1.slot_owners[idx].ref_count_perm.id()
730                    == r0.slot_owners[idx].ref_count_perm.id()
731                &&& r1.slot_owners[idx].ref_count() != REF_COUNT_UNUSED
732                &&& r1.slot_owners[idx].ref_count()
733                    > 0
734                // Needed to re-establish the node branch's SHARED range (`<= MAX`).
735                &&& r1.slot_owners[idx].ref_count() <= REF_COUNT_MAX
736                &&& r1.slot_owners[idx].storage_perm() == r0.slot_owners[idx].storage_perm()
737                &&& r1.slot_owners[idx].vtable_ptr_perm() == r0.slot_owners[idx].vtable_ptr_perm()
738                &&& r1.slot_owners[idx].in_list_perm == r0.slot_owners[idx].in_list_perm
739                &&& r1.slot_owners[idx].slot_vaddr == r0.slot_owners[idx].slot_vaddr
740                &&& r1.slot_owners[idx].paths_in_pt
741                    == r0.slot_owners[idx].paths_in_pt
742                // `usage` is part of `metaregion_sound_node` (node-repark
743                // discriminator), so it must be preserved to carry soundness.
744                &&& r1.slot_owners[idx].usage == r0.slot_owners[idx].usage
745            }),
746            // All other slot_owners unchanged: preserves sub-page validity for huge frames.
747            forall|i: int|
748                #![trigger r1.slot_owners[i]]
749                i != frame_to_index(self.meta_slot_paddr()->0) && r0.slot_owners.contains_key(i)
750                    ==> r0.slot_owners[i] == r1.slot_owners[i],
751        ensures
752            self.metaregion_sound(r1),
753    {
754        if self.is_frame() && self.parent_level > 1 {
755            let pa = self.frame().mapped_pa;
756            let nr_pages = page_size(self.parent_level) / PAGE_SIZE;
757            let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
758            assert forall|j: usize|
759                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
760                0 < j < nr_pages implies {
761                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
762                &&& r1.slots.contains_key(sub_idx)
763                &&& r1.slot_owners[sub_idx].usage !is MMIO ==> {
764                    &&& r1.slot_owners[sub_idx].ref_count() != REF_COUNT_UNUSED
765                    &&& r1.slot_owners[sub_idx].ref_count() > 0
766                }
767            } by {
768                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
769                let pa_plus_int: int = pa + j * PAGE_SIZE;
770                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_ge_page_size(
771                self.parent_level);
772                crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_div_mul_eq(
773                    self.parent_level,
774                );
775                // sub_idx = (pa + j*PAGE_SIZE) / PAGE_SIZE = pa/PAGE_SIZE + j (since pa % PAGE_SIZE == 0).
776                vstd::arithmetic::div_mod::lemma_div_multiples_vanish_quotient(
777                    j as int,
778                    pa as int,
779                    PAGE_SIZE as int,
780                );
781            }
782        }
783    }
784
785    /// Two nodes whose `paths_in_pt` matches their paths have different addresses
786    /// if they have different paths.
787    pub proof fn nodes_different_paths_different_addrs(self, other: Self, regions: MetaRegionOwners)
788        requires
789            self.is_node(),
790            other.is_node(),
791            self.meta_slot_paddr() is Some ==> regions.slot_owner(
792                self.meta_slot_paddr()->0,
793            ).paths_in_pt == set![self.path],
794            other.meta_slot_paddr() is Some ==> regions.slot_owner(
795                other.meta_slot_paddr()->0,
796            ).paths_in_pt == set![other.path],
797            self.path != other.path,
798        ensures
799            self.node().meta_vaddr() != other.node().meta_vaddr(),
800    {
801        let slot_vaddr = self.node().meta_vaddr();
802        let other_addr = other.node().meta_vaddr();
803        let self_idx = meta_to_index(slot_vaddr);
804        let other_idx = meta_to_index(other_addr);
805
806        if slot_vaddr == other_addr {
807            assert(set![self.path].contains(other.path));
808            assert(false);  // Contradiction
809        }
810    }
811
812    /// Two node entries with `metaregion_sound` under the same regions cannot share
813    /// a meta slot paddr if their paths have different lengths.
814    ///
815    /// For nodes, `metaregion_sound` requires `paths_in_pt == set![path]` (singleton).
816    /// Equal slot indices would force equal singleton sets, hence equal paths —
817    /// contradicting the length difference.
818    pub proof fn nodes_different_path_lengths_neq_slot(self, other: Self, regions: MetaRegionOwners)
819        requires
820            self.is_node(),
821            other.is_node(),
822            self.metaregion_sound(regions),
823            other.metaregion_sound(regions),
824            self.path.len() != other.path.len(),
825        ensures
826            self.meta_slot_paddr_neq(other),
827    {
828        let self_idx = frame_to_index(self.meta_slot_paddr().unwrap());
829        let other_idx = frame_to_index(other.meta_slot_paddr().unwrap());
830        if self_idx == other_idx {
831            assert(set![self.path].contains(other.path));
832            assert(false);
833        }
834    }
835}
836
837impl<C: PageTableConfig> EntryOwner<C> {
838    /// Structural invariant of an entry owner. This is the whole of `inv()`,
839    /// and is also used directly by `Child::invariants`.
840    pub open spec fn inv_base(self) -> bool {
841        &&& self.is_node() ==> {
842            &&& self.node().inv()
843            &&& self.parent_level == self.node().level + 1
844        }
845        &&& self.is_frame() ==> {
846            // Architectural constraint: frames only exist at PT levels that the
847            // ISA actually supports as leaves (4K, 2M, 1G on x86). `parent_level
848            // == NR_LEVELS` would be a 512 GiB huge page, which no current arch
849            // permits — and `Mapping::inv` would reject its page_size.
850            &&& 1 <= self.parent_level < NR_LEVELS
851            &&& valid_frame_paddr(self.frame().mapped_pa)
852            &&& self.frame().mapped_pa % page_size(self.parent_level) == 0
853            &&& self.frame().mapped_pa + page_size(self.parent_level) <= MAX_PADDR
854            &&& C::raw_item_well_formed(
855                self.frame().mapped_pa,
856                self.parent_level,
857                self.frame().prop,
858            )
859            &&& C::E::new_page_req(self.frame().mapped_pa, self.parent_level, self.frame().prop)
860        }
861        &&& self.is_borrowed() ==> { true }
862        &&& self.path.inv()
863    }
864}
865
866impl<C: PageTableConfig> Inv for EntryOwner<C> {
867    open spec fn inv(self) -> bool {
868        self.inv_base()
869    }
870}
871
872impl<C: PageTableConfig> View for EntryOwner<C> {
873    type V = EntryView<C>;
874
875    open spec fn view(&self) -> <Self as View>::V {
876        if self.is_frame() {
877            let frame = self.frame();
878            EntryView::Leaf {
879                leaf: LeafPageTableEntryView {
880                    map_va: vaddr(self.path) as int,
881                    //                    frame_pa: self.base_addr as int,
882                    //                    in_frame_index: self.index as int,
883                    map_to_pa: frame.mapped_pa as int,
884                    level: self.path.len() as u8,
885                    prop: frame.prop,
886                    phantom: PhantomData,
887                },
888            }
889        } else if self.is_node() {
890            let node = self.node();
891            EntryView::Intermediate {
892                node: IntermediatePageTableEntryView {
893                    map_va: vaddr(self.path) as int,
894                    //                    frame_pa: self.base_addr as int,
895                    //                    in_frame_index: self.index as int,
896                    map_to_pa: meta_to_frame(node.meta_vaddr()) as int,
897                    level: self.path.len() as u8,
898                    phantom: PhantomData,
899                },
900            }
901        } else {
902            EntryView::Absent
903        }
904    }
905}
906
907impl<C: PageTableConfig> InvView for EntryOwner<C> {
908    proof fn view_preserves_inv(self) {
909        // `EntryView::inv()` is trivially `true` (the view of an `EntryOwner`
910        // is never inspected outside this trait obligation), so the
911        // postcondition `self.view().inv()` discharges automatically.
912    }
913}
914
915impl<'a, 'rcu, C: PageTableConfig> OwnerOf for Entry<'a, 'rcu, C> {
916    type Owner = EntryOwner<C>;
917
918    open spec fn wf(self, owner: Self::Owner) -> bool {
919        &&& self.idx < NR_ENTRIES
920        &&& owner.match_pte(self.pte, owner.parent_level)
921        &&& valid_frame_paddr(self.pte.paddr())
922    }
923}
924
925} // verus!
ostd/specs/mm/page_table/node/entry_owners.rs

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