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,