Skip to main content

sibling_paths_disjoint

ostd::specs::mm::page_table

Function sibling_paths_disjoint 

Source 
pub proof fn sibling_paths_disjoint<C: PageTableConfig>(
    prefix: TreePath<NR_ENTRIES>,
    j: usize,
    k: usize,
    size: usize,
)
Expand description
requires
prefix.inv(),
prefix.len() < INC_LEVELS - 1,
j < NR_ENTRIES,
k < NR_ENTRIES,
j != k,
size == page_size((INC_LEVELS - prefix.len() - 1) 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, separated by at least the child page size.

Generic in C only so the proof can reach PageTableOwner<C>::lemma_vaddr_push_tail_eq; the body does not depend on C.