Skip to main content

axiom_mmio_usage_iff_mmio_paddr

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

Function axiom_mmio_usage_iff_mmio_paddr 

Source 
pub broadcast proof fn axiom_mmio_usage_iff_mmio_paddr(slot: MetaSlotOwner)
Expand description
ensures
(#[trigger] slot.usage == PageUsage::MMIO)
    <==> is_mmio_paddr(meta_to_frame(slot.self_addr)),

Connects a slot’s PageUsage::MMIO discriminant to its paddr’s range membership. Used to derive disjointness between MMIO mappings and the regular allocator pool: a slot can be MMIO iff its paddr is in MMIO range, so a slot with usage != MMIO (e.g. Unused) cannot share an idx with any MMIO mapping.