Skip to main content

meta_slot_from_perm_ids

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

Function meta_slot_from_perm_ids 

Source 
pub proof fn meta_slot_from_perm_ids(perm: MetadataInnerPerms)
Expand description
ensures
meta_slot_from_perm(perm).storage.id() == perm.storage.id(),
meta_slot_from_perm(perm).ref_count.id() == perm.ref_count.id(),
meta_slot_from_perm(perm).vtable_ptr == perm.vtable_ptr.pptr(),
meta_slot_from_perm(perm).in_list.id() == perm.in_list.id(),