lemma_meta_frame_vaddr_properties

ostd::specs::arch::kspace

Function lemma_meta_frame_vaddr_properties 

Source 
pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
Expand description
requires
meta % META_SLOT_SIZE() == 0,
FRAME_METADATA_RANGE().start <= meta
    < FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE(),
ensures
LINEAR_MAPPING_BASE_VADDR() <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
    < VMALLOC_BASE_VADDR(),
#[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE() == 0,