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

ostd/specs/mm/embedding/
cursor.rs
