pub exec fn meta_to_frame(vaddr: Vaddr) -> res : PaddrExpand description
requires
FRAME_METADATA_RANGE.start <= vaddr && vaddr < FRAME_METADATA_RANGE.end,vaddr % META_SLOT_SIZE == 0,ensuresres == meta_to_frame_spec(vaddr),res % PAGE_SIZE == 0,