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

ostd/specs/mm/embedding/
cursor.rs
