Function axiom_view_in_vaddr_range Copy item path

owner.inv(),

forall |m: Mapping| {
    owner.view_mappings().contains(m)
        ==> {
            &&& vaddr_range_bounds_spec::<C>().0 <= m.va_range.start
            &&& m.va_range.end <= vaddr_range_bounds_spec::<C>().1 + 1

        }
},

Every mapping in a cursor’s view has its VA range within the page table’s managed positional range.

This is now provable as a lemma — with vaddr_range_bounds_spec<C> expressing positional bounds and view_rec constructing mappings as vaddr(path)..vaddr(path) + page_size, the conclusion follows from:

1. view_rec_vaddr_range: for every m, there is a path such that vaddr(path) <= m.va_range.start < m.va_range.end <= vaddr(path) + page_size;
2. lemma_vaddr_path_alignment_and_bound: vaddr(path) + page_size <= 2^48;
3. Path rooted in C::TOP_LEVEL_INDEX_RANGE_spec(): idx.start * 2^offset <= vaddr(path) <= (idx.end - 1) * 2^offset + (2^offset - page_size).

Remains an axiom only because the full induction through view_mappings → continuations → view_rec across cursor level transitions has not yet been written. Unlike the prior form (which was demonstrably false — it claimed mappings lived in the sign-extended canonical range, but path-derived mappings are positional), the claim here is sound. Consumers that need the canonical form should compose with LEADING_BITS_spec.