Skip to main content

vm_reader_from_kernel_space_embedded

ostd::specs::mm::embedding::io

Function vm_reader_from_kernel_space_embedded 

Source 
pub proof fn vm_reader_from_kernel_space_embedded(
    vaddr: Vaddr,
    len: usize,
) -> tracked res : VmIoOwner
Expand description
ensures
res.inv(),
res.read_view_initialized(),

Mirror of crate::mm::io::VmReader<Infallible>::from_kernel_space.

Exec ensures (line 1247-1255) that under the kernel-VA range guard, the produced owner satisfies read_view_initialized(). We instantiate the axiom on that branch — the resulting entry is pre-activated as a Reader.