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;
52use crate::mm::frame::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED};
53use crate::mm::page_prop::PageProperty;
54use crate::mm::vm_space::UserPtConfig;
55use crate::mm::vm_space::vm_space_specs::VmSpaceOwner;
56use crate::mm::{Paddr, Vaddr};
57use crate::specs::arch::*;
58use crate::specs::mm::frame::mapping::frame_to_index;
59use crate::specs::mm::frame::meta_owners::PageUsage;
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`, `slot_vaddr`, `vtable_ptr`) is preserved.
247            &&& final(regions).slot_owners[frame_to_index(paddr)].slot_vaddr == old(
248                regions,
249            ).slot_owners[frame_to_index(paddr)].slot_vaddr
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`/`slot_vaddr`/`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].slot_vaddr == old(
522                    regions,
523                ).slot_owners[i].slot_vaddr
524                &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
525                &&& final(regions).slot_owners[i].inner_perms.in_list == old(
526                    regions,
527                ).slot_owners[i].inner_perms.in_list
528                &&& final(regions).slot_owners[i].inner_perms.vtable_ptr == old(
529                    regions,
530                ).slot_owners[i].inner_perms.vtable_ptr
531                // `rc` doesn't bump to UNIQUE.
532                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNIQUE
533                    ==> final(regions).slot_owners[i].inner_perms.ref_count.value()
534                    != REF_COUNT_UNIQUE
535                // Storage preserved at slots that end non-UNUSED.
536                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
537                    ==> final(regions).slot_owners[i].inner_perms.storage == old(
538                    regions,
539                ).slot_owners[i].inner_perms.storage
540            },
541        // Unparked (page-table-node) slots are untouched: a slot whose
542        // perm is not parked in `regions.slots` is a PT root, an ancestor
543        // of (hence outside) the unmapped range, so unmap leaves its
544        // `slot_owner` (rc/usage/…) intact. Preserves the embedding's
545        // slot-perm coverage exception.
546        forall|i: usize|
547            #![trigger final(regions).slot_owners[i]]
548            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
549                regions,
550            ).slot_owners[i],
551        // **Frame-slot per-PTE accounting.** For each Frame-usage slot
552        // affected by unmap, removing `k` PTEs decreases both `rc` and
553        // `paths_in_pt.len()` by `k`, preserving the difference
554        // (the "non-mapping count" = handles). Stated as
555        // `final.rc + old.paths.len == old.rc + final.paths.len` to
556        // avoid `nat` subtraction. The accompanying `rc ≤ old.rc` /
557        // `paths.len ≤ old.paths.len` clauses pin the direction of
558        // change (unmap only removes). The `post rc != 0` clause
559        // rules out the transient "rc == 0" state at Frame slots:
560        // exec teardown collapses Frame ∧ rc==0 to `REF_COUNT_UNUSED`
561        // atomically; the embedding sees the post-teardown state.
562        forall|i: usize|
563            #![trigger final(regions).slot_owners[i]]
564            old(regions).slot_owners[i].usage == PageUsage::Frame ==> {
565                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() + old(
566                    regions,
567                ).slot_owners[i].paths_in_pt.len() == old(
568                    regions,
569                ).slot_owners[i].inner_perms.ref_count.value()
570                    + final(regions).slot_owners[i].paths_in_pt.len()
571                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() <= old(
572                    regions,
573                ).slot_owners[i].inner_perms.ref_count.value()
574                &&& final(regions).slot_owners[i].paths_in_pt.len() <= old(
575                    regions,
576                ).slot_owners[i].paths_in_pt.len()
577                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != 0
578            },
579        // **MMIO slots untouched.** Unmap only walks tracked user VAs;
580        // MMIO PTEs (`PageUsage::MMIO`) require explicit
581        // unmap-via-other-API. Without this, the
582        // `MetaSlotOwner::inv` MMIO exception (UNUSED + MMIO allows
583        // non-empty `paths_in_pt`) would block
584        // `accounting_inv` clause 1 (UNUSED ⟹ paths empty) at
585        // post-UNUSED MMIO slots.
586        forall|i: usize|
587            #![trigger final(regions).slot_owners[i]]
588            old(regions).slot_owners[i].usage == PageUsage::MMIO ==> final(regions).slot_owners[i]
589                == old(regions).slot_owners[i],
590        forall|c: CursorOwner<'rcu, UserPtConfig>|
591            #![auto]
592            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
593;
594
595/// Mirror of [`crate::mm::vm_space::CursorMut::protect_next`].
596///
597/// Exec requires (line 1443-1450):
598/// - `invariants(owner, regions, guards)`
599/// - `forall |p: PageProperty| op.requires((p,))` — MODEL GAP (closure).
600/// - The trackedness-preservation closure constraint — MODEL GAP.
601///
602/// Does NOT require `in_locked_range()` directly.
603pub axiom fn cursor_mut_protect_next_embedded<'rcu>(
604    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
605    tracked regions: &mut MetaRegionOwners,
606    tracked guards: &mut Guards<'rcu>,
607    len: usize,
608)
609    requires
610        old(owner).inv(),
611        old(regions).inv(),
612        old(owner).children_not_locked(*old(guards)),
613        old(owner).nodes_locked(*old(guards)),
614        old(owner).metaregion_sound(*old(regions)),
615        !old(
616            owner,
617        ).popped_too_high,
618// MODEL GAP: closure preconditions on `op`.
619
620    ensures
621        final(owner).inv(),
622        final(regions).inv(),
623        final(owner).children_not_locked(*final(guards)),
624        final(owner).nodes_locked(*final(guards)),
625        final(owner).metaregion_sound(*final(regions)),
626        !final(owner).popped_too_high,
627        // `protect_next` rewrites PTE `prop` fields in place but neither
628        // bumps refcounts nor mutates `paths_in_pt` (the path set is
629        // about *which* tree positions map a frame, not *how*). So the
630        // entire `slot_owners` map is preserved.
631        final(regions).slots == old(regions).slots,
632        forall|i: usize|
633            #![trigger final(regions).slot_owners[i]]
634            final(regions).slot_owners[i] == old(regions).slot_owners[i],
635        forall|c: CursorOwner<'rcu, UserPtConfig>|
636            #![auto]
637            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
638;
639
640// =============================================================================
641// dispatch tags + step proofs
642// =============================================================================
643/// Internal: dispatch tag for cursor methods that also touch
644/// `MetaRegionOwners` and `TlbModel`. `Map` is handled via its own
645/// [`map_step`].
646pub enum CursorMutRegionsMethod {
647    Unmap(usize),
648}
649
650/// Per-op step for `Op::OpenCursor` (read-only [`Cursor`]). Calls the
651/// embedded axiom; on `Some`, wraps the cursor owner + guards into a
652/// `CursorEntry` with the supplied `vs` (so the resulting entry's
653/// `vm_space` field correctly references the parent VmSpace).
654///
655/// Monomorphic in the cursor kind — read-only vs mutable are *separate*
656/// functions, each calling a single `_embedded` axiom. This is
657/// deliberate: a `match kind { ReadOnly => axiom_a, Mutable => axiom_b }`
658/// wrapper blocks Verus from chaining the per-branch axioms' quantified
659/// ensures (the Stage 5.3 changed-slots clause) into the wrapper's own
660/// ensures. With one axiom call per function the forall flows straight
661/// through. See [`open_cursor_mut_step`] for the mutable twin.
662pub(super) proof fn open_cursor_step<'a, 'rcu>(
663    tracked vm_space: &VmSpaceOwner,
664    tracked regions: &mut MetaRegionOwners,
665    vs: VmSpaceId,
666    va: Range<Vaddr>,
667) -> (tracked res: Option<CursorEntry<'rcu>>)
668    requires
669        vm_space.inv(),
670        old(regions).inv(),
671    ensures
672        final(regions).inv(),
673        // Page-table cursor ops never touch the metadata slot-perm map
674        // (`slots` is the boot-fixed metadata region) nor the
675        // ManuallyDrop `raw_count` / free-list `in_list` fields; only
676        // `slot_owners` refcount / `paths_in_pt` changes. Preserving the
677        // `slots` domain (#2 / #3b) and `raw_count` / `in_list` (#4
678        // partial) keeps `VmStore::inv`'s coverage clauses chainable
679        // across cursor methods.
680        final(regions).slots == old(regions).slots,
681        forall|i: usize|
682            #![trigger final(regions).slot_owners[i]]
683            final(regions).slot_owners[i].inner_perms.in_list == old(
684                regions,
685            ).slot_owners[i].inner_perms.in_list,
686        // Stage 5.3: opening a cursor only allocates fresh PT nodes —
687        // every *changed* slot was UNUSED before and becomes a
688        // non-UNUSED PT node (usage != Frame). `accounting_inv` chains
689        // from this single clause.
690        forall|i: usize|
691            #![trigger final(regions).slot_owners[i]]
692            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
693                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
694                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
695                &&& final(regions).slot_owners[i].usage != PageUsage::Frame
696            },
697        forall|c: CursorOwner<'rcu, UserPtConfig>|
698            #![auto]
699            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
700        res matches Some(e) ==> e.inv(),
701        res matches Some(e) ==> e.owner.metaregion_sound(*final(regions)),
702        res matches Some(e) ==> e.kind == CursorKind::ReadOnly,
703        res matches Some(e) ==> e.va == va,
704        res matches Some(e) ==> e.vm_space == vs,
705{
706    let tracked owner_opt = vm_space_cursor_embedded(vm_space, regions, va);
707    match owner_opt {
708        Option::Some((owner, guards)) => {
709            let tracked entry = axiom_cursor_entry_new(vs, CursorKind::ReadOnly, va, owner, guards);
710            Option::Some(entry)
711        },
712        Option::None => Option::None,
713    }
714}
715
716/// Per-op step for `Op::OpenCursorMut` (mutable [`CursorMut`]). The
717/// mutable twin of [`open_cursor_step`]; see its docs for why the two
718/// cursor kinds are separate monomorphic functions.
719pub(super) proof fn open_cursor_mut_step<'a, 'rcu>(
720    tracked vm_space: &VmSpaceOwner,
721    tracked regions: &mut MetaRegionOwners,
722    vs: VmSpaceId,
723    va: Range<Vaddr>,
724) -> (tracked res: Option<CursorEntry<'rcu>>)
725    requires
726        vm_space.inv(),
727        old(regions).inv(),
728    ensures
729        final(regions).inv(),
730        final(regions).slots == old(regions).slots,
731        forall|i: usize|
732            #![trigger final(regions).slot_owners[i]]
733            final(regions).slot_owners[i].inner_perms.in_list == old(
734                regions,
735            ).slot_owners[i].inner_perms.in_list,
736        forall|i: usize|
737            #![trigger final(regions).slot_owners[i]]
738            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
739                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
740                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
741                &&& final(regions).slot_owners[i].usage != PageUsage::Frame
742            },
743        forall|c: CursorOwner<'rcu, UserPtConfig>|
744            #![auto]
745            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
746        res matches Some(e) ==> e.inv(),
747        res matches Some(e) ==> e.owner.metaregion_sound(*final(regions)),
748        res matches Some(e) ==> e.kind == CursorKind::Mutable,
749        res matches Some(e) ==> e.va == va,
750        res matches Some(e) ==> e.vm_space == vs,
751{
752    let tracked owner_opt = vm_space_cursor_mut_embedded(vm_space, regions, va);
753    match owner_opt {
754        Option::Some((owner, guards)) => {
755            let tracked entry = axiom_cursor_entry_new(vs, CursorKind::Mutable, va, owner, guards);
756            Option::Some(entry)
757        },
758        Option::None => Option::None,
759    }
760}
761
762/// Per-op step for `Op::DropCursor`. The caller has already extracted
763/// the entry from the store; this function drops it.
764pub(super) proof fn drop_cursor_step<'rcu>(tracked _entry: CursorEntry<'rcu>) {
765}
766
767/// Per-op step for cursor methods that mutate only the cursor owner
768/// (and thread `regions` / `guards`): query, find_next, jump,
769/// protect_next.
770///
771/// None of these require `owner.in_locked_range()`. Exec `query`
772/// handles an out-of-range cursor with a graceful `Err`; exec `jump`'s
773/// `in_locked_range` precondition was relaxed (a drifted cursor that
774/// cannot be repositioned aborts via a sound `panic_diverge`).
775/// Per-op step for `Op::Query`. Mirrors
776/// [`cursor_query_embedded`]'s `Option<Paddr>` result: `Some(paddr)`
777/// when query returned a tracked `MappedItem` (and `rc` was bumped at
778/// the leaf), `None` otherwise. The store-level [`step_query`]
779/// (mod.rs) consumes that paddr to register a fresh `FrameEntry`,
780/// closing accounting.
781pub(super) proof fn cursor_query_step<'rcu>(
782    tracked entry: &mut CursorEntry<'rcu>,
783    tracked regions: &mut MetaRegionOwners,
784) -> (res: Option<Paddr>)
785    requires
786        old(entry).inv(),
787        old(regions).inv(),
788        old(entry).owner.metaregion_sound(*old(regions)),
789    ensures
790        final(entry).vm_space == old(entry).vm_space,
791        final(entry).kind == old(entry).kind,
792        final(entry).va == old(entry).va,
793        final(entry).inv(),
794        final(regions).inv(),
795        final(entry).owner.metaregion_sound(*final(regions)),
796        final(regions).slots == old(regions).slots,
797        res is None ==> forall|i: usize|
798            #![trigger final(regions).slot_owners[i]]
799            final(regions).slot_owners[i] == old(regions).slot_owners[i],
800        res matches Some(paddr) ==> {
801            &&& has_safe_slot(paddr)
802            &&& old(regions).slot_owners[frame_to_index(paddr)].usage == PageUsage::Frame
803            &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == (
804            old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
805                + 1) as nat
806            &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
807                <= REF_COUNT_MAX
808            &&& forall|i: usize|
809                #![trigger final(regions).slot_owners[i]]
810                i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
811                    regions,
812                ).slot_owners[i]
813            &&& final(regions).slot_owners[frame_to_index(paddr)].usage == old(
814                regions,
815            ).slot_owners[frame_to_index(paddr)].usage
816            &&& final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt == old(
817                regions,
818            ).slot_owners[frame_to_index(paddr)].paths_in_pt
819            &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list == old(
820                regions,
821            ).slot_owners[frame_to_index(paddr)].inner_perms.in_list
822            &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage == old(
823                regions,
824            ).slot_owners[frame_to_index(paddr)].inner_perms.storage
825        },
826        forall|c: CursorOwner<'rcu, UserPtConfig>|
827            #![auto]
828            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
829{
830    cursor_query_embedded(&mut entry.owner, regions, &mut entry.guards)
831}
832
833/// Per-op step for `Op::FindNext`. Navigates the cursor forward
834/// without touching any frame slot — full `slot_owners` preservation.
835pub(super) proof fn cursor_find_next_step<'rcu>(
836    tracked entry: &mut CursorEntry<'rcu>,
837    tracked regions: &mut MetaRegionOwners,
838    len: usize,
839)
840    requires
841        old(entry).inv(),
842        old(regions).inv(),
843        old(entry).owner.metaregion_sound(*old(regions)),
844    ensures
845        final(entry).vm_space == old(entry).vm_space,
846        final(entry).kind == old(entry).kind,
847        final(entry).va == old(entry).va,
848        final(entry).inv(),
849        final(regions).inv(),
850        final(entry).owner.metaregion_sound(*final(regions)),
851        final(regions).slots == old(regions).slots,
852        // Full `slot_owners` preservation — `find_next` writes no PTE
853        // and clones no leaf.
854        forall|i: usize|
855            #![trigger final(regions).slot_owners[i]]
856            final(regions).slot_owners[i] == old(regions).slot_owners[i],
857        forall|c: CursorOwner<'rcu, UserPtConfig>|
858            #![auto]
859            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
860{
861    cursor_find_next_embedded(&mut entry.owner, regions, &mut entry.guards, len)
862}
863
864/// Per-op step for `Op::Jump`. Repositions the cursor without
865/// touching any frame slot — full `slot_owners` preservation.
866pub(super) proof fn cursor_jump_step<'rcu>(
867    tracked entry: &mut CursorEntry<'rcu>,
868    tracked regions: &mut MetaRegionOwners,
869    va: Vaddr,
870)
871    requires
872        old(entry).inv(),
873        old(regions).inv(),
874        old(entry).owner.metaregion_sound(*old(regions)),
875    ensures
876        final(entry).vm_space == old(entry).vm_space,
877        final(entry).kind == old(entry).kind,
878        final(entry).va == old(entry).va,
879        final(entry).inv(),
880        final(regions).inv(),
881        final(entry).owner.metaregion_sound(*final(regions)),
882        final(regions).slots == old(regions).slots,
883        forall|i: usize|
884            #![trigger final(regions).slot_owners[i]]
885            final(regions).slot_owners[i] == old(regions).slot_owners[i],
886        forall|c: CursorOwner<'rcu, UserPtConfig>|
887            #![auto]
888            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
889{
890    cursor_jump_embedded(&mut entry.owner, regions, &mut entry.guards, va)
891}
892
893/// Per-op step for `Op::ProtectNext`. Rewrites PTE `prop` fields in
894/// place — no `rc` or `paths_in_pt` mutation; full `slot_owners`
895/// preservation.
896pub(super) proof fn cursor_protect_next_step<'rcu>(
897    tracked entry: &mut CursorEntry<'rcu>,
898    tracked regions: &mut MetaRegionOwners,
899    len: usize,
900)
901    requires
902        old(entry).inv(),
903        old(regions).inv(),
904        old(entry).owner.metaregion_sound(*old(regions)),
905    ensures
906        final(entry).vm_space == old(entry).vm_space,
907        final(entry).kind == old(entry).kind,
908        final(entry).va == old(entry).va,
909        final(entry).inv(),
910        final(regions).inv(),
911        final(entry).owner.metaregion_sound(*final(regions)),
912        final(regions).slots == old(regions).slots,
913        forall|i: usize|
914            #![trigger final(regions).slot_owners[i]]
915            final(regions).slot_owners[i] == old(regions).slot_owners[i],
916        forall|c: CursorOwner<'rcu, UserPtConfig>|
917            #![auto]
918            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
919{
920    cursor_mut_protect_next_embedded(&mut entry.owner, regions, &mut entry.guards, len)
921}
922
923/// Per-op step for cursor methods that mutate the cursor owner,
924/// `MetaRegionOwners`, AND `TlbModel`: `unmap` (and `map`, via
925/// [`map_step`]).
926pub(super) proof fn cursor_mut_regions_step<'rcu>(
927    tracked entry: &mut CursorEntry<'rcu>,
928    tracked regions: &mut MetaRegionOwners,
929    tracked tlb_model: &mut TlbModel,
930    method: CursorMutRegionsMethod,
931)
932    requires
933        old(entry).inv(),
934        old(regions).inv(),
935        old(entry).owner.metaregion_sound(*old(regions)),
936        old(tlb_model).inv(),
937    ensures
938        final(entry).vm_space == old(entry).vm_space,
939        final(entry).kind == old(entry).kind,
940        final(entry).va == old(entry).va,
941        final(entry).inv(),
942        final(regions).inv(),
943        final(entry).owner.metaregion_sound(*final(regions)),
944        final(tlb_model).inv(),
945        // Mirror the faithful `cursor_mut_unmap_embedded` ensures: per-
946        // slot universal preservation (raw_count, in_list, usage,
947        // slot_vaddr, vtable_ptr); rc doesn't bump to UNIQUE; storage
948        // preserved at non-UNUSED post; and at Frame slots, the
949        // "non-mapping count" `rc - paths.len()` is invariant with
950        // `rc` and `paths.len` monotonically non-increasing.
951        final(regions).slots == old(regions).slots,
952        forall|i: usize|
953            #![trigger final(regions).slot_owners[i]]
954            {
955                &&& final(regions).slot_owners[i].slot_vaddr == old(
956                    regions,
957                ).slot_owners[i].slot_vaddr
958                &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
959                &&& final(regions).slot_owners[i].inner_perms.in_list == old(
960                    regions,
961                ).slot_owners[i].inner_perms.in_list
962                &&& final(regions).slot_owners[i].inner_perms.vtable_ptr == old(
963                    regions,
964                ).slot_owners[i].inner_perms.vtable_ptr
965                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNIQUE
966                    ==> final(regions).slot_owners[i].inner_perms.ref_count.value()
967                    != REF_COUNT_UNIQUE
968                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
969                    ==> final(regions).slot_owners[i].inner_perms.storage == old(
970                    regions,
971                ).slot_owners[i].inner_perms.storage
972            },
973        // Unparked (page-table-node) slots untouched (see
974        // `cursor_mut_unmap_embedded`); preserves the coverage exception.
975        forall|i: usize|
976            #![trigger final(regions).slot_owners[i]]
977            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
978                regions,
979            ).slot_owners[i],
980        forall|i: usize|
981            #![trigger final(regions).slot_owners[i]]
982            old(regions).slot_owners[i].usage == PageUsage::Frame ==> {
983                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() + old(
984                    regions,
985                ).slot_owners[i].paths_in_pt.len() == old(
986                    regions,
987                ).slot_owners[i].inner_perms.ref_count.value()
988                    + final(regions).slot_owners[i].paths_in_pt.len()
989                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() <= old(
990                    regions,
991                ).slot_owners[i].inner_perms.ref_count.value()
992                &&& final(regions).slot_owners[i].paths_in_pt.len() <= old(
993                    regions,
994                ).slot_owners[i].paths_in_pt.len()
995                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != 0
996            },
997        forall|i: usize|
998            #![trigger final(regions).slot_owners[i]]
999            old(regions).slot_owners[i].usage == PageUsage::MMIO ==> final(regions).slot_owners[i]
1000                == old(regions).slot_owners[i],
1001        forall|c: CursorOwner<'rcu, UserPtConfig>|
1002            #![auto]
1003            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
1004{
1005    match method {
1006        CursorMutRegionsMethod::Unmap(len) => {
1007            cursor_mut_unmap_embedded(&mut entry.owner, regions, &mut entry.guards, tlb_model, len);
1008        },
1009    }
1010}
1011
1012/// Per-op step for `Op::Map`. Mutates the cursor owner, the regions,
1013/// and the TLB model. Has its own function rather than a dispatch tag
1014/// because the argument shape (UFrame, PageProperty) doesn't match the
1015/// others.
1016///
1017/// Does NOT require `owner.in_locked_range()`: exec `map` panics on an
1018/// out-of-range cursor (`assert!(va < barrier_va.end)`) and re-derives
1019/// `in_locked_range` from that panic + the cursor invariant.
1020pub(super) proof fn map_step<'rcu>(
1021    tracked entry: &mut CursorEntry<'rcu>,
1022    tracked regions: &mut MetaRegionOwners,
1023    tracked tlb_model: &mut TlbModel,
1024    paddr: Paddr,
1025    prop: PageProperty,
1026)
1027    requires
1028        old(entry).inv(),
1029        old(regions).inv(),
1030        old(entry).owner.metaregion_sound(*old(regions)),
1031        old(tlb_model).inv(),
1032        has_safe_slot(paddr),
1033    ensures
1034        final(entry).vm_space == old(entry).vm_space,
1035        final(entry).kind == old(entry).kind,
1036        final(entry).va == old(entry).va,
1037        final(entry).inv(),
1038        final(regions).inv(),
1039        final(entry).owner.metaregion_sound(*final(regions)),
1040        final(tlb_model).inv(),
1041        final(regions).slots == old(regions).slots,
1042        // Mirror the strengthened `cursor_mut_map_embedded` ensures.
1043        forall|i: usize|
1044            #![trigger final(regions).slot_owners[i]]
1045            final(regions).slot_owners[i].inner_perms.in_list == old(
1046                regions,
1047            ).slot_owners[i].inner_perms.in_list,
1048        forall|i: usize|
1049            #![trigger final(regions).slot_owners[i]]
1050            i != frame_to_index(paddr) && old(regions).slot_owners[i].inner_perms.ref_count.value()
1051                != REF_COUNT_UNUSED ==> final(regions).slot_owners[i] == old(
1052                regions,
1053            ).slot_owners[i],
1054        forall|i: usize|
1055            #![trigger final(regions).slot_owners[i].inner_perms.ref_count.value()]
1056            old(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
1057                ==> final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED,
1058        final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == old(
1059            regions,
1060        ).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value(),
1061        final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.len() == old(
1062            regions,
1063        ).slot_owners[frame_to_index(paddr)].paths_in_pt.len() + 1,
1064        final(regions).slot_owners[frame_to_index(paddr)].usage == old(
1065            regions,
1066        ).slot_owners[frame_to_index(paddr)].usage,
1067        final(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage == old(
1068            regions,
1069        ).slot_owners[frame_to_index(paddr)].inner_perms.storage,
1070        forall|i: usize|
1071            #![trigger final(regions).slot_owners[i]]
1072            final(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
1073                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
1074        forall|i: usize|
1075            #![trigger final(regions).slot_owners[i]]
1076            i != frame_to_index(paddr) && old(regions).slot_owners[i].inner_perms.ref_count.value()
1077                == REF_COUNT_UNUSED && final(regions).slot_owners[i].inner_perms.ref_count.value()
1078                != REF_COUNT_UNUSED ==> final(regions).slot_owners[i].usage != PageUsage::Frame,
1079        forall|c: CursorOwner<'rcu, UserPtConfig>|
1080            #![auto]
1081            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
1082{
1083    cursor_mut_map_embedded(&mut entry.owner, regions, &mut entry.guards, tlb_model, paddr, prop);
1084}
1085
1086} // verus!
ostd/specs/mm/embedding/cursor.rs

ostd/specs/mm/embedding/
cursor.rs
