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

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

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