ostd/specs/mm/page_table/cursor/
cursor_fn_specs.rs

1use vstd::prelude::*;
2
3use crate::mm::page_table::*;
4use crate::mm::{PagingConstsTrait, Vaddr};
5use crate::specs::arch::mm::{NR_LEVELS, PAGE_SIZE};
6use crate::specs::mm::frame::mapping::frame_to_index;
7use crate::specs::mm::frame::meta_owners::{REF_COUNT_MAX, REF_COUNT_UNUSED, is_mmio_paddr};
8use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
9use crate::specs::mm::page_table::cursor::owners::*;
10use crate::specs::mm::page_table::*;
11use crate::specs::task::InAtomicMode;
12
13use core::ops::Range;
14
15verus! {
16
17// ─── Cursor specs ─────────────────────────────────────────────────────────────
18impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
19    pub open spec fn cursor_new_success_conditions(va: &Range<Vaddr>) -> bool {
20        &&& va.start < va.end
21        &&& va.start % C::BASE_PAGE_SIZE() == 0
22        &&& va.end % C::BASE_PAGE_SIZE() == 0
23        &&& crate::mm::page_table::is_valid_range_spec::<C>(va)
24    }
25
26    pub open spec fn invariants(
27        self,
28        owner: CursorOwner<'rcu, C>,
29        regions: MetaRegionOwners,
30        guards: Guards<'rcu>,
31    ) -> bool {
32        &&& owner.inv()
33        &&& self.inv()
34        &&& self.wf(owner)
35        &&& regions.inv()
36        &&& owner.children_not_locked(guards)
37        &&& owner.nodes_locked(guards)
38        &&& owner.metaregion_sound(regions)
39        &&& !owner.popped_too_high
40    }
41
42    pub open spec fn query_some_condition(self, owner: CursorOwner<'rcu, C>) -> bool {
43        self.model(owner).present()
44    }
45
46    /// Panic condition for [`Self::query`]. `query` diverges *only* via the
47    /// Arc-style refcount-saturation abort when it clones the **specific**
48    /// frame the cursor resolves to. That happens iff:
49    ///  - the cursor is in range (out-of-range returns `Err` *before* any
50    ///    clone — the early `self.va >= barrier_va.end` exit), and
51    ///  - a mapping is present at the cursor (`owner@.present()`), and
52    ///  - the resolved leaf frame is tracked (non-MMIO, so cloning it bumps
53    ///    its slot's refcount — MMIO/untracked leaves never bump), and
54    ///  - that slot's refcount is already at `REF_COUNT_MAX`, so the
55    ///    `inc_ref_count` in `clone_item` would overflow and abort.
56    /// `owner@.query_mapping().pa_range.start` is exactly the paddr the
57    /// descent lands on (bridged by [`CursorOwner::cur_entry_frame_present`]).
58    pub open spec fn query_panic_condition(
59        self,
60        owner: CursorOwner<'rcu, C>,
61        regions: MetaRegionOwners,
62    ) -> bool {
63        let pa = owner@.query_mapping().pa_range.start;
64        let idx = frame_to_index(pa);
65        &&& self.barrier_va.start <= self.va < self.barrier_va.end
66        &&& owner@.present()
67        &&& !is_mmio_paddr(pa)
68        &&& regions.slot_owners[idx].inner_perms.ref_count.value() >= REF_COUNT_MAX
69    }
70
71    pub open spec fn query_some_ensures(
72        self,
73        owner: CursorOwner<'rcu, C>,
74        res: PagesState<C>,
75    ) -> bool {
76        &&& owner.cur_va_range().start.reflect(res.0.start)
77        &&& owner.cur_va_range().end.reflect(res.0.end)
78        &&& res.1 is Some
79        &&& {
80            let qr = owner@.query_range();
81            owner@.query_item_spec(res.1.unwrap()) == Some(qr.start as Vaddr..qr.end as Vaddr)
82        }
83    }
84
85    pub open spec fn query_none_ensures(
86        self,
87        owner: CursorOwner<'rcu, C>,
88        res: PagesState<C>,
89    ) -> bool {
90        &&& res.1 is None
91    }
92
93    /// Whether the level-`lv` node around the cursor's own VA contains `va`
94    /// — exactly the per-iteration test in `jump`'s loop
95    /// (`node_start <= va && va - node_start < node_size`, with
96    /// `node_start == nat_align_down(self.va, page_size(lv + 1))` and
97    /// `node_size == page_size(lv + 1)`).
98    pub open spec fn jump_node_holds(self, lv: PagingLevel, va: Vaddr) -> bool {
99        let nstart = nat_align_down(self.va as nat, page_size((lv + 1) as PagingLevel) as nat);
100        &&& nstart <= va as nat
101        &&& (va as nat) - nstart < page_size((lv + 1) as PagingLevel) as nat
102    }
103
104    /// Structural (reachability) panic condition for `jump`: it diverges on a
105    /// misaligned `va` (the `assert_eq!`), or when `va` is in the barrier
106    /// range but **no** node on the ascending path within the guard levels
107    /// `[level, guard_level]` contains it — exactly the case where the loop
108    /// never finds `va`, pops above the guard, and hits `pop_level`'s
109    /// `None`-slot unwrap. (An out-of-range `va` returns `Err`, no panic.)
110    /// This mirrors the loop's own search, so it neither over- nor
111    /// under-approximates: an out-of-locked-range cursor that *can* still
112    /// reach `va` via a shared ancestor node does **not** satisfy it.
113    pub open spec fn jump_panic_condition(self, va: Vaddr) -> bool {
114        ||| va % PAGE_SIZE != 0
115        ||| (self.barrier_va.start <= va < self.barrier_va.end && forall|lv: PagingLevel|
116            #![trigger self.jump_node_holds(lv, va)]
117            self.level <= lv <= self.guard_level ==> !self.jump_node_holds(lv, va))
118    }
119
120    pub open spec fn find_next_panic_condition(self, len: usize) -> bool {
121        ||| len % PAGE_SIZE != 0
122        ||| self.va + len > self.barrier_va.end
123    }
124}
125
126// ─── CursorMut specs ──────────────────────────────────────────────────────────
127impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
128    // TODO: trace the `level >= guard_level` panic to its actual location in `pop_level`
129    // (unwrap of None path entry). The lock treatment of the invariant has now been
130    // fixed (`Cursor::wf` and `CursorOwner::nodes_locked` are gated on `guard_level`
131    // rather than hardcoding `NR_LEVELS`, so `path[i]`/continuations above
132    // `guard_level` are unlocked/`None`), which is the prerequisite for expressing
133    // the `level >= guard_level` pop as a precondition violation. What remains is
134    // routing that `path[level-1] is None` fact into `pop_level`'s panic precondition.
135    pub open spec fn map_panic_conditions(self, item: C::Item) -> bool {
136        ||| self.0.va >= self.0.barrier_va.end
137        ||| C::item_into_raw(item).1 > C::HIGHEST_TRANSLATION_LEVEL()
138        ||| C::item_into_raw(item).1 >= self.0.guard_level
139        ||| (!C::TOP_LEVEL_CAN_UNMAP_spec() && C::item_into_raw(item).1 >= NR_LEVELS)
140        ||| self.0.va % page_size(C::item_into_raw(item).1) != 0
141        ||| self.0.va + page_size(C::item_into_raw(item).1) > self.0.barrier_va.end
142    }
143
144    // TODO: ideally this should be an `OwnerOf` impl for `C::Item`
145    pub open spec fn item_wf(self, item: C::Item, entry_owner: EntryOwner<C>) -> bool {
146        let (paddr, level, prop) = C::item_into_raw(item);
147        &&& entry_owner.inv()
148        &&& (entry_owner.is_absent() || Child::Frame(paddr, level, prop).wf(entry_owner))
149    }
150
151    pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
152        let (pa, level, prop) = C::item_into_raw(item);
153        let size = page_size(level);
154        let range = pa..(pa + size) as usize;
155        regions.paddr_range_not_mapped(range)
156    }
157
158    pub open spec fn item_slot_in_regions(item: C::Item, regions: MetaRegionOwners) -> bool {
159        let (pa, level, prop) = C::item_into_raw(item);
160        let idx = frame_to_index(pa);
161        &&& regions.slots.contains_key(idx)
162        &&& regions.slot_owners[idx].inner_perms.ref_count.value()
163            != REF_COUNT_UNUSED
164        // Tracked items hold a refcount; untracked (MMIO) don't.
165        &&& C::tracked(item) ==> regions.slot_owners[idx].inner_perms.ref_count.value()
166            > 0
167        // Sub-page slot existence for huge frames (unconditional). Rc parts gated on tracked.
168        &&& level > 1 ==> {
169            forall|j: usize|
170                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
171                0 < j < page_size(level) / PAGE_SIZE ==> {
172                    let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
173                    &&& regions.slots.contains_key(sub_idx)
174                    &&& C::tracked(item)
175                        ==> regions.slot_owners[sub_idx].inner_perms.ref_count.value()
176                        != REF_COUNT_UNUSED
177                    &&& C::tracked(item)
178                        ==> regions.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
179                }
180        }
181    }
182
183    pub open spec fn map_item_ensures(
184        self,
185        item: C::Item,
186        old_view: CursorView<C>,
187        new_view: CursorView<C>,
188    ) -> bool {
189        let (pa, level, prop) = C::item_into_raw(item);
190        new_view == old_view.map_spec(pa, page_size(level), prop)
191    }
192}
193
194} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs

ostd/specs/mm/page_table/cursor/
cursor_fn_specs.rs
