Skip to main content

write_metadata_into_storage

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

Function write_metadata_into_storage 

Source 
pub exec fn write_metadata_into_storage<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
    cell: &PCell<MetaSlotStorage>,
    Tracked(metadata_perms): Tracked<&mut MetadataPerm>,
    Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
    metadata: M,
)
Expand description
requires
cell.id() == old(metadata_perms).storage_perm.id(),
ensures
final(metadata_perms).storage_perm.id() == old(metadata_perms).storage_perm.id(),
final(metadata_perms).storage_perm.is_init(),
final(metadata_perms).vtable_ptr_perm == old(metadata_perms).vtable_ptr_perm,
M::wf(final(metadata_perms).storage_perm.value(), *final(repr_perm)),
M::from_repr_spec(final(metadata_perms).storage_perm.value(), *final(repr_perm))
    == metadata,

Writes metadata into the byte storage and establishes its direct Repr<MetaSlotStorage> interpretation.