Skip to main content

axiom_mmio_paddr_huge_page_closed

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

Function axiom_mmio_paddr_huge_page_closed 

Source 
pub proof fn axiom_mmio_paddr_huge_page_closed(
    pa: Paddr,
    page_size: usize,
    offset: usize,
)
Expand description
requires
pa % page_size == 0,
offset < page_size,
ensures
is_mmio_paddr((pa + offset) as crate::mm::Paddr) == is_mmio_paddr(pa),

MMIO ranges are aligned to (and closed under) huge-page granularities: every sub-paddr within a huge frame inherits the huge frame’s MMIO-ness. This is a hardware-layout convention — MMIO BARs are mapped at huge-page boundaries, and the verified split_if_mapped_huge relies on it to transfer MMIO-ness from a huge frame to its 4KB sub-pages. Non-broadcast: callers invoke this explicitly with the relevant page_size.