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

1use vstd::prelude::*;
2
3use crate::specs::{
4    arch::{NR_LEVELS, PAGE_SIZE},
5    mm::{
6        frame::{
7            mapping::frame_to_index,
8            meta_owners::{PageUsage, is_mmio_paddr},
9            meta_region_owners::MetaRegionOwners,
10        },
11        page_table::{cursor::owners::*, is_valid_range_spec, *},
12    },
13    task::InAtomicMode,
14};
15
16use crate::arch::mm::PagingConsts;
17use crate::mm::{
18    PagingConstsTrait, Vaddr,
19    frame::meta::{REF_COUNT_MAX, REF_COUNT_UNUSED},
20    page_table::*,
21};
22use core::ops::Range;
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,
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::lemma_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.ref_count(idx) >= 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() == res.0
86        &&& res.1 is Some
87        &&& {
88            let qr = owner@.query_range();
89            owner@.query_item_spec(res.1->0) == Some(qr.start as Vaddr..qr.end as Vaddr)
90        }
91    }
92
93    pub open spec fn query_none_ensures(
94        self,
95        owner: CursorOwner<'rcu, C>,
96        res: PagesState<C>,
97    ) -> bool {
98        &&& res.1 is None
99    }
100
101    /// Whether the level-`lv` node around the cursor's own VA contains `va`
102    /// — exactly the per-iteration test in `jump`'s loop
103    /// (`node_start <= va && va - node_start < node_size`, with
104    /// `node_start == nat_align_down(self.va, page_size(lv + 1))` and
105    /// `node_size == page_size(lv + 1)`).
106    pub open spec fn jump_node_holds(self, lv: PagingLevel, va: Vaddr) -> bool {
107        let nstart = nat_align_down(
108            self.va as nat,
109            page_size::<PagingConsts>((lv + 1) as PagingLevel) as nat,
110        );
111        &&& nstart <= va as nat
112        &&& (va as nat) - nstart < page_size::<PagingConsts>((lv + 1) as PagingLevel) as nat
113    }
114
115    /// Structural (reachability) panic condition for `jump`: it diverges on a
116    /// misaligned `va` (the `assert_eq!`), or when `va` is in the barrier
117    /// range but **no** node on the ascending path within the guard levels
118    /// `[level, guard_level]` contains it — exactly the case where the loop
119    /// never finds `va`, pops above the guard, and hits `pop_level`'s
120    /// `None`-slot unwrap. (An out-of-range `va` returns `Err`, no panic.)
121    /// This mirrors the loop's own search, so it neither over- nor
122    /// under-approximates: an out-of-locked-range cursor that *can* still
123    /// reach `va` via a shared ancestor node does **not** satisfy it.
124    pub open spec fn jump_panic_condition(self, va: Vaddr) -> bool {
125        ||| va % PAGE_SIZE != 0
126        ||| (self.barrier_va.start <= va < self.barrier_va.end && forall|lv: PagingLevel|
127            #![trigger self.jump_node_holds(lv, va)]
128            self.level <= lv <= self.guard_level ==> !self.jump_node_holds(lv, va))
129    }
130
131    pub open spec fn find_next_panic_condition(self, len: usize) -> bool {
132        ||| len % PAGE_SIZE != 0
133        ||| self.va + len > self.barrier_va.end
134    }
135}
136
137// ─── CursorMut specs ──────────────────────────────────────────────────────────
138impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
139    // TODO: trace the `level >= guard_level` panic to its actual location in `pop_level`
140    // (unwrap of None path entry). The lock treatment of the invariant has now been
141    // fixed (`Cursor::wf` and `CursorOwner::nodes_locked` are gated on `guard_level`
142    // rather than hardcoding `NR_LEVELS`, so `path[i]`/continuations above
143    // `guard_level` are unlocked/`None`), which is the prerequisite for expressing
144    // the `level >= guard_level` pop as a precondition violation. What remains is
145    // routing that `path[level-1] is None` fact into `pop_level`'s panic precondition.
146    pub open spec fn map_panic_conditions(self, item: C::Item) -> bool {
147        ||| self.0.va >= self.0.barrier_va.end
148        ||| C::item_into_raw(item).1 > C::HIGHEST_TRANSLATION_LEVEL()
149        ||| C::item_into_raw(item).1 >= self.0.guard_level
150        ||| (!C::TOP_LEVEL_CAN_UNMAP_spec() && C::item_into_raw(item).1 >= NR_LEVELS)
151        ||| self.0.va % page_size::<PagingConsts>(C::item_into_raw(item).1) != 0
152        ||| self.0.va + page_size::<PagingConsts>(C::item_into_raw(item).1) > self.0.barrier_va.end
153    }
154
155    // TODO: ideally this should be an `OwnerOf` impl for `C::Item`
156    pub open spec fn item_wf(self, item: C::Item, entry_owner: EntryOwner<C>) -> bool {
157        let (paddr, level, prop, _perm) = C::item_into_raw(item);
158        &&& C::item_well_formed(item)
159        &&& entry_owner.inv()
160        &&& (entry_owner.is_absent() || Child::Frame(paddr, level, prop).wf(entry_owner))
161    }
162
163    pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
164        let (pa, level, prop, perm) = C::item_into_raw(item);
165        let size = page_size::<PagingConsts>(level);
166        let range = pa..(pa + size) as usize;
167        regions.paddr_range_not_mapped(range)
168    }
169
170    pub open spec fn item_slot_in_regions_except_perm(
171        item: C::Item,
172        regions: MetaRegionOwners,
173    ) -> bool {
174        let (pa, level, prop, perm) = C::item_into_raw(item);
175        let idx = frame_to_index(pa);
176        &&& regions.contains(idx)
177        &&& regions.slot_owners[idx].usage !is PageTable
178        &&& regions.ref_count(idx)
179            != REF_COUNT_UNUSED
180        // Tracked items hold a refcount; untracked (MMIO) don't.
181        &&& perm@ is Some ==> regions.ref_count(idx)
182            > 0
183        // A tracked (mapped) item is a SHARED frame, never the UNIQUE sentinel:
184        // `rc <= MAX < REF_COUNT_UNIQUE`. Carries the bound into the mapped
185        // slot's `metaregion_sound`, keeping the UNIQUE-branch `paths_in_pt`
186        // inv clause vacuous.
187        &&& perm@ is Some ==> regions.ref_count(idx)
188            <= REF_COUNT_MAX
189        // Sub-page slot existence for huge frames (unconditional). Rc parts gated on tracked.
190        &&& level > 1 ==> {
191            forall|j: usize|
192                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
193                0 < j < page_size::<PagingConsts>(level) / PAGE_SIZE ==> {
194                    let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
195                    &&& regions.contains(sub_idx)
196                    &&& perm@ is Some ==> regions.ref_count(sub_idx) != REF_COUNT_UNUSED
197                    &&& perm@ is Some ==> regions.ref_count(sub_idx)
198                        > 0
199                    // SHARED upper bound for tracked sub-pages — carries `rc <= MAX`
200                    // into the mapped huge frame's `frame_sub_pages_valid`.
201                    &&& perm@ is Some ==> regions.ref_count(sub_idx) <= REF_COUNT_MAX
202                }
203        }
204    }
205
206    pub closed spec fn item_slot_in_regions(item: C::Item, regions: MetaRegionOwners) -> bool {
207        let (pa, _level, _prop, perm) = C::item_into_raw(item);
208        &&& Self::item_slot_in_regions_except_perm(item, regions)
209        &&& C::perm_well_formed_with_region(pa, perm, regions)
210    }
211
212    pub proof fn item_slot_in_regions_facts(item: C::Item, regions: MetaRegionOwners)
213        requires
214            Self::item_slot_in_regions(item, regions),
215        ensures
216            Self::item_slot_in_regions_except_perm(item, regions),
217            C::perm_well_formed_with_region(
218                C::item_into_raw(item).0,
219                C::item_into_raw(item).3,
220                regions,
221            ),
222    {
223    }
224
225    pub proof fn item_slot_in_regions_preserved(
226        item: C::Item,
227        regions0: MetaRegionOwners,
228        regions1: MetaRegionOwners,
229    )
230        requires
231            Self::item_slot_in_regions(item, regions0),
232            Self::item_slot_in_regions_except_perm(item, regions1),
233            regions0.slots[frame_to_index(C::item_into_raw(item).0)]
234                == regions1.slots[frame_to_index(C::item_into_raw(item).0)],
235            regions0.slot_owners[frame_to_index(C::item_into_raw(item).0)].metadata_perm.id()
236                == regions1.slot_owners[frame_to_index(
237                C::item_into_raw(item).0,
238            )].metadata_perm.id(),
239        ensures
240            Self::item_slot_in_regions(item, regions1),
241    {
242        C::lemma_perm_well_formed_with_region_preserved(
243            C::item_into_raw(item).0,
244            C::item_into_raw(item).3,
245            regions0,
246            regions1,
247        );
248    }
249
250    pub proof fn all_item_slots_preserved(regions0: MetaRegionOwners, regions1: MetaRegionOwners)
251        requires
252            forall|idx: int| regions0.contains(idx) ==> #[trigger] regions1.contains(idx),
253            forall|idx: int|
254                regions0.ref_count(idx) != REF_COUNT_UNUSED ==> #[trigger] regions1.slot_owners[idx]
255                    == regions0.slot_owners[idx],
256            forall|idx: int|
257                regions0.contains(idx) && regions0.ref_count(idx) != REF_COUNT_UNUSED
258                    ==> #[trigger] regions1.slots[idx] == regions0.slots[idx],
259        ensures
260            forall|item: C::Item|
261                #![trigger Self::item_slot_in_regions(item, regions0)]
262                Self::item_slot_in_regions(item, regions0) ==> Self::item_slot_in_regions(
263                    item,
264                    regions1,
265                ),
266    {
267        assert forall|item: C::Item|
268            Self::item_slot_in_regions(
269                item,
270                regions0,
271            ) implies #[trigger] Self::item_slot_in_regions(item, regions1) by {
272            let (pa, level, _prop, perm) = C::item_into_raw(item);
273            let idx = frame_to_index(pa);
274            assert(regions0.ref_count(idx) != REF_COUNT_UNUSED);
275            assert(Self::item_slot_in_regions_except_perm(item, regions1)) by {
276                if level > 1 {
277                    assert forall|j: usize|
278                        #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
279                        0 < j < page_size::<PagingConsts>(level) / PAGE_SIZE implies {
280                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
281                        &&& regions1.contains(sub_idx)
282                        &&& perm@ is Some ==> regions1.ref_count(sub_idx) != REF_COUNT_UNUSED
283                        &&& perm@ is Some ==> regions1.ref_count(sub_idx) > 0
284                        &&& perm@ is Some ==> regions1.ref_count(sub_idx) <= REF_COUNT_MAX
285                    } by {};
286                }
287            };
288            Self::item_slot_in_regions_preserved(item, regions0, regions1);
289        };
290    }
291
292    pub open spec fn map_item_ensures(
293        self,
294        item: C::Item,
295        old_view: CursorView<C>,
296        new_view: CursorView<C>,
297    ) -> bool {
298        let (pa, level, prop, _perm) = C::item_into_raw(item);
299        new_view == old_view.map_spec(pa, page_size::<PagingConsts>(level), prop)
300    }
301}
302
303} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs

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