pub proof fn axiom_cursor_entry_new<'rcu>(
vm_space: VmSpaceId,
kind: CursorKind,
tracked owner: CursorOwner<'rcu, UserPtConfig>,
) -> tracked res : CursorEntry<'rcu>Expand description
ensures
res.vm_space == vm_space,res.kind == kind,res.owner == owner,Tracked constructor for CursorEntry.
Verus does not let a proof fn construct a tracked struct via a
struct-literal when ghost-mode and tracked-mode fields are mixed; the
idiomatic workaround is a constructor axiom (cf.
[CursorContinuation::new]).