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

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