Function write_metadata_into_storage 

pub exec fn write_metadata_into_storage<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
    cell: &PCell<MetaSlotStorage>,
    Tracked(storage): Tracked<&mut PointsTo<MetaSlotStorage>>,
    Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
    metadata: M,
)

requires

cell.id() == old(storage).id(),

ensures

final(storage).id() == old(storage).id(),

final(storage).is_init(),

M::wf(final(storage).value(), *final(repr_perm)),

M::from_repr_spec(final(storage).value(), *final(repr_perm)) == metadata,

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