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        // `slots` preserved (the boot-fixed metadata perm map).
226        final(regions).slots == old(regions).slots,
227        // `None` ⟹ slot_owners fully preserved (no clone happened).
228        res is None ==> forall|i: int|
229            #![trigger final(regions).slot_owners[i]]
230            final(regions).slot_owners[i] == old(regions).slot_owners[i],
231        // `Some(paddr)` ⟹ `rc++` at the cloned leaf's slot; all other
232        // slots fully preserved. The cloned leaf must be a tracked
233        // (non-MMIO) data Frame whose slot is in-bound and active.
234        res matches Some(paddr) ==> {
235            &&& valid_frame_paddr(paddr)
236            &&& old(regions).slot_owner(paddr).usage is Frame
237            &&& final(regions).slot_owner(paddr).ref_count() == (old(regions).slot_owner(
238                paddr,
239            ).ref_count() + 1) as nat
240            &&& final(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX
241            &&& forall|i: int|
242                #![trigger final(regions).slot_owners[i]]
243                i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
244                    regions,
245                ).slot_owners[i]
246            // At the cloned slot, only `ref_count` changes — everything
247            // else (`raw_count`, `in_list`, `usage`, `paths_in_pt`,
248            // `storage`, `slot_vaddr`, `vtable_ptr`) is preserved.
249            &&& final(regions).slot_owner(paddr).slot_vaddr == old(regions).slot_owner(
250                paddr,
251            ).slot_vaddr
252            &&& final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage
253            &&& final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(
254                paddr,
255            ).paths_in_pt
256            &&& final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
257                paddr,
258            ).in_list_perm
259            &&& final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
260                paddr,
261            ).storage_perm()
262            &&& final(regions).slot_owner(paddr).vtable_ptr_perm() == old(regions).slot_owner(
263                paddr,
264            ).vtable_ptr_perm()
265        },
266        forall|c: CursorOwner<'rcu, UserPtConfig>|
267            #![auto]
268            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
269;
270
271/// Mirror of [`crate::mm::vm_space::Cursor::jump`] /
272/// [`crate::mm::vm_space::CursorMut::jump`].
273///
274/// Exec requires `invariants(owner, regions, guards)` (which includes
275/// `!owner.popped_too_high`). It does **not** require
276/// `owner.in_locked_range()`: the exec `requires` was relaxed. A drifted
277/// cursor that cannot be repositioned within the target node aborts the
278/// program (a sound `panic_diverge`, mirroring the real `pop_level`
279/// `unwrap` panic), so an out-of-range cursor is a safety non-issue —
280/// `in_locked_range` now only governs the success postcondition, and
281/// this proof soundly models the returning path.
282pub proof fn lemma_cursor_jump_embedded<'rcu>(
283    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
284    tracked regions: &mut MetaRegionOwners,
285    tracked guards: &mut Guards<'rcu>,
286    va: Vaddr,
287)
288    requires
289        old(owner).inv(),
290        old(regions).inv(),
291        old(owner).children_not_locked(*old(guards)),
292        old(owner).nodes_locked(*old(guards)),
293        old(owner).metaregion_sound(*old(regions)),
294        !old(owner).popped_too_high,
295    ensures
296        final(owner).inv(),
297        final(regions).inv(),
298        final(owner).children_not_locked(*final(guards)),
299        final(owner).nodes_locked(*final(guards)),
300        final(owner).metaregion_sound(*final(regions)),
301        !final(owner).popped_too_high,
302        // `jump` repositions the cursor but touches no frame slot — no
303        // PTE writes, no leaf clone. Full `slot_owners` preservation,
304        // same shape as `find_next`.
305        final(regions).slots == old(regions).slots,
306        forall|i: int|
307            #![trigger final(regions).slot_owners[i]]
308            final(regions).slot_owners[i] == old(regions).slot_owners[i],
309        forall|c: CursorOwner<'rcu, UserPtConfig>|
310            #![auto]
311            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
312{
313}
314
315/// Mirror of [`crate::mm::vm_space::CursorMut::map`].
316///
317/// Exec requires:
318/// - `tlb_model.inv()`
319/// - `invariants(cursor_owner, regions, guards)` (incl. `!popped_too_high`)
320/// - `item_wf(frame, prop, entry_owner, regions)` — MODEL GAP.
321///
322/// Does **not** require `in_locked_range()`: an out-of-range cursor
323/// panics at `map`'s `assert!(va < barrier_va.end)` (the real
324/// `map_panic_conditions` out-of-range abort); the exec re-derives
325/// `in_locked_range` from that panic + the cursor invariant. This axiom
326/// soundly models the returning path.
327pub axiom fn cursor_mut_map_embedded<'rcu>(
328    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
329    tracked regions: &mut MetaRegionOwners,
330    tracked guards: &mut Guards<'rcu>,
331    tracked tlb_model: &mut TlbModel,
332    paddr: Paddr,
333    prop: PageProperty,
334)
335    requires
336        old(owner).inv(),
337        old(regions).inv(),
338        old(owner).children_not_locked(*old(guards)),
339        old(owner).nodes_locked(*old(guards)),
340        old(owner).metaregion_sound(*old(regions)),
341        !old(owner).popped_too_high,
342        old(tlb_model).inv(),
343        // The mapped paddr is page-aligned and in-bounds (these come
344        // from a consumed `FrameEntry`'s paddr; `valid_frame_paddr` is
345        // guaranteed by the embedding's structural_inv `frames` clause).
346        valid_frame_paddr(
347            paddr,
348        ),
349// MODEL GAP: `item_wf(frame, prop, entry_owner, regions)`
350// depends on a separate `EntryOwner<UserPtConfig>` arg we don't
351// model. The exec call assumes the caller supplies one.
352
353    ensures
354        final(owner).inv(),
355        final(regions).inv(),
356        final(owner).children_not_locked(*final(guards)),
357        final(owner).nodes_locked(*final(guards)),
358        final(owner).metaregion_sound(*final(regions)),
359        !final(owner).popped_too_high,
360        final(tlb_model).inv(),
361        final(regions).slots == old(regions).slots,
362        // Universal `raw_count` / `in_list` preservation (map doesn't
363        // forget references or touch the free-list).
364        forall|i: int|
365            #![trigger final(regions).slot_owners[i]]
366            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
367        // Per exec cursor/mod.rs:2853 + 2836: at non-mapped slots that
368        // were already in use (pre rc != UNUSED), the entire
369        // slot_owner is preserved. NB: slots that were UNUSED pre may
370        // transition to non-UNUSED as the cursor allocates fresh PT
371        // nodes, so the "fully preserved" guard requires `pre rc != UNUSED`.
372        forall|i: int|
373            #![trigger final(regions).slot_owners[i]]
374            i != frame_to_index(paddr) && old(regions).slot_owners[i].ref_count()
375                != REF_COUNT_UNUSED ==> final(regions).slot_owners[i] == old(
376                regions,
377            ).slot_owners[i],
378        // Per exec cursor/mod.rs:2844-2846: any pre-non-UNUSED slot
379        // stays non-UNUSED.
380        forall|i: int|
381            #![trigger final(regions).slot_owners[i].ref_count()]
382            old(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
383                ==> final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED,
384        // **`ref_count` PRESERVED at the mapped slot.** Faithful axiom
385        // strengthening relative to the exec contract (which only says
386        // `pre rc > 0 ⟹ post rc > 0`): exec map `ManuallyDrop`s the
387        // input UFrame (so its handle's ref-count contribution stays
388        // put rather than running `Drop`) and writes a PTE pointing to
389        // the frame; the UFrame's ref is "transferred" to the new PTE,
390        // net zero rc change. Combined with `Op::Map` consuming the
391        // corresponding `FrameEntry` (`H_post = H_pre - 1`) and
392        // `paths_in_pt += {cursor.path}` at the mapped slot
393        // (`P_post = P_pre + 1`), `accounting_inv` clause 4
394        // (`rc == H + P`) chains: `pre rc == pre H + pre P` ⟹
395        // `post rc = pre rc = (H_post + 1) + (P_post - 1) = H_post + P_post`.
396        final(regions).slot_owner(paddr).ref_count() == old(regions).slot_owner(paddr).ref_count(),
397        // **`paths_in_pt.len() += 1` at the mapped slot.** The cursor's
398        // current path is inserted into the mapped slot's `paths_in_pt`
399        // (this is the bookkeeping side of writing the PTE; see
400        // [cursor/mod.rs:2613] for the exec insertion site).
401        final(regions).slot_owner(paddr).paths_in_pt.len() == old(regions).slot_owner(
402            paddr,
403        ).paths_in_pt.len() + 1,
404        // **`usage` / `storage` PRESERVED at the mapped slot.** Map
405        // doesn't change the slot's identity or metadata — it only
406        // updates the PTE and the bookkeeping `paths_in_pt`.
407        final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
408        final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
409            paddr,
410        ).storage_perm(),
411        // Slots that stay UNUSED are fully preserved.
412        forall|i: int|
413            #![trigger final(regions).slot_owners[i]]
414            final(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
415                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
416        // **Changed-slots clause.** At any slot *other* than the
417        // mapped frame, a pre-UNUSED → post-non-UNUSED transition
418        // means the cursor allocated a fresh PT node (not a data
419        // frame), so `usage != Frame`. Combined with the other clauses
420        // this lets `accounting_inv`'s Frame-scoped clauses 3 and 4
421        // become vacuous at newly-allocated PT-node slots; the
422        // mapped slot itself is handled by the per-slot ensures
423        // above.
424        forall|i: int|
425            #![trigger final(regions).slot_owners[i]]
426            i != frame_to_index(paddr) && old(regions).slot_owners[i].ref_count()
427                == REF_COUNT_UNUSED && final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
428                ==> final(regions).slot_owners[i].usage !is Frame,
429        forall|c: CursorOwner<'rcu, UserPtConfig>|
430            #![auto]
431            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
432;
433
434/// Mirror of [`crate::mm::vm_space::CursorMut::unmap`].
435///
436/// Exec requires (line 865-866):
437/// - `invariants(cursor_owner, regions, guards)`
438/// - `tlb_model.inv()`
439///
440/// Does NOT require `in_locked_range()` (the method walks `len` bytes
441/// from the cursor, advancing into the locked range as needed).
442pub axiom fn cursor_mut_unmap_embedded<'rcu>(
443    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
444    tracked regions: &mut MetaRegionOwners,
445    tracked guards: &mut Guards<'rcu>,
446    tracked tlb_model: &mut TlbModel,
447    len: usize,
448)
449    requires
450        old(owner).inv(),
451        old(regions).inv(),
452        old(owner).children_not_locked(*old(guards)),
453        old(owner).nodes_locked(*old(guards)),
454        old(owner).metaregion_sound(*old(regions)),
455        !old(owner).popped_too_high,
456        old(tlb_model).inv(),
457    ensures
458        final(owner).inv(),
459        final(regions).inv(),
460        final(owner).children_not_locked(*final(guards)),
461        final(owner).nodes_locked(*final(guards)),
462        final(owner).metaregion_sound(*final(regions)),
463        !final(owner).popped_too_high,
464        final(tlb_model).inv(),
465        // `slots` (the boot-fixed metadata perm map) preserved.
466        final(regions).slots == old(regions).slots,
467        // **Universal per-slot preservation.** Unmap doesn't change a
468        // slot's identity (`usage`/`slot_vaddr`/`raw_count`/`in_list`/
469        // `vtable_ptr`) and never bumps `rc` to `UNIQUE` (UNIQUE is a
470        // unique-handle sentinel produced only by
471        // `Frame::into_unique`, not by unmap).
472        forall|i: int|
473            #![trigger final(regions).slot_owners[i]]
474            {
475                &&& final(regions).slot_owners[i].slot_vaddr == old(
476                    regions,
477                ).slot_owners[i].slot_vaddr
478                &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
479                &&& final(regions).slot_owners[i].in_list_perm == old(
480                    regions,
481                ).slot_owners[i].in_list_perm
482                &&& final(regions).slot_owners[i].vtable_ptr_perm() == old(
483                    regions,
484                ).slot_owners[i].vtable_ptr_perm()
485                // `rc` doesn't bump to UNIQUE.
486                &&& old(regions).slot_owners[i].ref_count() != REF_COUNT_UNIQUE
487                    ==> final(regions).slot_owners[i].ref_count()
488                    != REF_COUNT_UNIQUE
489                // Storage preserved at slots that end non-UNUSED.
490                &&& final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
491                    ==> final(regions).slot_owners[i].storage_perm() == old(
492                    regions,
493                ).slot_owners[i].storage_perm()
494            },
495        // Unparked (page-table-node) slots are untouched: a slot whose
496        // perm is not parked in `regions.slots` is a PT root, an ancestor
497        // of (hence outside) the unmapped range, so unmap leaves its
498        // `slot_owner` (rc/usage/…) intact. Preserves the embedding's
499        // slot-perm coverage exception.
500        forall|i: int|
501            #![trigger final(regions).slot_owners[i]]
502            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
503                regions,
504            ).slot_owners[i],
505        // **Frame-slot per-PTE accounting.** For each Frame-usage slot
506        // affected by unmap, removing `k` PTEs decreases both `rc` and
507        // `paths_in_pt.len()` by `k`, preserving the difference
508        // (the "non-mapping count" = handles). Stated as
509        // `final.rc + old.paths.len == old.rc + final.paths.len` to
510        // avoid `nat` subtraction. The accompanying `rc ≤ old.rc` /
511        // `paths.len ≤ old.paths.len` clauses pin the direction of
512        // change (unmap only removes). The `post rc != 0` clause
513        // rules out the transient "rc == 0" state at Frame slots:
514        // exec teardown collapses Frame ∧ rc==0 to `REF_COUNT_UNUSED`
515        // atomically; the embedding sees the post-teardown state.
516        forall|i: int|
517            #![trigger final(regions).slot_owners[i]]
518            old(regions).slot_owners[i].usage is Frame ==> {
519                &&& final(regions).slot_owners[i].ref_count() + old(
520                    regions,
521                ).slot_owners[i].paths_in_pt.len() == old(regions).slot_owners[i].ref_count()
522                    + final(regions).slot_owners[i].paths_in_pt.len()
523                &&& final(regions).slot_owners[i].ref_count() <= old(
524                    regions,
525                ).slot_owners[i].ref_count()
526                &&& final(regions).slot_owners[i].paths_in_pt.len() <= old(
527                    regions,
528                ).slot_owners[i].paths_in_pt.len()
529                &&& final(regions).slot_owners[i].ref_count() != 0
530            },
531        // **MMIO slots untouched.** Unmap only walks tracked user VAs;
532        // MMIO PTEs (`PageUsage::MMIO`) require explicit
533        // unmap-via-other-API. Without this, the
534        // `MetaSlotOwner::inv` MMIO exception (UNUSED + MMIO allows
535        // non-empty `paths_in_pt`) would block
536        // `accounting_inv` clause 1 (UNUSED ⟹ paths empty) at
537        // post-UNUSED MMIO slots.
538        forall|i: int|
539            #![trigger final(regions).slot_owners[i]]
540            old(regions).slot_owners[i].usage == PageUsage::MMIO ==> final(regions).slot_owners[i]
541                == old(regions).slot_owners[i],
542        forall|c: CursorOwner<'rcu, UserPtConfig>|
543            #![auto]
544            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
545;
546
547// =============================================================================
548// dispatch tags + step proofs
549// =============================================================================
550/// Internal: dispatch tag for cursor methods that also touch
551/// `MetaRegionOwners` and `TlbModel`. `Map` is handled via its own
552/// [`map_step`].
553pub enum CursorMutRegionsMethod {
554    Unmap(usize),
555}
556
557/// Per-op step for `Op::OpenCursor` (read-only [`Cursor`]). Calls the
558/// embedded axiom; on `Some`, wraps the cursor owner + guards into a
559/// `CursorEntry` with the supplied `vs` (so the resulting entry's
560/// `vm_space` field correctly references the parent VmSpace).
561///
562/// Monomorphic in the cursor kind — read-only vs mutable are *separate*
563/// functions, each calling a single `_embedded` axiom. This is
564/// deliberate: a `match kind { ReadOnly => axiom_a, Mutable => axiom_b }`
565/// wrapper blocks Verus from chaining the per-branch axioms' quantified
566/// ensures (the Stage 5.3 changed-slots clause) into the wrapper's own
567/// ensures. With one axiom call per function the forall flows straight
568/// through. See [`open_cursor_mut_step`] for the mutable twin.
569pub(super) proof fn open_cursor_step<'a, 'rcu>(
570    tracked vm_space: &VmSpaceOwner,
571    tracked regions: &mut MetaRegionOwners,
572    vs: VmSpaceId,
573    va: Range<Vaddr>,
574) -> (tracked res: Option<CursorEntry<'rcu>>)
575    requires
576        vm_space.inv(),
577        old(regions).inv(),
578    ensures
579        final(regions).inv(),
580        // Page-table cursor ops never touch the metadata slot-perm map
581        // (`slots` is the boot-fixed metadata region) nor the
582        // ManuallyDrop `raw_count` / free-list `in_list` fields; only
583        // `slot_owners` refcount / `paths_in_pt` changes. Preserving the
584        // `slots` domain (#2 / #3b) and `raw_count` / `in_list` (#4
585        // partial) keeps `VmStore::inv`'s coverage clauses chainable
586        // across cursor methods.
587        final(regions).slots == old(regions).slots,
588        forall|i: int|
589            #![trigger final(regions).slot_owners[i]]
590            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
591        // Stage 5.3: opening a cursor only allocates fresh PT nodes —
592        // every *changed* slot was UNUSED before and becomes a
593        // non-UNUSED PT node (usage != Frame). `accounting_inv` chains
594        // from this single clause.
595        forall|i: int|
596            #![trigger final(regions).slot_owners[i]]
597            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
598                &&& old(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
599                &&& final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
600                &&& final(regions).slot_owners[i].usage !is Frame
601            },
602        forall|c: CursorOwner<'rcu, UserPtConfig>|
603            #![auto]
604            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
605        res matches Some(e) ==> e.inv(),
606        res matches Some(e) ==> e.owner.metaregion_sound(*final(regions)),
607        res matches Some(e) ==> e.kind == CursorKind::ReadOnly,
608        res matches Some(e) ==> e.va == va,
609        res matches Some(e) ==> e.vm_space == vs,
610{
611    let tracked owner_opt = vm_space_cursor_embedded(vm_space, regions, va);
612    match owner_opt {
613        Option::Some((owner, guards)) => {
614            let tracked entry = tracked_cursor_entry_new(
615                vs,
616                CursorKind::ReadOnly,
617                va,
618                owner,
619                guards,
620            );
621            Option::Some(entry)
622        },
623        Option::None => Option::None,
624    }
625}
626
627/// Per-op step for `Op::OpenCursorMut` (mutable [`CursorMut`]). The
628/// mutable twin of [`open_cursor_step`]; see its docs for why the two
629/// cursor kinds are separate monomorphic functions.
630pub(super) proof fn open_cursor_mut_step<'a, 'rcu>(
631    tracked vm_space: &VmSpaceOwner,
632    tracked regions: &mut MetaRegionOwners,
633    vs: VmSpaceId,
634    va: Range<Vaddr>,
635) -> (tracked res: Option<CursorEntry<'rcu>>)
636    requires
637        vm_space.inv(),
638        old(regions).inv(),
639    ensures
640        final(regions).inv(),
641        final(regions).slots == old(regions).slots,
642        forall|i: int|
643            #![trigger final(regions).slot_owners[i]]
644            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
645        forall|i: int|
646            #![trigger final(regions).slot_owners[i]]
647            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
648                &&& old(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
649                &&& final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
650                &&& final(regions).slot_owners[i].usage !is Frame
651            },
652        forall|c: CursorOwner<'rcu, UserPtConfig>|
653            #![auto]
654            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
655        res matches Some(e) ==> e.inv(),
656        res matches Some(e) ==> e.owner.metaregion_sound(*final(regions)),
657        res matches Some(e) ==> e.kind == CursorKind::Mutable,
658        res matches Some(e) ==> e.va == va,
659        res matches Some(e) ==> e.vm_space == vs,
660{
661    let tracked owner_opt = vm_space_cursor_mut_embedded(vm_space, regions, va);
662    match owner_opt {
663        Option::Some((owner, guards)) => {
664            let tracked entry = tracked_cursor_entry_new(
665                vs,
666                CursorKind::Mutable,
667                va,
668                owner,
669                guards,
670            );
671            Option::Some(entry)
672        },
673        Option::None => Option::None,
674    }
675}
676
677/// Per-op step for `Op::DropCursor`. The caller has already extracted
678/// the entry from the store; this function drops it.
679pub(super) proof fn drop_cursor_step<'rcu>(tracked _entry: CursorEntry<'rcu>) {
680}
681
682/// Per-op step for cursor methods that mutate only the cursor owner
683/// (and thread `regions` / `guards`): query, find_next, jump,
684/// protect_next.
685///
686/// None of these require `owner.in_locked_range()`. Exec `query`
687/// handles an out-of-range cursor with a graceful `Err`; exec `jump`'s
688/// `in_locked_range` precondition was relaxed (a drifted cursor that
689/// cannot be repositioned aborts via a sound `panic_diverge`).
690/// Per-op step for `Op::Query`. Mirrors
691/// [`cursor_query_embedded`]'s `Option<Paddr>` result: `Some(paddr)`
692/// when query returned a tracked `MappedItem` (and `rc` was bumped at
693/// the leaf), `None` otherwise. The store-level [`super::lemma_step_query`]
694/// (mod.rs) consumes that paddr to register a fresh `FrameEntry`,
695/// closing accounting.
696pub(super) proof fn cursor_query_step<'rcu>(
697    tracked entry: &mut CursorEntry<'rcu>,
698    tracked regions: &mut MetaRegionOwners,
699) -> (res: Option<Paddr>)
700    requires
701        old(entry).inv(),
702        old(regions).inv(),
703        old(entry).owner.metaregion_sound(*old(regions)),
704    ensures
705        final(entry).vm_space == old(entry).vm_space,
706        final(entry).kind == old(entry).kind,
707        final(entry).va == old(entry).va,
708        final(entry).inv(),
709        final(regions).inv(),
710        final(entry).owner.metaregion_sound(*final(regions)),
711        final(regions).slots == old(regions).slots,
712        res is None ==> forall|i: int|
713            #![trigger final(regions).slot_owners[i]]
714            final(regions).slot_owners[i] == old(regions).slot_owners[i],
715        res matches Some(paddr) ==> {
716            &&& valid_frame_paddr(paddr)
717            &&& old(regions).slot_owner(paddr).usage is Frame
718            &&& final(regions).slot_owner(paddr).ref_count() == (old(regions).slot_owner(
719                paddr,
720            ).ref_count() + 1) as nat
721            &&& final(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX
722            &&& forall|i: int|
723                #![trigger final(regions).slot_owners[i]]
724                i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
725                    regions,
726                ).slot_owners[i]
727            &&& final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage
728            &&& final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(
729                paddr,
730            ).paths_in_pt
731            &&& final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
732                paddr,
733            ).in_list_perm
734            &&& final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
735                paddr,
736            ).storage_perm()
737        },
738        forall|c: CursorOwner<'rcu, UserPtConfig>|
739            #![auto]
740            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
741{
742    cursor_query_embedded(&mut entry.owner, regions, &mut entry.guards)
743}
744
745/// Per-op step for `Op::FindNext`. Navigates the cursor forward
746/// without touching any frame slot — full `slot_owners` preservation.
747pub(super) proof fn cursor_find_next_step<'rcu>(
748    tracked entry: &mut CursorEntry<'rcu>,
749    tracked regions: &mut MetaRegionOwners,
750    len: usize,
751)
752    requires
753        old(entry).inv(),
754        old(regions).inv(),
755        old(entry).owner.metaregion_sound(*old(regions)),
756    ensures
757        final(entry).vm_space == old(entry).vm_space,
758        final(entry).kind == old(entry).kind,
759        final(entry).va == old(entry).va,
760        final(entry).inv(),
761        final(regions).inv(),
762        final(entry).owner.metaregion_sound(*final(regions)),
763        final(regions).slots == old(regions).slots,
764        // Full `slot_owners` preservation — `find_next` writes no PTE
765        // and clones no leaf.
766        forall|i: int|
767            #![trigger final(regions).slot_owners[i]]
768            final(regions).slot_owners[i] == old(regions).slot_owners[i],
769        forall|c: CursorOwner<'rcu, UserPtConfig>|
770            #![auto]
771            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
772{
773}
774
775/// Per-op step for `Op::Jump`. Repositions the cursor without
776/// touching any frame slot — full `slot_owners` preservation.
777pub(super) proof fn cursor_jump_step<'rcu>(
778    tracked entry: &mut CursorEntry<'rcu>,
779    tracked regions: &mut MetaRegionOwners,
780    va: Vaddr,
781)
782    requires
783        old(entry).inv(),
784        old(regions).inv(),
785        old(entry).owner.metaregion_sound(*old(regions)),
786    ensures
787        final(entry).vm_space == old(entry).vm_space,
788        final(entry).kind == old(entry).kind,
789        final(entry).va == old(entry).va,
790        final(entry).inv(),
791        final(regions).inv(),
792        final(entry).owner.metaregion_sound(*final(regions)),
793        final(regions).slots == old(regions).slots,
794        forall|i: int|
795            #![trigger final(regions).slot_owners[i]]
796            final(regions).slot_owners[i] == old(regions).slot_owners[i],
797        forall|c: CursorOwner<'rcu, UserPtConfig>|
798            #![auto]
799            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
800{
801    lemma_cursor_jump_embedded(&mut entry.owner, regions, &mut entry.guards, va)
802}
803
804/// Per-op step for `Op::ProtectNext`. Rewrites PTE `prop` fields in
805/// place — no `rc` or `paths_in_pt` mutation; full `slot_owners`
806/// preservation.
807pub(super) proof fn cursor_protect_next_step<'rcu>(
808    tracked entry: &mut CursorEntry<'rcu>,
809    tracked regions: &mut MetaRegionOwners,
810    len: usize,
811)
812    requires
813        old(entry).inv(),
814        old(regions).inv(),
815        old(entry).owner.metaregion_sound(*old(regions)),
816    ensures
817        final(entry).vm_space == old(entry).vm_space,
818        final(entry).kind == old(entry).kind,
819        final(entry).va == old(entry).va,
820        final(entry).inv(),
821        final(regions).inv(),
822        final(entry).owner.metaregion_sound(*final(regions)),
823        final(regions).slots == old(regions).slots,
824        forall|i: int|
825            #![trigger final(regions).slot_owners[i]]
826            final(regions).slot_owners[i] == old(regions).slot_owners[i],
827        forall|c: CursorOwner<'rcu, UserPtConfig>|
828            #![auto]
829            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
830{
831}
832
833/// Per-op step for cursor methods that mutate the cursor owner,
834/// `MetaRegionOwners`, AND `TlbModel`: `unmap` (and `map`, via
835/// [`map_step`]).
836pub(super) proof fn cursor_mut_regions_step<'rcu>(
837    tracked entry: &mut CursorEntry<'rcu>,
838    tracked regions: &mut MetaRegionOwners,
839    tracked tlb_model: &mut TlbModel,
840    method: CursorMutRegionsMethod,
841)
842    requires
843        old(entry).inv(),
844        old(regions).inv(),
845        old(entry).owner.metaregion_sound(*old(regions)),
846        old(tlb_model).inv(),
847    ensures
848        final(entry).vm_space == old(entry).vm_space,
849        final(entry).kind == old(entry).kind,
850        final(entry).va == old(entry).va,
851        final(entry).inv(),
852        final(regions).inv(),
853        final(entry).owner.metaregion_sound(*final(regions)),
854        final(tlb_model).inv(),
855        // Mirror the faithful `cursor_mut_unmap_embedded` ensures: per-
856        // slot universal preservation (raw_count, in_list, usage,
857        // slot_vaddr, vtable_ptr); rc doesn't bump to UNIQUE; storage
858        // preserved at non-UNUSED post; and at Frame slots, the
859        // "non-mapping count" `rc - paths.len()` is invariant with
860        // `rc` and `paths.len` monotonically non-increasing.
861        final(regions).slots == old(regions).slots,
862        forall|i: int|
863            #![trigger final(regions).slot_owners[i]]
864            {
865                &&& final(regions).slot_owners[i].slot_vaddr == old(
866                    regions,
867                ).slot_owners[i].slot_vaddr
868                &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
869                &&& final(regions).slot_owners[i].in_list_perm == old(
870                    regions,
871                ).slot_owners[i].in_list_perm
872                &&& final(regions).slot_owners[i].vtable_ptr_perm() == old(
873                    regions,
874                ).slot_owners[i].vtable_ptr_perm()
875                &&& old(regions).slot_owners[i].ref_count() != REF_COUNT_UNIQUE
876                    ==> final(regions).slot_owners[i].ref_count() != REF_COUNT_UNIQUE
877                &&& final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
878                    ==> final(regions).slot_owners[i].storage_perm() == old(
879                    regions,
880                ).slot_owners[i].storage_perm()
881            },
882        // Unparked (page-table-node) slots untouched (see
883        // `cursor_mut_unmap_embedded`); preserves the coverage exception.
884        forall|i: int|
885            #![trigger final(regions).slot_owners[i]]
886            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
887                regions,
888            ).slot_owners[i],
889        forall|i: int|
890            #![trigger final(regions).slot_owners[i]]
891            old(regions).slot_owners[i].usage is Frame ==> {
892                &&& final(regions).slot_owners[i].ref_count() + old(
893                    regions,
894                ).slot_owners[i].paths_in_pt.len() == old(regions).slot_owners[i].ref_count()
895                    + final(regions).slot_owners[i].paths_in_pt.len()
896                &&& final(regions).slot_owners[i].ref_count() <= old(
897                    regions,
898                ).slot_owners[i].ref_count()
899                &&& final(regions).slot_owners[i].paths_in_pt.len() <= old(
900                    regions,
901                ).slot_owners[i].paths_in_pt.len()
902                &&& final(regions).slot_owners[i].ref_count() != 0
903            },
904        forall|i: int|
905            #![trigger final(regions).slot_owners[i]]
906            old(regions).slot_owners[i].usage == PageUsage::MMIO ==> final(regions).slot_owners[i]
907                == old(regions).slot_owners[i],
908        forall|c: CursorOwner<'rcu, UserPtConfig>|
909            #![auto]
910            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
911{
912    match method {
913        CursorMutRegionsMethod::Unmap(len) => {
914            cursor_mut_unmap_embedded(&mut entry.owner, regions, &mut entry.guards, tlb_model, len);
915        },
916    }
917}
918
919/// Per-op step for `Op::Map`. Mutates the cursor owner, the regions,
920/// and the TLB model. Has its own function rather than a dispatch tag
921/// because the argument shape (UFrame, PageProperty) doesn't match the
922/// others.
923///
924/// Does NOT require `owner.in_locked_range()`: exec `map` panics on an
925/// out-of-range cursor (`assert!(va < barrier_va.end)`) and re-derives
926/// `in_locked_range` from that panic + the cursor invariant.
927pub(super) proof fn map_step<'rcu>(
928    tracked entry: &mut CursorEntry<'rcu>,
929    tracked regions: &mut MetaRegionOwners,
930    tracked tlb_model: &mut TlbModel,
931    paddr: Paddr,
932    prop: PageProperty,
933)
934    requires
935        old(entry).inv(),
936        old(regions).inv(),
937        old(entry).owner.metaregion_sound(*old(regions)),
938        old(tlb_model).inv(),
939        valid_frame_paddr(paddr),
940    ensures
941        final(entry).vm_space == old(entry).vm_space,
942        final(entry).kind == old(entry).kind,
943        final(entry).va == old(entry).va,
944        final(entry).inv(),
945        final(regions).inv(),
946        final(entry).owner.metaregion_sound(*final(regions)),
947        final(tlb_model).inv(),
948        final(regions).slots == old(regions).slots,
949        // Mirror the strengthened `cursor_mut_map_embedded` ensures.
950        forall|i: int|
951            #![trigger final(regions).slot_owners[i]]
952            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
953        forall|i: int|
954            #![trigger final(regions).slot_owners[i]]
955            i != frame_to_index(paddr) && old(regions).slot_owners[i].ref_count()
956                != REF_COUNT_UNUSED ==> final(regions).slot_owners[i] == old(
957                regions,
958            ).slot_owners[i],
959        forall|i: int|
960            #![trigger final(regions).slot_owners[i].ref_count()]
961            old(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
962                ==> final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED,
963        final(regions).slot_owner(paddr).ref_count() == old(regions).slot_owner(paddr).ref_count(),
964        final(regions).slot_owner(paddr).paths_in_pt.len() == old(regions).slot_owner(
965            paddr,
966        ).paths_in_pt.len() + 1,
967        final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
968        final(regions).slot_owner(paddr).storage_perm() == old(regions).slot_owner(
969            paddr,
970        ).storage_perm(),
971        forall|i: int|
972            #![trigger final(regions).slot_owners[i]]
973            final(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
974                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
975        forall|i: int|
976            #![trigger final(regions).slot_owners[i]]
977            i != frame_to_index(paddr) && old(regions).slot_owners[i].ref_count()
978                == REF_COUNT_UNUSED && final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
979                ==> final(regions).slot_owners[i].usage !is Frame,
980        forall|c: CursorOwner<'rcu, UserPtConfig>|
981            #![auto]
982            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
983{
984    cursor_mut_map_embedded(&mut entry.owner, regions, &mut entry.guards, tlb_model, paddr, prop);
985}
986
987} // verus!
ostd/specs/mm/embedding/cursor.rs

ostd/specs/mm/embedding/
cursor.rs
