Skip to main content

vaddr_upper_part_spec

ostd::specs::mm::page_table

Function vaddr_upper_part_spec 

Source 
pub open spec fn vaddr_upper_part_spec<C: PagingConstsTrait>(va: Vaddr) -> int
Expand description
{
    vaddr_upper_bits_spec::<C>(va) as int
        * pow2(page_table_vaddr_bits_spec::<C>() as nat) as int
}

Contribution of the uninterpreted upper virtual-address bits to the concrete address. Unlike the legacy fixed leading_bits * 2^48 expression, the boundary is derived from C.