ostd::specs::mm::embedding::list_store

Function axiom_empty_list_owner

pub proof fn axiom_empty_list_owner<M: AnyFrameMeta + Repr<MetaSlotSmall>>() -> tracked res : LinkedListOwner<M>

Expand description

ensures

res.list =~= Seq::<LinkOwner>::empty(),

res.list_id == 0,

Tracked constructor for a fresh empty list owner. Sound: an empty LinkedListOwner claims no permissions (cf. LinkedListOwner::tracked_destroy_empty), and carries list_id == 0 — the real id is minted lazily on first push.

axiom_empty_list_owner

Function axiom_empty_list_owner Copy item path

Function axiom_empty_list_owner