Skip to main content

vaddr_range_bounds_spec

Function vaddr_range_bounds_spec 

Source
pub closed spec fn vaddr_range_bounds_spec<C: PageTableConfig>() -> (Vaddr, Vaddr)
Expand description

Canonical bounds of the VA range managed by a page-table config, returned as inclusive (start, end_inclusive). end_inclusive may equal usize::MAX for sign-extended kernel configs, which is why the inclusive form is used — Range<Vaddr> cannot represent that.

Derived from LEADING_BITS_spec and TOP_LEVEL_INDEX_RANGE_spec. For UserPtConfig (LEADING_BITS=0, idx=0..256) this is (0, 2^47 - 1); for KernelPtConfig (LEADING_BITS=0xffff, idx=256..512) this is (0xffff_8000_0000_0000, 0xffff_ffff_ffff_ffff).