sibling_paths_disjoint

ostd::specs::mm::page_table

Function sibling_paths_disjoint 

Source 
pub proof fn sibling_paths_disjoint(
    prefix: TreePath<NR_ENTRIES>,
    j: usize,
    k: usize,
    size: usize,
)
Expand description
requires
j < NR_ENTRIES,
k < NR_ENTRIES,
j != k,
size == page_size((INC_LEVELS - prefix.len()) as PagingLevel),
ensures
vaddr(prefix.push_tail(j)) + size <= vaddr(prefix.push_tail(k))
    || vaddr(prefix.push_tail(k)) + size <= vaddr(prefix.push_tail(j)),

Sibling paths (same prefix, different last index) have disjoint VA ranges. This is a fundamental property of page table virtual address layout: each entry at a given level covers a distinct, non-overlapping range.