Skip to main content

axiom_slice_in_kernel

ostd::specs::mm::io

Function axiom_slice_in_kernel 

Source 
pub proof fn axiom_slice_in_kernel(slice: &[u8])
Expand description
ensures
::vstd_extra::external::slice::as_ptr_spec(slice) as usize >= KERNEL_BASE_VADDR,
::vstd_extra::external::slice::as_ptr_spec(slice) as usize + slice.len()
    <= KERNEL_END_VADDR,

AXIOM: every &[u8] reaching ostd refers to kernel-space memory.

ostd is only ever called from kernel code, so any “native” Rust slice it receives points into kernel-managed memory. The natural trust boundary is here, at the conversion from a native slice to a tracked VirtPtr / owner; downstream proofs discharge VmWriter::from_kernel_space’s kernel-VA preconditions via this fact.