ostd/specs/mm/embedding/
cursor.rs

1//! Embedding of `Cursor` / `CursorMut` operations: open, drop,
2//! navigation (query/find_next/jump), and mutation
3//! (map/unmap/protect_next).
4//!
5//! Per-op steps operate on tracked owners directly — no store lookups,
6//! no preconditions on store membership, no `if`-guards. The store-side
7//! extract / insert and id-management lives in
8//! [`super::VmStore`]'s methods and the [`super::lemma_step`] dispatcher.
9//!
10//! # Mirroring exec preconditions
11//!
12//! Each `_embedded` axiom carries the same `requires` as its exec
13//! counterpart, expressed against our model. The expressible parts are:
14//!
15//! - `owner.inv()`, `owner.children_not_locked(guards)`,
16//!   `owner.nodes_locked(guards)`, `!owner.popped_too_high` —
17//!   bundled as `CursorEntry::inv` (entry-side); see [`super::CursorEntry`].
18//! - `owner.in_barrier_va()` — NOT a precondition of `query`, `jump`,
19//!   or `map`: each handles an out-of-range cursor itself (graceful
20//!   `Err` for `query`; a faithful `panic_diverge` otherwise) and
21//!   re-derives `in_barrier_va` internally. `protect_next` still
22//!   requires it; see exec clauses.
23//! - `regions.inv()`, `owner.metaregion_sound(regions)` — passed via
24//!   `&mut regions`.
25//! - `tlb_model.inv()` — passed via `&mut tlb_model` to `map` / `unmap`.
26//!
27//! # Model gaps
28//!
29//! - **Exec `Cursor` handle**: the exec `Cursor::invariants` requires
30//!   `self.inv()` and `self.wf(owner)` over the runtime `Cursor`
31//!   struct. Our embedding doesn't carry that handle (it's tied to the
32//!   `&'rcu RCU guard` reference, not constructible in pure ghost
33//!   mode), so these conjuncts are MODEL GAPS. Owner-side state
34//!   already mirrors handle state (`owner.va`, `owner.level`,
35//!   `owner.guard_level`), so `wf(owner)` is essentially tautological
36//!   if we postulate the handle's existence; `inv()` follows from
37//!   `owner.inv()` plus this projection.
38//! - **`item_wf` on map**: the exec [`crate::mm::vm_space::CursorMut::map`]
39//!   requires `old(self).item_wf(frame, prop, entry_owner, *old(regions))`,
40//!   which constrains a separate `EntryOwner<UserPtConfig>` argument
41//!   produced by cursor traversal. We don't model `EntryOwner` here.
42//! - **`protect_next` closure preconditions**: the exec method takes a
43//!   closure `op: impl FnOnce(PageProperty) -> PageProperty` with
44//!   `forall |p| op.requires((p,))` plus a trackedness-preservation
45//!   constraint. Our `Op::ProtectNext` doesn't carry the closure.
46use vstd::prelude::*;
47use vstd_extra::ownership::*;
48
49use crate::specs::{
50    arch::*,
51    mm::{
52        frame::{
53            mapping::frame_to_index, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners,
54        },
55        page_table::{cursor::owners::CursorOwner, node::Guards},
56        tlb::TlbModel,
57    },
58};
59
60use super::{CursorEntry, CursorKind, VmSpaceId, tracked_cursor_entry_new};
61use crate::mm::{
62    Paddr, Vaddr,
63    frame::{
64        UFrame,
65        meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
66    },
67    page_prop::PageProperty,
68    vm_space::{UserPtConfig, vm_space_specs::VmSpaceOwner},
69};
70use core::ops::Range;
71
72verus! {
73
74// =============================================================================
75// _embedded axioms
76// =============================================================================
77/// Mirror of [`crate::mm::vm_space::VmSpace::cursor`].
78///
79/// The exec method mutates `&mut Guards` (adding locks for the new
80/// cursor) and `&mut MetaRegionOwners`. Here, since each `CursorEntry`
81/// carries its own self-contained `Guards` (a per-cursor model
82/// restriction; see module-level docs), we *return* a fresh `Guards`
83/// alongside the owner instead of mutating a shared one.
84///
85/// The `metaregion_sound_preserves` ensures clause says that any
86/// `CursorOwner` that was sound w.r.t. the old `regions` is still
87/// sound w.r.t. the new `regions`. This mirrors the exec
88/// `PageTable::cursor` ensures that preserves `paths_in_pt` and
89/// non-saturation across all slots ([page_table/mod.rs:1599-1661]).
90pub axiom fn vm_space_cursor_embedded<'a, 'rcu>(
91    tracked vm_space: &VmSpaceOwner,
92    tracked regions: &mut MetaRegionOwners,
93    va: Range<Vaddr>,
94) -> (tracked res: Option<(CursorOwner<'rcu, UserPtConfig>, Guards)>)
95    requires
96        vm_space.inv(),
97        old(regions).inv(),
98    ensures
99        final(regions).inv(),
100        // Page-table cursor ops never touch the metadata slot-perm map
101        // (`slots` is the boot-fixed metadata region) nor the
102        // ManuallyDrop `raw_count` / free-list `in_list` fields; only
103        // `slot_owners` refcount / `paths_in_pt` changes. Preserving the
104        // `slots` domain (#2 / #3b) and `raw_count` / `in_list` (#4
105        // partial) keeps `VmStore::inv`'s coverage clauses chainable
106        // across cursor methods.
107        final(regions).slots == old(regions).slots,
108        forall|i: int|
109            #![trigger final(regions).slot_owners[i]]
110            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
111        forall|i: int|
112            #![trigger final(regions).slot_owners[i]]
113            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
114                &&& old(regions).ref_count(i) == REF_COUNT_UNUSED
115                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
116                &&& final(regions).slot_owners[i].usage !is Frame
117            },
118        forall|c: CursorOwner<'rcu, UserPtConfig>|
119            #![auto]
120            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
121        res matches Some((c, g)) ==> {
122            &&& c.barrier_va == va
123            &&& c.inv()
124            &&& c.children_not_locked(g)
125            &&& c.nodes_locked(g)
126            &&& !c.popped_too_high
127            &&& c.metaregion_sound(*final(regions))
128        },
129;
130
131/// Mirror of [`crate::mm::vm_space::VmSpace::cursor_mut`].
132pub axiom fn vm_space_cursor_mut_embedded<'a, 'rcu>(
133    tracked vm_space: &VmSpaceOwner,
134    tracked regions: &mut MetaRegionOwners,
135    va: Range<Vaddr>,
136) -> (tracked res: Option<(CursorOwner<'rcu, UserPtConfig>, Guards)>)
137    requires
138        vm_space.inv(),
139        old(regions).inv(),
140    ensures
141        final(regions).inv(),
142        // Page-table cursor ops never touch the metadata slot-perm map
143        // (`slots` is the boot-fixed metadata region) nor the
144        // ManuallyDrop `raw_count` / free-list `in_list` fields; only
145        // `slot_owners` refcount / `paths_in_pt` changes. Preserving the
146        // `slots` domain (#2 / #3b) and `raw_count` / `in_list` (#4
147        // partial) keeps `VmStore::inv`'s coverage clauses chainable
148        // across cursor methods.
149        final(regions).slots == old(regions).slots,
150        forall|i: int|
151            #![trigger final(regions).slot_owners[i]]
152            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
153        forall|i: int|
154            #![trigger final(regions).slot_owners[i]]
155            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
156                &&& old(regions).ref_count(i) == REF_COUNT_UNUSED
157                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
158                &&& final(regions).slot_owners[i].usage !is Frame
159            },
160        forall|c: CursorOwner<'rcu, UserPtConfig>|
161            #![auto]
162            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
163        res matches Some((c, g)) ==> {
164            &&& c.barrier_va == va
165            &&& c.inv()
166            &&& c.children_not_locked(g)
167            &&& c.nodes_locked(g)
168            &&& !c.popped_too_high
169            &&& c.metaregion_sound(*final(regions))
170        },
171;
172
173/// Mirror of [`crate::mm::vm_space::Cursor::query`] /
174/// [`crate::mm::vm_space::CursorMut::query`].
175///
176/// Exec requires `invariants(owner, regions, guards)`. It does **not**
177/// require `owner.in_barrier_va()`: an out-of-range cursor is handled
178/// by `Cursor::query`'s graceful `Err` (the exec `requires` was relaxed
179/// accordingly; `in_barrier_va` now only governs success, not safety).
180///
181/// `metaregion_sound_preserves`: a `CursorOwner` that was sound w.r.t.
182/// the old `regions` is still sound w.r.t. the new `regions`. This
183/// keeps `VmStore::inv` chainable across method calls that touch
184/// regions.
185///
186/// **Result `Some(paddr)` / `None`.** Exec `query` returns
187/// `(Range<Vaddr>, Option<MappedItem>)`. When the inner `Option` is
188/// `Some(item)` and the item is *tracked* (non-MMIO), exec
189/// `clone_item` bumps `rc` at the leaf slot by one. The returned
190/// `Paddr` here is the cloned leaf's physical address (i.e. the
191/// new handle the caller now logically owns); the embedding's
192/// [`super::lemma_step_query`] registers a fresh [`FrameEntry`] at that paddr
193/// to keep `accounting_inv`'s `rc == H + P` chained. `None` covers
194/// three cases: query returned `Err` (out of range), query returned
195/// `Ok(_, None)` (cursor not at a leaf), or query returned a `Some`
196/// non-tracked (MMIO) item (`clone_item` is a no-op for those).
197/// In all three `None` subcases `slot_owners` is fully preserved.
198pub axiom fn cursor_query_embedded<'rcu>(
199    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
200    tracked regions: &mut MetaRegionOwners,
201    tracked guards: &mut Guards,
202) -> (res: Option<Paddr>)
203    requires
204        old(owner).inv(),
205        old(regions).inv(),
206        old(owner).children_not_locked(*old(guards)),
207        old(owner).nodes_locked(*old(guards)),
208        old(owner).metaregion_sound(*old(regions)),
209        !old(owner).popped_too_high,
210    ensures
211        final(owner).inv(),
212        final(owner).barrier_va == old(owner).barrier_va,
213        final(regions).inv(),
214        final(owner).children_not_locked(*final(guards)),
215        final(owner).nodes_locked(*final(guards)),
216        final(owner).metaregion_sound(*final(regions)),
217        !final(owner).popped_too_high,
218        final(regions).slots == old(regions).slots,
219        res is None ==> forall|i: int|
220            #![trigger final(regions).slot_owners[i]]
221            final(regions).slot_owners[i] == old(regions).slot_owners[i],
222        res matches Some(paddr) ==> {
223            &&& old(owner).in_barrier_va()
224            &&& valid_frame_paddr(paddr)
225            &&& old(regions).slot_owner(paddr).usage is Frame
226            &&& final(regions).slot_owner(paddr).ref_count() == (old(regions).slot_owner(
227                paddr,
228            ).ref_count() + 1) as nat
229            &&& final(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX
230            &&& forall|i: int|
231                #![trigger final(regions).slot_owners[i]]
232                i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
233                    regions,
234                ).slot_owners[i]
235            &&& final(regions).slot_owner(paddr).slot_vaddr == old(regions).slot_owner(
236                paddr,
237            ).slot_vaddr
238            &&& final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage
239            &&& final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(
240                paddr,
241            ).paths_in_pt
242            &&& final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
243                paddr,
244            ).in_list_perm
245            &&& final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
246                paddr,
247            ).storage_perm()
248            &&& final(regions).slot_owner(paddr).vtable_ptr_perm() == old(regions).slot_owner(
249                paddr,
250            ).vtable_ptr_perm()
251        },
252        forall|c: CursorOwner<'rcu, UserPtConfig>|
253            #![auto]
254            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
255;
256
257/// Mirror of [`crate::mm::vm_space::Cursor::jump`] /
258/// [`crate::mm::vm_space::CursorMut::jump`].
259///
260/// Exec requires `invariants(owner, regions, guards)` (which includes
261/// `!owner.popped_too_high`). It does **not** require
262/// `owner.in_barrier_va()`: the exec `requires` was relaxed. A drifted
263/// cursor that cannot be repositioned within the target node aborts the
264/// program (a sound `panic_diverge`, mirroring the real `pop_level`
265/// `unwrap` panic), so an out-of-range cursor is a safety non-issue —
266/// `in_barrier_va` now only governs the success postcondition, and
267/// this proof soundly models the returning path.
268pub proof fn lemma_cursor_jump_embedded<'rcu>(
269    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
270    tracked regions: &mut MetaRegionOwners,
271    tracked guards: &mut Guards,
272    va: Vaddr,
273)
274    requires
275        old(owner).inv(),
276        old(regions).inv(),
277        old(owner).children_not_locked(*old(guards)),
278        old(owner).nodes_locked(*old(guards)),
279        old(owner).metaregion_sound(*old(regions)),
280        !old(owner).popped_too_high,
281    ensures
282        final(owner).inv(),
283        final(owner).barrier_va == old(owner).barrier_va,
284        final(regions).inv(),
285        final(owner).children_not_locked(*final(guards)),
286        final(owner).nodes_locked(*final(guards)),
287        final(owner).metaregion_sound(*final(regions)),
288        !final(owner).popped_too_high,
289        // `jump` repositions the cursor but touches no frame slot — no
290        // PTE writes, no leaf clone. Full `slot_owners` preservation,
291        // same shape as `find_next`.
292        final(regions).slots == old(regions).slots,
293        forall|i: int|
294            #![trigger final(regions).slot_owners[i]]
295            final(regions).slot_owners[i] == old(regions).slot_owners[i],
296        forall|c: CursorOwner<'rcu, UserPtConfig>|
297            #![auto]
298            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
299{
300}
301
302/// Mirror of [`crate::mm::vm_space::CursorMut::map`].
303pub axiom fn cursor_mut_map_embedded<'rcu>(
304    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
305    tracked regions: &mut MetaRegionOwners,
306    tracked guards: &mut Guards,
307    tracked tlb_model: &mut TlbModel,
308    paddr: Paddr,
309    prop: PageProperty,
310)
311    requires
312        old(owner).inv(),
313        old(regions).inv(),
314        old(owner).children_not_locked(*old(guards)),
315        old(owner).nodes_locked(*old(guards)),
316        old(owner).metaregion_sound(*old(regions)),
317        !old(owner).popped_too_high,
318        old(tlb_model).inv(),
319        // The mapped paddr is page-aligned and in-bounds (these come
320        // from a consumed `FrameEntry`'s paddr; `valid_frame_paddr` is
321        // guaranteed by the embedding's structural_inv `frames` clause).
322        valid_frame_paddr(
323            paddr,
324        ),
325// MODEL GAP: `item_wf(frame, prop, entry_owner, regions)`
326// depends on a separate `EntryOwner<UserPtConfig>` arg we don't
327// model. The exec call assumes the caller supplies one.
328
329    ensures
330        final(owner).inv(),
331        final(owner).barrier_va == old(owner).barrier_va,
332        final(regions).inv(),
333        final(owner).children_not_locked(*final(guards)),
334        final(owner).nodes_locked(*final(guards)),
335        final(owner).metaregion_sound(*final(regions)),
336        !final(owner).popped_too_high,
337        final(tlb_model).inv(),
338        final(regions).slots == old(regions).slots,
339        forall|i: int|
340            #![trigger final(regions).slot_owners[i]]
341            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
342        forall|i: int|
343            #![trigger final(regions).slot_owners[i]]
344            i != frame_to_index(paddr) && old(regions).ref_count(i) != REF_COUNT_UNUSED
345                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
346        forall|i: int|
347            #![trigger final(regions).slot_owners[i].ref_count()]
348            old(regions).ref_count(i) != REF_COUNT_UNUSED ==> final(regions).ref_count(i)
349                != REF_COUNT_UNUSED,
350        // **`ref_count` PRESERVED at the mapped slot.
351        final(regions).slot_owner(paddr).ref_count() == old(regions).slot_owner(paddr).ref_count(),
352        // **`paths_in_pt.len() += 1` at the mapped slot.**
353        final(regions).slot_owner(paddr).paths_in_pt.len() == old(regions).slot_owner(
354            paddr,
355        ).paths_in_pt.len() + 1,
356        final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
357        final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
358            paddr,
359        ).storage_perm(),
360        // Slots that stay UNUSED are fully preserved.
361        forall|i: int|
362            #![trigger final(regions).slot_owners[i]]
363            final(regions).ref_count(i) == REF_COUNT_UNUSED ==> final(regions).slot_owners[i]
364                == old(regions).slot_owners[i],
365        forall|i: int|
366            #![trigger final(regions).slot_owners[i]]
367            i != frame_to_index(paddr) && old(regions).ref_count(i) == REF_COUNT_UNUSED
368                && final(regions).ref_count(i) != REF_COUNT_UNUSED
369                ==> final(regions).slot_owners[i].usage !is Frame,
370        forall|c: CursorOwner<'rcu, UserPtConfig>|
371            #![auto]
372            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
373;
374
375/// Mirror of [`crate::mm::vm_space::CursorMut::unmap`].
376pub axiom fn cursor_mut_unmap_embedded<'rcu>(
377    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
378    tracked regions: &mut MetaRegionOwners,
379    tracked guards: &mut Guards,
380    tracked tlb_model: &mut TlbModel,
381    len: usize,
382)
383    requires
384        old(owner).inv(),
385        old(regions).inv(),
386        old(owner).children_not_locked(*old(guards)),
387        old(owner).nodes_locked(*old(guards)),
388        old(owner).metaregion_sound(*old(regions)),
389        !old(owner).popped_too_high,
390        old(tlb_model).inv(),
391    ensures
392        final(owner).inv(),
393        final(owner).barrier_va == old(owner).barrier_va,
394        final(regions).inv(),
395        final(owner).children_not_locked(*final(guards)),
396        final(owner).nodes_locked(*final(guards)),
397        final(owner).metaregion_sound(*final(regions)),
398        !final(owner).popped_too_high,
399        final(tlb_model).inv(),
400        final(regions).slots == old(regions).slots,
401        forall|i: int|
402            #![trigger final(regions).slot_owners[i]]
403            {
404                &&& final(regions).slot_owners[i].slot_vaddr == old(
405                    regions,
406                ).slot_owners[i].slot_vaddr
407                &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
408                &&& final(regions).slot_owners[i].in_list_perm == old(
409                    regions,
410                ).slot_owners[i].in_list_perm
411                &&& final(regions).slot_owners[i].vtable_ptr_perm() == old(
412                    regions,
413                ).slot_owners[i].vtable_ptr_perm()
414                // `rc` doesn't bump to UNIQUE.
415                &&& old(regions).ref_count(i) != REF_COUNT_UNIQUE ==> final(regions).ref_count(i)
416                    != REF_COUNT_UNIQUE
417                // Storage preserved at slots that end non-UNUSED.
418                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
419                    ==> final(regions).slot_owners[i].storage_perm() == old(
420                    regions,
421                ).slot_owners[i].storage_perm()
422            },
423        // Unparked (page-table-node) slots are untouched.
424        forall|i: int|
425            #![trigger final(regions).slot_owners[i]]
426            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
427                regions,
428            ).slot_owners[i],
429        forall|i: int|
430            #![trigger final(regions).slot_owners[i]]
431            old(regions).slot_owners[i].usage is Frame ==> {
432                &&& final(regions).ref_count(i) + old(regions).slot_owners[i].paths_in_pt.len()
433                    == old(regions).ref_count(i) + final(regions).slot_owners[i].paths_in_pt.len()
434                &&& final(regions).ref_count(i) <= old(regions).ref_count(i)
435                &&& final(regions).slot_owners[i].paths_in_pt.len() <= old(
436                    regions,
437                ).slot_owners[i].paths_in_pt.len()
438                &&& final(regions).ref_count(i) != 0
439            },
440        forall|c: CursorOwner<'rcu, UserPtConfig>|
441            #![auto]
442            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
443;
444
445// =============================================================================
446// dispatch tags + step proofs
447// =============================================================================
448/// Internal: dispatch tag for cursor methods that also touch
449/// `MetaRegionOwners` and `TlbModel`. `Map` is handled via its own
450/// [`map_step`].
451pub enum CursorMutRegionsMethod {
452    Unmap(usize),
453}
454
455/// Per-op step for `Op::OpenCursor`.
456pub(super) proof fn open_cursor_step<'a, 'rcu>(
457    tracked vm_space: &VmSpaceOwner,
458    tracked regions: &mut MetaRegionOwners,
459    vs: VmSpaceId,
460    va: Range<Vaddr>,
461) -> (tracked res: Option<CursorEntry<'rcu>>)
462    requires
463        vm_space.inv(),
464        old(regions).inv(),
465    ensures
466        final(regions).inv(),
467        final(regions).slots == old(regions).slots,
468        forall|i: int|
469            #![trigger final(regions).slot_owners[i]]
470            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
471        forall|i: int|
472            #![trigger final(regions).slot_owners[i]]
473            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
474                &&& old(regions).ref_count(i) == REF_COUNT_UNUSED
475                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
476                &&& final(regions).slot_owners[i].usage !is Frame
477            },
478        forall|c: CursorOwner<'rcu, UserPtConfig>|
479            #![auto]
480            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
481        res matches Some(e) ==> e.inv(),
482        res matches Some(e) ==> e.owner.metaregion_sound(*final(regions)),
483        res matches Some(e) ==> e.kind == CursorKind::ReadOnly,
484        res matches Some(e) ==> e.va == va,
485        res matches Some(e) ==> e.vm_space == vs,
486{
487    let tracked owner_opt = vm_space_cursor_embedded(vm_space, regions, va);
488    match owner_opt {
489        Option::Some((owner, guards)) => {
490            let tracked entry = tracked_cursor_entry_new(
491                vs,
492                CursorKind::ReadOnly,
493                va,
494                owner,
495                guards,
496            );
497            Option::Some(entry)
498        },
499        Option::None => Option::None,
500    }
501}
502
503/// Per-op step for `Op::OpenCursorMut`.
504pub(super) proof fn open_cursor_mut_step<'a, 'rcu>(
505    tracked vm_space: &VmSpaceOwner,
506    tracked regions: &mut MetaRegionOwners,
507    vs: VmSpaceId,
508    va: Range<Vaddr>,
509) -> (tracked res: Option<CursorEntry<'rcu>>)
510    requires
511        vm_space.inv(),
512        old(regions).inv(),
513    ensures
514        final(regions).inv(),
515        final(regions).slots == old(regions).slots,
516        forall|i: int|
517            #![trigger final(regions).slot_owners[i]]
518            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
519        forall|i: int|
520            #![trigger final(regions).slot_owners[i]]
521            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
522                &&& old(regions).ref_count(i) == REF_COUNT_UNUSED
523                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
524                &&& final(regions).slot_owners[i].usage !is Frame
525            },
526        forall|c: CursorOwner<'rcu, UserPtConfig>|
527            #![auto]
528            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
529        res matches Some(e) ==> e.inv(),
530        res matches Some(e) ==> e.owner.metaregion_sound(*final(regions)),
531        res matches Some(e) ==> e.kind == CursorKind::Mutable,
532        res matches Some(e) ==> e.va == va,
533        res matches Some(e) ==> e.vm_space == vs,
534{
535    let tracked owner_opt = vm_space_cursor_mut_embedded(vm_space, regions, va);
536    match owner_opt {
537        Option::Some((owner, guards)) => {
538            let tracked entry = tracked_cursor_entry_new(
539                vs,
540                CursorKind::Mutable,
541                va,
542                owner,
543                guards,
544            );
545            Option::Some(entry)
546        },
547        Option::None => Option::None,
548    }
549}
550
551/// Per-op step for `Op::DropCursor`. The caller has already extracted
552/// the entry from the store; this function drops it.
553pub(super) proof fn drop_cursor_step<'rcu>(tracked _entry: CursorEntry<'rcu>) {
554}
555
556pub(super) proof fn cursor_query_step<'rcu>(
557    tracked entry: &mut CursorEntry<'rcu>,
558    tracked regions: &mut MetaRegionOwners,
559) -> (res: Option<Paddr>)
560    requires
561        old(entry).inv(),
562        old(regions).inv(),
563        old(entry).owner.metaregion_sound(*old(regions)),
564    ensures
565        final(entry).vm_space == old(entry).vm_space,
566        final(entry).kind == old(entry).kind,
567        final(entry).va == old(entry).va,
568        final(entry).inv(),
569        final(regions).inv(),
570        final(entry).owner.metaregion_sound(*final(regions)),
571        final(regions).slots == old(regions).slots,
572        res is None ==> forall|i: int|
573            #![trigger final(regions).slot_owners[i]]
574            final(regions).slot_owners[i] == old(regions).slot_owners[i],
575        res matches Some(paddr) ==> {
576            &&& old(entry).owner.in_barrier_va()
577            &&& valid_frame_paddr(paddr)
578            &&& old(regions).slot_owner(paddr).usage is Frame
579            &&& final(regions).slot_owner(paddr).ref_count() == (old(regions).slot_owner(
580                paddr,
581            ).ref_count() + 1) as nat
582            &&& final(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX
583            &&& forall|i: int|
584                #![trigger final(regions).slot_owners[i]]
585                i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
586                    regions,
587                ).slot_owners[i]
588            &&& final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage
589            &&& final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(
590                paddr,
591            ).paths_in_pt
592            &&& final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
593                paddr,
594            ).in_list_perm
595            &&& final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
596                paddr,
597            ).storage_perm()
598        },
599        forall|c: CursorOwner<'rcu, UserPtConfig>|
600            #![auto]
601            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
602{
603    cursor_query_embedded(&mut entry.owner, regions, &mut entry.guards)
604}
605
606/// Per-op step for `Op::FindNext`. Navigates the cursor forward
607/// without touching any frame slot — full `slot_owners` preservation.
608pub(super) proof fn cursor_find_next_step<'rcu>(
609    tracked entry: &mut CursorEntry<'rcu>,
610    tracked regions: &mut MetaRegionOwners,
611    len: usize,
612)
613    requires
614        old(entry).inv(),
615        old(regions).inv(),
616        old(entry).owner.metaregion_sound(*old(regions)),
617    ensures
618        final(entry).vm_space == old(entry).vm_space,
619        final(entry).kind == old(entry).kind,
620        final(entry).va == old(entry).va,
621        final(entry).inv(),
622        final(regions).inv(),
623        final(entry).owner.metaregion_sound(*final(regions)),
624        final(regions).slots == old(regions).slots,
625        // Full `slot_owners` preservation — `find_next` writes no PTE
626        // and clones no leaf.
627        forall|i: int|
628            #![trigger final(regions).slot_owners[i]]
629            final(regions).slot_owners[i] == old(regions).slot_owners[i],
630        forall|c: CursorOwner<'rcu, UserPtConfig>|
631            #![auto]
632            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
633{
634}
635
636/// Per-op step for `Op::Jump`. Repositions the cursor without
637/// touching any frame slot — full `slot_owners` preservation.
638pub(super) proof fn cursor_jump_step<'rcu>(
639    tracked entry: &mut CursorEntry<'rcu>,
640    tracked regions: &mut MetaRegionOwners,
641    va: Vaddr,
642)
643    requires
644        old(entry).inv(),
645        old(regions).inv(),
646        old(entry).owner.metaregion_sound(*old(regions)),
647    ensures
648        final(entry).vm_space == old(entry).vm_space,
649        final(entry).kind == old(entry).kind,
650        final(entry).va == old(entry).va,
651        final(entry).inv(),
652        final(regions).inv(),
653        final(entry).owner.metaregion_sound(*final(regions)),
654        final(regions).slots == old(regions).slots,
655        forall|i: int|
656            #![trigger final(regions).slot_owners[i]]
657            final(regions).slot_owners[i] == old(regions).slot_owners[i],
658        forall|c: CursorOwner<'rcu, UserPtConfig>|
659            #![auto]
660            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
661{
662    lemma_cursor_jump_embedded(&mut entry.owner, regions, &mut entry.guards, va)
663}
664
665/// Per-op step for `Op::ProtectNext`. Rewrites PTE `prop` fields in
666/// place — no `rc` or `paths_in_pt` mutation; full `slot_owners`
667/// preservation.
668pub(super) proof fn cursor_protect_next_step<'rcu>(
669    tracked entry: &mut CursorEntry<'rcu>,
670    tracked regions: &mut MetaRegionOwners,
671    len: usize,
672)
673    requires
674        old(entry).inv(),
675        old(regions).inv(),
676        old(entry).owner.metaregion_sound(*old(regions)),
677    ensures
678        final(entry).vm_space == old(entry).vm_space,
679        final(entry).kind == old(entry).kind,
680        final(entry).va == old(entry).va,
681        final(entry).inv(),
682        final(regions).inv(),
683        final(entry).owner.metaregion_sound(*final(regions)),
684        final(regions).slots == old(regions).slots,
685        forall|i: int|
686            #![trigger final(regions).slot_owners[i]]
687            final(regions).slot_owners[i] == old(regions).slot_owners[i],
688        forall|c: CursorOwner<'rcu, UserPtConfig>|
689            #![auto]
690            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
691{
692}
693
694/// Per-op step for cursor methods that mutate the cursor owner,
695/// `MetaRegionOwners`, AND `TlbModel`: `unmap` (and `map`, via
696/// [`map_step`]).
697pub(super) proof fn cursor_mut_regions_step<'rcu>(
698    tracked entry: &mut CursorEntry<'rcu>,
699    tracked regions: &mut MetaRegionOwners,
700    tracked tlb_model: &mut TlbModel,
701    method: CursorMutRegionsMethod,
702)
703    requires
704        old(entry).inv(),
705        old(regions).inv(),
706        old(entry).owner.metaregion_sound(*old(regions)),
707        old(tlb_model).inv(),
708    ensures
709        final(entry).vm_space == old(entry).vm_space,
710        final(entry).kind == old(entry).kind,
711        final(entry).va == old(entry).va,
712        final(entry).inv(),
713        final(regions).inv(),
714        final(entry).owner.metaregion_sound(*final(regions)),
715        final(tlb_model).inv(),
716        final(regions).slots == old(regions).slots,
717        forall|i: int|
718            #![trigger final(regions).slot_owners[i]]
719            {
720                &&& final(regions).slot_owners[i].slot_vaddr == old(
721                    regions,
722                ).slot_owners[i].slot_vaddr
723                &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
724                &&& final(regions).slot_owners[i].in_list_perm == old(
725                    regions,
726                ).slot_owners[i].in_list_perm
727                &&& final(regions).slot_owners[i].vtable_ptr_perm() == old(
728                    regions,
729                ).slot_owners[i].vtable_ptr_perm()
730                &&& old(regions).ref_count(i) != REF_COUNT_UNIQUE ==> final(regions).ref_count(i)
731                    != REF_COUNT_UNIQUE
732                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
733                    ==> final(regions).slot_owners[i].storage_perm() == old(
734                    regions,
735                ).slot_owners[i].storage_perm()
736            },
737        // Unparked (page-table-node) slots untouched (see
738        // `cursor_mut_unmap_embedded`); preserves the coverage exception.
739        forall|i: int|
740            #![trigger final(regions).slot_owners[i]]
741            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
742                regions,
743            ).slot_owners[i],
744        forall|i: int|
745            #![trigger final(regions).slot_owners[i]]
746            old(regions).slot_owners[i].usage is Frame ==> {
747                &&& final(regions).ref_count(i) + old(regions).slot_owners[i].paths_in_pt.len()
748                    == old(regions).ref_count(i) + final(regions).slot_owners[i].paths_in_pt.len()
749                &&& final(regions).ref_count(i) <= old(regions).ref_count(i)
750                &&& final(regions).slot_owners[i].paths_in_pt.len() <= old(
751                    regions,
752                ).slot_owners[i].paths_in_pt.len()
753                &&& final(regions).ref_count(i) != 0
754            },
755        forall|c: CursorOwner<'rcu, UserPtConfig>|
756            #![auto]
757            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
758{
759    match method {
760        CursorMutRegionsMethod::Unmap(len) => {
761            cursor_mut_unmap_embedded(&mut entry.owner, regions, &mut entry.guards, tlb_model, len);
762        },
763    }
764}
765
766/// Per-op step for `Op::Map`.
767pub(super) proof fn map_step<'rcu>(
768    tracked entry: &mut CursorEntry<'rcu>,
769    tracked regions: &mut MetaRegionOwners,
770    tracked tlb_model: &mut TlbModel,
771    paddr: Paddr,
772    prop: PageProperty,
773)
774    requires
775        old(entry).inv(),
776        old(regions).inv(),
777        old(entry).owner.metaregion_sound(*old(regions)),
778        old(tlb_model).inv(),
779        valid_frame_paddr(paddr),
780    ensures
781        final(entry).vm_space == old(entry).vm_space,
782        final(entry).kind == old(entry).kind,
783        final(entry).va == old(entry).va,
784        final(entry).inv(),
785        final(regions).inv(),
786        final(entry).owner.metaregion_sound(*final(regions)),
787        final(tlb_model).inv(),
788        final(regions).slots == old(regions).slots,
789        // Mirror the strengthened `cursor_mut_map_embedded` ensures.
790        forall|i: int|
791            #![trigger final(regions).slot_owners[i]]
792            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
793        forall|i: int|
794            #![trigger final(regions).slot_owners[i]]
795            i != frame_to_index(paddr) && old(regions).ref_count(i) != REF_COUNT_UNUSED
796                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
797        forall|i: int|
798            #![trigger final(regions).slot_owners[i].ref_count()]
799            old(regions).ref_count(i) != REF_COUNT_UNUSED ==> final(regions).ref_count(i)
800                != REF_COUNT_UNUSED,
801        final(regions).slot_owner(paddr).ref_count() == old(regions).slot_owner(paddr).ref_count(),
802        final(regions).slot_owner(paddr).paths_in_pt.len() == old(regions).slot_owner(
803            paddr,
804        ).paths_in_pt.len() + 1,
805        final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
806        final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
807            paddr,
808        ).storage_perm(),
809        forall|i: int|
810            #![trigger final(regions).slot_owners[i]]
811            final(regions).ref_count(i) == REF_COUNT_UNUSED ==> final(regions).slot_owners[i]
812                == old(regions).slot_owners[i],
813        forall|i: int|
814            #![trigger final(regions).slot_owners[i]]
815            i != frame_to_index(paddr) && old(regions).ref_count(i) == REF_COUNT_UNUSED
816                && final(regions).ref_count(i) != REF_COUNT_UNUSED
817                ==> final(regions).slot_owners[i].usage !is Frame,
818        forall|c: CursorOwner<'rcu, UserPtConfig>|
819            #![auto]
820            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
821{
822    cursor_mut_map_embedded(&mut entry.owner, regions, &mut entry.guards, tlb_model, paddr, prop);
823}
824
825} // verus!
ostd/specs/mm/embedding/cursor.rs

ostd/specs/mm/embedding/
cursor.rs
