Skip to main content

meta_slot_eq_by_ids

ostd::specs::mm::frame::meta_owners

Function meta_slot_eq_by_ids 

Source 
pub proof fn meta_slot_eq_by_ids(a: MetaSlot, b: MetaSlot)
Expand description
ensures
(a.storage.id() == b.storage.id() && a.ref_count.id() == b.ref_count.id()
    && a.vtable_ptr == b.vtable_ptr && a.in_list.id() == b.in_list.id()) ==> a == b,

A MetaSlot is uniquely determined by its cell ids + vtable_ptr address. This is a structural fact about the opaque atomic/cell primitives — two MetaSlot values whose ids agree on every field are equal.