Skip to main content

axiom_kernel_mem_view

ostd::specs::mm::io

Function axiom_kernel_mem_view 

Source 
pub proof fn axiom_kernel_mem_view(range: Range<usize>) -> tracked mv : MemView
Expand description
ensures
mv.mappings.finite(),
mv.mappings_are_disjoint(),
forall |va: usize| {
    range.start <= va < range.end
        ==> {
            &&& mv.addr_transl(va) is Some
            &&& mv.memory.contains_key(mv.addr_transl(va).unwrap().0)
            &&& mv
                .memory[mv.addr_transl(va).unwrap().0]
                .contents[mv.addr_transl(va).unwrap().1 as int] is Init

        }
},

AXIOM: a fresh MemView covering a kernel-VA range exists.

The kernel guarantees that every byte in [KERNEL_BASE_VADDR, KERNEL_END_VADDR) is backed by a valid mapping; this axiom packages that fact as a tracked MemView value, suitable for embedding inside a VmIoOwner. The Init part of the returned view (used by VmIoOwner::read_view_initialized) is claimed unconditionally — &[u8] / &mut [u8] borrows in safe Rust point to initialized memory, so this is the natural companion to axiom_slice_in_kernel.