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

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

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