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

ostd/specs/mm/embedding/
cursor.rs
