Module cursor 

Embedding of Cursor / CursorMut operations: open, drop, navigation (query/find_next/jump), and mutation (map/unmap/protect_next).

Per-op steps operate on tracked owners directly — no store lookups, no preconditions on store membership, no if-guards. The store-side extract / insert and id-management lives in super::VmStore’s methods and the super::step dispatcher.

Mirroring exec preconditions

Each _embedded axiom carries the same requires as its exec counterpart, expressed against our model. The expressible parts are:

• owner.inv(), owner.children_not_locked(guards), owner.nodes_locked(guards), !owner.popped_too_high — bundled as CursorEntry::inv (entry-side); see super::CursorEntry.
• owner.in_locked_range() — NOT a precondition of query, jump, or map: each handles an out-of-range cursor itself (graceful Err for query; a faithful panic_diverge otherwise) and re-derives in_locked_range internally. protect_next still requires it; see exec clauses.
• regions.inv(), owner.metaregion_sound(regions) — passed via &mut regions.
• tlb_model.inv() — passed via &mut tlb_model to map / unmap.

Model gaps

• Exec Cursor handle: the exec Cursor::invariants requires self.inv() and self.wf(owner) over the runtime Cursor struct. Our embedding doesn’t carry that handle (it’s tied to the &'rcu RCU guard reference, not constructible in pure ghost mode), so these conjuncts are MODEL GAPS. Owner-side state already mirrors handle state (owner.va, owner.level, owner.guard_level), so wf(owner) is essentially tautological if we postulate the handle’s existence; inv() follows from owner.inv() plus this projection.
• item_wf on map: the exec crate::mm::vm_space::CursorMut::map requires old(self).item_wf(frame, prop, entry_owner, *old(regions)), which constrains a separate EntryOwner<UserPtConfig> argument produced by cursor traversal. We don’t model EntryOwner here.
• protect_next closure preconditions: the exec method takes a closure op: impl FnOnce(PageProperty) -> PageProperty with forall |p| op.requires((p,)) plus a trackedness-preservation constraint. Our Op::ProtectNext doesn’t carry the closure.

Enums

CursorMutRegionsMethod

Internal: dispatch tag for cursor methods that also touch MetaRegionOwners and TlbModel. Map is handled via its own [map_step].

Functions

cursor_find_next_embedded

cursor_jump_embedded

cursor_mut_map_embedded

cursor_mut_protect_next_embedded

cursor_mut_unmap_embedded

cursor_query_embedded

vm_space_cursor_embedded

vm_space_cursor_mut_embedded