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

ostd/specs/mm/embedding/
cursor.rs
